From 0d210cae04c25c090349f4c58002153a12c790ea Mon Sep 17 00:00:00 2001 From: Leon Gondelman Date: Sat, 3 Jun 2017 00:08:12 +0200 Subject: [PATCH] first step toward cons-union iso: construction of min function for FSet A, where A is Totally Ordered. To construct min, various lemmas about empty set are needed. This min function is constructed in a very inefficient way w.r.t. proofs of assoc, comm, etc. --- FiniteSets/_CoqProject | 2 + FiniteSets/definition.v | 4 + FiniteSets/empty_set.v | 227 ++++++++++++++++ FiniteSets/ordered.v | 574 ++++++++++++++++++++++++++++++++++++++++ FiniteSets/properties.v | 338 ++++++++++++++++------- 5 files changed, 1054 insertions(+), 91 deletions(-) create mode 100644 FiniteSets/empty_set.v create mode 100644 FiniteSets/ordered.v diff --git a/FiniteSets/_CoqProject b/FiniteSets/_CoqProject index e14f2d8..c94b7d5 100644 --- a/FiniteSets/_CoqProject +++ b/FiniteSets/_CoqProject @@ -3,3 +3,5 @@ definition.v operations.v properties.v +empty_set.v +ordered.v diff --git a/FiniteSets/definition.v b/FiniteSets/definition.v index 4ceee60..ecdd2e3 100644 --- a/FiniteSets/definition.v +++ b/FiniteSets/definition.v @@ -190,3 +190,7 @@ Instance FSet_recursion A : HitRecursion (FSet A) := { H_inductor := FSet_ind A; H_recursor := FSet_rec A }. End FSet. + +Notation "{| x |}" := (L x). +Infix "∪" := U (at level 8, right associativity). +Notation "∅" := E. diff --git a/FiniteSets/empty_set.v b/FiniteSets/empty_set.v new file mode 100644 index 0000000..4bf61aa --- /dev/null +++ b/FiniteSets/empty_set.v @@ -0,0 +1,227 @@ +Require Import HoTT. +Require Import HitTactics. +Require Import definition. +Require Import operations. +Require Import properties. + + +Ltac destruct_match := repeat + match goal with + | [|- match ?X with | _ => _ end ] => destruct X + end. + +Ltac destruct_match_1 := + repeat match goal with + | [|- match ?X with | _ => _ end ] => destruct X + | [|- ?X = ?Y ] => apply path_ishprop + | [ H: ?x <> E |- Empty ] => destruct H + | [ H1: ?x = E, H2: ?y = E, H3: ?w ∪ ?q = E |- ?r = E] + => rewrite H1, H2 in H3; rewrite nl in H3; rewrite nl in H3 + end. + +Ltac eq_neq_tac := +match goal with + | [ H: ?x <> E, H': ?x = E |- _ ] => destruct H; assumption +end. + +Section EmptySetProperties. + +Context {A : Type}. +Context {A_deceq : DecidablePaths A}. + + +(*Should go to properties *) +Lemma union_subset `{Funext} : + forall x y z: FSet A, x ∪ y ⊆ z = true -> x ⊆ z = true /\ y ⊆ z = true. +intros x y z Hu. +split. +- eapply subset_isIn. intros a Ha. + eapply subset_isIn in Hu. + + instantiate (1 := a) in Hu. + assumption. + + transitivity (a ∈ x || a ∈ y)%Bool . + apply union_isIn. + rewrite Ha. cbn; reflexivity. +- eapply subset_isIn. intros a Ha. + eapply subset_isIn in Hu. + + instantiate (1 := a) in Hu. + assumption. + + rewrite comm. transitivity (a ∈ y || a ∈ x)%Bool . + apply union_isIn. + rewrite Ha. cbn. reflexivity. +Defined. + + +Lemma eset_subset_l `{Funext} : forall x: FSet A, x ⊆ ∅ = true -> x = ∅. +intros x He. +apply eq_subset. +split. +- cbn; reflexivity. +- assumption. +Defined. + +Lemma eset_subset_r `{Funext} : forall x: FSet A, x = ∅ -> x ⊆ ∅ = true. +intros x He. +apply eq_subset. apply symmetry. assumption. +Defined. + +Lemma subset_transitive `{Funext}: + forall x y z, x ⊆ y = true -> y ⊆ z = true -> x ⊆ z = true. +intros. +Admitted. + +Lemma eset_union_l `{Funext} : forall x y: FSet A, x ∪ y = ∅ -> x = ∅ . +Proof. +intros. +assert (x ⊆ (x ∪ y) = true). +apply subset_union_equiv. rewrite assoc. rewrite (union_idem x). reflexivity. +apply eset_subset_r in X. +assert (x ⊆ ∅ = true). +apply (subset_transitive x (U x y)); assumption. +apply eset_subset_l. +assumption. +Defined. + +Lemma eset_union_lr `{Funext} : +forall x y: FSet A, x ∪ y = ∅ -> ((x = ∅) /\ (y = ∅)). +Proof. +intros. +split. +apply eset_union_l in X; assumption. +rewrite comm in X. +apply eset_union_l in X. assumption. +Defined. + + + +Lemma non_empty_union_l `{Funext} : + forall x y: FSet A, x <> E -> x ∪ y <> E. +intros x y He. +intro Hu. +apply He. +apply eq_subset in Hu. +destruct Hu as [_ H1]. +apply union_subset in H1. +apply eset_subset_l. +destruct H1. +assumption. +Defined. + +Lemma non_empty_union_r `{Funext} : + forall x y: FSet A, y <> E -> x ∪ y <> E. +intros x y He. +intro Hu. +apply He. +apply eq_subset in Hu. +destruct Hu as [_ H1]. +apply union_subset in H1. +apply eset_subset_l. +destruct H1. +assumption. +Defined. + + + +Theorem contrapositive : forall P Q : Type, + (P -> Q) -> (not Q -> not P) . +Proof. +intros p q H1 H2. +unfold "~". +intro H3. +apply H1 in H3. apply H2 in H3. assumption. +Defined. + + + +Lemma non_empty_singleton : forall a: A, L a <> E. +intros a H. +enough (false = true). + contradiction (false_ne_true X). +transitivity (isIn a E). +cbn. reflexivity. +transitivity (a ∈ (L a)). +apply (ap (fun x => a ∈ x) H^) . +cbn. destruct (dec (a = a)). +reflexivity. +destruct n. +reflexivity. +Defined. + + +(* Lemma aux `{Funext}: forall x: FSet A, forall p q: x = ∅ -> False, p = q. +intros. apply path_forall. intro. +apply path_ishprop. +Defined.*) + + +Lemma fset_eset_dec `{Funext}: forall x: FSet A, x = ∅ \/ x <> ∅. +hinduction. +- left; reflexivity. +- right. apply non_empty_singleton. +- intros x y [G1 | G2] [G3 | G4]. + + left. rewrite G1, G3. apply nl. + + right. apply non_empty_union_r; assumption. + + right. apply non_empty_union_l; assumption. + + right. apply non_empty_union_l; assumption. +- intros. destruct px, py, pz; apply path_sum; destruct_match_1. + + rewrite p, p0, p1. rewrite nl. rewrite nl. reflexivity. + + assumption. + + rewrite p, p0 in p1. rewrite nl in p1. rewrite comm in p1. rewrite nl in p1. + assumption. + + rewrite p in p0. rewrite nl in p0. + apply (non_empty_union_l y z) in n. eq_neq_tac. + + rewrite p, p0 in p1. rewrite nr in p1. rewrite nr in p1. assumption. + + rewrite p in p0. rewrite nr in p0. + apply (non_empty_union_l x z) in n. eq_neq_tac. + + rewrite p in p0. rewrite nr in p0. + apply (non_empty_union_l x y) in n. eq_neq_tac. + + apply (non_empty_union_l x y) in n. + apply (non_empty_union_l (x ∪ y) z) in n. eq_neq_tac. +- intros. destruct px, py; apply path_sum; destruct_match_1. + + rewrite p, p0; apply union_idem. + + rewrite p in p0. rewrite nr in p0. assumption. + + rewrite p in p0. rewrite nl in p0. assumption. + + apply (non_empty_union_r y x) in n. eq_neq_tac. +- intros x px. + destruct px. apply path_sum; destruct_match_1. + + assumption. + + apply path_sum; destruct_match_1. assumption. +- intros x px. + destruct px. apply path_sum; destruct_match_1. + + assumption. + + apply path_sum; destruct_match_1. assumption. +- intros. cbn. apply path_sum. destruct_match_1. + + apply (non_empty_singleton x). apply p. +Defined. + + + + + +Lemma union_non_empty `{Funext}: + forall X1 X2: FSet A, U X1 X2 <> ∅ -> X1 <> ∅ \/ X2 <> ∅. +intros X1 X2 G. +specialize (fset_eset_dec X1). +intro. destruct X. rewrite p in G. rewrite nl in G. +right. assumption. left. apply n. +Defined. + +Lemma union_non_empty' `{Funext}: + forall X1 X2: FSet A, U X1 X2 <> ∅ -> + (X1 <> ∅ /\ X2 = ∅) \/ + (X1 = ∅ /\ X2 <> ∅) \/ + (X1 <> ∅ /\ X2 <> ∅ ). +intros X1 X2 G. +specialize (fset_eset_dec X1). +specialize (fset_eset_dec X2). +intros H1 H2. +destruct H1, H2. +- rewrite p, p0 in G. destruct G. apply union_idem. +- left; split; assumption. +- right. left. split; assumption. +- right. right. split; assumption. +Defined. + + + +End EmptySetProperties. diff --git a/FiniteSets/ordered.v b/FiniteSets/ordered.v new file mode 100644 index 0000000..40ee27a --- /dev/null +++ b/FiniteSets/ordered.v @@ -0,0 +1,574 @@ +Require Import HoTT. +Require Import HitTactics. +Require Import definition. +Require Import operations. +Require Import properties. +Require Import empty_set. +Class Antisymmetric {A} (R : relation A) := + antisymmetry : forall x y, R x y -> R y x -> x = y. + + +Class Total {A} (R : relation A) := + total : forall x y, x = y \/ R x y \/ R y x. + +Class TotalOrder {A} (R : relation A) := + { TotalOrder_Reflexive : Reflexive R | 2 ; + TotalOrder_Antisymmetric : Antisymmetric R | 2; + TotalOrder_Transitive : Transitive R | 2; + TotalOrder_Total : Total R | 2; }. + +Context {A : Type0}. +Context {A_deceq : DecidablePaths A}. +Context {R: relation A}. +Context {A_ordered : TotalOrder R}. + + +Ltac eq_neq_tac := +match goal with + | [ H: ?x <> E, H': ?x = E |- _ ] => destruct H; assumption +end. + + +Ltac destruct_match_1 := + repeat match goal with + | [|- match ?X with | _ => _ end ] => destruct X + | [|- ?X = ?Y ] => apply path_ishprop + | [ H: ?x <> E |- Empty ] => destruct H + | [ H1: ?x = E, H2: ?y = E, H3: ?w ∪ ?q = E |- ?r = E] + => rewrite H1, H2 in H3; rewrite nl in H3; rewrite nl in H3 + end. + + +Lemma transport_dom_eq (D1 D2 C: Type) (P: D1 = D2) (f: D1 -> C) : +transport (fun T: Type => T -> C) P f = fun y => f (transport (fun X => X) P^ y). +Proof. +induction P. +hott_simpl. +Defined. + +Lemma transport_dom_eq_gen (Ty: Type) (D1 D2: Ty) (C: Type) (P: D1 = D2) + (Q : Ty -> Type) (f: Q D1 -> C) : +transport (fun X: Ty => Q X -> C) P f = fun y => f (transport Q P^ y). +Proof. +induction P. +hott_simpl. +Defined. + +Lemma min {HFun: Funext} (x: FSet A): x <> ∅ -> A. +Proof. +hrecursion x. +- intro H. destruct H. reflexivity. +- intros. exact a. +- intros x y rx ry H. + apply union_non_empty' in H. + destruct H. + + destruct p. specialize (rx fst). exact rx. + + destruct s. + * destruct p. specialize (ry snd). exact ry. + * destruct p. specialize (rx fst). specialize (ry snd). + destruct (TotalOrder_Total rx ry) as [Heq | [ Hx | Hy ]]. + ** exact rx. + ** exact rx. + ** exact ry. +- intros. rewrite transport_dom_eq_gen. + apply path_forall. intro y0. + destruct ( union_non_empty' x y ∪ z + (transport (fun X : FSet A => X <> ∅) (assoc x y z)^ y0)) + as [[ G1 G2] | [[ G3 G4] | [G5 G6]]]. + + pose (G2' := G2). apply eset_union_lr in G2'; destruct G2'. cbn. + destruct (union_non_empty' x ∪ y z y0) as + [[H'x H'y] | [ [H'a H'b] | [H'c H'd]]]; try eq_neq_tac. + destruct (union_non_empty' x y H'x). + ** destruct p. assert (G1 = fst0). apply path_forall. intro. + apply path_ishprop. rewrite X. reflexivity. + ** destruct s; destruct p; eq_neq_tac. + + destruct (union_non_empty' y z G4) as + [[H'x H'y] | [ [H'a H'b] | [H'c H'd]]]; try eq_neq_tac. + destruct (union_non_empty' x ∪ y z y0). + ** destruct p. cbn. destruct (union_non_empty' x y fst). + *** destruct p; eq_neq_tac. + *** destruct s. destruct p. + **** assert (H'x = snd0). apply path_forall. intro. + apply path_ishprop. rewrite X. reflexivity. + **** destruct p. eq_neq_tac. + ** destruct s; destruct p; try eq_neq_tac. + ** destruct (union_non_empty' x ∪ y z y0). + *** destruct p. eq_neq_tac. + *** destruct s. destruct p. + **** assert (H'b = snd). apply path_forall. intro. + apply path_ishprop. rewrite X. reflexivity. + **** destruct p. assert (x ∪ y = E). + rewrite H'a, G3. apply union_idem. eq_neq_tac. + ** cbn. destruct (TotalOrder_Total (py H'c) (pz H'd)). + *** destruct (union_non_empty' x ∪ y z y0). + **** destruct p0. eq_neq_tac. + **** destruct s. + ***** destruct p0. rewrite G3, nl in fst. eq_neq_tac. + ***** destruct p0. destruct (union_non_empty' x y fst). + ****** destruct p0. eq_neq_tac. + ****** destruct s. + ******* destruct p0. + destruct (TotalOrder_Total (py snd0) (pz snd)). + f_ap. apply path_forall. intro. + apply path_ishprop. + destruct s. f_ap. apply path_forall. intro. + apply path_ishprop. + rewrite p. f_ap. apply path_forall. intro. + apply path_ishprop. + ******* destruct p0. eq_neq_tac. + *** destruct (union_non_empty' x ∪ y z y0). + **** destruct p. eq_neq_tac. + **** destruct s0. destruct p. rewrite comm in fst. + apply eset_union_l in fst. eq_neq_tac. + destruct p. + destruct (union_non_empty' x y fst). + ***** destruct p; eq_neq_tac. + ***** destruct s0. destruct p. + destruct (TotalOrder_Total (py snd0) (pz snd)); + destruct s; try (f_ap; apply path_forall; intro; + apply path_ishprop). + rewrite p. f_ap; apply path_forall; intro; + apply path_ishprop. + destruct s0. f_ap; apply path_forall; intro; + apply path_ishprop. + assert (snd0 = H'c). apply path_forall; intro; + apply path_ishprop. + assert (snd = H'd). apply path_forall; intro; + apply path_ishprop. + rewrite <- X0 in r. rewrite X in r0. + apply TotalOrder_Antisymmetric; assumption. + destruct s0. + assert (snd0 = H'c). apply path_forall; intro; + apply path_ishprop. + assert (snd = H'd). apply path_forall; intro; + apply path_ishprop. + rewrite <- X in r. rewrite X0 in r0. + apply TotalOrder_Antisymmetric; assumption. + f_ap; apply path_forall; intro; + apply path_ishprop. + destruct p; eq_neq_tac. + + cbn. destruct (union_non_empty' y z G6). + ** destruct p. destruct ( union_non_empty' x ∪ y z y0). + *** destruct p. destruct (union_non_empty' x y fst0). + **** destruct p; eq_neq_tac. + **** destruct s; destruct p. eq_neq_tac. + assert (fst1 = G5). apply path_forall; intro; + apply path_ishprop. + assert (fst = snd1). apply path_forall; intro; + apply path_ishprop. + rewrite X, X0. + destruct (TotalOrder_Total (px G5) (py snd1)). + reflexivity. + destruct s; reflexivity. + *** destruct s; destruct p; eq_neq_tac. + ** destruct (union_non_empty' x ∪ y z y0). + *** destruct p. destruct s; destruct p; eq_neq_tac. + *** destruct s. destruct p. destruct s0. destruct p. + apply eset_union_l in fst0. eq_neq_tac. + **** destruct p. + assert (snd = snd0). apply path_forall; intro; + apply path_ishprop. + + destruct (union_non_empty' x y fst0). + destruct p. + assert (fst1 = G5). apply path_forall; intro; + apply path_ishprop. + assert (fst = snd1). apply set_path2. + ***** rewrite X0. rewrite <- X. reflexivity. + ***** destruct s; destruct p; eq_neq_tac. + **** destruct s0. destruct p0. destruct p. + ***** apply eset_union_l in fst. eq_neq_tac. + ***** destruct p, p0. + assert (snd0 = snd). apply path_forall; intro; + apply path_ishprop. + rewrite X. + destruct (union_non_empty' x y fst0). + destruct p; eq_neq_tac. + destruct s. destruct p; eq_neq_tac. + destruct p. + assert (fst = snd1). apply path_forall; intro; + apply path_ishprop. + assert (fst1 = G5). apply path_forall; intro; + apply path_ishprop. + rewrite <- X0. rewrite X1. + destruct (TotalOrder_Total (py fst) (pz snd)). + ****** rewrite <- p. + destruct (TotalOrder_Total (px G5) (py fst)). + rewrite <- p0. + destruct (TotalOrder_Total (px G5) (px G5)). + reflexivity. + destruct s; reflexivity. + destruct s. destruct (TotalOrder_Total (px G5) (py fst)). + reflexivity. + destruct s. + reflexivity. + apply TotalOrder_Antisymmetric; assumption. + destruct (TotalOrder_Total (py fst) (py fst)). + reflexivity. + destruct s; + reflexivity. + ****** destruct s. + destruct (TotalOrder_Total (px G5) (py fst)). + destruct (TotalOrder_Total (px G5) (pz snd)). + reflexivity. + destruct s. + reflexivity. rewrite <- p in r. + apply TotalOrder_Antisymmetric; assumption. + destruct s. + destruct ( TotalOrder_Total (px G5) (pz snd)). + reflexivity. + destruct s. reflexivity. + apply (TotalOrder_Transitive (px G5)) in r. + apply TotalOrder_Antisymmetric; assumption. + assumption. + destruct (TotalOrder_Total (py fst) (pz snd)). reflexivity. + destruct s. reflexivity. + apply TotalOrder_Antisymmetric; assumption. + ******* + destruct ( TotalOrder_Total (px G5) (py fst)). + reflexivity. + destruct s. destruct (TotalOrder_Total (px G5) (pz snd)). + reflexivity. destruct s; reflexivity. + destruct ( TotalOrder_Total (px G5) (pz snd)). + rewrite <- p. + destruct (TotalOrder_Total (py fst) (px G5)). + apply symmetry; assumption. + destruct s. rewrite <- p in r. + apply TotalOrder_Antisymmetric; assumption. + reflexivity. destruct s. + assert ((py fst) = (pz snd)). apply TotalOrder_Antisymmetric. + apply (TotalOrder_Transitive (py fst) (px G5)); assumption. + assumption. rewrite X2. assert (px G5 = pz snd). + apply TotalOrder_Antisymmetric. assumption. + apply (TotalOrder_Transitive (pz snd) (py fst)); assumption. + rewrite X3. + destruct ( TotalOrder_Total (pz snd) (pz snd)). + reflexivity. destruct s; reflexivity. + destruct (TotalOrder_Total (py fst) (pz snd)). + apply TotalOrder_Antisymmetric. assumption. rewrite p. + apply (TotalOrder_Reflexive). destruct s. + apply TotalOrder_Antisymmetric; assumption. reflexivity. +- intros. rewrite transport_dom_eq_gen. + apply path_forall. intro y0. cbn. + destruct + (union_non_empty' x y + (transport (fun X : FSet A => X <> ∅) (comm x y)^ y0)) as + [[Hx Hy] | [ [Ha Hb] | [Hc Hd]]]; + destruct (union_non_empty' y x y0) as + [[H'x H'y] | [ [H'a H'b] | [H'c H'd]]]; + try (eq_neq_tac). + assert (Hx = H'b). apply path_forall. intro. + apply path_ishprop. rewrite X. reflexivity. + assert (Hb = H'x). apply path_forall. intro. + apply path_ishprop. rewrite X. reflexivity. + assert (Hd = H'c). apply path_forall. intro. + apply path_ishprop. rewrite X. + assert (H'd = Hc). apply path_forall. intro. + apply path_ishprop. + rewrite X0. rewrite <- X. + destruct + (TotalOrder_Total (px Hc) (py Hd)) as [G1 | [G2 | G3]]; + destruct + (TotalOrder_Total (py Hd) (px Hc)) as [T1 | [T2 | T3]]; + try (assumption); + try (reflexivity); + try (apply symmetry; assumption); + try (apply TotalOrder_Antisymmetric; assumption). + +- intros. rewrite transport_dom_eq_gen. + apply path_forall. intro y. + destruct (union_non_empty' ∅ x (transport (fun X : FSet A => X <> ∅) (nl x)^ y)). + destruct p. eq_neq_tac. + destruct s. + destruct p. + assert (y = snd). + apply path_forall. intro. + apply path_ishprop. rewrite X. reflexivity. + destruct p. destruct fst. +- intros. rewrite transport_dom_eq_gen. + apply path_forall. intro y. + destruct (union_non_empty' x ∅ (transport (fun X : FSet A => X <> ∅) (nr x)^ y)). + destruct p. assert (y = fst). apply path_forall. intro. +apply path_ishprop. rewrite X. reflexivity. + destruct s. + destruct p. + eq_neq_tac. + destruct p. + destruct snd. +- intros. rewrite transport_dom_eq_gen. + apply path_forall. intro y. + destruct ( union_non_empty' {|x|} {|x|} (transport (fun X : FSet A => X <> ∅) (idem x)^ y)). + reflexivity. + destruct s. + reflexivity. + destruct p. + cbn. destruct (TotalOrder_Total x x). reflexivity. + destruct s; reflexivity. +Defined. + + +Definition minfset {HFun: Funext} : + FSet A -> { Y: (FSet A) & (Y = E) + { a: A & Y = L a } }. +intro X. +hinduction X. +- exists E. left. reflexivity. +- intro a. exists (L a). right. exists a. reflexivity. +- intros IH1 IH2. + destruct IH1 as [R1 HR1]. + destruct IH2 as [R2 HR2]. + destruct HR1. + destruct HR2. + exists E; left. reflexivity. + destruct s as [a Ha]. exists (L a). right. + exists a. reflexivity. + destruct HR2. + destruct s as [a Ha]. + exists (L a). right. exists a. reflexivity. + destruct s as [a1 Ha1]. + destruct s0 as [a2 Ha2]. + assert (a1 = a2 \/ R a1 a2 \/ R a2 a1). + apply TotalOrder_Total. + destruct X. + exists (L a1). right. exists a1. reflexivity. + destruct s. + exists (L a1). right. exists a1. reflexivity. + exists (L a2). right. exists a2. reflexivity. + - cbn. intros R1 R2 R3. + destruct R1 as [Res1 HR1]. + destruct HR1 as [HR1E | HR1S]. + destruct R2 as [Res2 HR2]. + destruct HR2 as [HR2E | HR2S]. + destruct R3 as [Res3 HR3]. + destruct HR3 as [HR3E | HR3S]. + + cbn. reflexivity. + + cbn. reflexivity. + + cbn. destruct R3 as [Res3 HR3]. + destruct HR3 as [HR3E | HR3S]. + * cbn. reflexivity. + * destruct HR2S as [a2 Ha2]. + destruct HR3S as [a3 Ha3]. + destruct (TotalOrder_Total a2 a3). + ** cbn. reflexivity. + ** destruct s. cbn. reflexivity. + cbn. reflexivity. + + destruct HR1S as [a1 Ha1]. + destruct R2 as [Res2 HR2]. + destruct HR2 as [HR2E | HR2S]. + destruct R3 as [Res3 HR3]. + destruct HR3 as [HR3E | HR3S]. + * cbn. reflexivity. + * destruct HR3S as [a3 Ha3]. + destruct (TotalOrder_Total a1 a3). + reflexivity. + destruct s; reflexivity. + * destruct HR2S as [a2 Ha2]. + destruct R3 as [Res3 HR3]. + destruct HR3 as [HR3E | HR3S]. + cbn. destruct (TotalOrder_Total a1 a2). + cbn. reflexivity. + destruct s. + cbn. reflexivity. + cbn. reflexivity. + destruct HR3S as [a3 Ha3]. + destruct (TotalOrder_Total a2 a3). + ** rewrite p. + destruct (TotalOrder_Total a1 a3). + rewrite p0. + destruct ( TotalOrder_Total a3 a3). + reflexivity. + destruct s; reflexivity. + destruct s. cbn. + destruct (TotalOrder_Total a1 a3). + reflexivity. + destruct s. reflexivity. + assert (a1 = a3). + apply TotalOrder_Antisymmetric; assumption. + rewrite X. reflexivity. + cbn. destruct (TotalOrder_Total a3 a3). + reflexivity. + destruct s; reflexivity. + ** destruct s. + *** cbn. destruct (TotalOrder_Total a1 a2). + cbn. destruct (TotalOrder_Total a1 a3). + reflexivity. + destruct s. reflexivity. + rewrite <- p in r. + assert (a1 = a3). + apply TotalOrder_Antisymmetric; assumption. + rewrite X. reflexivity. + destruct s. cbn. + destruct (TotalOrder_Total a1 a3). + reflexivity. + destruct s. reflexivity. + assert (R a1 a3). + apply (TotalOrder_Transitive a1 a2); assumption. + assert (a1 = a3). + apply TotalOrder_Antisymmetric; assumption. + rewrite X0. reflexivity. + cbn. destruct (TotalOrder_Total a2 a3). + reflexivity. + destruct s. + reflexivity. + assert (a2 = a3). + apply TotalOrder_Antisymmetric; assumption. + rewrite X. reflexivity. + *** cbn. destruct (TotalOrder_Total a1 a3). + rewrite p. destruct (TotalOrder_Total a3 a2). + cbn. destruct (TotalOrder_Total a3 a3). + reflexivity. destruct s; reflexivity. + destruct s. cbn. + destruct (TotalOrder_Total a3 a3). + reflexivity. destruct s; reflexivity. + cbn. destruct (TotalOrder_Total a2 a3). + rewrite p0. + reflexivity. + destruct s. + assert (a2 = a3). + apply TotalOrder_Antisymmetric; assumption. + rewrite X. reflexivity. reflexivity. + destruct s. + cbn. + destruct (TotalOrder_Total a1 a2). + cbn. + destruct (TotalOrder_Total a1 a3). + reflexivity. + assert (a1 = a3). + apply TotalOrder_Antisymmetric. assumption. + rewrite <- p in r. assumption. + destruct s. reflexivity. rewrite X. reflexivity. + destruct s. cbn. + destruct (TotalOrder_Total a1 a3). reflexivity. + destruct s. reflexivity. + assert (a1 = a3). + apply TotalOrder_Antisymmetric; assumption. + rewrite X. reflexivity. + cbn. destruct (TotalOrder_Total a2 a3). + rewrite p in r1. + assert (a2 = a1). + transitivity a3. + assumption. + apply TotalOrder_Antisymmetric; assumption. + rewrite X. reflexivity. + destruct s. + assert (a1 = a2). + apply TotalOrder_Antisymmetric. + apply (TotalOrder_Transitive a1 a3); assumption. + assumption. + rewrite X. reflexivity. + assert (a1 = a3). + apply TotalOrder_Antisymmetric. + assumption. + apply (TotalOrder_Transitive a3 a2); assumption. + rewrite X. reflexivity. + destruct ( TotalOrder_Total a1 a2). + cbn. + destruct (TotalOrder_Total a1 a3). + rewrite p0. + reflexivity. + destruct s. + assert (a1 = a3). + apply TotalOrder_Antisymmetric; assumption. + rewrite X. reflexivity. reflexivity. + destruct s. + cbn. + destruct (TotalOrder_Total a1 a3 ). + rewrite p. + reflexivity. + destruct s. + assert (a1 = a3). + apply TotalOrder_Antisymmetric; assumption. + rewrite X. reflexivity. reflexivity. + cbn. + destruct (TotalOrder_Total a1 a3 ). + assert (a2 = a3). + rewrite p in r1. + apply TotalOrder_Antisymmetric; assumption. + rewrite X. destruct (TotalOrder_Total a3 a3). reflexivity. + destruct s; reflexivity. + destruct s. + destruct (TotalOrder_Total a2 a3). + rewrite p. + reflexivity. + destruct s. + assert (a2 = a3). + apply TotalOrder_Antisymmetric; assumption. + rewrite X. reflexivity. + reflexivity. + cbn. destruct (TotalOrder_Total a2 a3). + rewrite p. + reflexivity. + destruct s. + assert (a2 = a3). + apply TotalOrder_Antisymmetric; assumption. + rewrite X. reflexivity. reflexivity. + - cbn. intros R1 R2. + destruct R1 as [La1 HR1]. + destruct HR1 as [HR1E | HR1S]. + destruct R2 as [La2 HR2]. + destruct HR2 as [HR2E | HR2S]. + reflexivity. + reflexivity. + destruct R2 as [La2 HR2]. + destruct HR2 as [HR2E | HR2S]. + reflexivity. + destruct HR1S as [a1 Ha1]. + destruct HR2S as [a2 Ha2]. + destruct (TotalOrder_Total a1 a2). + rewrite p. + destruct (TotalOrder_Total a2 a2). + reflexivity. + destruct s; reflexivity. + destruct s. + destruct (TotalOrder_Total a2 a1). + rewrite p. + reflexivity. + destruct s. + assert (a1 = a2). + apply TotalOrder_Antisymmetric; assumption. + rewrite X. + reflexivity. + reflexivity. + destruct (TotalOrder_Total a2 a1). + rewrite p. + reflexivity. + destruct s. + reflexivity. + assert (a1 = a2). + apply TotalOrder_Antisymmetric; assumption. + rewrite X. + reflexivity. + - cbn. intro R. destruct R as [La HR]. + destruct HR. rewrite <- p. reflexivity. + destruct s as [a1 H]. + apply (path_sigma' _ H^). + rewrite transport_sum. + f_ap. + rewrite transport_sigma. + simpl. + simple refine (path_sigma' _ _ _ ). + apply transport_const. + apply set_path2. + + - intros R. cbn. + destruct R as [ R HR]. + destruct HR as [HE | Ha ]. + rewrite <- HE. reflexivity. + destruct Ha as [a Ha]. + apply (path_sigma' _ Ha^). + rewrite transport_sum. + f_ap. + rewrite transport_sigma. + simpl. + simple refine (path_sigma' _ _ _ ). + apply transport_const. + apply set_path2. + - cbn. intro. + destruct (TotalOrder_Total x x). + reflexivity. + destruct s. + reflexivity. + reflexivity. +Defined. + + + diff --git a/FiniteSets/properties.v b/FiniteSets/properties.v index 6cfa9b3..f78706f 100644 --- a/FiniteSets/properties.v +++ b/FiniteSets/properties.v @@ -1,5 +1,5 @@ Require Import HoTT HitTactics. -Require Import definition operations. +Require Export definition operations. Section properties. @@ -9,7 +9,7 @@ Context {A_deceq : DecidablePaths A}. (** union properties *) Theorem union_idem : forall x: FSet A, U x x = x. Proof. -hinduction; +hinduction; try (intros ; apply set_path2) ; cbn. - apply nl. - apply idem. @@ -20,28 +20,27 @@ try (intros ; apply set_path2) ; cbn. rewrite P. rewrite (comm y x). rewrite <- (assoc x y y). - rewrite Q. - reflexivity. + f_ap. Defined. - + (** isIn properties *) Lemma isIn_singleton_eq (a b: A) : isIn a (L b) = true -> a = b. -Proof. unfold isIn. simpl. +Proof. unfold isIn. simpl. destruct (dec (a = b)). intro. apply p. -intro X. +intro X. contradiction (false_ne_true X). Defined. Lemma isIn_empty_false (a: A) : isIn a E = true -> Empty. -Proof. +Proof. cbv. intro X. -contradiction (false_ne_true X). +contradiction (false_ne_true X). Defined. -Lemma isIn_union (a: A) (X Y: FSet A) : +Lemma isIn_union (a: A) (X Y: FSet A) : isIn a (U X Y) = (isIn a X || isIn a Y)%Bool. -Proof. reflexivity. Qed. +Proof. reflexivity. Qed. (** comprehension properties *) Lemma comprehension_false Y : comprehension (fun a => isIn a E) Y = E. @@ -58,20 +57,20 @@ hrecursion Y; try (intros; apply set_path2). Defined. Theorem comprehension_or : forall ϕ ψ (x: FSet A), - comprehension (fun a => orb (ϕ a) (ψ a)) x = U (comprehension ϕ x) + comprehension (fun a => orb (ϕ a) (ψ a)) x = U (comprehension ϕ x) (comprehension ψ x). Proof. intros ϕ ψ. -hinduction; try (intros; apply set_path2). +hinduction; try (intros; apply set_path2). - cbn. symmetry ; apply nl. - cbn. intros. destruct (ϕ a) ; destruct (ψ a) ; symmetry. * apply idem. - * apply nr. + * apply nr. * apply nl. * apply nl. - simpl. intros x y P Q. - cbn. + cbn. rewrite P. rewrite Q. rewrite <- assoc. @@ -105,8 +104,8 @@ Defined. (** intersection properties *) Lemma intersection_0l: forall X: FSet A, intersection E X = E. -Proof. -hinduction; +Proof. +hinduction; try (intros ; apply set_path2). - reflexivity. - intro a. @@ -144,7 +143,7 @@ hinduction; try (intros ; apply set_path2). destruct (isIn a x) ; destruct (isIn a y). * apply idem. * apply nr. - * apply nl. + * apply nl. * apply nl. Defined. @@ -163,7 +162,7 @@ hrecursion X; try (intros; apply set_path2). * destruct (dec (b = a)) as [pb|]; [|reflexivity]. by contradiction npa. + cbn -[isIn]. intros Y1 Y2 IH1 IH2. - rewrite IH1. + rewrite IH1. rewrite IH2. symmetry. apply (comprehension_or (fun a => isIn a Y1) (fun a => isIn a Y2) (L a)). @@ -171,32 +170,34 @@ hrecursion X; try (intros; apply set_path2). cbn. unfold intersection in *. rewrite <- IH1. - rewrite <- IH2. + rewrite <- IH2. apply comprehension_or. Defined. Theorem intersection_idem : forall (X : FSet A), intersection X X = X. Proof. -hinduction; try (intros; apply set_path2). +hinduction; try (intros ; apply set_path2). - reflexivity. - intro a. destruct (dec (a = a)). * reflexivity. * contradiction (n idpath). - intros X Y IHX IHY. + f_ap; unfold intersection in *. - rewrite comprehension_or. - rewrite comprehension_or. - rewrite IHX. - rewrite IHY. - rewrite comprehension_subset. - rewrite (comm X). - rewrite comprehension_subset. - reflexivity. + + transitivity (U (comprehension (fun a => isIn a X) X) (comprehension (fun a => isIn a Y) X)). + apply comprehension_or. + rewrite IHX. + rewrite (comm X). + apply comprehension_subset. + + transitivity (U (comprehension (fun a => isIn a X) Y) (comprehension (fun a => isIn a Y) Y)). + apply comprehension_or. + rewrite IHY. + apply comprehension_subset. Defined. (** assorted lattice laws *) -Lemma distributive_La (z : FSet A) (a : A) : forall Y : FSet A, +Lemma distributive_La (z : FSet A) (a : A) : forall Y : FSet A, intersection (U (L a) z) Y = U (intersection (L a) Y) (intersection z Y). Proof. hinduction; try (intros ; apply set_path2) ; cbn. @@ -266,12 +267,10 @@ hinduction x; try (intros ; apply set_path2) ; cbn. cbn. rewrite P. rewrite Q. - destruct (isIn a X1) ; destruct (isIn a X2) ; destruct (isIn a y) ; + destruct (isIn a X1) ; destruct (isIn a X2) ; destruct (isIn a y) ; reflexivity. Defined. - - Theorem intersection_assoc (X Y Z: FSet A) : intersection X (intersection Y Z) = intersection (intersection X Y) Z. Proof. @@ -292,7 +291,7 @@ hinduction X; try (intros ; apply set_path2). + reflexivity. + reflexivity. * rewrite intersection_0l. - reflexivity. + reflexivity. - unfold intersection. cbn. intros X1 X2 P Q. rewrite comprehension_or. @@ -314,17 +313,15 @@ hinduction; try (intros ; apply set_path2). * reflexivity. * contradiction (n idpath). - intros X1 X2 P Q. - rewrite comprehension_or. - rewrite comprehension_or. - rewrite P. + f_ap; (etransitivity; [ apply comprehension_or |]). + rewrite P. rewrite (comm X1). + apply comprehension_subset. + rewrite Q. - rewrite comprehension_subset. - rewrite (comm X1). - rewrite comprehension_subset. - reflexivity. + apply comprehension_subset. Defined. - + Theorem distributive_U_int (X1 X2 Y : FSet A) : U (intersection X1 X2) Y = intersection (U X1 Y) (U X2 Y). Proof. @@ -338,18 +335,21 @@ hinduction X1; try (intros ; apply set_path2) ; cbn. rewrite p. rewrite comprehension_subset. reflexivity. -- intros. unfold intersection. (* TODO isIn is simplified too much *) - rewrite comprehension_or. - rewrite comprehension_or. - (* rewrite intersection_La. *) +- intros. + assert (Y = intersection (U (L a) Y) Y) as HY. + { unfold intersection. symmetry. + transitivity (U (comprehension (fun x => isIn x (L a)) Y) (comprehension (fun x => isIn x Y) Y)). + apply comprehension_or. + rewrite comprehension_all. + apply comprehension_subset. } + rewrite <- HY. admit. - unfold intersection. - cbn. intros Z1 Z2 P Q. rewrite comprehension_or. - assert (U (U (comprehension (fun a : A => isIn a Z1) X2) + assert (U (U (comprehension (fun a : A => isIn a Z1) X2) (comprehension (fun a : A => isIn a Z2) X2)) - Y = U (U (comprehension (fun a : A => isIn a Z1) X2) + Y = U (U (comprehension (fun a : A => isIn a Z1) X2) (comprehension (fun a : A => isIn a Z2) X2)) (U Y Y)). rewrite (union_idem Y). @@ -358,22 +358,23 @@ hinduction X1; try (intros ; apply set_path2) ; cbn. rewrite <- assoc. rewrite (assoc (comprehension (fun a : A => isIn a Z2) X2)). rewrite Q. - rewrite + cbn. + rewrite (comm (U (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2) (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y)) Y). rewrite assoc. rewrite P. - rewrite <- assoc. + rewrite <- assoc. cbn. rewrite (assoc (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) Y)). rewrite (comm (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) Y)). rewrite <- assoc. rewrite assoc. enough (C : (U (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) X2) - (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2)) + (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) X2)) = (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) X2)). - rewrite C. + rewrite C. enough (D : (U (comprehension (fun a : A => (isIn a Z1 || isIn a Y)%Bool) Y) - (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y)) + (comprehension (fun a : A => (isIn a Z2 || isIn a Y)%Bool) Y)) = (comprehension (fun a : A => (isIn a Z1 || isIn a Z2 || isIn a Y)%Bool) Y)). rewrite D. reflexivity. @@ -436,49 +437,204 @@ hrecursion X; try (intros ; apply set_path2). rewrite <- Q. Admitted. +Theorem union_isIn (X Y : FSet A) (a : A) : isIn a (U X Y) = orb (isIn a X) (isIn a Y). +Proof. +reflexivity. +Defined. (* Properties about subset relation. *) -Lemma subsect_intersection `{Funext} (X Y : FSet A) : - X ⊆ Y = true -> U X Y = Y. +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). - (*intros. apply equiv_hprop_allpath.*) - + intro. cbn. 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). - specialize (IH2 idpath). - rewrite assoc. rewrite IH1. reflexivity. - specialize (IH1 idpath). - rewrite assoc. rewrite IH1. reflexivity. - specialize (IH2 idpath). - rewrite assoc. rewrite (comm (L a)). rewrite <- assoc. rewrite IH2. - reflexivity. - cbn in Ho. 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. rewrite IH1. reflexivity. - specialize (IH1 idpath). - apply IH2 in G. - rewrite <- assoc. rewrite G. rewrite IH1. reflexivity. - specialize (IH2 idpath). - apply IH1 in G. - rewrite <- assoc. rewrite IH2. rewrite G. reflexivity. - specialize (IH1 G). specialize (IH2 G). - rewrite <- assoc. rewrite IH2. rewrite IH1. reflexivity. + 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. -Theorem +Lemma eq1 (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. -End properties. + +Lemma subset_union_l `{Funext} X : + forall Y, subset X (U X Y) = true. +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. + enough (subset X1 (U (U X1 X2) Y) = true). + enough (subset X2 (U (U X1 X2) Y) = true). + rewrite X. rewrite X0. reflexivity. + { rewrite (comm X1 X2). + rewrite <- (assoc X2 X1 Y). + apply (HX2 (U X1 Y)). } + { rewrite <- (assoc X1 X2 Y). apply (HX1 (U X2 Y)). } +Defined. + +Lemma subset_union_equiv `{Funext} + : forall X Y : FSet A, subset X Y = true <~> U X Y = Y. +Proof. + intros X Y. + unshelve eapply BuildEquiv. + apply subset_union. + unshelve esplit. + { intros HXY. rewrite <- HXY. clear HXY. + apply subset_union_l. } + 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 eq1. + symmetry. + eapply equiv_functor_prod'; apply subset_union_equiv. +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. + 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. + +Lemma HPropEquiv (X Y : Type) (P : IsHProp X) (Q : IsHProp Y) : + (X <-> Y) -> (X <~> Y). +Proof. +intros [f g]. +simple refine (BuildEquiv _ _ _ _). +apply f. +simple refine (BuildIsEquiv _ _ _ _ _ _ _). +- apply g. +- unfold Sect. + intro x. + apply Q. +- unfold Sect. + intro x. + apply P. +- intros. + apply set_path2. +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 HPropEquiv. + exact _. + exact _. + split ; apply subset_isIn. + apply HPropEquiv. + exact _. + exact _. + split ; apply subset_isIn. + - apply HPropEquiv. + exact _. + exact _. + 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. + +End properties. \ No newline at end of file