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

Finish the comprehension_idem proof with functional extensionality

Browse Source
This commit is contained in:
Dan Frumin
2017-05-23 00:17:33 +02:00
parent f23d4aeacb
commit 2f68e833af
1 changed files with 26 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

30
FinSets.v
View File

@@ -334,6 +334,19 @@ Parameter A : Type.
Parameter A_eqdec : forall (x y : A), Decidable (x = y). Parameter A_eqdec : forall (x y : A), Decidable (x = y).
Definition deceq (x y : A) := Definition deceq (x y : A) :=
if dec (x = y) then true else false. if dec (x = y) then true else false.
Lemma union_idem : forall (X : FSet A), U X X = X.
Proof.
hinduction; try (intros; apply set_path2).
- apply nr.
- intros. apply idem.
- intros X Y HX HY. etransitivity.
rewrite assoc. rewrite (comm _ X Y). rewrite <- (assoc _ Y X X).
rewrite comm.
rewrite assoc. rewrite HX. rewrite HY. reflexivity.
rewrite comm. reflexivity.
Defined.
Definition isIn : A -> FSet A -> Bool. Definition isIn : A -> FSet A -> Bool.
Proof. Proof.
intros a. intros a.
@@ -397,11 +410,11 @@ hrecursion Y; try (intros; apply set_path2).
reflexivity. reflexivity.
Defined. Defined.
Require Import FunextAxiom. Lemma comprehension_idem' `{Funext}:
Lemma comprehension_idem:
forall (X:FSet A), forall Y, comprehension (fun x => isIn x (U X Y)) X = X. forall (X:FSet A), forall Y, comprehension (fun x => isIn x (U X Y)) X = X.
Proof. Proof.
hinduction; try (intros; apply set_path2). hinduction.
all: try (intros; apply path_forall; intro; apply set_path2).
- intro Y. cbv. reflexivity. - intro Y. cbv. reflexivity.
- intros a Y. cbn. - intros a Y. cbn.
unfold deceq; unfold deceq;
@@ -415,7 +428,16 @@ hinduction; try (intros; apply set_path2).
+ rewrite (comm _ X1 X2). + rewrite (comm _ X1 X2).
rewrite <- (assoc _ X2 X1 Y). rewrite <- (assoc _ X2 X1 Y).
apply (IH2 (U X1 Y)). apply (IH2 (U X1 Y)).
Admitted. Defined.
Lemma comprehension_idem `{Funext}:
forall (X:FSet A), comprehension (fun x => isIn x X) X = X.
Proof.
intros X.
enough (comprehension (fun x : A => isIn x (U X X)) X = X).
rewrite (union_idem) in X0. assumption.
apply comprehension_idem'.
Defined.
Definition intersection : Definition intersection :
FSet A -> FSet A -> FSet A. FSet A -> FSet A -> FSet A.