From 6340f4cd773050433d0455917dc677c522c9ac0c Mon Sep 17 00:00:00 2001 From: Niels Date: Mon, 22 May 2017 18:11:47 +0200 Subject: [PATCH] Work on finite sets --- FSet.v | 672 +++++++++++++++++++-------------------------------------- 1 file changed, 218 insertions(+), 454 deletions(-) diff --git a/FSet.v b/FSet.v index cf70dfb..95be7b4 100644 --- a/FSet.v +++ b/FSet.v @@ -1,34 +1,35 @@ Require Import HoTT. Require Export HoTT. +Require Import FunextAxiom. Module Export FinSet. -Set Implicit Arguments. - -Parameter A: Type. +Section FSet. +Variable A : Type. Private Inductive FSet : Type := - | empty : FSet - | L : A -> FSet + | E : FSet + | L : A -> FSet | U : FSet -> FSet -> FSet. -Infix "∪" := U (at level 8, right associativity). -Notation "∅" := empty. +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 assoc : forall (x y z : FSet ), + x ∪ (y ∪ z) = (x ∪ y) ∪ z. Axiom comm : forall (x y : FSet), - x ∪ y = y ∪ x. + x ∪ y = y ∪ x. -Axiom neutl : forall (x : FSet), - ∅ ∪ x = x. +Axiom nl : forall (x : FSet), + ∅ ∪ x = x. -Axiom neutr : forall (x : FSet), - x ∪ ∅ = x. +Axiom nr : forall (x : FSet), + x ∪ ∅ = x. Axiom idem : forall (x : A), - (L x) ∪ (L x) = L x. + {| x |} ∪ {|x|} = {|x|}. Axiom trunc : IsHSet FSet. @@ -47,14 +48,13 @@ Fixpoint FSet_rec {struct x} : P := (match x return _ -> _ -> _ -> _ -> _ -> _ -> P with - | empty => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => e + | 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 H e l u assocP commP nlP nrP idemP y) - (FSet_rec H e l u assocP commP nlP nrP idemP z) + (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) @@ -67,11 +67,11 @@ Axiom FSet_rec_beta_assoc : forall (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 H e l u assocP commP nlP nrP idemP) (assoc x y z) + ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (assoc x y z) = - (assocP (FSet_rec H e l u assocP commP nlP nrP idemP x) - (FSet_rec H e l u assocP commP nlP nrP idemP y) - (FSet_rec H e l u assocP commP nlP nrP idemP 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 @@ -86,10 +86,10 @@ Axiom FSet_rec_beta_comm : forall (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 H e l u assocP commP nlP nrP idemP) (comm x y) + ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (comm x y) = - (commP (FSet_rec H e l u assocP commP nlP nrP idemP x) - (FSet_rec H e l u assocP commP nlP nrP idemP 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 @@ -104,9 +104,9 @@ Axiom FSet_rec_beta_nl : forall (nrP : forall (x : P), u x e = x) (idemP : forall (x : A), u (l x) (l x) = l x) (x : FSet), - ap (FSet_rec H e l u assocP commP nlP nrP idemP) (neutl x) + ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (nl x) = - (nlP (FSet_rec H e l u assocP commP nlP nrP idemP x) + (nlP (FSet_rec P H e l u assocP commP nlP nrP idemP x) ). Axiom FSet_rec_beta_nr : forall @@ -121,9 +121,9 @@ Axiom FSet_rec_beta_nr : forall (nrP : forall (x : P), u x e = x) (idemP : forall (x : A), u (l x) (l x) = l x) (x : FSet), - ap (FSet_rec H e l u assocP commP nlP nrP idemP) (neutr x) + ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (nr x) = - (nrP (FSet_rec H e l u assocP commP nlP nrP idemP x) + (nrP (FSet_rec P H e l u assocP commP nlP nrP idemP x) ). Axiom FSet_rec_beta_idem : forall @@ -138,14 +138,16 @@ Axiom FSet_rec_beta_idem : forall (nrP : forall (x : P), u x e = x) (idemP : forall (x : A), u (l x) (l x) = l x) (x : A), - ap (FSet_rec H e l u assocP commP nlP nrP idemP) (idem x) + 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 empty) + (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) @@ -158,16 +160,16 @@ Fixpoint FSet_ind comm x y # uP x y px py = uP y x py px) (nlP : forall (x : FSet) (px: P x), - neutl x # uP empty x eP px = px) + nl x # uP E x eP px = px) (nrP : forall (x : FSet) (px: P x), - neutr x # uP x empty px eP = px) + 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 - | empty => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => eP + | 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) @@ -176,517 +178,279 @@ Fixpoint FSet_ind Axiom FSet_ind_beta_assoc : forall - (A : Type) - (P : FSet A -> Type) - (eP : P (empty A)) + (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 A), P x -> P y -> P (U x y)) - (assocP : forall (x y z : FSet 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 A) (px: P x) (py: P y), + (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 A) (px: P x), - nl x # uP (empty A) x eP px = px) - (nrP : forall (x : FSet A) (px: P x), - nr x # uP x (empty A) px eP = 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 A), - apD (FSet_ind P eP lP uP assocP commP nlP nrP idemP) + (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 eP lP uP assocP commP nlP nrP idemP x) - (FSet_ind P eP lP uP assocP commP nlP nrP idemP y) - (FSet_ind P eP lP uP assocP commP nlP nrP idemP 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 - (A : Type) - (P : FSet A -> Type) - (eP : P (empty A)) +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 A), P x -> P y -> P (U x y)) - (assocP : forall (x y z : FSet 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 A) (px: P x) (py: P y), + (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 A) (px: P x), - nl x # uP (empty A) x eP px = px) - (nrP : forall (x : FSet A) (px: P x), - nr x # uP x (empty A) px eP = 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 A), - apD (FSet_ind P eP lP uP assocP commP nlP nrP idemP) (comm x y) + (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 eP lP uP assocP commP nlP nrP idemP x) - (FSet_ind P eP lP uP assocP commP nlP nrP idemP 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 - (A : Type) - (P : FSet A -> Type) - (eP : P (empty A)) + (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 A), P x -> P y -> P (U x y)) - (assocP : forall (x y z : FSet 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 A) (px: P x) (py: P y), + (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 A) (px: P x), - nl x # uP (empty A) x eP px = px) - (nrP : forall (x : FSet A) (px: P x), - nr x # uP x (empty A) px eP = 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 A), - apD (FSet_ind P eP lP uP assocP commP nlP nrP idemP) (nl x) + (x : FSet), + apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (nl x) = - (nlP x (FSet_ind P eP lP uP assocP commP nlP nrP idemP x) + (nlP x (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x) ). Axiom FSet_ind_beta_nr : forall - (A : Type) - (P : FSet A -> Type) - (eP : P (empty A)) + (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 A), P x -> P y -> P (U x y)) - (assocP : forall (x y z : FSet 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 A) (px: P x) (py: P y), + (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 A) (px: P x), - nl x # uP (empty A) x eP px = px) - (nrP : forall (x : FSet A) (px: P x), - nr x # uP x (empty A) px eP = 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 A), - apD (FSet_ind P eP lP uP assocP commP nlP nrP idemP) (nr x) + (x : FSet), + apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (nr x) = - (nrP x (FSet_ind P eP lP uP assocP commP nlP nrP idemP x) + (nrP x (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x) ). Axiom FSet_ind_beta_idem : forall - (A : Type) - (P : FSet A -> Type) - (eP : P (empty A)) + (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 A), P x -> P y -> P (U x y)) - (assocP : forall (x y z : FSet 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 A) (px: P x) (py: P y), + (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 A) (px: P x), - nl x # uP (empty A) x eP px = px) - (nrP : forall (x : FSet A) (px: P x), - nr x # uP x (empty A) px eP = 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 eP lP uP assocP commP nlP nrP idemP) (idem x) + apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (idem x) = idemP x. -Parameter A: Type. +End FSet. -Theorem idemSet : - forall x: FSet A, U x x = x. -Proof. -simple refine (FSet_ind _ _ _ _ _ _ _ _ _). -- cbn. -apply nl. -- cbn. -apply idem. -- cbn. -intros. -rewrite assoc. -rewrite (comm (U x y)). -rewrite assoc. -rewrite X. -rewrite <- assoc. -rewrite X0. -reflexivity. -- cbn. +Parameter A : Type. +Parameter eq : A -> A -> Bool. +Parameter eq_refl: forall a:A, eq a a = true. -(* todo optimisation *) -Theorem FSetRec (A : Type) - (P : Type) - (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 A) : P. +Arguments E {_}. +Arguments U {_} _ _. +Arguments L {_} _. + +Definition isIn : A -> FSet A -> Bool. Proof. -simple refine (FSet_ind _ _ _ _ _ _ _ _ _ x). -- apply e. -- apply l. -- apply (fun _ => fun _ => u). -- cbn. -intros. -transitivity (u px (u py pz)). -apply transport_const. -apply assocP. -- cbn. -intros. -transitivity (u px py). -apply transport_const. -apply commP. -- cbn. -intros. -transitivity (u e px). -apply transport_const. -apply nlP. -- cbn. -intros. -transitivity (u px e). -apply transport_const. -apply nrP. -- cbn. -intros. -transitivity (u (l x0) (l x0)). -apply transport_const. -apply idemP. +intros a. +simple refine (FSet_rec A _ _ _ _ _ _ _ _ _ _). +- exact false. +- intro a'. apply (eq 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 (eq a a'); reflexivity. Defined. - +Set Implicit Arguments. - -Theorem FSet_rec_beta_assocT : forall - (A : Type) - (P : Type) - (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 A), - ap (FSetRec e l u assocP commP nlP nrP idemP) (assoc x y z) - = - (assocP (FSetRec e l u assocP commP nlP nrP idemP x) - (FSetRec e l u assocP commP nlP nrP idemP y) - (FSetRec e l u assocP commP nlP nrP idemP z) - ). -Proof. -intros. -eapply (cancelL (transport_const (assoc x y z) _ ) ). -simple refine -((apD_const - (FSetRec e l u assocP commP nlP nrP idemP) - (assoc x y z))^ @ _). -apply FSet_ind_beta_assoc. - - -Theorem FSet_rec_beta_commT : forall - (A : Type) - (P : Type) - (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 A), - ap (FSet_rec e l u assocP commP nlP nrP idemP) (comm x y) - = - (commP (FSet_rec e l u assocP commP nlP nrP idemP x) - (FSet_rec e l u assocP commP nlP nrP idemP y) - ). - -Axiom FSet_rec_beta_nl : forall - (A : Type) - (P : Type) - (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 A), - ap (FSet_rec e l u assocP commP nlP nrP idemP) (nl x) - = - (nlP (FSet_rec e l u assocP commP nlP nrP idemP x) - ). - -Axiom FSet_rec_beta_nr : forall - (A : Type) - (P : Type) - (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 A), - ap (FSet_rec e l u assocP commP nlP nrP idemP) (nr x) - = - (nrP (FSet_rec e l u assocP commP nlP nrP idemP x) - ). - -Axiom FSet_rec_beta_idem : forall - (A : Type) - (P : Type) - (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 e l u assocP commP nlP nrP idemP) (idem x) - = - idemP x. - - -End FinSet. - -Definition isIn : forall - (A : Type) - (eq : A -> A -> Bool), - A -> FSet A -> Bool. -Proof. -intro A. -intro eq. -intro a. -refine (FSet_rec A _ _ _ _ _ _ _ _ _). - Unshelve. - - Focus 6. - apply false. - - Focus 6. - intro a'. - apply (eq a a'). - - Focus 6. - intro b. - intro b'. - apply (orb b b'). - - Focus 3. - intros. - compute. - reflexivity. - - Focus 1. - intros. - compute. - destruct x. - reflexivity. - destruct y. - reflexivity. - reflexivity. - - Focus 1. - intros. - compute. - destruct x. - destruct y. - reflexivity. - reflexivity. - destruct y. - reflexivity. - reflexivity. - - Focus 1. - intros. - compute. - destruct x. - reflexivity. - reflexivity. - - intros. - compute. - destruct (eq a x). - reflexivity. - reflexivity. -Defined. - -Definition comprehension : forall - (A : Type) - (eq : A -> A -> Bool), +Definition comprehension : (A -> Bool) -> FSet A -> FSet A. Proof. -intro A. -intro eq. -intro phi. -refine (FSet_rec A _ _ _ _ _ _ _ _ _). - Unshelve. - - Focus 6. - apply empty. - - Focus 6. - intro a. - apply (if (phi a) then L A a else (empty A)). - - Focus 6. - intro x. - intro y. - apply (U A x y). - - Focus 3. - intros. - compute. - apply nl. - - Focus 1. - intros. - compute. - apply assoc. - - Focus 1. - intros. - compute. - apply comm. - - Focus 1. - intros. - compute. - apply nr. - - intros. - compute. - destruct (phi x). - apply idem. - apply nl. +intros P. +simple refine (FSet_rec A _ _ _ _ _ _ _ _ _ _). +- 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. -Definition intersection : forall (A : Type) (eq : A -> A -> Bool), +Definition intersection : FSet A -> FSet A -> FSet A. Proof. -intro A. -intro eq. -intro x. -intro y. -apply (comprehension A eq (fun (a : A) => isIn A eq a x) y). +intros X Y. +apply (comprehension (fun (a : A) => isIn a X) Y). Defined. -Definition subset (A : Type) (eq : A -> A -> Bool) (x : FSet A) (y : FSet A) : Bool. +Lemma intersection_E : forall x, + intersection E x = E. Proof. -refine (FSet_rec A _ _ _ _ _ _ _ _ _ _). - Unshelve. - - Focus 6. - apply x. - - Focus 6. - apply true. - - Focus 6. - intro a. - apply (isIn A eq a y). - - Focus 6. - intro b. - intro b'. - apply (andb b b'). - - Focus 1. - intros. - compute. - destruct x0. - destruct y0. - reflexivity. - reflexivity. - reflexivity. - - Focus 1. - intros. - compute. - destruct x0. - destruct y0. - reflexivity. - reflexivity. - destruct y0. - reflexivity. - reflexivity. - - Focus 1. - intros. - compute. - reflexivity. - - Focus 1. - intros. - compute. - destruct x0. - reflexivity. - reflexivity. - - intros. - destruct (isIn A eq x0 y). - compute. - reflexivity. - compute. +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 equal_set (A : Type) (eq : A -> A -> Bool) (x : FSet A) (y : FSet A) : Bool - := andb (subset A eq x y) (subset A eq y x). - -Fixpoint eq_nat n m : Bool := - match n, m with - | O, O => true - | O, S _ => false - | S _, O => false - | S n1, S m1 => eq_nat n1 m1 - end. - - - -Theorem test : forall (A:Type) (eq : A -> A -> Bool) -(u: FSet A), ~(u = empty _) -> exists (a: A) (v: FSet A), -u = U _ (L _ a) v /\ (isIn _ eq a v) = False. +Theorem intersection_La : forall a x, + intersection (L a) x = if isIn a x then L a else E. Proof. -intros A eq. -i - - - +intro a. +simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; try (intros ; apply set_path2). +- reflexivity. +- intro b. + admit. +- 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. +Admitted. +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. + +Theorem intersection_assoc : forall x y z, + intersection x (intersection y z) = intersection (intersection x y) z. +Proof. +simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; try (intros ; apply set_path2). +- cbn. + intros y z. + rewrite intersection_E. + rewrite intersection_E. + rewrite intersection_E. + reflexivity. +- intro a. + cbn. + intros y z. +(* simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _ y) ; try (intros ; apply set_path2). *) + admit. +- unfold intersection. + intros x y P Q z z'. + cbn. + rewrite Q. + + rewrite intersection_La. + rewrite intersection_La. + destruct (isIn a y). + * rewrite intersection_La. + destruct (isIn a (intersection y z)). + + reflexivity. + + + * + destruct (isIn a (intersection y z)). + \ No newline at end of file