mirror of https://github.com/nmvdw/HITs-Examples
trailing white spaces
This commit is contained in:
Leon Gondelman
parent
140b02e9f4
commit
f8ed41e5fe
|
|
@ -19,7 +19,6 @@ hrecursion.
|
|||
- intros a'. compute. destruct (A_deceq a a'); reflexivity.
|
||||
Defined.
|
||||
|
||||
Infix "∈" := isIn (at level 9, right associativity).
|
||||
|
||||
Definition comprehension :
|
||||
(A -> Bool) -> FSet A -> FSet A.
|
||||
|
|
@ -54,15 +53,16 @@ Proof.
|
|||
intros X Y.
|
||||
hrecursion X.
|
||||
- exact true.
|
||||
- exact (fun a => (a ∈ Y)).
|
||||
- exact (fun a => (isIn a Y)).
|
||||
- exact andb.
|
||||
- intros. compute. destruct x; reflexivity.
|
||||
- intros x y; compute; destruct x, y; reflexivity.
|
||||
- intros x; compute; destruct x; reflexivity.
|
||||
- intros x; compute; destruct x; reflexivity.
|
||||
- intros x; cbn; destruct (x ∈ Y); reflexivity.
|
||||
- intros x; cbn; destruct (isIn x Y); reflexivity.
|
||||
Defined.
|
||||
|
||||
Notation "⊆" := subset.
|
||||
|
||||
End operations.
|
||||
|
||||
Infix "∈" := isIn (at level 9, right associativity).
|
||||
Infix "⊆" := subset (at level 10, right associativity).
|
||||
|
|
@ -9,7 +9,7 @@ Context {A_deceq : DecidablePaths A}.
|
|||
(** union properties *)
|
||||
Theorem union_idem : forall x: FSet A, U x x = x.
|
||||
Proof.
|
||||
hinduction;
|
||||
hinduction;
|
||||
try (intros ; apply set_path2) ; cbn.
|
||||
- apply nl.
|
||||
- apply idem.
|
||||
|
|
@ -24,24 +24,24 @@ try (intros ; apply set_path2) ; cbn.
|
|||
reflexivity.
|
||||
Defined.
|
||||
|
||||
|
||||
|
||||
(** isIn properties *)
|
||||
Lemma isIn_singleton_eq (a b: A) : isIn a (L b) = true -> a = b.
|
||||
Proof. unfold isIn. simpl.
|
||||
Proof. unfold isIn. simpl.
|
||||
destruct (dec (a = b)). intro. apply p.
|
||||
intro X.
|
||||
intro X.
|
||||
contradiction (false_ne_true X).
|
||||
Defined.
|
||||
|
||||
Lemma isIn_empty_false (a: A) : isIn a E = true -> Empty.
|
||||
Proof.
|
||||
Proof.
|
||||
cbv. intro X.
|
||||
contradiction (false_ne_true X).
|
||||
contradiction (false_ne_true X).
|
||||
Defined.
|
||||
|
||||
Lemma isIn_union (a: A) (X Y: FSet A) :
|
||||
Lemma isIn_union (a: A) (X Y: FSet A) :
|
||||
isIn a (U X Y) = (isIn a X || isIn a Y)%Bool.
|
||||
Proof. reflexivity. Qed.
|
||||
Proof. reflexivity. Qed.
|
||||
|
||||
(** comprehension properties *)
|
||||
Lemma comprehension_false Y : comprehension (fun a => isIn a E) Y = E.
|
||||
|
|
@ -58,20 +58,20 @@ hrecursion Y; try (intros; apply set_path2).
|
|||
Defined.
|
||||
|
||||
Theorem comprehension_or : forall ϕ ψ (x: FSet A),
|
||||
comprehension (fun a => orb (ϕ a) (ψ a)) x = U (comprehension ϕ x)
|
||||
comprehension (fun a => orb (ϕ a) (ψ a)) x = U (comprehension ϕ x)
|
||||
(comprehension ψ x).
|
||||
Proof.
|
||||
intros ϕ ψ.
|
||||
hinduction; try (intros; apply set_path2).
|
||||
hinduction; try (intros; apply set_path2).
|
||||
- cbn. symmetry ; apply nl.
|
||||
- cbn. intros.
|
||||
destruct (ϕ a) ; destruct (ψ a) ; symmetry.
|
||||
* apply idem.
|
||||
* apply nr.
|
||||
* apply nr.
|
||||
* apply nl.
|
||||
* apply nl.
|
||||
- simpl. intros x y P Q.
|
||||
cbn.
|
||||
cbn.
|
||||
rewrite P.
|
||||
rewrite Q.
|
||||
rewrite <- assoc.
|
||||
|
|
@ -105,8 +105,8 @@ Defined.
|
|||
|
||||
(** intersection properties *)
|
||||
Lemma intersection_0l: forall X: FSet A, intersection E X = E.
|
||||
Proof.
|
||||
hinduction;
|
||||
Proof.
|
||||
hinduction;
|
||||
try (intros ; apply set_path2).
|
||||
- reflexivity.
|
||||
- intro a.
|
||||
|
|
@ -144,7 +144,7 @@ hinduction; try (intros ; apply set_path2).
|
|||
destruct (isIn a x) ; destruct (isIn a y).
|
||||
* apply idem.
|
||||
* apply nr.
|
||||
* apply nl.
|
||||
* apply nl.
|
||||
* apply nl.
|
||||
Defined.
|
||||
|
||||
|
|
@ -163,7 +163,7 @@ hrecursion X; try (intros; apply set_path2).
|
|||
* destruct (dec (b = a)) as [pb|]; [|reflexivity].
|
||||
by contradiction npa.
|
||||
+ cbn -[isIn]. intros Y1 Y2 IH1 IH2.
|
||||
rewrite IH1.
|
||||
rewrite IH1.
|
||||
rewrite IH2.
|
||||
symmetry.
|
||||
apply (comprehension_or (fun a => isIn a Y1) (fun a => isIn a Y2) (L a)).
|
||||
|
|
@ -171,7 +171,7 @@ hrecursion X; try (intros; apply set_path2).
|
|||
cbn.
|
||||
unfold intersection in *.
|
||||
rewrite <- IH1.
|
||||
rewrite <- IH2.
|
||||
rewrite <- IH2.
|
||||
apply comprehension_or.
|
||||
Defined.
|
||||
|
||||
|
|
@ -196,7 +196,7 @@ hinduction; try (intros; apply set_path2).
|
|||
Defined.
|
||||
|
||||
(** assorted lattice laws *)
|
||||
Lemma distributive_La (z : FSet A) (a : A) : forall Y : FSet A,
|
||||
Lemma distributive_La (z : FSet A) (a : A) : forall Y : FSet A,
|
||||
intersection (U (L a) z) Y = U (intersection (L a) Y) (intersection z Y).
|
||||
Proof.
|
||||
hinduction; try (intros ; apply set_path2) ; cbn.
|
||||
|
|
@ -266,7 +266,7 @@ hinduction x; try (intros ; apply set_path2) ; cbn.
|
|||
cbn.
|
||||
rewrite P.
|
||||
rewrite Q.
|
||||
destruct (isIn a X1) ; destruct (isIn a X2) ; destruct (isIn a y) ;
|
||||
destruct (isIn a X1) ; destruct (isIn a X2) ; destruct (isIn a y) ;
|
||||
reflexivity.
|
||||
Defined.
|
||||
|
||||
|
|
@ -292,7 +292,7 @@ hinduction X; try (intros ; apply set_path2).
|
|||
+ reflexivity.
|
||||
+ reflexivity.
|
||||
* rewrite intersection_0l.
|
||||
reflexivity.
|
||||
reflexivity.
|
||||
- unfold intersection. cbn.
|
||||
intros X1 X2 P Q.
|
||||
rewrite comprehension_or.
|
||||
|
|
@ -324,7 +324,7 @@ hinduction; try (intros ; apply set_path2).
|
|||
reflexivity.
|
||||
Defined.
|
||||
|
||||
|
||||
|
||||
Theorem distributive_U_int (X1 X2 Y : FSet A) :
|
||||
U (intersection X1 X2) Y = intersection (U X1 Y) (U X2 Y).
|
||||
Proof.
|
||||
|
|
@ -347,9 +347,9 @@ hinduction X1; try (intros ; apply set_path2) ; cbn.
|
|||
cbn.
|
||||
intros Z1 Z2 P Q.
|
||||
rewrite comprehension_or.
|
||||
assert (U (U (comprehension (fun a : A => isIn a Z1) X2)
|
||||
assert (U (U (comprehension (fun a : A => isIn a Z1) X2)
|
||||
(comprehension (fun a : A => isIn a Z2) X2))
|
||||
Y = U (U (comprehension (fun a : A => isIn a Z1) X2)
|
||||
Y = U (U (comprehension (fun a : A => isIn a Z1) X2)
|
||||
(comprehension (fun a : A => isIn a Z2) X2))
|
||||
(U Y Y)).
|
||||
rewrite (union_idem Y).
|
||||
|
|
@ -358,7 +358,7 @@ hinduction X1; try (intros ; apply set_path2) ; cbn.
|
|||
rewrite <- assoc.
|
||||
rewrite (assoc (comprehension (fun a : A => isIn a Z2) X2)).
|
||||
rewrite Q.
|
||||
rewrite
|
||||
rewrite
|
||||
(comm (U (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2)
|
||||
(comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y)) Y).
|
||||
rewrite assoc.
|
||||
|
|
@ -369,11 +369,11 @@ hinduction X1; try (intros ; apply set_path2) ; cbn.
|
|||
rewrite <- assoc.
|
||||
rewrite assoc.
|
||||
enough (C : (U (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) X2)
|
||||
(comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2))
|
||||
(comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2))
|
||||
= (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) X2)).
|
||||
rewrite C.
|
||||
rewrite C.
|
||||
enough (D : (U (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) Y)
|
||||
(comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y))
|
||||
(comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y))
|
||||
= (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) Y)).
|
||||
rewrite D.
|
||||
reflexivity.
|
||||
|
|
@ -438,12 +438,12 @@ Admitted.
|
|||
|
||||
|
||||
(* Properties about subset relation. *)
|
||||
Lemma subsect_intersection `{Funext} (X Y : FSet A) :
|
||||
subset X Y = true -> U X Y = Y.
|
||||
Lemma subsect_intersection `{Funext} (X Y : FSet A) :
|
||||
X ⊆ Y = true -> U X Y = Y.
|
||||
Proof.
|
||||
hinduction X; try (intros; apply path_forall; intro; apply set_path2).
|
||||
- intros. apply nl.
|
||||
- intros a. hinduction Y;
|
||||
- intros a. hinduction Y;
|
||||
try (intros; apply path_forall; intro; apply set_path2).
|
||||
(*intros. apply equiv_hprop_allpath.*)
|
||||
+ intro. cbn. contradiction (false_ne_true).
|
||||
|
|
@ -460,10 +460,10 @@ hinduction X; try (intros; apply path_forall; intro; apply set_path2).
|
|||
specialize (IH1 idpath).
|
||||
rewrite assoc. rewrite IH1. reflexivity.
|
||||
specialize (IH2 idpath).
|
||||
rewrite assoc. rewrite (comm (L a)). rewrite <- assoc. rewrite IH2.
|
||||
rewrite assoc. rewrite (comm (L a)). rewrite <- assoc. rewrite IH2.
|
||||
reflexivity.
|
||||
cbn in Ho. contradiction (false_ne_true).
|
||||
- intros X1 X2 IH1 IH2 G.
|
||||
cbn in Ho. contradiction (false_ne_true).
|
||||
- intros X1 X2 IH1 IH2 G.
|
||||
destruct (subset X1 Y);
|
||||
destruct (subset X2 Y).
|
||||
specialize (IH1 idpath).
|
||||
|
|
@ -479,4 +479,6 @@ hinduction X; try (intros; apply path_forall; intro; apply set_path2).
|
|||
rewrite <- assoc. rewrite IH2. rewrite IH1. reflexivity.
|
||||
Defined.
|
||||
|
||||
End properties.
|
||||
Theorem
|
||||
|
||||
End properties.
|
||||
|
|
|
|||
Loading…
Reference in New Issue