Some cleanup

This commit is contained in:
Niels 2017-08-01 15:12:59 +02:00
parent 37e3017cfc
commit fed9546d11
16 changed files with 659 additions and 1733 deletions

638
FSet.v
View File

@ -1,638 +0,0 @@
Require Import HoTT.
Require Export HoTT.
Require Import FunextAxiom.
Module Export FinSet.
Section FSet.
Variable A : Type.
Private Inductive FSet : Type :=
| E : FSet
| L : A -> FSet
| U : FSet -> FSet -> FSet.
Notation "{| x |}" := (L x).
Infix "" := U (at level 8, right associativity).
Notation "" := E.
Axiom assoc : forall (x y z : FSet ),
x (y z) = (x y) z.
Axiom comm : forall (x y : FSet),
x y = y x.
Axiom nl : forall (x : FSet),
x = x.
Axiom nr : forall (x : FSet),
x = x.
Axiom idem : forall (x : A),
{| x |} {|x|} = {|x|}.
Axiom trunc : IsHSet FSet.
Fixpoint FSet_rec
(P : Type)
(H: IsHSet P)
(e : P)
(l : A -> P)
(u : P -> P -> P)
(assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
(commP : forall (x y : P), u x y = u y x)
(nlP : forall (x : P), u e x = x)
(nrP : forall (x : P), u x e = x)
(idemP : forall (x : A), u (l x) (l x) = l x)
(x : FSet)
{struct x}
: P
:= (match x return _ -> _ -> _ -> _ -> _ -> _ -> P with
| E => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => e
| L a => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => l a
| U y z => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => u
(FSet_rec P H e l u assocP commP nlP nrP idemP y)
(FSet_rec P H e l u assocP commP nlP nrP idemP z)
end) assocP commP nlP nrP idemP H.
Axiom FSet_rec_beta_assoc : forall
(P : Type)
(H: IsHSet P)
(e : P)
(l : A -> P)
(u : P -> P -> P)
(assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
(commP : forall (x y : P), u x y = u y x)
(nlP : forall (x : P), u e x = x)
(nrP : forall (x : P), u x e = x)
(idemP : forall (x : A), u (l x) (l x) = l x)
(x y z : FSet),
ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (assoc x y z)
=
(assocP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
(FSet_rec P H e l u assocP commP nlP nrP idemP y)
(FSet_rec P H e l u assocP commP nlP nrP idemP z)
).
Axiom FSet_rec_beta_comm : forall
(P : Type)
(H: IsHSet P)
(e : P)
(l : A -> P)
(u : P -> P -> P)
(assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
(commP : forall (x y : P), u x y = u y x)
(nlP : forall (x : P), u e x = x)
(nrP : forall (x : P), u x e = x)
(idemP : forall (x : A), u (l x) (l x) = l x)
(x y : FSet),
ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (comm x y)
=
(commP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
(FSet_rec P H e l u assocP commP nlP nrP idemP y)
).
Axiom FSet_rec_beta_nl : forall
(P : Type)
(H: IsHSet P)
(e : P)
(l : A -> P)
(u : P -> P -> P)
(assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
(commP : forall (x y : P), u x y = u y x)
(nlP : forall (x : P), u e x = x)
(nrP : forall (x : P), u x e = x)
(idemP : forall (x : A), u (l x) (l x) = l x)
(x : FSet),
ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (nl x)
=
(nlP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
).
Axiom FSet_rec_beta_nr : forall
(P : Type)
(H: IsHSet P)
(e : P)
(l : A -> P)
(u : P -> P -> P)
(assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
(commP : forall (x y : P), u x y = u y x)
(nlP : forall (x : P), u e x = x)
(nrP : forall (x : P), u x e = x)
(idemP : forall (x : A), u (l x) (l x) = l x)
(x : FSet),
ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (nr x)
=
(nrP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
).
Axiom FSet_rec_beta_idem : forall
(P : Type)
(H: IsHSet P)
(e : P)
(l : A -> P)
(u : P -> P -> P)
(assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
(commP : forall (x y : P), u x y = u y x)
(nlP : forall (x : P), u e x = x)
(nrP : forall (x : P), u x e = x)
(idemP : forall (x : A), u (l x) (l x) = l x)
(x : A),
ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (idem x)
=
idemP x.
(* Induction principle *)
Fixpoint FSet_ind
(P : FSet -> Type)
(H : forall a : FSet, IsHSet (P a))
(eP : P E)
(lP : forall a: A, P (L a))
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
(assocP : forall (x y z : FSet)
(px: P x) (py: P y) (pz: P z),
assoc x y z #
(uP x (U y z) px (uP y z py pz))
=
(uP (U x y) z (uP x y px py) pz))
(commP : forall (x y: FSet) (px: P x) (py: P y),
comm x y #
uP x y px py = uP y x py px)
(nlP : forall (x : FSet) (px: P x),
nl x # uP E x eP px = px)
(nrP : forall (x : FSet) (px: P x),
nr x # uP x E px eP = px)
(idemP : forall (x : A),
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
(x : FSet)
{struct x}
: P x
:= (match x return _ -> _ -> _ -> _ -> _ -> _ -> P x with
| E => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => eP
| L a => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => lP a
| U y z => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => uP y z
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP z)
end) H assocP commP nlP nrP idemP.
Axiom FSet_ind_beta_assoc : forall
(P : FSet -> Type)
(H : forall a : FSet, IsHSet (P a))
(eP : P E)
(lP : forall a: A, P (L a))
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
(assocP : forall (x y z : FSet)
(px: P x) (py: P y) (pz: P z),
assoc x y z #
(uP x (U y z) px (uP y z py pz))
=
(uP (U x y) z (uP x y px py) pz))
(commP : forall (x y: FSet) (px: P x) (py: P y),
comm x y #
uP x y px py = uP y x py px)
(nlP : forall (x : FSet) (px: P x),
nl x # uP E x eP px = px)
(nrP : forall (x : FSet) (px: P x),
nr x # uP x E px eP = px)
(idemP : forall (x : A),
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
(x y z : FSet),
apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP)
(assoc x y z)
=
(assocP x y z
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP z)
).
Axiom FSet_ind_beta_comm : forall
(P : FSet -> Type)
(H : forall a : FSet, IsHSet (P a))
(eP : P E)
(lP : forall a: A, P (L a))
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
(assocP : forall (x y z : FSet)
(px: P x) (py: P y) (pz: P z),
assoc x y z #
(uP x (U y z) px (uP y z py pz))
=
(uP (U x y) z (uP x y px py) pz))
(commP : forall (x y : FSet) (px: P x) (py: P y),
comm x y #
uP x y px py = uP y x py px)
(nlP : forall (x : FSet) (px: P x),
nl x # uP E x eP px = px)
(nrP : forall (x : FSet) (px: P x),
nr x # uP x E px eP = px)
(idemP : forall (x : A),
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
(x y : FSet),
apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (comm x y)
=
(commP x y
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
).
Axiom FSet_ind_beta_nl : forall
(P : FSet -> Type)
(H : forall a : FSet, IsHSet (P a))
(eP : P E)
(lP : forall a: A, P (L a))
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
(assocP : forall (x y z : FSet)
(px: P x) (py: P y) (pz: P z),
assoc x y z #
(uP x (U y z) px (uP y z py pz))
=
(uP (U x y) z (uP x y px py) pz))
(commP : forall (x y : FSet) (px: P x) (py: P y),
comm x y #
uP x y px py = uP y x py px)
(nlP : forall (x : FSet) (px: P x),
nl x # uP E x eP px = px)
(nrP : forall (x : FSet) (px: P x),
nr x # uP x E px eP = px)
(idemP : forall (x : A),
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
(x : FSet),
apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (nl x)
=
(nlP x (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
).
Axiom FSet_ind_beta_nr : forall
(P : FSet -> Type)
(H : forall a : FSet, IsHSet (P a))
(eP : P E)
(lP : forall a: A, P (L a))
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
(assocP : forall (x y z : FSet)
(px: P x) (py: P y) (pz: P z),
assoc x y z #
(uP x (U y z) px (uP y z py pz))
=
(uP (U x y) z (uP x y px py) pz))
(commP : forall (x y : FSet) (px: P x) (py: P y),
comm x y #
uP x y px py = uP y x py px)
(nlP : forall (x : FSet) (px: P x),
nl x # uP E x eP px = px)
(nrP : forall (x : FSet) (px: P x),
nr x # uP x E px eP = px)
(idemP : forall (x : A),
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
(x : FSet),
apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (nr x)
=
(nrP x (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
).
Axiom FSet_ind_beta_idem : forall
(P : FSet -> Type)
(H : forall a : FSet, IsHSet (P a))
(eP : P E)
(lP : forall a: A, P (L a))
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
(assocP : forall (x y z : FSet)
(px: P x) (py: P y) (pz: P z),
assoc x y z #
(uP x (U y z) px (uP y z py pz))
=
(uP (U x y) z (uP x y px py) pz))
(commP : forall (x y : FSet) (px: P x) (py: P y),
comm x y #
uP x y px py = uP y x py px)
(nlP : forall (x : FSet) (px: P x),
nl x # uP E x eP px = px)
(nrP : forall (x : FSet) (px: P x),
nr x # uP x E px eP = px)
(idemP : forall (x : A),
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
(x : A),
apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (idem x)
=
idemP x.
End FSet.
Parameter A : Type.
Parameter A_eqdec : forall (x y : A), Decidable (x = y).
Definition deceq (x y : A) :=
if dec (x = y) then true else false.
Theorem deceq_sym : forall x y, deceq x y = deceq y x.
Proof.
intros x y.
unfold deceq.
destruct (dec (x = y)) ; destruct (dec (y = x)) ; cbn.
- reflexivity.
- pose (n (p^)) ; contradiction.
- pose (n (p^)) ; contradiction.
- reflexivity.
Defined.
Arguments E {_}.
Arguments U {_} _ _.
Arguments L {_} _.
Theorem idemU : forall x : FSet A, U x x = x.
Proof.
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; try (intros ; apply set_path2) ; cbn.
- apply nl.
- apply idem.
- intros x y P Q.
etransitivity. apply assoc.
etransitivity. apply (ap (fun p => U (U p x) y) (comm A x y)).
etransitivity. apply (ap (fun p => U p y) (assoc A y x x))^.
etransitivity. apply (ap (fun p => U (U y p) y) P).
etransitivity. apply (ap (fun p => U p y) (comm A y x)).
etransitivity. apply (assoc A x y y)^.
apply (ap (fun p => U x p) Q).
Defined.
Definition isIn : A -> FSet A -> Bool.
Proof.
intros a.
simple refine (FSet_rec A _ _ _ _ _ _ _ _ _ _).
- exact false.
- intro a'. apply (deceq a a').
- apply orb.
- intros x y z. destruct x; reflexivity.
- intros x y. destruct x, y; reflexivity.
- intros x. reflexivity.
- intros x. destruct x; reflexivity.
- intros a'. destruct (deceq a a'); reflexivity.
Defined.
Definition comprehension :
(A -> Bool) -> FSet A -> FSet A.
Proof.
intros P.
simple refine (FSet_rec A _ _ _ _ _ _ _ _ _ _).
- apply E.
- intro a.
refine (if (P a) then L a else E).
- apply U.
- intros. apply assoc.
- intros. apply comm.
- intros. apply nl.
- intros. apply nr.
- intros. cbn.
destruct (P x).
+ apply idem.
+ apply nl.
Defined.
Theorem comprehension_or : forall ϕ ψ x,
comprehension (fun a => orb (ϕ a) (ψ a)) x = U (comprehension ϕ x) (comprehension ψ x).
Proof.
intros ϕ ψ.
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; try (intros ; apply set_path2).
- cbn. symmetry ; apply nl.
- cbn. intros.
destruct (ϕ a) ; destruct (ψ a) ; symmetry.
* apply idem.
* apply nr.
* apply nl.
* apply nl.
- simpl. intros x y P Q.
cbn.
rewrite P.
rewrite Q.
rewrite <- assoc.
rewrite (assoc A (comprehension ψ x)).
rewrite (comm A (comprehension ψ x) (comprehension ϕ y)).
rewrite <- assoc.
rewrite <- assoc.
reflexivity.
Defined.
Definition intersection (X Y : FSet A) : FSet A := comprehension (fun (a : A) => isIn a X) Y.
Theorem intersection_idem : forall x, intersection x x = x.
Proof.
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; try (intros ; apply set_path2) ; cbn.
- reflexivity.
- intro a.
unfold deceq.
destruct (dec (a = a)).
* reflexivity.
* pose (n idpath) ; contradiction.
- intros x y P Q.
rewrite comprehension_or.
rewrite comprehension_or.
unfold intersection in P.
unfold intersection in Q.
rewrite P.
rewrite Q.
Admitted.
Theorem intersection_EX : forall x,
intersection E x = E.
Proof.
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; try (intros ; apply set_path2).
- reflexivity.
- intro a.
reflexivity.
- unfold intersection.
intros x y P Q.
cbn.
rewrite P.
rewrite Q.
apply nl.
Defined.
Definition intersection_XE x : intersection x E = E := idpath.
Theorem intersection_La : forall a x,
intersection (L a) x = if isIn a x then L a else E.
Proof.
intro a.
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; try (intros ; apply set_path2).
- reflexivity.
- intro b.
cbn.
rewrite deceq_sym.
unfold deceq.
destruct (dec (a = b)).
* rewrite p ; reflexivity.
* reflexivity.
- unfold intersection.
intros x y P Q.
cbn.
rewrite P.
rewrite Q.
destruct (isIn a x) ; destruct (isIn a y).
* apply idem.
* apply nr.
* apply nl.
* apply nl.
Defined.
(*
Theorem intersection_comm : forall x y,
intersection x y = intersection y x.
Proof.
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; cbn.
- intros.
rewrite intersection_E.
reflexivity.
- intros a.
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; cbn.
* reflexivity.
* intro b.
admit.
* intros x y.
destruct (isIn a x) ; destruct (isIn a y) ; intros P Q.
+ rewrite P.
*)
Theorem comp_false : forall x,
comprehension (fun _ => false) x = E.
Proof.
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; try (intros ; apply set_path2) ; cbn.
- reflexivity.
- intro a ; reflexivity.
- intros x y P Q.
rewrite P.
rewrite Q.
apply nl.
Defined.
(*Theorem union_dist : forall x y z,
intersection z (U x y) = U (intersection z x) (intersection z y).
Proof.
intros x y.
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; cbn.
- rewrite intersection_E.
rewrite intersection_E.
rewrite comp_false.
rewrite comp_false.
reflexivity.
- intro a.
*)
Theorem union_dist : forall x y z,
intersection (U x y) z = U (intersection x z) (intersection y z).
Proof.
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; cbn.
- intros.
rewrite nl.
rewrite intersection_EX.
rewrite nl.
reflexivity.
- intro a.
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; cbn.
* intros.
rewrite nr.
rewrite intersection_EX.
rewrite nr.
reflexivity.
* intros b.
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; cbn.
+ rewrite nl. reflexivity.
+ intros c.
unfold deceq.
destruct (dec (c = a)) ; destruct (dec (c = b)) ; cbn.
{ rewrite idem. reflexivity. }
{ rewrite nr. reflexivity. }
{ rewrite nl. reflexivity. }
{ rewrite nl. reflexivity. }
+ intros x y P Q.
rewrite comprehension_or.
rewrite comprehension_or.
rewrite assoc.
rewrite <- (assoc A (comprehension (fun a0 : A => deceq a0 a) x) (comprehension (fun a0 : A => deceq a0 b) x)).
rewrite (comm A (comprehension (fun a0 : A => deceq a0 b) x) (comprehension (fun a0 : A => deceq a0 a) y)).
rewrite assoc.
rewrite <- assoc.
reflexivity.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
* intros x y P Q z.
cbn.
Admitted.
Theorem intersection_isIn : forall a x y,
isIn a (intersection x y) = andb (isIn a x) (isIn a y).
Proof.
intros a.
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; cbn.
- intros y.
rewrite intersection_EX.
reflexivity.
- intros b y.
rewrite intersection_La.
unfold deceq.
destruct (dec (a = b)) ; cbn.
* rewrite p.
destruct (isIn b y).
+ cbn.
unfold deceq.
destruct (dec (b = b)).
{ reflexivity. }
{ pose (n idpath). contradiction. }
+ reflexivity.
* destruct (isIn b y).
+ cbn.
unfold deceq.
destruct (dec (a = b)).
{ pose (n p). contradiction. }
{ reflexivity. }
+ reflexivity.
- intros x y P Q z.
rewrite union_dist.
cbn.
rewrite P.
rewrite Q.
destruct (isIn a x) ; destruct (isIn a y) ; destruct (isIn a z) ; reflexivity.
Admitted.
Theorem intersection_assoc x y z :
intersection x (intersection y z) = intersection (intersection x y) z.
Proof.
simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _ x) ; cbn ; try (intros ; apply set_path2).
- intros.
exact _.
- cbn.
rewrite intersection_E.
rewrite intersection_E.
rewrite intersection_E.
reflexivity.
- intros a y z.
cbn.
rewrite intersection_La.
rewrite intersection_La.
rewrite intersection_isIn.
destruct (isIn a y).
* rewrite intersection_La.
destruct (isIn a z).
+ reflexivity.
+ reflexivity.
* rewrite intersection_E.
reflexivity.
- unfold intersection. cbn.
intros x y P Q z z'.
rewrite comprehension_or.
rewrite P.
rewrite Q.
rewrite comprehension_or.
cbn.
rewrite comprehension_or.
reflexivity.
Admitted.

532
FinSets.v
View File

@ -1,532 +0,0 @@
Require Export HoTT.
Require Import HitTactics.
Module Export FinSet.
Section FSet.
Variable A : Type.
Private Inductive FSet : Type :=
| E : FSet
| L : A -> FSet
| U : FSet -> FSet -> FSet.
Notation "{| x |}" := (L x).
Infix "" := U (at level 8, right associativity).
Notation "" := E.
Axiom assoc : forall (x y z : FSet ),
x (y z) = (x y) z.
Axiom comm : forall (x y : FSet),
x y = y x.
Axiom nl : forall (x : FSet),
x = x.
Axiom nr : forall (x : FSet),
x = x.
Axiom idem : forall (x : A),
{| x |} {|x|} = {|x|}.
Axiom trunc : IsHSet FSet.
Fixpoint FSet_rec
(P : Type)
(H: IsHSet P)
(e : P)
(l : A -> P)
(u : P -> P -> P)
(assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
(commP : forall (x y : P), u x y = u y x)
(nlP : forall (x : P), u e x = x)
(nrP : forall (x : P), u x e = x)
(idemP : forall (x : A), u (l x) (l x) = l x)
(x : FSet)
{struct x}
: P
:= (match x return _ -> _ -> _ -> _ -> _ -> _ -> P with
| E => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => e
| L a => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => l a
| U y z => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => u
(FSet_rec P H e l u assocP commP nlP nrP idemP y)
(FSet_rec P H e l u assocP commP nlP nrP idemP z)
end) assocP commP nlP nrP idemP H.
Axiom FSet_rec_beta_assoc : forall
(P : Type)
(H: IsHSet P)
(e : P)
(l : A -> P)
(u : P -> P -> P)
(assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
(commP : forall (x y : P), u x y = u y x)
(nlP : forall (x : P), u e x = x)
(nrP : forall (x : P), u x e = x)
(idemP : forall (x : A), u (l x) (l x) = l x)
(x y z : FSet),
ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (assoc x y z)
=
(assocP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
(FSet_rec P H e l u assocP commP nlP nrP idemP y)
(FSet_rec P H e l u assocP commP nlP nrP idemP z)
).
Axiom FSet_rec_beta_comm : forall
(P : Type)
(H: IsHSet P)
(e : P)
(l : A -> P)
(u : P -> P -> P)
(assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
(commP : forall (x y : P), u x y = u y x)
(nlP : forall (x : P), u e x = x)
(nrP : forall (x : P), u x e = x)
(idemP : forall (x : A), u (l x) (l x) = l x)
(x y : FSet),
ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (comm x y)
=
(commP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
(FSet_rec P H e l u assocP commP nlP nrP idemP y)
).
Axiom FSet_rec_beta_nl : forall
(P : Type)
(H: IsHSet P)
(e : P)
(l : A -> P)
(u : P -> P -> P)
(assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
(commP : forall (x y : P), u x y = u y x)
(nlP : forall (x : P), u e x = x)
(nrP : forall (x : P), u x e = x)
(idemP : forall (x : A), u (l x) (l x) = l x)
(x : FSet),
ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (nl x)
=
(nlP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
).
Axiom FSet_rec_beta_nr : forall
(P : Type)
(H: IsHSet P)
(e : P)
(l : A -> P)
(u : P -> P -> P)
(assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
(commP : forall (x y : P), u x y = u y x)
(nlP : forall (x : P), u e x = x)
(nrP : forall (x : P), u x e = x)
(idemP : forall (x : A), u (l x) (l x) = l x)
(x : FSet),
ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (nr x)
=
(nrP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
).
Axiom FSet_rec_beta_idem : forall
(P : Type)
(H: IsHSet P)
(e : P)
(l : A -> P)
(u : P -> P -> P)
(assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
(commP : forall (x y : P), u x y = u y x)
(nlP : forall (x : P), u e x = x)
(nrP : forall (x : P), u x e = x)
(idemP : forall (x : A), u (l x) (l x) = l x)
(x : A),
ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (idem x)
=
idemP x.
(* Induction principle *)
Fixpoint FSet_ind
(P : FSet -> Type)
(H : forall a : FSet, IsHSet (P a))
(eP : P E)
(lP : forall a: A, P (L a))
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
(assocP : forall (x y z : FSet)
(px: P x) (py: P y) (pz: P z),
assoc x y z #
(uP x (U y z) px (uP y z py pz))
=
(uP (U x y) z (uP x y px py) pz))
(commP : forall (x y: FSet) (px: P x) (py: P y),
comm x y #
uP x y px py = uP y x py px)
(nlP : forall (x : FSet) (px: P x),
nl x # uP E x eP px = px)
(nrP : forall (x : FSet) (px: P x),
nr x # uP x E px eP = px)
(idemP : forall (x : A),
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
(x : FSet)
{struct x}
: P x
:= (match x return _ -> _ -> _ -> _ -> _ -> _ -> P x with
| E => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => eP
| L a => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => lP a
| U y z => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => uP y z
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP z)
end) H assocP commP nlP nrP idemP.
Axiom FSet_ind_beta_assoc : forall
(P : FSet -> Type)
(H : forall a : FSet, IsHSet (P a))
(eP : P E)
(lP : forall a: A, P (L a))
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
(assocP : forall (x y z : FSet)
(px: P x) (py: P y) (pz: P z),
assoc x y z #
(uP x (U y z) px (uP y z py pz))
=
(uP (U x y) z (uP x y px py) pz))
(commP : forall (x y: FSet) (px: P x) (py: P y),
comm x y #
uP x y px py = uP y x py px)
(nlP : forall (x : FSet) (px: P x),
nl x # uP E x eP px = px)
(nrP : forall (x : FSet) (px: P x),
nr x # uP x E px eP = px)
(idemP : forall (x : A),
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
(x y z : FSet),
apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP)
(assoc x y z)
=
(assocP x y z
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP z)
).
Axiom FSet_ind_beta_comm : forall
(P : FSet -> Type)
(H : forall a : FSet, IsHSet (P a))
(eP : P E)
(lP : forall a: A, P (L a))
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
(assocP : forall (x y z : FSet)
(px: P x) (py: P y) (pz: P z),
assoc x y z #
(uP x (U y z) px (uP y z py pz))
=
(uP (U x y) z (uP x y px py) pz))
(commP : forall (x y : FSet) (px: P x) (py: P y),
comm x y #
uP x y px py = uP y x py px)
(nlP : forall (x : FSet) (px: P x),
nl x # uP E x eP px = px)
(nrP : forall (x : FSet) (px: P x),
nr x # uP x E px eP = px)
(idemP : forall (x : A),
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
(x y : FSet),
apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (comm x y)
=
(commP x y
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
(FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
).
Axiom FSet_ind_beta_nl : forall
(P : FSet -> Type)
(H : forall a : FSet, IsHSet (P a))
(eP : P E)
(lP : forall a: A, P (L a))
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
(assocP : forall (x y z : FSet)
(px: P x) (py: P y) (pz: P z),
assoc x y z #
(uP x (U y z) px (uP y z py pz))
=
(uP (U x y) z (uP x y px py) pz))
(commP : forall (x y : FSet) (px: P x) (py: P y),
comm x y #
uP x y px py = uP y x py px)
(nlP : forall (x : FSet) (px: P x),
nl x # uP E x eP px = px)
(nrP : forall (x : FSet) (px: P x),
nr x # uP x E px eP = px)
(idemP : forall (x : A),
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
(x : FSet),
apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (nl x)
=
(nlP x (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
).
Axiom FSet_ind_beta_nr : forall
(P : FSet -> Type)
(H : forall a : FSet, IsHSet (P a))
(eP : P E)
(lP : forall a: A, P (L a))
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
(assocP : forall (x y z : FSet)
(px: P x) (py: P y) (pz: P z),
assoc x y z #
(uP x (U y z) px (uP y z py pz))
=
(uP (U x y) z (uP x y px py) pz))
(commP : forall (x y : FSet) (px: P x) (py: P y),
comm x y #
uP x y px py = uP y x py px)
(nlP : forall (x : FSet) (px: P x),
nl x # uP E x eP px = px)
(nrP : forall (x : FSet) (px: P x),
nr x # uP x E px eP = px)
(idemP : forall (x : A),
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
(x : FSet),
apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (nr x)
=
(nrP x (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
).
Axiom FSet_ind_beta_idem : forall
(P : FSet -> Type)
(H : forall a : FSet, IsHSet (P a))
(eP : P E)
(lP : forall a: A, P (L a))
(uP : forall (x y: FSet), P x -> P y -> P (U x y))
(assocP : forall (x y z : FSet)
(px: P x) (py: P y) (pz: P z),
assoc x y z #
(uP x (U y z) px (uP y z py pz))
=
(uP (U x y) z (uP x y px py) pz))
(commP : forall (x y : FSet) (px: P x) (py: P y),
comm x y #
uP x y px py = uP y x py px)
(nlP : forall (x : FSet) (px: P x),
nl x # uP E x eP px = px)
(nrP : forall (x : FSet) (px: P x),
nr x # uP x E px eP = px)
(idemP : forall (x : A),
idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
(x : A),
apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (idem x)
=
idemP x.
End FSet.
Instance FSet_recursion A : HitRecursion (FSet A) := {
indTy := _; recTy := _;
H_inductor := FSet_ind A; H_recursor := FSet_rec A }.
Arguments E {_}.
Arguments U {_} _ _.
Arguments L {_} _.
End FinSet.
Section functions.
Parameter A : Type.
Context {A_eqdec: DecidablePaths A}.
Notation "{| x |}" := (L x).
Infix "" := U (at level 8, right associativity).
Notation "" := E.
(** Properties of union *)
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.
(** Membership predicate *)
Definition isIn : A -> FSet A -> Bool.
Proof.
intros a.
hrecursion.
- exact false.
- intro a'. destruct (dec (a = a')); [exact true | exact false].
- apply orb.
- intros x y z. compute. destruct x; reflexivity.
- intros x y. compute. destruct x, y; reflexivity.
- intros x. compute. reflexivity.
- intros x. compute. destruct x; reflexivity.
- intros a'. compute. destruct (A_eqdec a a'); reflexivity.
Defined.
Infix "" := isIn (at level 9, right associativity).
Lemma isIn_singleton_eq a b : a {| b |} = true -> a = b.
Proof. cbv.
destruct (A_eqdec a b). intro. apply p.
intro X.
contradiction (false_ne_true X).
Defined.
Lemma isIn_empty_false a : a = true -> Empty.
Proof.
cbv. intro X.
contradiction (false_ne_true X).
Defined.
Lemma isIn_union a X Y : a (X Y) = (a X || a Y)%Bool.
Proof. reflexivity. Qed.
(** Set comprehension *)
Definition comprehension :
(A -> Bool) -> FSet A -> FSet A.
Proof.
intros P.
hrecursion.
- apply E.
- intro a.
refine (if (P a) then L a else E).
- apply U.
- intros. cbv. apply assoc.
- intros. cbv. apply comm.
- intros. cbv. apply nl.
- intros. cbv. apply nr.
- intros. cbv.
destruct (P x); simpl.
+ apply idem.
+ apply nl.
Defined.
Lemma comprehension_false Y : comprehension (fun a => a ) Y = E.
Proof.
hrecursion Y; try (intros; apply set_path2).
- cbn. reflexivity.
- cbn. reflexivity.
- intros x y IHa IHb.
cbn.
rewrite IHa.
rewrite IHb.
rewrite nl.
reflexivity.
Defined.
Lemma comprehension_union X Y Z :
U (comprehension (fun a => isIn a Y) X)
(comprehension (fun a => isIn a Z) X) =
comprehension (fun a => isIn a (U Y Z)) X.
Proof.
hrecursion X; try (intros; apply set_path2).
- cbn. apply nl.
- cbn. intro a.
destruct (isIn a Y); simpl;
destruct (isIn a Z); simpl.
apply idem.
apply nr.
apply nl.
apply nl.
- cbn. intros X1 X2 IH1 IH2.
rewrite assoc.
rewrite (comm _ (comprehension (fun a : A => isIn a Y) X1)
(comprehension (fun a : A => isIn a Y) X2)).
rewrite <- (assoc _
(comprehension (fun a : A => isIn a Y) X2)
(comprehension (fun a : A => isIn a Y) X1)
(comprehension (fun a : A => isIn a Z) X1)
).
rewrite IH1.
rewrite comm.
rewrite assoc.
rewrite (comm _ (comprehension (fun a : A => isIn a Z) X2) _).
rewrite IH2.
apply comm.
Defined.
Lemma comprehension_idem' `{Funext}:
forall (X:FSet A), forall Y, comprehension (fun x => x (U X Y)) X = X.
Proof.
hinduction.
all: try (intros; apply path_forall; intro; apply set_path2).
- intro Y. cbv. reflexivity.
- intros a Y. cbn.
destruct (dec (a = a)); simpl.
+ reflexivity.
+ contradiction n. reflexivity.
- intros X1 X2 IH1 IH2 Y.
cbn -[isIn].
f_ap.
+ rewrite <- assoc. apply (IH1 (U X2 Y)).
+ rewrite (comm _ X1 X2).
rewrite <- (assoc _ X2 X1 Y).
apply (IH2 (U X1 Y)).
Defined.
Lemma comprehension_idem `{Funext}:
forall (X:FSet A), comprehension (fun x => 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.
(** Set intersection *)
Definition intersection :
FSet A -> FSet A -> FSet A.
Proof.
intros X Y.
apply (comprehension (fun (a : A) => isIn a X) Y).
Defined.
Lemma intersection_comm X Y: intersection X Y = intersection Y X.
Proof.
hrecursion X; try (intros; apply set_path2).
- cbn. unfold intersection. apply comprehension_false.
- cbn. unfold intersection. intros a.
hrecursion Y; try (intros; apply set_path2).
+ cbn. reflexivity.
+ cbn. intros.
destruct (dec (a0 = a)).
rewrite p. destruct (dec (a=a)).
reflexivity.
contradiction n.
reflexivity.
destruct (dec (a = a0)).
contradiction n. apply p^. reflexivity.
+ cbn -[isIn]. intros Y1 Y2 IH1 IH2.
rewrite IH1.
rewrite IH2.
apply (comprehension_union (L a)).
- intros X1 X2 IH1 IH2.
cbn.
unfold intersection in *.
rewrite <- IH1.
rewrite <- IH2. symmetry.
apply comprehension_union.
Defined.
(** Subset ordering *)
Definition subset (x : FSet A) (y : FSet A) : Bool.
Proof.
hrecursion x.
- apply true.
- intro a. apply (isIn a y).
- intros a b. apply (andb a b).
- intros a b c. compute. destruct a; reflexivity.
- intros a b. compute. destruct a, b; reflexivity.
- intros x. compute. reflexivity.
- intros x. compute. destruct x;reflexivity.
- intros a. simpl.
destruct (isIn a y); reflexivity.
Defined.
Infix "" := subset (at level 8, right associativity).
End functions.

View File

@ -7,7 +7,7 @@ Definition Sub A := A -> hProp.
Fixpoint listExt {A} (ls : list A) : Sub A := fun x => Fixpoint listExt {A} (ls : list A) : Sub A := fun x =>
match ls with match ls with
| nil => False_hp | nil => False_hp
| cons a ls' => BuildhProp (Trunc (-1) (x = a)) \/ listExt ls' x | cons a ls' => BuildhProp (Trunc (-1) (x = a)) listExt ls' x
end. end.
Fixpoint map {A B} (f : A -> B) (ls : list A) : list B := Fixpoint map {A B} (f : A -> B) (ls : list A) : list B :=
@ -20,7 +20,7 @@ Fixpoint filterD {A} (P : A -> Bool) (ls : list A) : list { x : A | P x = true }
Proof. Proof.
destruct ls as [|x xs]. destruct ls as [|x xs].
- exact nil. - exact nil.
- enough (P x = true \/ P x = false) as HP. - enough ((P x = true) + (P x = false)) as HP.
{ destruct HP as [HP | HP]. { destruct HP as [HP | HP].
+ refine (cons (exist _ x HP) (filterD _ P xs)). + refine (cons (exist _ x HP) (filterD _ P xs)).
+ refine (filterD _ P xs). + refine (filterD _ P xs).
@ -55,7 +55,7 @@ Lemma filterD_lookup {A} (P : A -> Bool) (x : A) (ls : list A) (Px : P x = true)
Proof. Proof.
induction ls as [| a ls]. induction ls as [| a ls].
- simpl. exact idmap. - simpl. exact idmap.
- assert (P a = true \/ P a = false) as HPA. - assert ((P a = true) + (P a = false)) as HPA.
{ destruct (P a); [left | right]; reflexivity. } { destruct (P a); [left | right]; reflexivity. }
destruct HPA as [Pa | Pa]. destruct HPA as [Pa | Pa].
+ rewrite (filterD_cons P a ls Pa). simpl. + rewrite (filterD_cons P a ls Pa). simpl.

View File

@ -1,206 +0,0 @@
(** Extensionality of the FSets *)
Require Import HoTT HitTactics.
Require Import definition operations.
Section ext.
Context {A : Type}.
Context {A_deceq : DecidablePaths A}.
Theorem union_idem : forall x: FSet A, U x x = x.
Proof.
hinduction;
try (intros ; apply set_path2) ; cbn.
- apply nl.
- apply idem.
- intros x y P Q.
rewrite assoc.
rewrite (comm x y).
rewrite <- (assoc y x x).
rewrite P.
rewrite (comm y x).
rewrite <- (assoc x y y).
f_ap.
Defined.
(** ** Properties about subset relation. *)
Lemma subset_union `{Funext} (X Y : FSet A) :
subset 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;
try (intros; apply path_forall; intro; apply set_path2).
+ intro. contradiction (false_ne_true).
+ intros. destruct (dec (a = a0)).
rewrite p; apply idem.
contradiction (false_ne_true).
+ intros X1 X2 IH1 IH2.
intro Ho.
destruct (isIn a X1);
destruct (isIn a X2).
* specialize (IH1 idpath).
rewrite assoc. f_ap.
* specialize (IH1 idpath).
rewrite assoc. f_ap.
* specialize (IH2 idpath).
rewrite (comm X1 X2).
rewrite assoc. f_ap.
* contradiction (false_ne_true).
- intros X1 X2 IH1 IH2 G.
destruct (subset X1 Y);
destruct (subset X2 Y).
* specialize (IH1 idpath).
specialize (IH2 idpath).
rewrite <- assoc. rewrite IH2. apply IH1.
* contradiction (false_ne_true).
* contradiction (false_ne_true).
* contradiction (false_ne_true).
Defined.
Lemma subset_union_l `{Funext} X :
forall Y, subset X (U X Y) = true.
Proof.
hinduction X;
try (intros; apply path_forall; intro; apply set_path2).
- reflexivity.
- intros a Y. destruct (dec (a = a)).
* reflexivity.
* by contradiction n.
- intros X1 X2 HX1 HX2 Y.
refine (ap (fun z => (X1 z && X2 (X1 X2) Y))%Bool (assoc X1 X2 Y)^ @ _).
refine (ap (fun z => (X1 _ && X2 z Y))%Bool (comm _ _) @ _).
refine (ap (fun z => (X1 _ && X2 z))%Bool (assoc _ _ _)^ @ _).
rewrite HX1. simpl. apply HX2.
Defined.
Lemma subset_union_equiv `{Funext}
: forall X Y : FSet A, subset X Y = true <~> U X Y = Y.
Proof.
intros X Y.
eapply equiv_iff_hprop_uncurried.
split.
- apply subset_union.
- intros HXY. etransitivity.
apply (ap _ HXY^).
apply subset_union_l.
Defined.
Lemma subset_isIn `{FE : Funext} (X Y : FSet A) :
(forall (a : A), isIn a X = true -> isIn a Y = true)
<~> (subset X Y = true).
Proof.
eapply equiv_iff_hprop_uncurried.
split.
- hinduction X ; try (intros ; apply path_forall ; intro ; apply set_path2).
+ intros ; reflexivity.
+ intros a H.
apply H.
destruct (dec (a = a)).
* reflexivity.
* contradiction (n idpath).
+ intros X1 X2 H1 H2 H.
enough (subset X1 Y = true).
rewrite X.
enough (subset X2 Y = true).
rewrite X0.
reflexivity.
* apply H2.
intros a Ha.
apply H.
rewrite Ha.
destruct (isIn a X1) ; reflexivity.
* apply H1.
intros a Ha.
apply H.
rewrite Ha.
reflexivity.
- hinduction X.
+ intros. contradiction (false_ne_true X0).
+ intros b H a.
destruct (dec (a = b)).
* intros ; rewrite p ; apply H.
* intros X ; contradiction (false_ne_true X).
+ intros X1 X2.
intros IH1 IH2 H1 a H2.
destruct (subset X1 Y) ; destruct (subset X2 Y);
cbv in H1; try by contradiction false_ne_true.
specialize (IH1 idpath a). specialize (IH2 idpath a).
destruct (isIn a X1); destruct (isIn a X2);
cbv in H2; try by contradiction false_ne_true.
by apply IH1.
by apply IH1.
by apply IH2.
+ repeat (intro; intros; apply path_forall).
intros; intro; intros; apply set_path2.
+ repeat (intro; intros; apply path_forall).
intros; intro; intros; apply set_path2.
+ repeat (intro; intros; apply path_forall).
intros; intro; intros; apply set_path2.
+ repeat (intro; intros; apply path_forall).
intros; intro; intros; apply set_path2.
+ repeat (intro; intros; apply path_forall).
intros; intro; intros; apply set_path2.
Defined.
(** ** Extensionality proof *)
Lemma eq_subset' (X Y : FSet A) : X = Y <~> (U Y X = X) * (U X Y = Y).
Proof.
unshelve eapply BuildEquiv.
{ intro H. rewrite H. split; apply union_idem. }
unshelve esplit.
{ intros [H1 H2]. etransitivity. apply H1^.
rewrite comm. apply H2. }
intro; apply path_prod; apply set_path2.
all: intro; apply set_path2.
Defined.
Lemma eq_subset `{Funext} (X Y : FSet A) :
X = Y <~> ((subset Y X = true) * (subset X Y = true)).
Proof.
transitivity ((U Y X = X) * (U X Y = Y)).
apply eq_subset'.
symmetry.
eapply equiv_functor_prod'; apply subset_union_equiv.
Defined.
Theorem fset_ext `{Funext} (X Y : FSet A) :
X = Y <~> (forall (a : A), isIn a X = isIn a Y).
Proof.
etransitivity. apply eq_subset.
transitivity
((forall a, isIn a Y = true -> isIn a X = true)
*(forall a, isIn a X = true -> isIn a Y = true)).
- eapply equiv_functor_prod';
apply equiv_iff_hprop_uncurried;
split ; apply subset_isIn.
- apply equiv_iff_hprop_uncurried.
split.
* intros [H1 H2 a].
specialize (H1 a) ; specialize (H2 a).
destruct (isIn a X).
+ symmetry ; apply (H2 idpath).
+ destruct (isIn a Y).
{ apply (H1 idpath). }
{ reflexivity. }
* intros H1.
split ; intro a ; intro H2.
+ rewrite (H1 a).
apply H2.
+ rewrite <- (H1 a).
apply H2.
Defined.
(* With extensionality we can prove decidable equality *)
Instance fsets_dec_eq `{Funext} : DecidablePaths (FSet A).
Proof.
intros X Y.
apply (decidable_equiv ((subset Y X = true) * (subset X Y = true)) (eq_subset X Y)^-1). (* TODO: this is so slow?*)
destruct (Y X), (X Y).
- left. refine (idpath, idpath).
- right. refine (false_ne_true o snd).
- right. refine (false_ne_true o fst).
- right. refine (false_ne_true o fst).
Defined.
End ext.

View File

@ -1,3 +1,4 @@
(* Typeclass for lattices *)
Require Import HoTT. Require Import HoTT.
Definition operation (A : Type) := A -> A -> A. Definition operation (A : Type) := A -> A -> A.
@ -50,8 +51,8 @@ Section Lattice.
associative_max :> Associative max ; associative_max :> Associative max ;
idempotent_min :> Idempotent min ; idempotent_min :> Idempotent min ;
idempotent_max :> Idempotent max ; idempotent_max :> Idempotent max ;
neutralL_min :> NeutralL min empty ; neutralL_min :> NeutralL max empty ;
neutralR_min :> NeutralR min empty ; neutralR_min :> NeutralR max empty ;
absorption_min_max :> Absorption min max ; absorption_min_max :> Absorption min max ;
absorption_max_min :> Absorption max min absorption_max_min :> Absorption max min
}. }.
@ -63,65 +64,65 @@ Arguments Lattice {_} _ _ _.
Section BoolLattice. Section BoolLattice.
Local Ltac solve := Ltac solve :=
let x := fresh in let x := fresh in
repeat (intro x ; destruct x) repeat (intro x ; destruct x)
; compute ; compute
; auto ; auto
; try contradiction. ; try contradiction.
Instance min_com : Commutative orb. Instance orb_com : Commutative orb.
Proof. Proof.
solve. solve.
Defined. Defined.
Instance max_com : Commutative andb. Instance andb_com : Commutative andb.
Proof. Proof.
solve. solve.
Defined. Defined.
Instance min_assoc : Associative orb. Instance orb_assoc : Associative orb.
Proof. Proof.
solve. solve.
Defined. Defined.
Instance max_assoc : Associative andb. Instance andb_assoc : Associative andb.
Proof. Proof.
solve. solve.
Defined. Defined.
Instance min_idem : Idempotent orb. Instance orb_idem : Idempotent orb.
Proof. Proof.
solve. solve.
Defined. Defined.
Instance max_idem : Idempotent andb. Instance andb_idem : Idempotent andb.
Proof. Proof.
solve. solve.
Defined. Defined.
Instance min_nl : NeutralL orb false. Instance orb_nl : NeutralL orb false.
Proof. Proof.
solve. solve.
Defined. Defined.
Instance min_nr : NeutralR orb false. Instance orb_nr : NeutralR orb false.
Proof. Proof.
solve. solve.
Defined. Defined.
Instance bool_absorption_min_max : Absorption orb andb. Instance bool_absorption_orb_andb : Absorption orb andb.
Proof. Proof.
solve. solve.
Defined. Defined.
Instance bool_absorption_max_min : Absorption andb orb. Instance bool_absorption_andb_orb : Absorption andb orb.
Proof. Proof.
solve. solve.
Defined. Defined.
Global Instance lattice_bool : Lattice orb andb false := Global Instance lattice_bool : Lattice andb orb false :=
{ commutative_min := _ ; { commutative_min := _ ;
commutative_max := _ ; commutative_max := _ ;
associative_min := _ ; associative_min := _ ;
associative_max := _ ; associative_max := _ ;
@ -133,9 +134,38 @@ Section BoolLattice.
absorption_max_min := _ absorption_max_min := _
}. }.
Definition and_true : forall b, andb b true = b.
Proof.
solve.
Defined.
Definition and_false : forall b, andb b false = false.
Proof.
solve.
Defined.
Definition dist : forall b b b,
andb b (orb b b) = orb (andb b b) (andb b b).
Proof.
solve.
Defined.
Definition dist : forall b b b,
orb b (andb b b) = andb (orb b b) (orb b b).
Proof.
solve.
Defined.
Definition max_min : forall b b,
orb (andb b b) b = b.
Proof.
solve.
Defined.
End BoolLattice. End BoolLattice.
Hint Resolve Hint Resolve
min_com max_com min_assoc max_assoc min_idem max_idem min_nl min_nr orb_com andb_com orb_assoc andb_assoc orb_idem andb_idem orb_nl orb_nr
bool_absorption_min_max bool_absorption_max_min bool_absorption_orb_andb bool_absorption_andb_orb and_true and_false
dist dist max_min
: bool_lattice_hints. : bool_lattice_hints.

View File

@ -1,5 +1,5 @@
Require Import HoTT HitTactics. Require Import HoTT HitTactics.
Require Import cons_repr operations definition. Require Import cons_repr operations_decidable properties_decidable definition.
Section Operations. Section Operations.
Variable A : Type. Variable A : Type.
@ -43,11 +43,10 @@ Arguments append {_} _ _.
Arguments empty {_}. Arguments empty {_}.
Arguments filter {_} _ _. Arguments filter {_} _ _.
Arguments cardinality {_} {_} _. Arguments cardinality {_} {_} _.
Arguments intersection {_} {_} _ _.
Section ListToSet. Section ListToSet.
Variable A : Type. Variable A : Type.
Context {A_deceq : DecidablePaths A} `{Funext}. Context {A_deceq : DecidablePaths A} `{Univalence}.
Fixpoint list_to_setC (l : list A) : FSetC A := Fixpoint list_to_setC (l : list A) : FSetC A :=
match l with match l with
@ -71,13 +70,13 @@ Section ListToSet.
Defined. Defined.
Lemma member_isIn (l : list A) (a : A) : Lemma member_isIn (l : list A) (a : A) :
member l a = isIn a (FSetC_to_FSet (list_to_setC l)). member l a = isIn_b a (FSetC_to_FSet (list_to_setC l)).
Proof. Proof.
induction l ; cbn in *. induction l ; cbn in *.
- reflexivity. - reflexivity.
- destruct (dec (a = a0)) ; cbn. - destruct (dec (a = a0)) ; cbn.
* reflexivity. * rewrite ?p. simplify_isIn. reflexivity.
* apply IHl. * rewrite IHl. simplify_isIn. rewrite L_isIn_b_false ; auto.
Defined. Defined.
Lemma append_FSetCappend (l1 l2 : list A) : Lemma append_FSetCappend (l1 l2 : list A) :

View File

@ -1,15 +1,17 @@
-R . "" COQC = hoqc COQDEP = hoqdep -R . "" COQC = hoqc COQDEP = hoqdep
-R ../prelude "" -R ../prelude ""
definition.v lattice.v
disjunction.v disjunction.v
operations.v
Ext.v
properties.v
empty_set.v
ordered.v
cons_repr.v
Lattice.v
monad.v
Lists.v
bad.v bad.v
definition.v
operations.v
properties.v
operations_decidable.v
extensionality.v
properties_decidable.v
monad.v
cons_repr.v
lists.v
Enumerated.v Enumerated.v
#empty_set.v
#ordered.v

View File

@ -1,10 +1,5 @@
Require Import HoTT. Require Import HoTT HitTactics.
Require Import HitTactics. Require Import definition operations_decidable properties_decidable.
Require Import definition.
Require Import operations.
Require Import properties.
Require Import empty_set.
Module Export FSetC. Module Export FSetC.
@ -295,25 +290,25 @@ Section Length.
Context {A : Type}. Context {A : Type}.
Context {A_deceq : DecidablePaths A}. Context {A_deceq : DecidablePaths A}.
Context {H : Funext}. Context `{Univalence}.
Opaque isIn_b.
Definition length (x: FSetC A) : nat. Definition length (x: FSetC A) : nat.
Proof. Proof.
simple refine (FSetC_ind A _ _ _ _ _ _ x ); simpl. simple refine (FSetC_ind A _ _ _ _ _ _ x ); simpl.
- exact 0. - exact 0.
- intros a y n. - intros a y n.
pose (y' := FSetC_to_FSet y). pose (y' := FSetC_to_FSet y).
exact (if isIn a y' then n else (S n)). exact (if isIn_b a y' then n else (S n)).
- intros. rewrite transport_const. cbn. - intros. rewrite transport_const. cbn.
destruct (dec (a = a)); cbn. reflexivity. simplify_isIn. simpl. reflexivity.
destruct n; reflexivity.
- intros. rewrite transport_const. cbn. - intros. rewrite transport_const. cbn.
destruct (dec (a = b)), (dec (b = a)); cbn. simplify_isIn.
+ rewrite p. reflexivity. destruct (dec (a = b)) as [Hab | Hab].
+ contradiction (n p^). + rewrite Hab. simplify_isIn. simpl. reflexivity.
+ contradiction (n p^). + rewrite ?L_isIn_b_false; auto. simpl.
+ intros. destruct (isIn_b a (FSetC_to_FSet x0)), (isIn_b b (FSetC_to_FSet x0)) ; reflexivity.
destruct (a (FSetC_to_FSet x0)), (b (FSetC_to_FSet x0)); reflexivity. intro p. contradiction (Hab p^).
Defined. Defined.
Definition length_FSet (x: FSet A) := length (FSet_to_FSetC x). Definition length_FSet (x: FSet A) := length (FSet_to_FSetC x).
@ -325,8 +320,3 @@ cbn. reflexivity.
Defined. Defined.
End Length. End Length.

View File

@ -1,3 +1,4 @@
(* Definitions of the Kuratowski-finite sets via a HIT *)
Require Import HoTT. Require Import HoTT.
Require Import HitTactics. Require Import HitTactics.
@ -72,11 +73,9 @@ Fixpoint FSet_ind
{struct x} {struct x}
: P x : P x
:= (match x return _ -> _ -> _ -> _ -> _ -> _ -> P x with := (match x return _ -> _ -> _ -> _ -> _ -> _ -> P x with
| E => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => eP | E => fun _ _ _ _ _ _ => eP
| L a => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => lP a | L a => fun _ _ _ _ _ _ => lP a
| U y z => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => uP y z | U y z => fun _ _ _ _ _ _ => uP y z (FSet_ind y) (FSet_ind z)
(FSet_ind y)
(FSet_ind z)
end) H assocP commP nlP nrP idemP. end) H assocP commP nlP nrP idemP.

View File

@ -1,14 +1,18 @@
(* Logical disjunction in HoTT (see ch. 3 of the book) *)
Require Import HoTT. Require Import HoTT.
Definition lor (X Y : hProp) : hProp := BuildhProp (Trunc (-1) (sum X Y)). Definition lor (X Y : hProp) : hProp := BuildhProp (Trunc (-1) (sum X Y)).
Infix "\/" := lor. Delimit Scope logic_scope with L.
Notation "A B" := (lor A B) (at level 20, right associativity) : logic_scope.
Arguments lor _%L _%L.
Open Scope logic_scope.
Section lor_props. Section lor_props.
Variable X Y Z : hProp. Variable X Y Z : hProp.
Context `{Univalence}. Context `{Univalence}.
Theorem lor_assoc : (X \/ (Y \/ Z)) = ((X \/ Y) \/ Z). Theorem lor_assoc : X Y Z = (X Y) Z.
Proof. Proof.
apply path_iff_hprop ; cbn. apply path_iff_hprop ; cbn.
* simple refine (Trunc_ind _ _). * simple refine (Trunc_ind _ _).
@ -27,7 +31,7 @@ Section lor_props.
+ apply (tr (inr (tr (inr z)))). + apply (tr (inr (tr (inr z)))).
Defined. Defined.
Theorem lor_comm : (X \/ Y) = (Y \/ X). Theorem lor_comm : X Y = Y X.
Proof. Proof.
apply path_iff_hprop ; cbn. apply path_iff_hprop ; cbn.
* simple refine (Trunc_ind _ _). * simple refine (Trunc_ind _ _).
@ -40,7 +44,7 @@ Section lor_props.
+ apply (tr (inl x)). + apply (tr (inl x)).
Defined. Defined.
Theorem lor_nl : (False_hp \/ X) = X. Theorem lor_nl : False_hp X = X.
Proof. Proof.
apply path_iff_hprop ; cbn. apply path_iff_hprop ; cbn.
* simple refine (Trunc_ind _ _). * simple refine (Trunc_ind _ _).
@ -50,7 +54,7 @@ Section lor_props.
* apply (fun x => tr (inr x)). * apply (fun x => tr (inr x)).
Defined. Defined.
Theorem lor_nr : (X \/ False_hp) = X. Theorem lor_nr : X False_hp = X.
Proof. Proof.
apply path_iff_hprop ; cbn. apply path_iff_hprop ; cbn.
* simple refine (Trunc_ind _ _). * simple refine (Trunc_ind _ _).
@ -60,7 +64,7 @@ Section lor_props.
* apply (fun x => tr (inl x)). * apply (fun x => tr (inl x)).
Defined. Defined.
Theorem lor_idem : (X \/ X) = X. Theorem lor_idem : X X = X.
Proof. Proof.
apply path_iff_hprop ; cbn. apply path_iff_hprop ; cbn.
- simple refine (Trunc_ind _ _). - simple refine (Trunc_ind _ _).

110
FiniteSets/extensionality.v Normal file
View File

@ -0,0 +1,110 @@
(** Extensionality of the FSets *)
Require Import HoTT HitTactics.
Require Import definition operations properties.
Section ext.
Context {A : Type}.
Context `{Univalence}.
Lemma subset_union_equiv
: forall X Y : FSet A, subset X Y <~> U X Y = Y.
Proof.
intros X Y.
eapply equiv_iff_hprop_uncurried.
split.
- apply subset_union.
- intro HXY.
rewrite <- HXY.
apply subset_union_l.
Defined.
Lemma subset_isIn (X Y : FSet A) :
(forall (a : A), isIn a X -> isIn a Y)
<~> (subset X Y).
Proof.
eapply equiv_iff_hprop_uncurried.
split.
- hinduction X ;
try (intros; repeat (apply path_forall; intro); apply equiv_hprop_allpath ; apply _).
+ intros ; reflexivity.
+ intros a f.
apply f.
apply tr ; reflexivity.
+ intros X1 X2 H1 H2 f.
enough (subset X1 Y).
enough (subset X2 Y).
{ split. apply X. apply X0. }
* apply H2.
intros a Ha.
apply f.
apply tr.
right.
apply Ha.
* apply H1.
intros a Ha.
apply f.
apply tr.
left.
apply Ha.
- hinduction X ;
try (intros; repeat (apply path_forall; intro); apply equiv_hprop_allpath ; apply _).
+ intros. contradiction.
+ intros b f a.
simple refine (Trunc_ind _ _) ; cbn.
intro p.
rewrite p^ in f.
apply f.
+ intros X1 X2 IH1 IH2 [H1 H2] a.
simple refine (Trunc_ind _ _) ; cbn.
intros [C1 | C2].
++ apply (IH1 H1 a C1).
++ apply (IH2 H2 a C2).
Defined.
(** ** Extensionality proof *)
Lemma eq_subset' (X Y : FSet A) : X = Y <~> (U Y X = X) * (U X Y = Y).
Proof.
unshelve eapply BuildEquiv.
{ intro H'. rewrite H'. split; apply union_idem. }
unshelve esplit.
{ intros [H1 H2]. etransitivity. apply H1^.
rewrite comm. apply H2. }
intro; apply path_prod; apply set_path2.
all: intro; apply set_path2.
Defined.
Lemma eq_subset (X Y : FSet A) :
X = Y <~> (subset Y X * subset X Y).
Proof.
transitivity ((U Y X = X) * (U X Y = Y)).
apply eq_subset'.
symmetry.
eapply equiv_functor_prod'; apply subset_union_equiv.
Defined.
Theorem fset_ext (X Y : FSet A) :
X = Y <~> (forall (a : A), isIn a X = isIn a Y).
Proof.
refine (@equiv_compose' _ _ _ _ _) ; [ | apply eq_subset ].
refine (@equiv_compose' _ ((forall a, isIn a Y -> isIn a X)
*(forall a, isIn a X -> isIn a Y)) _ _ _).
- apply equiv_iff_hprop_uncurried.
split.
* intros [H1 H2 a].
specialize (H1 a) ; specialize (H2 a).
apply path_iff_hprop.
apply H2.
apply H1.
* intros H1.
split ; intro a ; intro H2.
+ rewrite (H1 a).
apply H2.
+ rewrite <- (H1 a).
apply H2.
- eapply equiv_functor_prod' ;
apply equiv_iff_hprop_uncurried ;
split ; apply subset_isIn.
Defined.
End ext.

View File

@ -1,6 +1,6 @@
(* [FSet] is a (strong and stable) finite powerset monad *) (* [FSet] is a (strong and stable) finite powerset monad *)
Require Export definition properties.
Require Import HoTT HitTactics. Require Import HoTT HitTactics.
Require Export definition properties.
Definition ffmap {A B : Type} : (A -> B) -> FSet A -> FSet B. Definition ffmap {A B : Type} : (A -> B) -> FSet A -> FSet B.
Proof. Proof.
@ -19,7 +19,7 @@ Defined.
Lemma ffmap_1 `{Funext} {A : Type} : @ffmap A A idmap = idmap. Lemma ffmap_1 `{Funext} {A : Type} : @ffmap A A idmap = idmap.
Proof. Proof.
apply path_forall. apply path_forall.
intro x. hinduction x; try (cbn; intros; f_ap); intro x. hinduction x; try (intros; f_ap);
try (intros; apply set_path2). try (intros; apply set_path2).
Defined. Defined.
@ -30,7 +30,7 @@ Lemma ffmap_compose {A B C : Type} `{Funext} (f : A -> B) (g : B -> C) :
fmap FSet (g o f) = fmap _ g o fmap _ f. fmap FSet (g o f) = fmap _ g o fmap _ f.
Proof. Proof.
apply path_forall. intro x. apply path_forall. intro x.
hrecursion x; try (cbn; intros; f_ap); hrecursion x; try (intros; f_ap);
try (intros; apply set_path2). try (intros; apply set_path2).
Defined. Defined.
@ -50,7 +50,7 @@ Defined.
Lemma join_assoc {A : Type} (X : FSet (FSet (FSet A))) : Lemma join_assoc {A : Type} (X : FSet (FSet (FSet A))) :
join (ffmap join X) = join (join X). join (ffmap join X) = join (join X).
Proof. Proof.
hrecursion X; try (cbn; intros; f_ap); hrecursion X; try (intros; f_ap);
try (intros; apply set_path2). try (intros; apply set_path2).
Defined. Defined.
@ -61,7 +61,7 @@ Proof. reflexivity. Defined.
Lemma join_return_fmap {A : Type} (X : FSet A) : Lemma join_return_fmap {A : Type} (X : FSet A) :
join ({| X |}) = join (ffmap (fun x => {|x|}) X). join ({| X |}) = join (ffmap (fun x => {|x|}) X).
Proof. Proof.
hrecursion X; try (cbn; intros; f_ap); hrecursion X; try (intros; f_ap);
try (intros; apply set_path2). try (intros; apply set_path2).
Defined. Defined.

View File

@ -1,28 +1,53 @@
(* Operations on the [FSet A] for an arbitrary [A] *)
Require Import HoTT HitTactics. Require Import HoTT HitTactics.
Require Import definition. Require Import definition disjunction lattice.
Section operations. Section operations.
Context {A : Type}. Context {A : Type}.
Context {A_deceq : DecidablePaths A}. Context `{Univalence}.
Definition isIn : A -> FSet A -> Bool. Definition isIn : A -> FSet A -> hProp.
Proof. Proof.
intros a. intros a.
hrecursion. hrecursion.
- exact false. - exists Empty.
- intro a'. destruct (dec (a = a')); [exact true | exact false]. exact _.
- apply orb. - intro a'.
- intros x y z. compute. destruct x; reflexivity. exists (Trunc (-1) (a = a')).
- intros x y. compute. destruct x, y; reflexivity. exact _.
- intros x. compute. reflexivity. - apply lor.
- intros x. compute. destruct x; reflexivity. - intros ; apply lor_assoc. exact _.
- intros a'. simpl. - intros ; apply lor_comm. exact _.
destruct (match dec (a = a') with - intros ; apply lor_nl. exact _.
| inl _ => true - intros ; apply lor_nr. exact _.
| inr _ => false - intros ; apply lor_idem. exact _.
end); compute; reflexivity.
Defined. Defined.
Definition subset : FSet A -> FSet A -> hProp.
Proof.
intros X Y.
hrecursion X.
- exists Unit.
exact _.
- intros a.
apply (isIn a Y).
- intros X1 X2.
exists (prod X1 X2).
exact _.
- intros.
apply path_trunctype ; apply equiv_prod_assoc.
- intros.
apply path_trunctype ; apply equiv_prod_symm.
- intros.
apply path_trunctype ; apply prod_unit_l.
- intros.
apply path_trunctype ; apply prod_unit_r.
- intros a'.
apply path_iff_hprop ; cbn.
* intros [p1 p2]. apply p1.
* intros p.
split ; apply p.
Defined.
Definition comprehension : Definition comprehension :
(A -> Bool) -> FSet A -> FSet A. (A -> Bool) -> FSet A -> FSet A.
@ -33,40 +58,28 @@ hrecursion.
- intro a. - intro a.
refine (if (P a) then L a else E). refine (if (P a) then L a else E).
- apply U. - apply U.
- intros. cbv. apply assoc. - apply assoc.
- intros. cbv. apply comm. - apply comm.
- intros. cbv. apply nl. - apply nl.
- intros. cbv. apply nr. - apply nr.
- intros. cbv. - intros; simpl.
destruct (P x); simpl. destruct (P x).
+ apply idem. + apply idem.
+ apply nl. + apply nl.
Defined. Defined.
Definition intersection : Definition isEmpty :
FSet A -> FSet A -> FSet A. FSet A -> Bool.
Proof. Proof.
intros X Y. hrecursion.
apply (comprehension (fun (a : A) => isIn a X) Y). - apply true.
Defined. - apply (fun _ => false).
- apply andb.
Definition difference : - intros. symmetry. eauto with bool_lattice_hints.
FSet A -> FSet A -> FSet A := fun X Y => - eauto with bool_lattice_hints.
comprehension (fun a => negb (isIn a X)) Y. - eauto with bool_lattice_hints.
- eauto with bool_lattice_hints.
Definition subset : - eauto with bool_lattice_hints.
FSet A -> FSet A -> Bool.
Proof.
intros X Y.
hrecursion X.
- exact true.
- 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 (isIn x Y); reflexivity.
Defined. Defined.
End operations. End operations.

View File

@ -0,0 +1,41 @@
(* Operations on [FSet A] when [A] has decidable equality *)
Require Import HoTT HitTactics.
Require Export definition operations.
Section decidable_A.
Context {A : Type}.
Context {A_deceq : DecidablePaths A}.
Context `{Univalence}.
Global Instance isIn_decidable : forall (a : A) (X : FSet A), Decidable (isIn a X).
Proof.
intros a.
hinduction ; try (intros ; apply path_ishprop).
- apply _.
- intros. apply _.
- intros. apply _.
Defined.
Definition isIn_b (a : A) (X : FSet A) :=
match dec (isIn a X) with
| inl _ => true
| inr _ => false
end.
Global Instance subset_decidable : forall (X Y : FSet A), Decidable (subset X Y).
Proof.
hinduction ; try (intros ; apply path_ishprop).
- intro ; apply _.
- intros ; apply _.
- intros ; apply _.
Defined.
Definition subset_b (X Y : FSet A) :=
match dec (subset X Y) with
| inl _ => true
| inr _ => false
end.
Definition intersection (X Y : FSet A) : FSet A := comprehension (fun a => isIn_b a Y) X.
End decidable_A.

View File

@ -1,68 +1,82 @@
Require Import HoTT HitTactics. Require Import HoTT HitTactics.
Require Export definition operations Ext Lattice. Require Export definition operations disjunction.
(* Lemmas relating operations to the membership predicate *) (* Lemmas relating operations to the membership predicate *)
Section operations_isIn. Section operations_isIn.
Context {A : Type} `{DecidablePaths A}. Context {A : Type}.
Context `{Univalence}.
Lemma ext `{Funext} : forall (S T : FSet A), (forall a, isIn a S = isIn a T) -> S = T.
Lemma union_idem : forall x: FSet A, U x x = x.
Proof. Proof.
apply fset_ext. hinduction;
try (intros ; apply set_path2) ; cbn.
- apply nl.
- apply idem.
- intros x y P Q.
rewrite assoc.
rewrite (comm x y).
rewrite <- (assoc y x x).
rewrite P.
rewrite (comm y x).
rewrite <- (assoc x y y).
f_ap.
Defined.
(** ** Properties about subset relation. *)
Lemma subset_union (X Y : FSet A) :
subset X Y -> U X Y = Y.
Proof.
hinduction X; try (intros; apply path_forall; intro; apply set_path2).
- intros. apply nl.
- intros a. hinduction Y;
try (intros; apply path_forall; intro; apply set_path2).
+ intro.
contradiction.
+ intro a0.
simple refine (Trunc_ind _ _).
intro p ; cbn.
rewrite p; apply idem.
+ intros X1 X2 IH1 IH2.
simple refine (Trunc_ind _ _).
intros [e1 | e2].
++ rewrite assoc.
rewrite (IH1 e1).
reflexivity.
++ rewrite comm.
rewrite <- assoc.
rewrite (comm X2).
rewrite (IH2 e2).
reflexivity.
- intros X1 X2 IH1 IH2 [G1 G2].
rewrite <- assoc.
rewrite (IH2 G2).
apply (IH1 G1).
Defined.
Lemma subset_union_l (X : FSet A) :
forall Y, subset X (U X Y).
Proof.
hinduction X ;
try (repeat (intro; intros; apply path_forall); intro; apply equiv_hprop_allpath ; apply _).
- apply (fun _ => tt).
- intros a Y.
apply tr ; left ; apply tr ; reflexivity.
- intros X1 X2 HX1 HX2 Y.
split.
* rewrite <- assoc. apply HX1.
* rewrite (comm X1 X2). rewrite <- assoc. apply HX2.
Defined. Defined.
(* Union and membership *) (* Union and membership *)
Lemma union_isIn (X Y : FSet A) (a : A) : Lemma union_isIn (X Y : FSet A) (a : A) :
isIn a (U X Y) = orb (isIn a X) (isIn a Y). isIn a (U X Y) = isIn a X isIn a Y.
Proof. Proof.
reflexivity. reflexivity.
Defined. Defined.
(* Intersection and membership. We need a bunch of supporting lemmas *)
Lemma intersection_0l: forall X: FSet A, intersection E X = E.
Proof.
hinduction;
try (intros ; apply set_path2).
- reflexivity.
- intro a.
reflexivity.
- intros x y P Q.
cbn.
rewrite P.
rewrite Q.
apply union_idem.
Defined.
Lemma intersection_0r (X : FSet A) : intersection X E = E.
Proof.
exact idpath.
Defined.
Lemma intersection_La (X : FSet A) (a : A) :
intersection (L a) X = if isIn a X then L a else E.
Proof.
hinduction X; try (intros ; apply set_path2).
- reflexivity.
- intro b.
cbn.
destruct (dec (a = b)) as [p|np].
* rewrite p.
destruct (dec (b = b)) as [|nb]; [reflexivity|].
by contradiction nb.
* destruct (dec (b = a)); [|reflexivity].
by contradiction np.
- unfold intersection.
intros X Y P Q.
cbn.
rewrite P.
rewrite Q.
destruct (isIn a X) ; destruct (isIn a Y).
* apply union_idem.
* apply nr.
* apply nl.
* apply union_idem.
Defined.
Lemma comprehension_or : forall ϕ ψ (x: FSet A), Lemma 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). (comprehension ψ x).
@ -87,174 +101,23 @@ hinduction; try (intros; apply set_path2).
reflexivity. reflexivity.
Defined. Defined.
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.
- symmetry ; apply nl.
- intros b.
destruct (dec (b = a)) ; cbn.
* destruct (isIn b z).
+ rewrite union_idem.
reflexivity.
+ rewrite nr.
reflexivity.
* rewrite nl ; reflexivity.
- intros X1 X2 P Q.
rewrite P. rewrite Q.
rewrite <- assoc.
rewrite (comm (comprehension (fun a0 : A => isIn a0 z) X1)).
rewrite <- assoc.
rewrite assoc.
rewrite (comm (comprehension (fun a0 : A => isIn a0 z) X2)).
reflexivity.
Defined.
Lemma distributive_intersection_U (X1 X2 Y : FSet A) :
intersection (U X1 X2) Y = U (intersection X1 Y) (intersection X2 Y).
Proof.
hinduction X1; try (intros ; apply set_path2) ; cbn.
- rewrite intersection_0l.
rewrite nl.
rewrite nl.
reflexivity.
- intro a.
rewrite intersection_La.
rewrite distributive_La.
rewrite intersection_La.
reflexivity.
- intros Z1 Z2 P Q.
unfold intersection in *. simpl in *.
apply comprehension_or.
Defined.
Theorem intersection_isIn (X Y: FSet A) (a : A) :
isIn a (intersection X Y) = andb (isIn a X) (isIn a Y).
Proof.
hinduction X; try (intros ; apply set_path2) ; cbn.
- rewrite intersection_0l.
reflexivity.
- intro b.
rewrite intersection_La.
destruct (dec (a = b)) ; cbn.
* rewrite p.
destruct (isIn b Y).
+ cbn.
destruct (dec (b = b)); [reflexivity|].
by contradiction n.
+ reflexivity.
* destruct (isIn b Y).
+ cbn.
destruct (dec (a = b)); [|reflexivity].
by contradiction n.
+ reflexivity.
- intros X1 X2 P Q.
rewrite distributive_intersection_U. simpl.
rewrite P.
rewrite Q.
destruct (isIn a X1) ; destruct (isIn a X2) ; destruct (isIn a Y) ;
reflexivity.
Defined.
End operations_isIn. End operations_isIn.
(* Some suporting tactics *)
Ltac simplify_isIn :=
repeat (rewrite ?intersection_isIn ;
rewrite ?union_isIn).
Ltac toBool := try (intro) ;
intros ; apply ext ; intros ; simplify_isIn ; eauto with bool_lattice_hints.
Section SetLattice.
Context {A : Type}.
Context {A_deceq : DecidablePaths A}.
Context `{Funext}.
Instance fset_union_com : Commutative (@U A).
Proof.
toBool.
Defined.
Instance fset_intersection_com : Commutative intersection.
Proof.
toBool.
Defined.
Instance fset_union_assoc : Associative (@U A).
Proof.
toBool.
Defined.
Instance fset_intersection_assoc : Associative intersection.
Proof.
toBool.
Defined.
Instance fset_union_idem : Idempotent (@U A).
Proof. exact union_idem. Defined.
Instance fset_intersection_idem : Idempotent intersection.
Proof.
toBool.
Defined.
Instance fset_union_nl : NeutralL (@U A) (@E A).
Proof.
toBool.
Defined.
Instance fset_union_nr : NeutralR (@U A) (@E A).
Proof.
toBool.
Defined.
Instance fset_absorption_intersection_union : Absorption (@U A) intersection.
Proof.
toBool.
Defined.
Instance fset_absorption_union_intersection : Absorption intersection (@U A).
Proof.
toBool.
Defined.
Instance lattice_fset : Lattice (@U A) intersection (@E A) :=
{
commutative_min := _ ;
commutative_max := _ ;
associative_min := _ ;
associative_max := _ ;
idempotent_min := _ ;
idempotent_max := _ ;
neutralL_min := _ ;
neutralR_min := _ ;
absorption_min_max := _ ;
absorption_max_min := _
}.
End SetLattice.
(* Other properties *) (* Other properties *)
Section properties. Section properties.
Context {A : Type}. Context {A : Type}.
Context {A_deceq : DecidablePaths A}. Context `{Univalence}.
(** isIn properties *) (** isIn properties *)
Lemma singleton_isIn (a b: A) : isIn a (L b) = true -> a = b. Lemma singleton_isIn (a b: A) : isIn a (L b) -> Trunc (-1) (a = b).
Proof. Proof.
simpl. apply idmap.
destruct (dec (a = b)).
- intro.
apply p.
- intro X.
contradiction (false_ne_true X).
Defined. Defined.
Lemma empty_isIn (a: A) : isIn a E = false. Lemma empty_isIn (a: A) : isIn a E -> Empty.
Proof. Proof.
reflexivity. apply idmap.
Defined. Defined.
(** comprehension properties *) (** comprehension properties *)
@ -269,7 +132,7 @@ hrecursion Y; try (intros; apply set_path2).
apply union_idem. apply union_idem.
Defined. Defined.
Theorem comprehension_subset : forall ϕ (X : FSet A), Lemma comprehension_subset : forall ϕ (X : FSet A),
U (comprehension ϕ X) X = X. U (comprehension ϕ X) X = X.
Proof. Proof.
intros ϕ. intros ϕ.
@ -290,29 +153,4 @@ hrecursion; try (intros ; apply set_path2) ; cbn.
reflexivity. reflexivity.
Defined. Defined.
Theorem comprehension_all : forall (X : FSet A),
comprehension (fun a => isIn a X) X = X.
Proof.
hinduction; try (intros ; apply set_path2).
- reflexivity.
- intro a.
destruct (dec (a = a)).
* reflexivity.
* contradiction (n idpath).
- intros X1 X2 P Q.
f_ap; (etransitivity; [ apply comprehension_or |]).
rewrite P. rewrite (comm X1).
apply comprehension_subset.
rewrite Q.
apply comprehension_subset.
Defined.
Theorem distributive_U_int `{Funext} (X1 X2 Y : FSet A) :
U (intersection X1 X2) Y = intersection (U X1 Y) (U X2 Y).
Proof.
toBool.
destruct (a X1), (a X2), (a Y); eauto.
Defined.
End properties. End properties.

View File

@ -0,0 +1,276 @@
(* Properties of [FSet A] where [A] has decidable equality *)
Require Import HoTT HitTactics.
Require Export properties extensionality lattice operations_decidable.
(* Lemmas relating operations to the membership predicate *)
Section operations_isIn.
Context {A : Type} `{DecidablePaths A} `{Univalence}.
Lemma ext : forall (S T : FSet A), (forall a, isIn_b a S = isIn_b a T) -> S = T.
Proof.
intros X Y H2.
apply fset_ext.
intro a.
specialize (H2 a).
unfold isIn_b, dec in H2.
destruct (isIn_decidable a X) ; destruct (isIn_decidable a Y).
- apply path_iff_hprop ; intro ; assumption.
- contradiction (true_ne_false).
- contradiction (true_ne_false) ; apply H2^.
- apply path_iff_hprop ; intro ; contradiction.
Defined.
Lemma empty_isIn (a : A) :
isIn_b a = false.
Proof.
reflexivity.
Defined.
Lemma L_isIn (a b : A) :
isIn a {|b|} -> a = b.
Proof.
intros. strip_truncations. assumption.
Defined.
Lemma L_isIn_b_true (a b : A) (p : a = b) :
isIn_b a {|b|} = true.
Proof.
unfold isIn_b, dec.
destruct (isIn_decidable a {|b|}) as [n | n] .
- reflexivity.
- simpl in n.
contradiction (n (tr p)).
Defined.
Lemma L_isIn_b_aa (a : A) :
isIn_b a {|a|} = true.
Proof.
apply L_isIn_b_true ; reflexivity.
Defined.
Lemma L_isIn_b_false (a b : A) (p : a <> b) :
isIn_b a {|b|} = false.
Proof.
unfold isIn_b, dec.
destruct (isIn_decidable a {|b|}).
- simpl in t.
strip_truncations.
contradiction.
- reflexivity.
Defined.
(* Union and membership *)
Lemma union_isIn (X Y : FSet A) (a : A) :
isIn_b a (U X Y) = orb (isIn_b a X) (isIn_b a Y).
Proof.
unfold isIn_b ; unfold dec.
simpl.
destruct (isIn_decidable a X) ; destruct (isIn_decidable a Y) ; reflexivity.
Defined.
Lemma intersection_isIn (X Y: FSet A) (a : A) :
isIn_b a (intersection X Y) = andb (isIn_b a X) (isIn_b a Y).
Proof.
hinduction X; try (intros ; apply set_path2).
- reflexivity.
- intro b.
destruct (dec (a = b)).
* rewrite p.
destruct (isIn_b b Y) ; symmetry ; eauto with bool_lattice_hints.
* destruct (isIn_b b Y) ; destruct (isIn_b a Y) ; symmetry ; eauto with bool_lattice_hints.
+ rewrite and_false.
symmetry.
apply (L_isIn_b_false a b n).
+ rewrite and_true.
apply (L_isIn_b_false a b n).
- intros X1 X2 P Q.
rewrite union_isIn ; rewrite union_isIn.
rewrite P.
rewrite Q.
unfold isIn_b, dec.
destruct (isIn_decidable a X1)
; destruct (isIn_decidable a X2)
; destruct (isIn_decidable a Y)
; reflexivity.
Defined.
Lemma comprehension_isIn (Y : FSet A) (ϕ : A -> Bool) (a : A) :
isIn_b a (comprehension ϕ Y) = andb (isIn_b a Y) (ϕ a).
Proof.
hinduction Y ; try (intros; apply set_path2).
- apply empty_isIn.
- intro b.
destruct (isIn_decidable a {|b|}).
* simpl in t.
strip_truncations.
rewrite t.
destruct (ϕ b).
** rewrite (L_isIn_b_true _ _ idpath).
eauto with bool_lattice_hints.
** rewrite empty_isIn ; rewrite (L_isIn_b_true _ _ idpath).
eauto with bool_lattice_hints.
* destruct (ϕ b).
** rewrite L_isIn_b_false.
*** eauto with bool_lattice_hints.
*** intro.
apply (n (tr X)).
** rewrite empty_isIn.
rewrite L_isIn_b_false.
*** eauto with bool_lattice_hints.
*** intro.
apply (n (tr X)).
- intros.
Opaque isIn_b.
rewrite ?union_isIn.
rewrite X.
rewrite X0.
assert (forall b1 b2 b3,
(b1 && b2 || b3 && b2)%Bool = ((b1 || b3) && b2)%Bool).
{ intros ; destruct b1, b2, b3 ; reflexivity. }
apply X1.
Defined.
End operations_isIn.
Global Opaque isIn_b.
(* Some suporting tactics *)
Ltac simplify_isIn :=
repeat (rewrite union_isIn
|| rewrite L_isIn_b_aa
|| rewrite intersection_isIn
|| rewrite comprehension_isIn).
Ltac toBool := try (intro) ;
intros ; apply ext ; intros ; simplify_isIn ; eauto with bool_lattice_hints.
Section SetLattice.
Context {A : Type}.
Context {A_deceq : DecidablePaths A}.
Context `{Univalence}.
Instance fset_union_com : Commutative (@U A).
Proof.
toBool.
Defined.
Instance fset_intersection_com : Commutative intersection.
Proof.
toBool.
Defined.
Instance fset_union_assoc : Associative (@U A).
Proof.
toBool.
Defined.
Instance fset_intersection_assoc : Associative intersection.
Proof.
toBool.
Defined.
Instance fset_union_idem : Idempotent (@U A).
Proof.
exact union_idem.
Defined.
Instance fset_intersection_idem : Idempotent intersection.
Proof.
toBool.
Defined.
Instance fset_union_nl : NeutralL (@U A) (@E A).
Proof.
toBool.
Defined.
Instance fset_union_nr : NeutralR (@U A) (@E A).
Proof.
toBool.
Defined.
Instance fset_absorption_intersection_union : Absorption (@U A) intersection.
Proof.
toBool.
Defined.
Instance fset_absorption_union_intersection : Absorption intersection (@U A).
Proof.
toBool.
Defined.
Instance lattice_fset : Lattice intersection (@U A) (@E A) :=
{
commutative_min := _ ;
commutative_max := _ ;
associative_min := _ ;
associative_max := _ ;
idempotent_min := _ ;
idempotent_max := _ ;
neutralL_min := _ ;
neutralR_min := _ ;
absorption_min_max := _ ;
absorption_max_min := _
}.
End SetLattice.
(* Comprehension properties *)
Section comprehension_properties.
Opaque isIn_b.
Context {A : Type}.
Context {A_deceq : DecidablePaths A}.
Context `{Univalence}.
Lemma comprehension_or : forall ϕ ψ (x: FSet A),
comprehension (fun a => orb (ϕ a) (ψ a)) x
= U (comprehension ϕ x) (comprehension ψ x).
Proof.
toBool.
Defined.
(** comprehension properties *)
Lemma comprehension_false Y : comprehension (fun (_ : A) => false) Y = E.
Proof.
toBool.
Defined.
Lemma comprehension_all : forall (X : FSet A),
comprehension (fun a => isIn_b a X) X = X.
Proof.
toBool.
Defined.
Lemma comprehension_subset : forall ϕ (X : FSet A),
U (comprehension ϕ X) X = X.
Proof.
toBool.
Defined.
End comprehension_properties.
(* With extensionality we can prove decidable equality *)
Section dec_eq.
Context (A : Type) `{DecidablePaths A} `{Univalence}.
Instance decidable_prod {X Y : Type} `{Decidable X} `{Decidable Y} :
Decidable (X * Y).
Proof.
unfold Decidable in *.
destruct H1 as [x | nx] ; destruct H2 as [y | ny].
- left ; split ; assumption.
- right. intros [p1 p2]. contradiction.
- right. intros [p1 p2]. contradiction.
- right. intros [p1 p2]. contradiction.
Defined.
Instance fsets_dec_eq : DecidablePaths (FSet A).
Proof.
intros X Y.
apply (decidable_equiv' ((subset Y X) * (subset X Y)) (eq_subset X Y)^-1).
apply _.
Defined.
End dec_eq.