From 3cda0d9bf296e6df022c62c5a8ae2c02b32a1924 Mon Sep 17 00:00:00 2001 From: Niels Date: Tue, 8 Aug 2017 17:00:30 +0200 Subject: [PATCH] Completely fixed notation --- FiniteSets/fsets/extensionality.v | 6 ++-- FiniteSets/fsets/isomorphism.v | 3 +- FiniteSets/fsets/length.v | 14 ++++---- FiniteSets/fsets/operations.v | 45 ++++++------------------- FiniteSets/fsets/operations_cons_repr.v | 5 ++- FiniteSets/fsets/operations_decidable.v | 38 ++++++++++++--------- FiniteSets/fsets/properties.v | 4 +-- FiniteSets/fsets/properties_decidable.v | 31 ++++++++--------- FiniteSets/notation.v | 36 ++++++++++++++------ FiniteSets/representations/bad.v | 6 ++-- FiniteSets/representations/cons_repr.v | 2 +- FiniteSets/representations/definition.v | 6 ++-- 12 files changed, 96 insertions(+), 100 deletions(-) diff --git a/FiniteSets/fsets/extensionality.v b/FiniteSets/fsets/extensionality.v index 5de10cf..7034a2c 100644 --- a/FiniteSets/fsets/extensionality.v +++ b/FiniteSets/fsets/extensionality.v @@ -45,7 +45,7 @@ Section ext. - intros a Y. apply (tr(inl(tr idpath))). - intros X1 X2 HX1 HX2 Y. - split. + split ; unfold subset in *. * rewrite <- assoc. apply HX1. * rewrite (comm X1 X2). rewrite <- assoc. apply HX2. Defined. @@ -64,7 +64,7 @@ Section ext. Lemma subset_isIn (X Y : FSet A) : (forall (a : A), a ∈ X -> a ∈ Y) - <~> (X ⊆ Y). + <~> X ⊆ Y. Proof. eapply equiv_iff_hprop_uncurried. split. @@ -149,4 +149,4 @@ Section ext. split ; apply subset_isIn. Defined. -End ext. +End ext. \ No newline at end of file diff --git a/FiniteSets/fsets/isomorphism.v b/FiniteSets/fsets/isomorphism.v index de85849..c6c2105 100644 --- a/FiniteSets/fsets/isomorphism.v +++ b/FiniteSets/fsets/isomorphism.v @@ -45,7 +45,7 @@ Section Iso. intros x. hrecursion x; try (intros; apply path_forall; intro; apply set_path2). - intros. symmetry. apply nl. - - intros a x HR y. rewrite HR. apply assoc. + - intros a x HR y. unfold union, fsetc_union in *. rewrite HR. apply assoc. Defined. Lemma repr_iso_id_l: forall (x: FSet A), FSetC_to_FSet (FSet_to_FSetC x) = x. @@ -56,7 +56,6 @@ Section Iso. - intros x y p q. rewrite append_union, p, q. reflexivity. Defined. - Lemma repr_iso_id_r: forall (x: FSetC A), FSet_to_FSetC (FSetC_to_FSet x) = x. Proof. hinduction; try (intros; apply set_path2). diff --git a/FiniteSets/fsets/length.v b/FiniteSets/fsets/length.v index 5bd9eb8..6f728b1 100644 --- a/FiniteSets/fsets/length.v +++ b/FiniteSets/fsets/length.v @@ -9,24 +9,22 @@ Section Length. Context {A_deceq : DecidablePaths A}. Context `{Univalence}. - Opaque isIn_b. - Definition length (x : FSetC A) : nat. Proof. simple refine (FSetC_ind A _ _ _ _ _ _ x ); simpl. - exact 0. - intros a y n. pose (y' := FSetC_to_FSet y). - exact (if isIn_b a y' then n else (S n)). - - intros. rewrite transport_const. cbn. - simplify_isIn_b. simpl. reflexivity. - - intros. rewrite transport_const. cbn. + exact (if a ∈_d y' then n else (S n)). + - intros. rewrite transport_const. simpl. + simplify_isIn_b. reflexivity. + - intros. rewrite transport_const. simpl. simplify_isIn_b. destruct (dec (a = b)) as [Hab | Hab]. - + rewrite Hab. simplify_isIn_b. simpl. reflexivity. + + rewrite Hab. simplify_isIn_b. reflexivity. + rewrite ?L_isIn_b_false; auto. ++ simpl. - destruct (isIn_b a (FSetC_to_FSet x0)), (isIn_b b (FSetC_to_FSet x0)) + destruct (a ∈_d (FSetC_to_FSet x0)), (b ∈_d (FSetC_to_FSet x0)) ; reflexivity. ++ intro p. contradiction (Hab p^). Defined. diff --git a/FiniteSets/fsets/operations.v b/FiniteSets/fsets/operations.v index c063108..ad742d0 100644 --- a/FiniteSets/fsets/operations.v +++ b/FiniteSets/fsets/operations.v @@ -3,12 +3,11 @@ Require Import HoTT HitTactics. Require Import representations.definition disjunction lattice. Section operations. - Context {A : Type}. Context `{Univalence}. - Definition isIn : A -> FSet A -> hProp. + Global Instance fset_member : forall A, hasMembership (FSet A) A. Proof. - intros a. + intros A a. hrecursion. - exists Empty. exact _. @@ -23,10 +22,9 @@ Section operations. - intros ; apply lor_idem. Defined. - Definition comprehension : - (A -> Bool) -> FSet A -> FSet A. + Global Instance fset_comprehension : forall A, hasComprehension (FSet A) A. Proof. - intros P. + intros A P. hrecursion. - apply ∅. - intro a. @@ -42,7 +40,7 @@ Section operations. + apply nl. Defined. - Definition isEmpty : + Definition isEmpty (A : Type) : FSet A -> Bool. Proof. simple refine (FSet_rec _ _ _ true (fun _ => false) andb _ _ _ _ _) @@ -50,7 +48,7 @@ Section operations. intros ; symmetry ; eauto with lattice_hints typeclass_instances. Defined. - Definition single_product {B : Type} (a : A) : FSet B -> FSet (A * B). + Definition single_product {A B : Type} (a : A) : FSet B -> FSet (A * B). Proof. hrecursion. - apply ∅. @@ -64,7 +62,7 @@ Section operations. - intros ; apply idem. Defined. - Definition product {B : Type} : FSet A -> FSet B -> FSet (A * B). + Definition product {A B : Type} : FSet A -> FSet B -> FSet (A * B). Proof. intros X Y. hrecursion X. @@ -78,29 +76,10 @@ Section operations. - intros ; apply nr. - intros ; apply union_idem. Defined. - -End operations. - -Section instances_operations. - Global Instance fset_comprehension : hasComprehension FSet. + + Global Instance fset_subset : forall A, hasSubset (FSet A). Proof. - intros A ϕ X. - apply (comprehension ϕ X). - Defined. - - Context `{Univalence}. - - Global Instance fset_member : hasMembership FSet. - Proof. - intros A a X. - apply (isIn a X). - Defined. - - Context {A : Type}. - - Definition subset : FSet A -> FSet A -> hProp. - Proof. - intros X Y. + intros A X Y. hrecursion X. - exists Unit. exact _. @@ -123,6 +102,4 @@ Section instances_operations. * intros p. split ; apply p. Defined. -End instances_operations. - -Infix "⊆" := subset (at level 10, right associativity). \ No newline at end of file +End operations. \ No newline at end of file diff --git a/FiniteSets/fsets/operations_cons_repr.v b/FiniteSets/fsets/operations_cons_repr.v index 1cdde40..57850cc 100644 --- a/FiniteSets/fsets/operations_cons_repr.v +++ b/FiniteSets/fsets/operations_cons_repr.v @@ -3,8 +3,7 @@ Require Import HoTT HitTactics. Require Import representations.cons_repr. Section operations. - - Global Instance fsetc_union : hasUnion FSetC. + Global Instance fsetc_union : forall A, hasUnion (FSetC A). Proof. intros A x y. hinduction x. @@ -14,6 +13,6 @@ Section operations. - apply comm. Defined. - Global Instance fsetc_singleton : hasSingleton FSetC := fun A a => a;;∅. + Global Instance fsetc_singleton : forall A, hasSingleton (FSetC A) A := fun A a => a;;∅. End operations. \ No newline at end of file diff --git a/FiniteSets/fsets/operations_decidable.v b/FiniteSets/fsets/operations_decidable.v index 012469c..dca5b9e 100644 --- a/FiniteSets/fsets/operations_decidable.v +++ b/FiniteSets/fsets/operations_decidable.v @@ -6,8 +6,9 @@ Section decidable_A. Context {A : Type}. Context {A_deceq : DecidablePaths A}. Context `{Univalence}. - - Global Instance isIn_decidable : forall (a : A) (X : FSet A), Decidable (a ∈ X). + + Global Instance isIn_decidable : forall (a : A) (X : FSet A), + Decidable (a ∈ X). Proof. intros a. hinduction ; try (intros ; apply path_ishprop). @@ -23,26 +24,31 @@ Section decidable_A. - intros. apply _. Defined. - Definition isIn_b (a : A) (X : FSet A) := - match dec (a ∈ X) with - | inl _ => true - | inr _ => false - end. - + Global Instance fset_member_bool : hasMembership_decidable (FSet A) A. + Proof. + intros a X. + destruct (dec (a ∈ X)). + - apply true. + - apply false. + Defined. + Global Instance subset_decidable : forall (X Y : FSet A), Decidable (X ⊆ Y). Proof. hinduction ; try (intros ; apply path_ishprop). - intro ; apply _. - - intros. apply _. - - intros ; apply _. + - intros ; apply _. + - intros. unfold subset in *. apply _. Defined. - Definition subset_b (X Y : FSet A) := - match dec (X ⊆ Y) with - | inl _ => true - | inr _ => false - end. + Global Instance fset_subset_bool : hasSubset_decidable (FSet A). + Proof. + intros X Y. + destruct (dec (X ⊆ Y)). + - apply true. + - apply false. + Defined. - Definition intersection (X Y : FSet A) : FSet A := comprehension (fun a => isIn_b a Y) X. + Global Instance fset_intersection : hasIntersection (FSet A) + := fun X Y => {|X & (fun a => a ∈_d Y)|}. End decidable_A. \ No newline at end of file diff --git a/FiniteSets/fsets/properties.v b/FiniteSets/fsets/properties.v index ccff710..5e61d98 100644 --- a/FiniteSets/fsets/properties.v +++ b/FiniteSets/fsets/properties.v @@ -150,7 +150,7 @@ Section properties. Defined. (** comprehension properties *) - Lemma comprehension_false X : {|X & (fun (_ : A) => false)|} = ∅. + Lemma comprehension_false : forall (X : FSet A), {|X & fun _ => false|} = ∅. Proof. toHProp. Defined. @@ -172,7 +172,7 @@ Section properties. Defined. Lemma comprehension_all : forall (X : FSet A), - comprehension (fun a => true) X = X. + {|X & fun _ => true|} = X. Proof. toHProp. Defined. diff --git a/FiniteSets/fsets/properties_decidable.v b/FiniteSets/fsets/properties_decidable.v index 4578a24..83656e0 100644 --- a/FiniteSets/fsets/properties_decidable.v +++ b/FiniteSets/fsets/properties_decidable.v @@ -8,13 +8,13 @@ Section operations_isIn. Context {A : Type} `{DecidablePaths A} `{Univalence}. - Lemma ext : forall (S T : FSet A), (forall a, isIn_b a S = isIn_b a T) -> S = T. + Lemma ext : forall (S T : FSet A), (forall a, a ∈_d S = a ∈_d T) -> S = T. Proof. intros X Y H2. apply fset_ext. intro a. specialize (H2 a). - unfold isIn_b, dec in H2. + unfold member_dec, fset_member_bool, dec in H2. destruct (isIn_decidable a X) ; destruct (isIn_decidable a Y). - apply path_iff_hprop ; intro ; assumption. - contradiction (true_ne_false). @@ -23,7 +23,7 @@ Section operations_isIn. Defined. Lemma empty_isIn (a : A) : - isIn_b a ∅ = false. + a ∈_d ∅ = false. Proof. reflexivity. Defined. @@ -35,9 +35,9 @@ Section operations_isIn. Defined. Lemma L_isIn_b_true (a b : A) (p : a = b) : - isIn_b a {|b|} = true. + a ∈_d {|b|} = true. Proof. - unfold isIn_b, dec. + unfold member_dec, fset_member_bool, dec. destruct (isIn_decidable a {|b|}) as [n | n] . - reflexivity. - simpl in n. @@ -45,15 +45,15 @@ Section operations_isIn. Defined. Lemma L_isIn_b_aa (a : A) : - isIn_b a {|a|} = true. + a ∈_d {|a|} = true. Proof. apply L_isIn_b_true ; reflexivity. Defined. Lemma L_isIn_b_false (a b : A) (p : a <> b) : - isIn_b a {|b|} = false. + a ∈_d {|b|} = false. Proof. - unfold isIn_b, dec. + unfold member_dec, fset_member_bool, dec in *. destruct (isIn_decidable a {|b|}). - simpl in t. strip_truncations. @@ -63,24 +63,25 @@ Section operations_isIn. (* Union and membership *) Lemma union_isIn_b (X Y : FSet A) (a : A) : - isIn_b a (X ∪ Y) = orb (isIn_b a X) (isIn_b a Y). + a ∈_d (X ∪ Y) = orb (a ∈_d X) (a ∈_d Y). Proof. - unfold isIn_b ; unfold dec. + unfold member_dec, fset_member_bool, dec. simpl. destruct (isIn_decidable a X) ; destruct (isIn_decidable a Y) ; reflexivity. Defined. Lemma comprehension_isIn_b (Y : FSet A) (ϕ : A -> Bool) (a : A) : - isIn_b a {|Y & ϕ|} = andb (isIn_b a Y) (ϕ a). + a ∈_d {|Y & ϕ|} = andb (a ∈_d Y) (ϕ a). Proof. - unfold isIn_b, dec ; simpl. + unfold member_dec, fset_member_bool, dec ; simpl. destruct (isIn_decidable a {|Y & ϕ|}) as [t | t] ; destruct (isIn_decidable a Y) as [n | n] ; rewrite comprehension_isIn in t - ; destruct (ϕ a) ; try reflexivity ; try contradiction. + ; destruct (ϕ a) ; try reflexivity ; try contradiction + ; try (contradiction (n t)) ; contradiction (t n). Defined. Lemma intersection_isIn_b (X Y: FSet A) (a : A) : - isIn_b a (intersection X Y) = andb (isIn_b a X) (isIn_b a Y). + a ∈_d (intersection X Y) = andb (a ∈_d X) (a ∈_d Y). Proof. apply comprehension_isIn_b. Defined. @@ -114,7 +115,7 @@ Section SetLattice. Instance fset_min : minimum (FSet A). Proof. intros x y. - apply (intersection x y). + apply (x ∩ y). Defined. Instance fset_bot : bottom (FSet A). diff --git a/FiniteSets/notation.v b/FiniteSets/notation.v index 76d66d5..cd3c53f 100644 --- a/FiniteSets/notation.v +++ b/FiniteSets/notation.v @@ -48,31 +48,44 @@ Arguments neutralityR {_} {_} {_} {_} _. Arguments absorb {_} {_} {_} {_} _ _. Section structure. - Variable (T : Type -> Type). + Variable (T A : Type). Class hasMembership : Type := - member : forall A : Type, A -> T A -> hProp. + member : A -> T -> hProp. + + Class hasMembership_decidable : Type := + member_dec : A -> T -> Bool. + + Class hasSubset : Type := + subset : T -> T -> hProp. + + Class hasSubset_decidable : Type := + subset_dec : T -> T -> Bool. Class hasEmpty : Type := - empty : forall A, T A. + empty : T. Class hasSingleton : Type := - singleton : forall A, A -> T A. + singleton : A -> T. Class hasUnion : Type := - union : forall A, T A -> T A -> T A. + union : T -> T -> T. Class hasIntersection : Type := - intersection : forall A, T A -> T A -> T A. + intersection : T -> T -> T. Class hasComprehension : Type := - filter : forall A, (A -> Bool) -> T A -> T A. + filter : (A -> Bool) -> T -> T. End structure. Arguments member {_} {_} {_} _ _. -Arguments empty {_} {_} {_}. +Arguments subset {_} {_} _ _. +Arguments member_dec {_} {_} {_} _ _. +Arguments subset_dec {_} {_} _ _. +Arguments empty {_} {_}. Arguments singleton {_} {_} {_} _. -Arguments union {_} {_} {_} _ _. +Arguments union {_} {_} _ _. +Arguments intersection {_} {_} _ _. Arguments filter {_} {_} {_} _ _. Notation "∅" := empty. @@ -86,4 +99,7 @@ Notation "( ∩ )" := intersection (only parsing). Notation "( X ∩ )" := (intersection X) (only parsing). Notation "( ∩ Y )" := (fun X => X ∩ Y) (only parsing). Notation "{| X & ϕ |}" := (filter ϕ X). -Infix "∈" := member (at level 9, right associativity). \ No newline at end of file +Infix "∈" := member (at level 9, right associativity). +Infix "⊆" := subset (at level 10, right associativity). +Infix "∈_d" := member_dec (at level 9, right associativity). +Infix "⊆_d" := subset_dec (at level 10, right associativity). \ No newline at end of file diff --git a/FiniteSets/representations/bad.v b/FiniteSets/representations/bad.v index eadd8f3..38e2a4e 100644 --- a/FiniteSets/representations/bad.v +++ b/FiniteSets/representations/bad.v @@ -12,9 +12,9 @@ Module Export FSet. | L : A -> FSet A | U : FSet A -> FSet A -> FSet A. - Global Instance fset_empty : hasEmpty FSet := E. - Global Instance fset_singleton : hasSingleton FSet := L. - Global Instance fset_union : hasUnion FSet := U. + Global Instance fset_empty : forall A, hasEmpty (FSet A) := E. + Global Instance fset_singleton : forall A, hasSingleton (FSet A) A := L. + Global Instance fset_union : forall A, hasUnion (FSet A) := U. Variable A : Type. diff --git a/FiniteSets/representations/cons_repr.v b/FiniteSets/representations/cons_repr.v index 6f03bef..fef3f84 100644 --- a/FiniteSets/representations/cons_repr.v +++ b/FiniteSets/representations/cons_repr.v @@ -9,7 +9,7 @@ Module Export FSetC. | Nil : FSetC A | Cns : A -> FSetC A -> FSetC A. - Global Instance fset_empty : hasEmpty FSetC := Nil. + Global Instance fset_empty : forall A,hasEmpty (FSetC A) := Nil. Variable A : Type. Arguments Cns {_} _ _. diff --git a/FiniteSets/representations/definition.v b/FiniteSets/representations/definition.v index 9dc1c60..6b2de43 100644 --- a/FiniteSets/representations/definition.v +++ b/FiniteSets/representations/definition.v @@ -9,9 +9,9 @@ Module Export FSet. | L : A -> FSet A | U : FSet A -> FSet A -> FSet A. - Global Instance fset_empty : hasEmpty FSet := E. - Global Instance fset_singleton : hasSingleton FSet := L. - Global Instance fset_union : hasUnion FSet := U. + Global Instance fset_empty : forall A, hasEmpty (FSet A) := E. + Global Instance fset_singleton : forall A, hasSingleton (FSet A) A := L. + Global Instance fset_union : forall A, hasUnion (FSet A) := U. Variable A : Type.