mirror of https://github.com/nmvdw/HITs-Examples
Fixes
This commit is contained in:
parent
4ae639ace3
commit
6c86d0c524
FiniteSets
|
@ -1,7 +1,2 @@
|
|||
Require Export HoTT HitTactics.
|
||||
Require Export representations.definition.
|
||||
From fsets Require Export
|
||||
monad
|
||||
extensionality
|
||||
properties
|
||||
properties_decidable.
|
||||
Require Export kuratowski_sets kuratowski.operations kuratowski.properties extensionality.
|
|
@ -1,30 +1,25 @@
|
|||
-R . "" COQC = hoqc COQDEP = hoqdep
|
||||
-R ../prelude ""
|
||||
notation.v
|
||||
plumbing.v
|
||||
lattice.v
|
||||
disjunction.v
|
||||
representations/bad.v
|
||||
representations/definition.v
|
||||
representations/cons_repr.v
|
||||
fsets/operations_cons_repr.v
|
||||
fsets/properties_cons_repr.v
|
||||
fsets/isomorphism.v
|
||||
fsets/operations.v
|
||||
fsets/operations_decidable.v
|
||||
fsets/extensionality.v
|
||||
fsets/properties.v
|
||||
fsets/properties_decidable.v
|
||||
fsets/length.v
|
||||
fsets/monad.v
|
||||
prelude.v
|
||||
interfaces/lattice_interface.v
|
||||
interfaces/lattice_examples.v
|
||||
interfaces/monad_interface.v
|
||||
interfaces/set_names.v
|
||||
kuratowski/kuratowski_sets.v
|
||||
kuratowski/extensionality.v
|
||||
list_representation/list_representation.v
|
||||
list_representation/operations.v
|
||||
list_representation/properties.v
|
||||
list_representation/isomorphism.v
|
||||
kuratowski/operations.v
|
||||
kuratowski/properties.v
|
||||
FSets.v
|
||||
Sub.v
|
||||
representations/T.v
|
||||
implementations/interface.v
|
||||
implementations/lists.v
|
||||
variations/enumerated.v
|
||||
variations/k_finite.v
|
||||
variations/b_finite.v
|
||||
variations/projective.v
|
||||
#empty_set.v
|
||||
ordered.v
|
||||
interfaces/set_interface.v
|
||||
subobjects/sub.v
|
||||
subobjects/k_finite.v
|
||||
subobjects/enumerated.v
|
||||
subobjects/b_finite.v
|
||||
misc/bad.v
|
||||
misc/dec_lem.v
|
||||
misc/ordered.v
|
||||
misc/projective.v
|
|
@ -1,84 +0,0 @@
|
|||
(* [FSet] is a (strong and stable) finite powerset monad *)
|
||||
Require Import HoTT HitTactics.
|
||||
Require Export representations.definition fsets.properties fsets.operations.
|
||||
|
||||
Definition ffmap {A B : Type} : (A -> B) -> FSet A -> FSet B.
|
||||
Proof.
|
||||
intro f.
|
||||
hrecursion.
|
||||
- exact ∅.
|
||||
- intro a. exact {| f a |}.
|
||||
- intros X Y. apply (X ∪ Y).
|
||||
- apply assoc.
|
||||
- apply comm.
|
||||
- apply nl.
|
||||
- apply nr.
|
||||
- simpl. intro x. apply idem.
|
||||
Defined.
|
||||
|
||||
Lemma ffmap_1 `{Funext} {A : Type} : @ffmap A A idmap = idmap.
|
||||
Proof.
|
||||
apply path_forall.
|
||||
intro x. hinduction x; try (intros; f_ap);
|
||||
try (intros; apply set_path2).
|
||||
Defined.
|
||||
|
||||
Global Instance fset_functorish `{Funext}: Functorish FSet
|
||||
:= { fmap := @ffmap; fmap_idmap := @ffmap_1 _ }.
|
||||
|
||||
Lemma ffmap_compose {A B C : Type} `{Funext} (f : A -> B) (g : B -> C) :
|
||||
fmap FSet (g o f) = fmap _ g o fmap _ f.
|
||||
Proof.
|
||||
apply path_forall. intro x.
|
||||
hrecursion x; try (intros; f_ap);
|
||||
try (intros; apply set_path2).
|
||||
Defined.
|
||||
|
||||
Definition join {A : Type} : FSet (FSet A) -> FSet A.
|
||||
Proof.
|
||||
hrecursion.
|
||||
- exact ∅.
|
||||
- exact idmap.
|
||||
- intros X Y. apply (X ∪ Y).
|
||||
- apply assoc.
|
||||
- apply comm.
|
||||
- apply nl.
|
||||
- apply nr.
|
||||
- simpl. apply union_idem.
|
||||
Defined.
|
||||
|
||||
Lemma join_assoc {A : Type} (X : FSet (FSet (FSet A))) :
|
||||
join (ffmap join X) = join (join X).
|
||||
Proof.
|
||||
hrecursion X; try (intros; f_ap);
|
||||
try (intros; apply set_path2).
|
||||
Defined.
|
||||
|
||||
Lemma join_return_1 {A : Type} (X : FSet A) :
|
||||
join ({| X |}) = X.
|
||||
Proof. reflexivity. Defined.
|
||||
|
||||
Lemma join_return_fmap {A : Type} (X : FSet A) :
|
||||
join ({| X |}) = join (ffmap (fun x => {|x|}) X).
|
||||
Proof.
|
||||
hrecursion X; try (intros; f_ap);
|
||||
try (intros; apply set_path2).
|
||||
Defined.
|
||||
|
||||
Lemma join_fmap_return_1 {A : Type} (X : FSet A) :
|
||||
join (ffmap (fun x => {|x|}) X) = X.
|
||||
Proof. refine ((join_return_fmap _)^ @ join_return_1 _). Defined.
|
||||
|
||||
Lemma fmap_isIn `{Univalence} {A B : Type} (f : A -> B) (a : A) (X : FSet A) :
|
||||
a ∈ X -> (f a) ∈ (ffmap f X).
|
||||
Proof.
|
||||
hinduction X; try (intros; apply path_ishprop).
|
||||
- apply idmap.
|
||||
- intros b Hab; strip_truncations.
|
||||
apply (tr (ap f Hab)).
|
||||
- intros X0 X1 HX0 HX1 Ha.
|
||||
strip_truncations. apply tr.
|
||||
destruct Ha as [Ha | Ha].
|
||||
+ left. by apply HX0.
|
||||
+ right. by apply HX1.
|
||||
Defined.
|
|
@ -1,54 +0,0 @@
|
|||
(* Operations on [FSet A] when [A] has decidable equality *)
|
||||
Require Import HoTT HitTactics.
|
||||
Require Export representations.definition fsets.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 (a ∈ X).
|
||||
Proof.
|
||||
intros a.
|
||||
hinduction ; try (intros ; apply path_ishprop).
|
||||
- apply _.
|
||||
- intros.
|
||||
unfold Decidable.
|
||||
destruct (dec (a = a0)) as [p | np].
|
||||
* apply (inl (tr p)).
|
||||
* right.
|
||||
intro p.
|
||||
strip_truncations.
|
||||
contradiction.
|
||||
- intros. apply _.
|
||||
Defined.
|
||||
|
||||
Global Instance fset_member_bool : hasMembership_decidable (FSet A) A.
|
||||
Proof.
|
||||
intros a X.
|
||||
destruct (dec (a ∈ X)).
|
||||
- apply true.
|
||||
- apply false.
|
||||
Defined.
|
||||
|
||||
Global Instance subset_decidable : forall (X Y : FSet A), Decidable (X ⊆ Y).
|
||||
Proof.
|
||||
hinduction ; try (intros ; apply path_ishprop).
|
||||
- intro ; apply _.
|
||||
- intros ; apply _.
|
||||
- intros. unfold subset in *. apply _.
|
||||
Defined.
|
||||
|
||||
Global Instance fset_subset_bool : hasSubset_decidable (FSet A).
|
||||
Proof.
|
||||
intros X Y.
|
||||
destruct (dec (X ⊆ Y)).
|
||||
- apply true.
|
||||
- apply false.
|
||||
Defined.
|
||||
|
||||
Global Instance fset_intersection : hasIntersection (FSet A)
|
||||
:= fun X Y => {|X & (fun a => a ∈_d Y)|}.
|
||||
|
||||
End decidable_A.
|
|
@ -1,145 +0,0 @@
|
|||
(* Properties of [FSet A] where [A] has decidable equality *)
|
||||
Require Import HoTT HitTactics.
|
||||
From fsets Require Export properties extensionality operations_decidable.
|
||||
Require Export lattice.
|
||||
|
||||
(* 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, a ∈_d S = a ∈_d T) -> S = T.
|
||||
Proof.
|
||||
intros X Y H2.
|
||||
apply fset_ext.
|
||||
intro a.
|
||||
specialize (H2 a).
|
||||
unfold member_dec, fset_member_bool, 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) :
|
||||
a ∈_d ∅ = false.
|
||||
Proof.
|
||||
reflexivity.
|
||||
Defined.
|
||||
|
||||
Lemma L_isIn (a b : A) :
|
||||
a ∈ {|b|} -> a = b.
|
||||
Proof.
|
||||
intros. strip_truncations. assumption.
|
||||
Defined.
|
||||
|
||||
Lemma L_isIn_b_true (a b : A) (p : a = b) :
|
||||
a ∈_d {|b|} = true.
|
||||
Proof.
|
||||
unfold member_dec, fset_member_bool, 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) :
|
||||
a ∈_d {|a|} = true.
|
||||
Proof.
|
||||
apply L_isIn_b_true ; reflexivity.
|
||||
Defined.
|
||||
|
||||
Lemma L_isIn_b_false (a b : A) (p : a <> b) :
|
||||
a ∈_d {|b|} = false.
|
||||
Proof.
|
||||
unfold member_dec, fset_member_bool, dec in *.
|
||||
destruct (isIn_decidable a {|b|}).
|
||||
- simpl in t.
|
||||
strip_truncations.
|
||||
contradiction.
|
||||
- reflexivity.
|
||||
Defined.
|
||||
|
||||
(* Union and membership *)
|
||||
Lemma union_isIn_b (X Y : FSet A) (a : A) :
|
||||
a ∈_d (X ∪ Y) = orb (a ∈_d X) (a ∈_d Y).
|
||||
Proof.
|
||||
unfold member_dec, fset_member_bool, dec.
|
||||
simpl.
|
||||
destruct (isIn_decidable a X) ; destruct (isIn_decidable a Y) ; reflexivity.
|
||||
Defined.
|
||||
|
||||
Lemma comprehension_isIn_b (Y : FSet A) (ϕ : A -> Bool) (a : A) :
|
||||
a ∈_d {|Y & ϕ|} = andb (a ∈_d Y) (ϕ a).
|
||||
Proof.
|
||||
unfold member_dec, fset_member_bool, dec ; simpl.
|
||||
destruct (isIn_decidable a {|Y & ϕ|}) as [t | t]
|
||||
; destruct (isIn_decidable a Y) as [n | n] ; rewrite comprehension_isIn in t
|
||||
; destruct (ϕ a) ; try reflexivity ; try contradiction
|
||||
; try (contradiction (n t)) ; contradiction (t n).
|
||||
Defined.
|
||||
|
||||
Lemma intersection_isIn_b (X Y: FSet A) (a : A) :
|
||||
a ∈_d (intersection X Y) = andb (a ∈_d X) (a ∈_d Y).
|
||||
Proof.
|
||||
apply comprehension_isIn_b.
|
||||
Defined.
|
||||
|
||||
End operations_isIn.
|
||||
|
||||
(* Some suporting tactics *)
|
||||
Ltac simplify_isIn_b :=
|
||||
repeat (rewrite union_isIn_b
|
||||
|| rewrite L_isIn_b_aa
|
||||
|| rewrite intersection_isIn_b
|
||||
|| rewrite comprehension_isIn_b).
|
||||
|
||||
Ltac toBool :=
|
||||
repeat intro;
|
||||
apply ext ; intros ;
|
||||
simplify_isIn_b ; eauto with bool_lattice_hints typeclass_instances.
|
||||
|
||||
Section SetLattice.
|
||||
|
||||
Context {A : Type}.
|
||||
Context {A_deceq : DecidablePaths A}.
|
||||
Context `{Univalence}.
|
||||
|
||||
Instance fset_max : maximum (FSet A).
|
||||
Proof.
|
||||
intros x y.
|
||||
apply (x ∪ y).
|
||||
Defined.
|
||||
|
||||
Instance fset_min : minimum (FSet A).
|
||||
Proof.
|
||||
intros x y.
|
||||
apply (x ∩ y).
|
||||
Defined.
|
||||
|
||||
Instance fset_bot : bottom (FSet A).
|
||||
Proof.
|
||||
unfold bottom.
|
||||
apply ∅.
|
||||
Defined.
|
||||
|
||||
Instance lattice_fset : Lattice (FSet A).
|
||||
Proof.
|
||||
split; toBool.
|
||||
Defined.
|
||||
|
||||
End SetLattice.
|
||||
|
||||
(* With extensionality we can prove decidable equality *)
|
||||
Section dec_eq.
|
||||
Context (A : Type) `{DecidablePaths A} `{Univalence}.
|
||||
|
||||
Instance fsets_dec_eq : DecidablePaths (FSet A).
|
||||
Proof.
|
||||
intros X Y.
|
||||
apply (decidable_equiv' ((Y ⊆ X) * (X ⊆ Y)) (eq_subset X Y)^-1).
|
||||
apply decidable_prod.
|
||||
Defined.
|
||||
|
||||
End dec_eq.
|
|
@ -1,6 +1,6 @@
|
|||
Require Import HoTT HitTactics.
|
||||
Require Import subobjects.k_finite subobjects.b_finite FSets.
|
||||
Require Import misc.T.
|
||||
Require Import misc.dec_lem.
|
||||
|
||||
Class IsProjective (X : Type) :=
|
||||
projective : forall {P Q : Type} (p : P -> Q) (f : X -> Q),
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
Require Import HoTT.
|
||||
Require Import disjunction lattice notation plumbing.
|
||||
Require Import set_names lattice_interface lattice_examples prelude.
|
||||
|
||||
Section subobjects.
|
||||
Variable A : Type.
|
Loading…
Reference in New Issue