From 80dabe3162af034992f9f503898041ec6d1f77f1 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Tue, 8 Aug 2017 17:06:53 +0200 Subject: [PATCH] Get a quotient from an implementation --- FiniteSets/implementations/interface.v | 220 +++++++++++++++++++++++-- prelude/HitTactics.v | 55 ++++--- 2 files changed, 236 insertions(+), 39 deletions(-) diff --git a/FiniteSets/implementations/interface.v b/FiniteSets/implementations/interface.v index 97b6510..e23ebd4 100644 --- a/FiniteSets/implementations/interface.v +++ b/FiniteSets/implementations/interface.v @@ -5,14 +5,18 @@ Section interface. Context `{Univalence}. Variable (T : Type -> Type) (f : forall A, T A -> FSet A). - Context `{hasMembership T, hasEmpty T, hasSingleton T, hasUnion T, hasComprehension T}. + Context `{forall A, hasMembership (T A) A + , forall A, hasEmpty (T A) + , forall A, hasSingleton (T A) A + , forall A, hasUnion (T A) + , forall A, hasComprehension (T A) A}. Class sets := { - f_empty : forall A, f A empty = ∅ ; + f_empty : forall A, f A ∅ = ∅ ; f_singleton : forall A a, f A (singleton a) = {|a|}; f_union : forall A X Y, f A (union X Y) = (f A X) ∪ (f A Y); - f_filter : forall A ϕ X, f A (filter ϕ X) = comprehension ϕ (f A X); + f_filter : forall A φ X, f A (filter φ X) = {| f A X & φ |}; f_member : forall A a X, member a X = a ∈ (f A X) }. End interface. @@ -30,26 +34,26 @@ Section properties. Ltac reduce := intros ; - repeat (rewrite (f_empty _ _) - || rewrite ?(f_singleton _ _) - || rewrite ?(f_union _ _) - || rewrite ?(f_filter _ _) - || rewrite ?(f_member _ _)). + repeat (rewrite (f_empty T _) + || rewrite (f_singleton T _) + || rewrite (f_union T _) + || rewrite (f_filter T _) + || rewrite (f_member T _)). Definition empty_isIn : forall (A : Type) (a : A), - member a empty = False_hp. + a ∈ ∅ = False_hp. Proof. by reduce. Defined. Definition singleton_isIn : forall (A : Type) (a b : A), - member a (singleton b) = merely (a = b). + a ∈ {|b|} = merely (a = b). Proof. by reduce. Defined. Definition union_isIn : forall (A : Type) (a : A) (X Y : T A), - member a (union X Y) = lor (member a X) (member a Y). + a ∈ (X ∪ Y) = lor (a ∈ X) (a ∈ Y). Proof. by reduce. Defined. @@ -90,10 +94,202 @@ Section properties. Defined. Lemma union_comm : forall A (X Y : T A), - set_eq A (union X Y) (union Y X). + set_eq A (X ∪ Y) (Y ∪ X). Proof. simplify. apply comm. Defined. + Lemma union_assoc : forall A (X Y Z : T A), + set_eq A ((X ∪ Y) ∪ Z) (X ∪ (Y ∪ Z)) . + Proof. + simplify. + symmetry. + apply assoc. + Defined. + + Lemma union_idem : forall A (X : T A), + set_eq A (X ∪ X) X. + Proof. + simplify. + apply union_idem. + Defined. + + Lemma union_neutral : forall A (X : T A), + set_eq A (∅ ∪ X) X. + Proof. + simplify. + apply nl. + Defined. + End properties. + +Section quot. +Variable (T : Type -> Type). +Variable (f : forall {A : Type}, T A -> FSet A). +Context `{sets T f}. + +Definition R A : relation (T A) := set_eq T f A. +Definition View A : Type := quotient (R A). + +Arguments f {_} _. + +Instance R_refl A : Reflexive (R A). +Proof. intro. reflexivity. Defined. + +Instance R_sym A : Symmetric (R A). +Proof. intros a b Hab. apply (Hab^). Defined. + +Instance R_trans A: Transitive (R A). +Proof. intros a b c Hab Hbc. apply (Hab @ Hbc). Defined. + +(* Instance quotient_recursion `{A : Type} (Q : relation A) `{is_mere_relation _ Q} : HitRecursion (quotient Q) := *) +(* { *) +(* indTy := _; recTy := _; *) +(* H_inductor := quotient_ind Q; H_recursor := quotient_rec Q *) +(* }. *) + +Instance View_recursion A : HitRecursion (View A) := + { + indTy := _; recTy := forall (P : Type) (HP: IsHSet P) (u : T A -> P), (forall x y : T A, set_eq T (@f) A x y -> u x = u y) -> View A -> P; + H_inductor := quotient_ind (R A); H_recursor := @quotient_rec _ (R A) _ + }. + +Arguments set_eq {_} _ {_} _ _. + +Definition View_rec2 {A} (P : Type) (HP : IsHSet P) (u : T A -> T A -> P) : + (forall (x x' : T A), set_eq (@f) x x' -> forall (y y' : T A), set_eq (@f) y y' -> u x y = u x' y') -> + forall (x y : View A), P. +Proof. +intros Hresp. +assert (resp1 : forall x y y', set_eq (@f) y y' -> u x y = u x y'). +{ intros x y y'. + apply Hresp. + reflexivity. } +assert (resp2 : forall x x' y, set_eq (@f) x x' -> u x y = u x' y). +{ intros x x' y Hxx'. + apply Hresp. apply Hxx'. + reflexivity. } +hrecursion. +- intros a. + hrecursion. + + intros b. + apply (u a b). + + intros b b' Hbb'. simpl. + by apply resp1. +- intros a a' Haa'. simpl. + apply path_forall. red. + hinduction. + + intros b. apply resp2. apply Haa'. + + intros; apply HP. +Defined. + +Instance View_max A : maximum (View A). +Proof. +compute-[View]. +simple refine (View_rec2 _ _ _ _). +- intros a b. apply class_of. apply (union a b). +- intros x x' Hxx' y y' Hyy'. simpl. + apply related_classes_eq. + unfold R in *. + eapply well_defined_union; eauto. +Defined. + +Ltac reduce := + intros ; + repeat (rewrite (f_empty T _) + || rewrite (f_singleton T _) + || rewrite (f_union T _) + || rewrite (f_filter T _) + || rewrite (f_member T _)). + +Instance View_member A: hasMembership (View A) A. +Proof. + intros a. + hrecursion. + - apply (member a). + - intros X Y HXY. + reduce. + unfold R, set_eq in HXY. rewrite HXY. + reflexivity. +Defined. + +Instance View_empty A: hasEmpty (View A). +Proof. + apply class_of. + apply ∅. +Defined. + +Instance View_singleton A: hasSingleton (View A) A. +Proof. + intros a. + apply class_of. + apply {|a|}. +Defined. + +Instance View_union A: hasUnion (View A). +Proof. + intros X Y. + apply (max_L X Y). +Defined. + +Instance View_comprehension A: hasComprehension (View A) A. +Proof. + intros ϕ. + hrecursion. + - intros X. + apply class_of. + apply (filter ϕ X). + - intros X X' HXX'. simpl. + apply related_classes_eq. + eapply well_defined_filter; eauto. +Defined. + +Instance View_max_comm A: Commutative (@max_L (View A) _). +Proof. + unfold Commutative. + hinduction. + - intros X. + hinduction. + + intros Y. cbn. + apply related_classes_eq. + eapply union_comm; eauto. + + intros. apply set_path2. + - intros. apply path_forall; intro. apply set_path2. +Defined. + +Ltac buggeroff := intros; + (repeat (apply path_forall; intro)); apply set_path2. + +Instance View_max_assoc A: Associative (@max_L (View A) _). +Proof. + unfold Associative. + hinduction; try buggeroff. + intros X. + hinduction; try buggeroff. + intros Y. + hinduction; try buggeroff. + intros Z. cbn. + apply related_classes_eq. + eapply union_assoc; eauto. +Defined. + +Instance View_max_idem A: Idempotent (@max_L (View A) _). +Proof. + unfold Idempotent. + hinduction; try buggeroff. + intros X; cbn. + apply related_classes_eq. + eapply union_idem; eauto. +Defined. + +Instance View_max_neut A: NeutralL (@max_L (View A) _) ∅. +Proof. + unfold NeutralL. + hinduction; try buggeroff. + intros X; cbn. + apply related_classes_eq. + eapply union_neutral; eauto. +Defined. + +End quot. diff --git a/prelude/HitTactics.v b/prelude/HitTactics.v index cd2a77d..e71773c 100644 --- a/prelude/HitTactics.v +++ b/prelude/HitTactics.v @@ -11,38 +11,39 @@ Definition hrecursion (H : Type) {HR : HitRecursion H} : @recTy H HR := Definition hinduction (H : Type) {HR : HitRecursion H} : @indTy H HR := @H_inductor H HR. + +(* TODO: use information from recTy instead of [typeof hrec]? *) Ltac hrecursion_ := lazymatch goal with | [ |- ?T -> ?P ] => let hrec1 := eval cbv[hrecursion H_recursor] in (hrecursion T) in let hrec := eval simpl in hrec1 in - match type of hrec with - | ?Q => - match (eval simpl in Q) with - | forall Y, T -> Y => - simple refine (hrec P) - | forall Y _, T -> Y => - simple refine (hrec P _) - | forall Y _ _, T -> Y => - simple refine (hrec P _ _) - | forall Y _ _ _, T -> Y => - simple refine (hrec P _ _ _) - | forall Y _ _ _ _, T -> Y => - simple refine (hrec P _ _ _ _) - | forall Y _ _ _ _ _, T -> Y => - simple refine (hrec P _ _ _ _ _) - | forall Y _ _ _ _ _ _, T -> Y => - simple refine (hrec P _ _ _ _ _ _) - | forall Y _ _ _ _ _ _ _, T -> Y => - simple refine (hrec P _ _ _ _ _ _ _) - | forall Y _ _ _ _ _ _ _ _, T -> Y => - simple refine (hrec P _ _ _ _ _ _ _ _) - | forall Y _ _ _ _ _ _ _ _ _, T -> Y => - simple refine (hrec P _ _ _ _ _ _ _ _ _) - | forall Y _ _ _ _ _ _ _ _ _ _, T -> Y => - simple refine (hrec P _ _ _ _ _ _ _ _ _ _) - | _ => fail "Cannot handle the recursion principle (too many parameters?) :(" - end + let hrecTy1 := eval cbv[recTy] in (@recTy T _) in + let hrecTy := eval simpl in hrecTy1 in + match hrecTy with + | forall Y, T -> Y => + simple refine (hrec P) + | forall Y _, T -> Y => + simple refine (hrec P _) + | forall Y _ _, T -> Y => + simple refine (hrec P _ _) + | forall Y _ _ _, T -> Y => + simple refine (hrec P _ _ _) + | forall Y _ _ _ _, T -> Y => + simple refine (hrec P _ _ _ _) + | forall Y _ _ _ _ _, T -> Y => + simple refine (hrec P _ _ _ _ _) + | forall Y _ _ _ _ _ _, T -> Y => + simple refine (hrec P _ _ _ _ _ _) + | forall Y _ _ _ _ _ _ _, T -> Y => + simple refine (hrec P _ _ _ _ _ _ _) + | forall Y _ _ _ _ _ _ _ _, T -> Y => + simple refine (hrec P _ _ _ _ _ _ _ _) + | forall Y _ _ _ _ _ _ _ _ _, T -> Y => + simple refine (hrec P _ _ _ _ _ _ _ _ _) + | forall Y _ _ _ _ _ _ _ _ _ _, T -> Y => + simple refine (hrec P _ _ _ _ _ _ _ _ _ _) + | _ => fail "Cannot handle the recursion principle (too many parameters?) :(" end | [ |- forall (target:?T), ?P] => let hind1 := eval cbv[hinduction H_inductor] in (hinduction T) in