dan
/
HITs-Examples
mirror of https://github.com/nmvdw/HITs-Examples
1
0
Fork 0
Code Issues Releases Wiki Activity

Clean up the interface.v proofs

This commit is contained in:
Dan Frumin 2017-08-08 13:18:45 +02:00
parent 4a98d84cbc
commit 4ade6e60cc
1 changed files with 30 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

61
FiniteSets/implementations/interface.v
View File

@ -53,77 +53,72 @@ Section properties.
Definition set_subset : forall A, T A -> T A -> hProp :=
fun A X Y => (f A X) ⊆ (f A Y).
Ltac reduce := intros ; repeat (rewrite ?(f_empty _ _) ; rewrite ?(f_singleton _ _) ;
rewrite ?(f_union _ _) ; rewrite ?(f_filter _ _) ;
rewrite ?(f_member _ _)).
Ltac reduce :=
intros ;
repeat (rewrite (f_empty _ _)
|| rewrite ?(f_singleton _ _)
|| rewrite ?(f_union _ _)
|| rewrite ?(f_filter _ _)
|| rewrite ?(f_member _ _)).
Definition empty_isIn : forall (A : Type) (a : A), member a empty = False_hp.
Definition empty_isIn : forall (A : Type) (a : A),
member a empty = False_hp.
Proof.
reduce.
reflexivity.
by reduce.
Defined.
Definition singleton_isIn : forall (A : Type) (a b : A),
member a (singleton b) = BuildhProp (Trunc (-1) (a = b)).
member a (singleton b) = merely (a = b).
Proof.
reduce.
reflexivity.
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).
member a (union X Y) = lor (member a X) (member a Y).
Proof.
reduce.
reflexivity.
by reduce.
Defined.
Definition filter_isIn : forall (A : Type) (a : A) (ϕ : A -> Bool) (X : T A),
member a (filter ϕ X) = if ϕ a then member a X else False_hp.
member a (filter ϕ X) = if ϕ a then member a X else False_hp.
Proof.
reduce.
apply properties.comprehension_isIn.
Defined.
Definition reflect_eq : forall (A : Type) (X Y : T A),
f A X = f A Y -> set_eq A X Y.
Proof.
auto.
Defined.
f A X = f A Y -> set_eq A X Y.
Proof. done. Defined.
Definition reflect_subset : forall (A : Type) (X Y : T A),
subset (f A X) (f A Y) -> set_subset A X Y.
Proof.
auto.
Defined.
subset (f A X) (f A Y) -> set_subset A X Y.
Proof. done. Defined.
Hint Unfold set_eq set_subset.
Ltac simplify := intros ; autounfold in * ; apply reflect_eq ; reduce.
Definition well_defined_union : forall (A : Type) (X1 X2 Y1 Y2 : T A),
set_eq A X1 Y1 -> set_eq A X2 Y2 -> set_eq A (union X1 X2) (union Y1 Y2).
set_eq A X1 Y1 -> set_eq A X2 Y2 -> set_eq A (union X1 X2) (union Y1 Y2).
Proof.
intros A X1 X2 Y1 Y2 HXY1 HXY2.
simplify.
rewrite X, X0.
reflexivity.
by rewrite HXY1, HXY2.
Defined.
Definition well_defined_filter : forall (A : Type) (ϕ : A -> Bool) (X Y : T A),
set_eq A X Y -> set_eq A (filter ϕ X) (filter ϕ Y).
set_eq A X Y -> set_eq A (filter ϕ X) (filter ϕ Y).
Proof.
intros A ϕ X Y HXY.
simplify.
rewrite X0.
reflexivity.
by rewrite HXY.
Defined.
Variable (A : Type).
Context `{DecidablePaths A}.
Lemma union_comm : forall (X Y : T A),
set_eq A (union X Y) (union Y X).
Lemma union_comm : forall A (X Y : T A),
set_eq A (union X Y) (union Y X).
Proof.
simplify.
apply lattice_fset.
apply comm.
Defined.
End properties.