dan/HITs-Examples
1
0
Fork 0
mirror of https://github.com/nmvdw/HITs-Examples synced 2025-11-03 23:23:51 +01:00
Code Issues Releases Wiki Activity

further simplifications

Browse Source
This commit is contained in:
Niels
2017-08-15 22:26:26 +02:00
parent e1bc900abc
commit 920fdd91ab
1 changed files with 17 additions and 23 deletions
Download Patch File Download Diff File Expand all files Collapse all files

40
FiniteSets/implementations/interface.v
View File

@@ -152,32 +152,26 @@ Section quotient_properties.
Definition set_eq A := f_eq (T A) (FSet A) (f A). Definition set_eq A := f_eq (T A) (FSet A) (f A).
Definition View A : Type := quotientB (T A) (FSet A) (f A). Definition View A : Type := quotientB (T A) (FSet A) (f A).
Definition View_rec2 {A} (P : Type) (HP : IsHSet P) (u : T A -> T A -> P) : Definition View_rec2 {A} (P : Type) (HP : IsHSet P) (u : T A -> T A -> P)
(forall (x x' : T A), set_eq A x x' -> forall (y y' : T A), set_eq A y y' -> u x y = u x' y') -> (Hresp : forall (x x' y y': T A), set_eq A x x' -> set_eq A y y' -> u x y = u x' y')
forall (x y : View A), P. : forall (x y : View A), P.
Proof. Proof.
intros Hresp. unfold View ; hrecursion.
assert (resp1 : forall x y y', set_eq A y y' -> u x y = u x y').
{ intros x y y'.
apply (Hresp _ _ idpath).
}
assert (resp2 : forall x x' y, set_eq A x x' -> u x y = u x' y).
{ intros x x' y Hxx'.
apply Hresp. apply Hxx'.
reflexivity. }
unfold View.
hrecursion.
- intros a. - intros a.
hrecursion. hrecursion.
+ intros b. + apply (u a).
apply (u a b). + intros b b' Hbb'.
+ intros b b' Hbb'. simpl. apply Hresp.
by apply resp1. ++ reflexivity.
- intros a a' Haa'. simpl. ++ assumption.
apply path_forall. red. - intros ; simpl.
hinduction. apply path_forall.
+ intros b. apply resp2. apply Haa'. red.
+ intros; apply HP. hinduction ; try (intros ; apply path_ishprop).
intros b.
apply Hresp.
++ assumption.
++ reflexivity.
Defined. Defined.
Definition well_defined_union (A : Type) (X1 X2 Y1 Y2 : T A) : Definition well_defined_union (A : Type) (X1 X2 Y1 Y2 : T A) :