mirror of https://github.com/nmvdw/HITs-Examples
292 lines
9.1 KiB
Coq
292 lines
9.1 KiB
Coq
Require Import HoTT HitTactics prelude interfaces.lattice_interface interfaces.lattice_examples.
|
||
Require Import kuratowski.operations kuratowski.properties kuratowski.kuratowski_sets isomorphism.
|
||
|
||
Section length.
|
||
Context {A : Type} `{MerelyDecidablePaths A} `{Univalence}.
|
||
|
||
Definition length : FSet A -> nat.
|
||
simple refine (FSet_cons_rec _ _ _ _ _ _).
|
||
- apply 0.
|
||
- intros a X n.
|
||
apply (if a ∈_d X then n else (S n)).
|
||
- intros X a n.
|
||
simpl.
|
||
simplify_isIn_d.
|
||
destruct (dec (a ∈ X)) ; reflexivity.
|
||
- intros X a b n.
|
||
simpl.
|
||
simplify_isIn_d.
|
||
destruct (m_dec_path a b) as [Hab | Hab].
|
||
+ strip_truncations.
|
||
rewrite Hab. simplify_isIn_d. reflexivity.
|
||
+ rewrite ?singleton_isIn_d_false; auto.
|
||
++ simpl.
|
||
destruct (a ∈_d X), (b ∈_d X) ; reflexivity.
|
||
++ intro p. contradiction (Hab (tr p^)).
|
||
++ intros p.
|
||
apply (Hab (tr p)).
|
||
Defined.
|
||
|
||
Open Scope nat.
|
||
(** Specification for length. *)
|
||
Definition length_empty : length ∅ = 0 := idpath.
|
||
|
||
Definition length_singleton a : length {|a|} = 1 := idpath.
|
||
|
||
Lemma length_compute (a : A) (X : FSet A) :
|
||
length ({|a|} ∪ X) = if (a ∈_d X) then length X else S(length X).
|
||
Proof.
|
||
unfold length.
|
||
rewrite FSet_cons_beta_cons.
|
||
reflexivity.
|
||
Defined.
|
||
|
||
Definition length_add (a : A) (X : FSet A) (p : a ∈_d X = false)
|
||
: length ({|a|} ∪ X) = 1 + (length X).
|
||
Proof.
|
||
rewrite length_compute.
|
||
destruct (a ∈_d X).
|
||
- contradiction (true_ne_false).
|
||
- reflexivity.
|
||
Defined.
|
||
|
||
Definition disjoint X Y := X ∩ Y = ∅.
|
||
|
||
Lemma disjoint_difference X Y : disjoint X (difference Y X).
|
||
Proof.
|
||
apply ext.
|
||
intros a.
|
||
rewrite intersection_isIn_d, empty_isIn_d, difference_isIn_d.
|
||
destruct (a ∈_d X), (a ∈_d Y) ; try reflexivity.
|
||
Defined.
|
||
|
||
Lemma disjoint_sub a X Y (H1 : disjoint ({|a|} ∪ X) Y) : disjoint X Y.
|
||
Proof.
|
||
unfold disjoint in *.
|
||
apply ext.
|
||
intros b.
|
||
simplify_isIn_d.
|
||
rewrite empty_isIn_d.
|
||
pose (ap (fun Z => b ∈_d Z) H1) as p.
|
||
simpl in p.
|
||
rewrite intersection_isIn_d, empty_isIn_d, union_isIn_d in p.
|
||
destruct (b ∈_d X), (b ∈_d Y) ; try reflexivity.
|
||
- destruct (b ∈_d {|a|}) ; simpl in * ; try (contradiction true_ne_false).
|
||
Defined.
|
||
|
||
Definition length_disjoint (X Y : FSet A) :
|
||
forall (HXY : disjoint X Y),
|
||
length (X ∪ Y) = (length X) + (length Y).
|
||
Proof.
|
||
simple refine (FSet_cons_ind (fun Z => _) _ _ _ _ _ X)
|
||
; try (intros ; apply path_ishprop) ; simpl.
|
||
- intros.
|
||
apply (ap length (nl _)).
|
||
- intros a X1 HX1 HX1Y.
|
||
rewrite <- assoc, ?length_compute, ?union_isIn_d in *.
|
||
pose (ap (fun Z => a ∈_d Z) HX1Y) as p.
|
||
simpl in p.
|
||
rewrite intersection_isIn_d, union_isIn_d, singleton_isIn_d_aa, empty_isIn_d in p.
|
||
assert (orb (a ∈_d X1) (a ∈_d Y) = a ∈_d X1) as HaY.
|
||
{ destruct (a ∈_d X1), (a ∈_d Y) ; try reflexivity.
|
||
contradiction true_ne_false.
|
||
}
|
||
rewrite ?HaY, HX1.
|
||
destruct (a ∈_d X1) ; try reflexivity.
|
||
apply (disjoint_sub a X1 Y HX1Y).
|
||
Defined.
|
||
|
||
Lemma set_as_difference X Y : X = (difference X Y) ∪ (X ∩ Y).
|
||
Proof.
|
||
toBool.
|
||
generalize (a ∈_d X), (a ∈_d Y).
|
||
intros b c ; destruct b, c ; reflexivity.
|
||
Defined.
|
||
|
||
Lemma length_single_disjoint (X Y : FSet A) :
|
||
length X = length (difference X Y) + length (X ∩ Y).
|
||
Proof.
|
||
refine (ap length (set_as_difference X Y) @ _).
|
||
apply length_disjoint.
|
||
apply ext.
|
||
intros a.
|
||
rewrite ?intersection_isIn_d, empty_isIn_d, difference_isIn_d.
|
||
destruct (a ∈_d X), (a ∈_d Y) ; try reflexivity.
|
||
Defined.
|
||
|
||
Lemma union_to_disjoint X Y : X ∪ Y = X ∪ (difference Y X).
|
||
Proof.
|
||
toBool.
|
||
generalize (a ∈_d X), (a ∈_d Y).
|
||
intros b c ; destruct b, c ; reflexivity.
|
||
Defined.
|
||
|
||
Lemma length_union_1 (X Y : FSet A) :
|
||
length (X ∪ Y) = length X + length (difference Y X).
|
||
Proof.
|
||
refine (ap length (union_to_disjoint X Y) @ _).
|
||
apply length_disjoint.
|
||
apply ext.
|
||
intros a.
|
||
rewrite ?intersection_isIn_d, empty_isIn_d, difference_isIn_d.
|
||
destruct (a ∈_d X), (a ∈_d Y) ; try reflexivity.
|
||
Defined.
|
||
|
||
Lemma plus_assoc n m k : n + (m + k) = (n + m) + k.
|
||
Proof.
|
||
induction n ; simpl.
|
||
- reflexivity.
|
||
- rewrite IHn.
|
||
reflexivity.
|
||
Defined.
|
||
|
||
Lemma inclusion_exclusion (X Y : FSet A) :
|
||
length (X ∪ Y) + length (Y ∩ X) = length X + length Y.
|
||
Proof.
|
||
rewrite length_union_1.
|
||
rewrite (length_single_disjoint Y X).
|
||
rewrite plus_assoc.
|
||
reflexivity.
|
||
Defined.
|
||
End length.
|
||
|
||
Section length_product.
|
||
Context {A B : Type} `{MerelyDecidablePaths A} `{MerelyDecidablePaths B} `{Univalence}.
|
||
|
||
Theorem length_singleproduct (a : A) (X : FSet B)
|
||
: length (single_product a X) = length X.
|
||
Proof.
|
||
simple refine (FSet_cons_ind (fun Z => _) _ _ _ _ _ X)
|
||
; try (intros ; apply path_ishprop) ; simpl.
|
||
- reflexivity.
|
||
- intros b X1 HX1.
|
||
rewrite ?length_compute, ?HX1.
|
||
enough(b ∈_d X1 = (a, b) ∈_d (single_product a X1)) as HE.
|
||
{ rewrite HE ; reflexivity. }
|
||
rewrite singleproduct_isIn_d_aa ; try reflexivity.
|
||
Defined.
|
||
|
||
Open Scope nat.
|
||
|
||
Lemma single_product_disjoint (a : A) (X1 : FSet A) (Y : FSet B)
|
||
: sum (prod (a ∈_d X1 = true)
|
||
((single_product a Y) ∪ (product X1 Y) = (product X1 Y)))
|
||
(prod (a ∈_d X1 = false)
|
||
(disjoint (single_product a Y) (product X1 Y))).
|
||
Proof.
|
||
pose (b := a ∈_d X1).
|
||
assert (a ∈_d X1 = b) as HaX1.
|
||
{ reflexivity. }
|
||
destruct b.
|
||
* refine (inl(HaX1,_)).
|
||
apply ext.
|
||
intros [a1 b1].
|
||
rewrite ?union_isIn_d.
|
||
unfold member_dec, fset_member_bool in *.
|
||
destruct (dec ((a1, b1) ∈ (single_product a Y))) as [t | t]
|
||
; destruct (dec ((a1, b1) ∈ (product X1 Y))) as [p | p]
|
||
; try reflexivity.
|
||
rewrite singleproduct_isIn in t.
|
||
destruct t as [t1 t2].
|
||
rewrite product_isIn in p.
|
||
strip_truncations.
|
||
rewrite <- t1 in HaX1.
|
||
destruct (dec (a1 ∈ X1)) ; try (contradiction false_ne_true).
|
||
contradiction (p(t,t2)).
|
||
* refine (inr(HaX1,_)).
|
||
apply ext.
|
||
intros [a1 b1].
|
||
rewrite intersection_isIn_d, empty_isIn_d.
|
||
unfold member_dec, fset_member_bool in *.
|
||
destruct (dec ((a1, b1) ∈ (single_product a Y))) as [t | t]
|
||
; destruct (dec ((a1, b1) ∈ (product X1 Y))) as [p | p]
|
||
; try reflexivity.
|
||
rewrite singleproduct_isIn in t ; destruct t as [t1 t2].
|
||
rewrite product_isIn in p ; destruct p as [p1 p2].
|
||
strip_truncations.
|
||
rewrite t1 in p1.
|
||
destruct (dec (a ∈ X1)).
|
||
** contradiction true_ne_false.
|
||
** contradiction (n p1).
|
||
Defined.
|
||
|
||
Theorem length_product (X : FSet A) (Y : FSet B)
|
||
: length (product X Y) = length X * length Y.
|
||
Proof.
|
||
simple refine (FSet_cons_ind (fun Z => _) _ _ _ _ _ X)
|
||
; try (intros ; apply path_ishprop) ; simpl.
|
||
- reflexivity.
|
||
- intros a X1 HX1.
|
||
rewrite length_compute.
|
||
destruct (single_product_disjoint a X1 Y) as [[p1 p2] | [p1 p2]].
|
||
* rewrite p2.
|
||
destruct (a ∈_d X1).
|
||
** apply HX1.
|
||
** contradiction false_ne_true.
|
||
* rewrite p1, length_disjoint, HX1 ; try assumption.
|
||
rewrite length_singleproduct.
|
||
reflexivity.
|
||
Defined.
|
||
End length_product.
|
||
|
||
Section length_sum.
|
||
Context `{Univalence}.
|
||
Lemma length_fmap_inj
|
||
{A B : Type} `{MerelyDecidablePaths A} `{MerelyDecidablePaths B}
|
||
(X : FSet A) (f : A -> B) `{IsEmbedding f}
|
||
: length (fset_fmap f X) = length X.
|
||
Proof.
|
||
simple refine (FSet_cons_ind (fun Z => _) _ _ _ _ _ X)
|
||
; try (intros ; apply path_ishprop) ; simpl.
|
||
- reflexivity.
|
||
- intros a Y HX.
|
||
rewrite ?length_compute, HX, (fmap_isIn_d_inj _ f)
|
||
; auto.
|
||
Defined.
|
||
|
||
Context {A B : Type} `{MerelyDecidablePaths A} `{MerelyDecidablePaths B}.
|
||
|
||
Lemma fmap_inl X a : (inl a) ∈_d (fset_fmap (@inr A B) X) = false.
|
||
Proof.
|
||
hinduction X ; try (intros ; apply path_ishprop).
|
||
- reflexivity.
|
||
- intros b.
|
||
rewrite singleton_isIn_d_false.
|
||
* reflexivity.
|
||
* apply inl_ne_inr.
|
||
- intros X1 X2 HX1 HX2.
|
||
rewrite union_isIn_d, HX1, HX2.
|
||
reflexivity.
|
||
Defined.
|
||
|
||
Lemma fmap_inr X a : (inr a) ∈_d (fset_fmap (@inl A B) X) = false.
|
||
Proof.
|
||
hinduction X ; try (intros ; apply path_ishprop).
|
||
- reflexivity.
|
||
- intros b.
|
||
rewrite singleton_isIn_d_false.
|
||
* reflexivity.
|
||
* apply inr_ne_inl.
|
||
- intros X1 X2 HX1 HX2.
|
||
rewrite union_isIn_d, HX1, HX2.
|
||
reflexivity.
|
||
Defined.
|
||
|
||
Lemma disjoint_summants X Y : disjoint (fset_fmap (@inl A B) X) (fset_fmap inr Y).
|
||
Proof.
|
||
apply ext.
|
||
intros [x1 | x2] ; rewrite empty_isIn_d, intersection_isIn_d, ?fmap_inl, ?fmap_inr
|
||
; simpl ; try reflexivity.
|
||
destruct ((inl x1) ∈_d (fset_fmap inl X)) ; reflexivity.
|
||
Defined.
|
||
|
||
Open Scope nat.
|
||
|
||
Theorem length_disjoint_sum (X : FSet A) (Y : FSet B)
|
||
: length (disjoint_sum X Y) = length X + length Y.
|
||
Proof.
|
||
rewrite (length_disjoint _ _ (disjoint_summants _ _)).
|
||
rewrite ?(length_fmap_inj _ _).
|
||
reflexivity.
|
||
Defined.
|
||
End length_sum. |