Opensource benchmark evaluating web operators/agents performance

(* This file is maintained by Jinfang Wang (wang@math.s.chiba-u.ac.jp). *) Require Import ssreflect ssrfun ssrnat ssrbool ssralg ssrint. Require Import eqtype seq choice bigop fintype finset finfun. (***********************************************************************************************) (* This file contains the scripts related to the following paper, *) (* `Formalization of Probabilistic Conditional Independence Using Coq/SSReflect` *) (* by Jinfang Wang, Manabu Hagiwara and Mitsuharu Yamamoto, *) (* submitted to ITP2015 for possible publication. *) (* *) (* These scripts are compatiable with Coq v8.4 and SSReflect v.1.5. *) (* This file was last updated on 2015/3/12. *) (* *) (* The theory of cain is built upon a bounded lattice. *) (* L == of eqType is a bounded lattice. *) (* bot == bottom of lattice L. *) (* top == top of lattice L. *) (* meet == the binary meet operator, a function of type L->L->L. *) (* join == the binary meet operator, a function of type L->L->L. *) (* ge x y == returns [true] if [x >= y], where x and y are elements of L. *) (* gt x y == returns [true] if [x >y], where x and y are elements of L. *) (* le x y == returns [true] if [x <= y], where x and y are elements of L. *) (* lt x y == returns [true] if [x <y], where x and y are elements of L. *) (* complement_P x y == a proposision if y is a complement of x. *) (* complement_b x y == returns [true] if y is a complement of x. *) (* com x == the complement of x. *) (* *) (* The following are basic components of a cainoid, a pre-form of a cain. *) (* coins == of choiceType is the set of coins. *) (* dot == the dot product, a function of coins. *) (* Mix x y == the Mixed coin . *) (* bob == the unit coin . *) (* up x == the up coin with raising context x. *) (* down x == the down coin with lowering context x . *) (* coin_prod_atomics == an axiom saying that each coin is a product of *) (* finite number of atom coins. *) (* up_injective up == asserting that [up] is an injective function. *) (* down_injective down == asserting that [down] is an injective function. *) (* [up_injective] and [down_injective] are triky and may be removed. *) (* *) (* The following are the five axioms of a cainoid. *) (* dotC == dot product is commutative. *) (* dotA == dot product is associative. *) (* bob_unitL == bob is a unit element from left. *) (* up_down_unitL x == [up x] is the inverse of [down x]; *) (* that is, [dot (up x) (down x) = bob]. *) (* Mix_up_down x y == a property corresponding to the definition of *) (* conditional desity functions in probability theory. *) (* *) (* Definition of independence and conditional independence. *) (* CIP x y z == a proposition for independence of x and y given z. *) (* IP x y == a proposition for independence of x and y. *) (* acinv (x, y) == defines the inverse of the atom coin [Mix x y]. *) (* dot_inv c == defines the inverse of an arbitrary coin c. *) (* *) (* A cainoid satisfies all properties of an abelian group. *) (* These properties can be put together using the record type ZmodMixin. *) (* zmodMixin == ZmodMixin dotA dotC bob_unitL dotV. *) (* zmodType == ZmodType _ zmodMixin. *) (* x \+ y == notation for dot x y. *) (* why not use the notation " _ . _" ? *) (***********************************************************************************************) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. (* (*formalization of the fintary case*) Variable T : finType. Variable D : {set T}. Variable X Y Z : {set T}. (*有限集合*) Definition finjoin (X Y : {set {set T}}) := X :|: Y. Definition finmeet (X Y : {set {set T}}) := X :&: Y. Lemma finjoin_commu : commutative finjoin. Proof. apply/ setUC. Qed. Lemma finjoin_assoc : associative finjoin. Proof. apply/ setUA. Qed. Lemma finjoin_absorp : forall X Y, finmeet X (finjoin X Y) = X. Proof. move=> X Y. rewrite finjoin_commu ; apply/ setKU. Qed. Lemma finmeet_commu : commutative finmeet. Proof. apply/ setIC. Qed. Lemma finmeet_assoc : associative finmeet. Proof. apply/ setIA. Qed. Lemma finmeet_absorp : forall X Y, finjoin X (finmeet X Y) = X. Proof. move=> X Y. rewrite finmeet_commu. apply/ setKI. Qed. Lemma finmeet_distr : forall X Y Z, finmeet X (finjoin Y Z) = finjoin (finmeet X Y) (finmeet X Z). Proof. move=> X Y Z. apply/ setIUr. Qed. Definition fincom (X : {set {set T}}) := ~:X. Lemma fincom_bot : forall X, finmeet X (fincom X) = set0. Proof. move=> X. apply/ setICr. Qed. Lemma fincom_top : forall X, finjoin X (fincom X) = setT. Proof. move=> X. apply/ setUCr. Qed. Record lattice_mixin_of (T : Type) : Type := LatticeMixin { join_op : T -> T -> T; meet_op : T -> T -> T; bot_op : T; top_op : T; _ : commutative join_op; _ : associative join_op; _ : forall x y, meet_op x (join_op x y) = x; _ : commutative meet_op; _ : associative meet_op; _ : forall x y, join_op x (meet_op x y) = x; _ : forall x y z, meet_op x (join_op y z) = join_op (meet_op x y) (meet_op x z); com_op : T -> T; com_op_bot : forall x, meet_op x (com_op x) = bot_op; com_op_top : forall x, join_op x (com_op x) = top_op }. Record lattice : Type := Lattice { carrier :> Type; spec : lattice_mixin_of carrier }. Definition finitary_latticemixin := LatticeMixin finjoin_commu finjoin_assoc finjoin_absorp finmeet_commu finmeet_assoc finmeet_absorp finmeet_distr fincom_bot fincom_top. Canonical fin_lattice := Lattice finitary_latticemixin. (*End of the formalization of the finitary Lattice*) *) (* Basic theories on bounded lattice with a bottom and a top. *) Section Lattice. Parameter L : eqType. Parameters bot top: L. Parameters meet join : L->L->L. Axiom join_commutative : commutative join. Axiom join_associative : associative join. Axiom join_absorption : forall x y, meet x (join x y) = x. Axiom meet_commutative : commutative meet. Axiom meet_associative : associative meet. Axiom meet_absorption : forall x y, join x (meet x y) = x. Axiom meet_distributive : forall x y z, meet x (join y z) = join (meet x y) (meet x z). Lemma join_distributive x y z : join x (meet y z) = meet (join x y) (join x z). Proof. by rewrite [in RHS]meet_distributive [meet _ x]meet_commutative join_absorption [in RHS]meet_commutative [in RHS]meet_distributive join_associative [meet z x]meet_commutative meet_absorption [in RHS]meet_commutative. Qed. Lemma join_idempotent(*冪等性*) : idempotent join. Proof. move=>x. move: (join_absorption x x) => Haj. move: (meet_absorption x (join x x)) => Ham. by rewrite -{2}[in LHS ]Haj. Qed. Lemma meet_idempotent : idempotent meet. Proof. move=>x. move: (meet_absorption x x) => Ham. move: (join_absorption x (meet x x)) => Haj. by rewrite -{2}[in LHS ]Ham. Qed. (* Introduce partial order in L *) Definition ge x y := join x y == x. (* <=> (y <= x) *) Definition gt x y := (ge x y) && (x !=y). (* <=> (y < x) *) Definition le x y := ge y x. (* <=> (x <= y)*) Definition lt x y := (le x y) && (x !=y). (* <=> (x < y)*) Axiom bot_minimum : forall x, ge x bot. Axiom top_maximum : forall x, ge top x. Lemma ge_reflexive : reflexive ge. Proof. by move => x; rewrite /ge join_idempotent. Qed. Lemma ge_transitive : transitive ge. Proof. rewrite /ge => x y z /eqP Hyx /eqP Hxz. apply/eqP. by rewrite -Hyx -[in RHS]Hxz join_associative. Qed. Lemma ge_antisymmetric : antisymmetric ge. (*反対称性、x~y & y~x => x=y*) Proof. rewrite /ge => x y /andP [] /eqP Hxy /eqP <-. by rewrite join_commutative. Qed. Lemma join_ge x y : ge (join x y) x. Proof. rewrite /ge. by rewrite -!join_associative [join y x] join_commutative join_associative join_idempotent. Qed. (* [complement_P x y] is a relation between x and y. *) Definition complement_P x y := (meet x y = bot) /\ (join x y = top). (* [complement_b x y] is [true] if y is a complement of x. *) Definition complement_b x y := (meet x y == bot) && (join x y == top). (* Given x of L, [com x] returns the complement of x. *) Parameter com : L -> L. Axiom com_bot : forall x, meet x (com x) = bot. Axiom com_top : forall x, join x (com x) = top. Lemma complement_eqP x y : complement_P x y <-> (complement_b x y) = true. Proof. apply conj. rewrite /complement_P /complement_b => c. apply /andP. destruct c. by rewrite H H0. rewrite /complement_P /complement_b. case /andP => h1 h2. by apply conj; apply/eqP. Qed. Lemma com_P x : complement_P x (com x). Proof. rewrite /complement_P. apply conj. apply com_bot. apply com_top. Restart. rewrite /complement_P. apply conj. by apply com_bot. by apply com_top. Qed. (* Like [ge], [gt] is also transitive. *) Lemma gt_transitive : transitive gt. Proof. rewrite /gt /transitive. move=>y x z. move /andP. case. move=>gxy nxy. move /andP. case. move=>gyz nyz. rewrite (ge_transitive gxy gyz) /=. (*?*) apply /eqP. case. move=>xz. move:nxy. move /eqP. case. apply:ge_antisymmetric. rewrite gxy. rewrite xz. rewrite gyz. by[]. Restart. rewrite /gt => y x z /andP [] gxy nxy /andP [] gyz nyz. rewrite (ge_transitive gxy gyz) /=. apply/eqP => xz. move: nxy. move/eqP. case. apply: ge_antisymmetric. by rewrite gxy xz gyz. Qed. (* an alternative proof *) Goal transitive gt. Proof. rewrite /gt => y x z /andP [] gxy nxy /andP [] gyz nyz. apply /andP; apply conj. by move: gyz; exact: ge_transitive. apply /negP. move=> /eqP xz. rewrite xz in gxy. move: nyz; move /negP. case. apply/eqP; apply: ge_antisymmetric. by apply /andP. Qed. Lemma top_unique y : (forall x, ge y x) -> y == top. Proof. move => Hge; apply /eqP; apply: ge_antisymmetric. by rewrite Hge top_maximum. Qed. Lemma bot_unique y : (forall x, ge x y) -> y == bot. Proof. move => Hge; apply /eqP; apply: ge_antisymmetric. by rewrite Hge bot_minimum. Qed. Lemma join_bot_unitL x : join bot x = x. Proof. by rewrite join_commutative; move: (bot_minimum x); rewrite/ge=> H; apply /eqP. Qed. Lemma join_bot_unitR x : join x bot = x. Proof. by rewrite join_commutative join_bot_unitL. Qed. Lemma meet_bot_unitL x : meet bot x = bot. Proof. move: (join_bot_unitL x). move=> H. by rewrite -H join_absorption. Qed. Lemma meet_bot_unitR x : meet x bot = bot. Proof. by rewrite meet_commutative meet_bot_unitL. Qed. Lemma join_bot : join bot bot = bot. Proof. by move: (join_bot_unitL bot). Qed. Lemma join_top_unitL x : join top x = top. Proof. by rewrite -(com_top x) join_commutative join_associative join_idempotent. Qed. Lemma join_top_unitR x : join x top = top. Proof. by rewrite join_commutative join_top_unitL. Qed. Lemma meet_top_unitL x : meet top x = x. Proof. move: (top_maximum x); rewrite/ge; move/eqP => join_top. by rewrite -[in LHS]join_top meet_commutative join_commutative join_absorption. Qed. Lemma meet_top_unitR x : meet x top = x. Proof. by rewrite meet_commutative meet_top_unitL. Qed. Lemma complement_unique x y z : (complement_P x y) /\ (complement_P x z) -> y = z. Proof. rewrite/complement_P. case => yCx zCx. move:yCx; case=> xy_bot xy_top. move:zCx; case=>xz_bot xz_top. have Hyxz: join (meet x z) y = y. - rewrite xz_bot. by apply: join_bot_unitL. rewrite -Hyxz. rewrite join_commutative join_distributive [join y x] join_commutative xy_top. move: (meet_top_unitL (join y z)) ; move => Hmeet_top. rewrite Hmeet_top. have Hzxy: join z (meet x y) = z. - by rewrite xy_bot join_commutative join_bot_unitL. rewrite -[in RHS]Hzxy join_distributive [join z x]join_commutative xz_top. move: (meet_top_unitL (join z y)); move => Hmeet_top'. by rewrite Hmeet_top' join_commutative. Qed. Lemma join_eq_bot x y : join x y == bot -> (x == bot) && (y == bot). Proof. suff H: forall x y, join x y == bot -> x == bot. by move => Hjoinbot; apply /andP; split; move: Hjoinbot; [| rewrite join_commutative]; exact: H. move => x0 y0 /eqP H. apply /eqP. apply: ge_antisymmetric. rewrite bot_minimum /ge /=. by rewrite -H -join_associative [join y0 x0]join_commutative join_associative join_idempotent. Qed. Theorem ge_bot : forall x, ge bot x -> x == bot. Proof. by move => x /join_eq_bot /andP []. Qed. Lemma minimum_unique: forall y, (forall x, ge x y) -> y == bot. Proof. move => y Hge. apply /eqP. apply: ge_antisymmetric. by rewrite Hge bot_minimum. Qed. End Lattice. (* >>> Begin formalization of the cainoid. *) Section Cainoid. (* Define coins, the dot product, and atom coins. *) Parameter coins : choiceType. Parameter dot : coins -> coins -> coins. Parameter mix : L -> L -> coins. Definition bob := mix bot bot. Definition up x := mix x bot. Definition down x := mix bot x. (* A coin is built as a product of mixed coins. *) Axiom coin_prod_atomics : forall c:coins, {acs:seq (L*L) | c = \big[dot/bob]_(ac <- acs) mix ac.1 ac.2}. (* [up] and [down] are both injective functions. *) Axiom up_injective : injective up. Axiom down_injective : injective down. (* Axioms of a cainoid. *) (* These axioms determine the properties of the dot product. *) Axiom dotC : commutative dot. Axiom dotA : associative dot. Axiom bob_unitL : left_id bob dot. Axiom up_down_unitL : forall x, dot (up x) (down x) = bob. Axiom mix_up_down : forall x y, x != bot -> mix x y = dot (up (join x y)) (down y). (* Basic properties on [bob], the unit of a cainoid. *) Lemma bob_unitR : right_id bob dot. Proof. by move=>x; rewrite dotC bob_unitL. Qed. Lemma down_up_unitL : forall x, dot (down x) (up x) = bob. Proof. by move=> x; rewrite dotC; apply up_down_unitL. Qed. Lemma up_bot_bob : up bot = bob. Proof. done. Qed. Lemma down_bot_bob : down bot = bob. Proof. by[]. Qed. Lemma mix_bot_bot_bob : mix bot bot = bob. Proof. by[]. Qed. Lemma lemma1_1 x : mix x x = bob. Proof. move: (altP (x =P bot)). (*move: (altP (x =P bot)) + caseで場合分け*) case. move=> H. rewrite H. by[]. move=> Hxneqbob. rewrite mix_up_down. rewrite join_idempotent. rewrite up_down_unitL. by[]. Restart. case: (altP (x =P bot)) => [-> | Hxneqbob] //. by rewrite mix_up_down // join_idempotent up_down_unitL. Qed. Lemma lemma1_2 x y : ge x y -> mix x y = dot (up x) (down y). Proof. have [->| Hxneqbob] := altP (x =P bot). (*altP~をスタックのトップに追加し[]があるためcaseを行う。さらに[]の中の->で１サブゴールで出てくるトップを代入する。|の後ろは2サブゴールのトップの名前。*) - move/ge_bot => /eqP ->. (*-は意味なし*) (*by rewrite up_bot_bob down_bot_bob bob_unitL.*) by rewrite up_down_unitL. - by rewrite mix_up_down // /ge => /eqP ->. Qed. Lemma lemma1_3 x y w : x != bot -> ge (join x y) w -> mix x y = mix (join x w) y. Proof. move => Hxneqbot. rewrite /ge !mix_up_down //. - move/eqP => <-. by rewrite -!join_associative [join y w]join_commutative. - apply/eqP => /eqP /join_eq_bot /andP [] /eqP. by move/eqP: Hxneqbot. Qed. (* This lemma concerns transforming a coin identity to another coin identity, by dividing an [up] or [down] coin, or equivalently, by multypling a corresponding [down] or [up] coin. *) Lemma div_up_down : forall (A B : coins) (x : L), dot A (down x) = B <-> A = dot B (up x). Proof. split. - by move=> h; rewrite -[in RHS]h -dotA [dot (_ x) (_ x)]dotC up_down_unitL bob_unitR. - by move=> h; rewrite h -dotA up_down_unitL bob_unitR. Qed. (* Representation of lattice order by a coin identity. *) (* [x <= y] if and only if [mix x y = 1]. *) (*prop1*) Lemma le_mix_bob_eq : forall x y, x != bot -> (le x y <-> mix x y = bob). Proof. split. - rewrite /le /ge mix_up_down; last by[]. rewrite div_up_down bob_unitL join_commutative. by move /eqP ->. - rewrite mix_up_down; last by[]. rewrite div_up_down bob_unitL. move=> Hup. apply up_injective in Hup. move /eqP in Hup. by rewrite /le /ge join_commutative. Qed. Lemma mix_up_ge_down: forall x y, ge x y -> mix x y = dot (up x) (down y). Proof. move => x y. have [-> | Hxneqbob] := altP (x =P bot). - move/ge_bot => /eqP ->. by rewrite up_bot_bob down_bot_bob bob_unitL. - by rewrite mix_up_down // /ge => /eqP ->. Qed. Lemma mix_join_ge_down: forall x y w, x != bot -> ge (join x y) w -> mix x y = mix (join x w) y. Proof. move => x y w Hxneqbot. rewrite /ge !mix_up_down //. - move/eqP => <-. by rewrite -!join_associative [join y w]join_commutative. - apply/eqP => /eqP /join_eq_bot /andP [] /eqP. by move/eqP: Hxneqbot. Qed. Theorem Bayes_Theorem: forall x y, x != bot -> y != bot -> mix x y = dot (mix y x) (dot (up x) (down y)). Proof. move=> x y Hx Hy. rewrite [in RHS]mix_up_down; last exact. by rewrite dotA -![dot (dot (up _) _) _]dotA [dot (_ x) (_ x)]dotC up_down_unitL bob_unitL join_commutative mix_up_down. Qed. Lemma div_down_right: forall A B x, dot A (down x) = B -> A = dot B (up x). Proof. move=> A B x <-. by rewrite -dotA [dot (_ x) _]dotC up_down_unitL dotC bob_unitL. Qed. (* >>> inverse coins*) (* [acinv (x, y)] defines the inverse of the atom coin [mix x y]. *) Definition acinv (ac : L * L) := let: (x, y) := ac in if x == bot then up y else dot (up y) (down (join x y)). (* Now show that [acinv (x, y)] is indeed the inverse of [mix x y]. *) Lemma acinvN : forall ac : L * L, dot (acinv ac) (mix ac.1 ac.2) = bob. Proof. move => [x y] /=. case: (altP (x =P bot)) => [-> | xneqbot]; first by exact: up_down_unitL. rewrite mix_up_down // -dotA [x in dot _ x]dotA. by rewrite [dot (down _) (up _)]dotC !(up_down_unitL, bob_unitL). Qed. (* A cainoid is an abelian group. To show this fact we first show that there exists an inverse coin for an arbitrary coin in a cainoid. *) Lemma dot_inv_sig: forall c:coins, {d | dot d c = bob}. Proof. move => c. case: (coin_prod_atomics c) => acs ->. elim: acs => [| ac acs [d Hd]] ; first by exists bob; rewrite big_nil bob_unitL. exists (dot d (acinv ac)). by rewrite big_cons -dotA [dot (acinv _) (dot _ _)]dotA acinvN bob_unitL. Qed. (* The following function [dot_inv], of type [coins -> coins], defines an inverse for an arbitrary coin of a cainoid. *) Definition dot_inv (c:coins) := sval (dot_inv_sig c). (* The definition for [dot_inv] is indeed a right one. *) Lemma dotV : left_inverse bob dot_inv dot. Proof. move => c. exact: (svalP (dot_inv_sig c)). Qed. (* A cainoid has all properties of an Abelian group. *) (* Now we put all these relevant properties together. *) Definition zmodMixin := ZmodMixin dotA dotC bob_unitL dotV. Canonical zmodType := ZmodType _ zmodMixin. (* Now we introduce the usual plus notation for abelian groups. *) Notation "x \+ y" := (dot x y)(at level 50, left associativity). (* All the properties known to abelian groups can now be exported to a cainoid directly. *) Lemma dotrC: forall a b, a \+ b = b \+ a. Proof. by apply: GRing.addrC. Qed. Lemma dotrA: forall x y z, x \+ (y \+ z) = (x \+ y) \+ z. Proof. by apply: GRing.addrA. Qed. Example dotrA': forall x y z, (x \+ y) \+ z = x \+ (y \+ z). Proof. move=> x y z; apply: Logic.eq_sym; exact: GRing.addrA. Qed. Example dotrA'': forall x y z, (x \+ y) \+ z = x \+ (y \+ z). Proof. move=> x y z; by rewrite dotrA. Qed. Lemma dotrAC: forall x y z, x \+ y \+ z = x \+ z \+ y. Proof. move=> x y z. by rewrite -dotrA [y \+ z]dotrC dotrA. Qed. Lemma dotrACA :forall x y z t, (x \+ y) \+ (z \+ t) = (x \+ z) \+ (y \+ t). Proof. exact: GRing.addrACA. Qed. Example dotr_perm :forall a b c d, a \+ b \+ c \+ d = d \+ c \+ b \+ a. Proof. move=> a b c d. by rewrite [_ \+ d]dotrC [(_ \+ _) \+ c]dotrC [a \+ b]dotrC [d \+ (c \+ _)]dotrA [_ \+ (b \+ a)]dotrA. Qed. (* In an abelian group, the unit element is 0. *) (* So in the ring scope (%R), bob corresponds to 0. *) Lemma bob0 : bob = 0%R. Proof. done. Qed. Lemma dot0r: forall x, bob \+ x = x. Proof. exact: GRing.add0r. Qed. Lemma dotr0: forall x, x \+ bob = x. Proof. exact: GRing.addr0. Qed. Lemma dotNr :forall x, (dot_inv x) \+ x = bob. Proof. exact: GRing.addNr. Qed. End Cainoid. (* The following are experimental *) (* updated 2015/3/26 *) (* Axioms from classic logic *) Axiom peirce_axiom : forall P Q: Prop, ((P->Q)->P)->P. Axiom classic_axiom : forall P:Prop, ~ ~P -> P. Axiom excluded_middle_axiom : forall P:Prop, P \/ ~P. Axiom de_morgan_not_and_not_axiom : forall P Q:Prop, ~(~P /\ ~Q) -> P\/Q. Axiom implies_to_or_axiom : forall P Q:Prop, (P->Q) -> (~P\/Q). Definition peirce := forall P Q: Prop, ((P->Q)->P)->P. Definition classic := forall P:Prop, ~ ~P -> P. Definition excluded_middle := forall P:Prop, P \/ ~P. Definition de_morgan_not_and_not := forall P Q:Prop, ~(~P/\~Q) -> P\/Q. Definition implies_to_or := forall P Q:Prop, (P->Q) -> (~P\/Q). Lemma or_imply_and: forall A B C:Prop, (A \/ B -> C) -> (A->C) /\ (B->C). Proof. move=> A B C H. apply conj. by move=>HA; apply: H; left . by move=>HB; apply: H; right . Qed. (* de Morgran's law: part 1 *) (* previously named not_a_or_b_implies_not_a_and_not_b *) Lemma morgan_not_or: forall (A B : Prop), ~(A \/ B) -> ~A /\ ~B. Proof. move=> A B. rewrite/not. by apply or_imply_and. Qed. (* an alternative proof *) Theorem not_a_or_b_implies_not_a_and_not_b : forall A B, ~ (A \/ B) -> (~ A) /\ (~ B). Proof. move=>A B nAB. split. by move=> HA; apply: nAB; left. by move=> HB; apply: nAB; right. Qed. Theorem peirce_implies_classic : peirce -> classic. Proof. rewrite /peirce /classic. move=> p P nnP; rewrite /not in nnP. by apply p with (Q := False). Qed. (* alternativ coq-proof *) Theorem peirce_implies_classic'': peirce -> classic. Proof. unfold peirce. unfold classic. intros p P nnP. unfold not in nnP. apply p with (Q := False). intros h. apply nnP in h. inversion h. Qed. Theorem classic_implies_peirce : classic -> peirce. Proof. rewrite/classic /peirce. move => nnp P Q HPQ. apply: nnp => np. by apply np; apply: HPQ. Qed. Lemma classic_eq_peirce : classic <-> peirce. Proof. apply conj. by apply classic_implies_peirce. by apply peirce_implies_classic. Qed. Example classic_implies_peirce': forall P Q: Prop, (~ ~P -> P) -> (((P->Q)->P)->P). Proof. move=> P Q nnP H. apply: nnP => nP. by apply nP; apply: H. Qed. Theorem classic_implies_excluded_middle : classic -> excluded_middle. Proof. rewrite /classic /excluded_middle => c P. apply: c. move=> h. apply not_a_or_b_implies_not_a_and_not_b in h. by destruct h as [nh nnh]. Qed. Example classic_implies_excluded_middle': forall P, (P \/ ~ P). Proof. move=>P; move:classic_axiom => c. move: (c (P\/~P)) => HPoP; apply: HPoP. move=> nnPoP. apply not_a_or_b_implies_not_a_and_not_b in nnPoP. by destruct nnPoP. Qed. Theorem excluded_middle_implies_classic : excluded_middle -> classic. Proof. rewrite /excluded_middle /classic. move=> em P nnP. by destruct (em P). Qed. (* an alternative proof *) Theorem excluded_middle_implies_classic' : excluded_middle -> classic. Proof. rewrite /excluded_middle /classic. move=> em P nnP. move: (em (P\/~P))=> H. destruct H as [PnP | nPnP]. by destruct PnP as [HP | HnP]. apply not_a_or_b_implies_not_a_and_not_b in nPnP. by destruct nPnP. Qed. Theorem classic_implies_de_morgan_not_and_not : classic -> de_morgan_not_and_not. Proof. rewrite /classic /de_morgan_not_and_not. move=> c P Q H; move: (c (P\/Q)). apply. move=> H1. by apply not_a_or_b_implies_not_a_and_not_b in H1. Qed. (* an alternative proof *) Theorem classic_implies_de_morgan_not_and_not' : classic -> de_morgan_not_and_not. Proof. rewrite /classic /de_morgan_not_and_not. move=> c P Q H; apply: c; move=> h. by apply not_a_or_b_implies_not_a_and_not_b in h. Qed. Theorem de_morgan_not_and_not_implies_excluded_middle : de_morgan_not_and_not -> excluded_middle. Proof. rewrite /de_morgan_not_and_not /excluded_middle. move=>dm P. apply: dm =>H. by destruct H. Qed. Theorem de_morgan_not_and_not_implies_classic : de_morgan_not_and_not -> classic. Proof. rewrite /de_morgan_not_and_not /classic. move=> dm P nnP. move: (dm P P)=> H. have t: P \/ P -> P. by case. apply:t; apply H; move=> h. by destruct h. Qed. (* an alternative proof using what have already been proved.*) Goal de_morgan_not_and_not -> classic. Proof. move=> dm. by apply excluded_middle_implies_classic; apply de_morgan_not_and_not_implies_excluded_middle; apply dm. Qed. Theorem excluded_middle_implies_implies_to_or: excluded_middle -> implies_to_or. Proof. rewrite /excluded_middle /implies_to_or. move=> em P Q h. destruct (em P). by right; apply: h. by left. Qed. Theorem implies_to_or_implies_excluded_middle: implies_to_or -> excluded_middle. Proof. rewrite /implies_to_or /excluded_middle. move=> to P. destruct (to P P) . by[]. by right. by left. Qed. (* beginner's proof *) Theorem implies_to_or_implies_excluded_middle' : implies_to_or -> excluded_middle. Proof. rewrite /implies_to_or /excluded_middle. move=> to P. move: (to P P) => H. suff: ~ P \/ P -> P \/ ~ P. by move=> h; apply h; apply H. move=> PnP; destruct PnP. by right. by left. Qed. (* previously known as not_a_and_b_implies_not_a_or_not_b *) Theorem morgan_not_and : forall A B, ~ (A /\ B) -> (~ A) \/ (~ B). Proof. move=>A B nAB. move: not_a_or_b_implies_not_a_and_not_b => dm. move: (dm (~A) (~B)) => Hdm. move: excluded_middle_axiom => em. move: (em (~A \/ ~B)) => Hem. destruct Hem. by[]. apply Hdm in H; destruct H as [ h1 h2]. apply classic_axiom in h1. apply classic_axiom in h2. by have t: A /\ B. Qed. (* proof by contradiction *) Lemma contradiction : forall P Q : Prop, (~Q -> ~P) <-> (P -> Q). Proof. move=> P Q. apply conj. move=> nQnP HP. move: excluded_middle_axiom => em. move: (em Q) => emQ. destruct emQ as [q | nq]. by[]. by apply nQnP in nq. move=> H Hq. move/H. by[]. Qed. (* an example using contradiction Lemma *) Example de_morgan_not_and : forall A B, ~ (A /\ B) -> (~ A) \/ (~ B). Proof. move=>A B; apply contradiction. move=> H. apply not_a_or_b_implies_not_a_and_not_b in H. move=>h; apply: h. by destruct H as [HA HB]; apply classic_axiom in HA; apply classic_axiom in HB. Qed. Lemma not_not_and_double_not: forall P Q: Prop, ~(~P /\ ~Q) -> ~ ~ P \/ ~ ~ Q . Proof. by move=>P Q H; apply de_morgan_not_and in H. Qed. Goal forall P Q:Prop, ~(~P /\ ~Q) -> P\/Q. Proof. move=> P Q H. apply de_morgan_not_and in H. destruct H as [HP | HQ]. apply classic_axiom in HP; by left. apply classic_axiom in HQ; by right. Qed. (* prove properties for [gt] *) (* Students should fill in here. *) (* prove the same properties for [le] *) (* Students should fill in here. *) (* prove the same properties for [lt] *) (* Students should fill in here. *) (* prove properties for [le] and [lt] *) (* Students should fill in here. *) (* [remove_last] removes the last element of a list. *) Fixpoint remove_last (T:Type) (l: seq T) := let l' := rev l in match l' with | nil => nil | h::t => rev t end. (* [tail] removes the first element of a list. *) Fixpoint tail (T:Type) (l: seq T) := match l with | [::] => [::] | _::t => t end. (* [big_cons] defines the rule for recursive computation. *) (* [big_cons_dot] (probably not needed) is a special case of [big_cons], with dot operator of coins: c1...cn = c1.(c2...cn) *) Lemma big_cons_dot: forall (cs: seq coins), \big[dot/bob]_(c <- cs) c = let first := head bob cs in dot first (\big[dot/bob]_(c <- tail cs) c). Proof. move=> cs. case: cs. rewrite big_nil /=. by rewrite bob_unitL. move=> a l. by rewrite big_cons /=. Qed. (* Power of a coin, [ncoins n c =c...c]. *) Definition ncoins n c := \big[dot/bob]_(i <- nseq n c) i. (* alternative definition of power using [iter]. *) Definition ncoins' n c := if (n==0) then bob else (iter n.-1 (dot c) c). (* power of a raising/lowering coin *) Definition nups n x := ncoins n (up x). Definition ndowns n x := ncoins n (down x). Lemma updownnK : forall n x, dot (nups n x) (ndowns n x) = bob. Proof. (* FILL IN HERE *) Admitted. Lemma ncoins1': forall n c, ncoins' n.+1 c = dot (ncoins' n c) c. Proof. case. move=>c. by rewrite /ncoins' /= bob_unitL. rewrite /ncoins'/=; move=> n c; by rewrite dotC. Qed. Lemma ncoins0_bob : forall x, ncoins 0 x = bob. Proof. by move => x; rewrite /ncoins big_nil. Qed. Lemma up_power0_bob : forall x, nups 0 x = bob. Proof. move=> x. rewrite /nups /ncoins big_cons_dot/=; by rewrite big_nil bob_unitR. Qed. Lemma down_power0_bob : forall x, ndowns 0 x = bob. Proof. move=> x. rewrite /ndowns /ncoins big_cons_dot /=; by rewrite big_nil bob_unitR. Qed. Lemma up_power1 : forall x, nups 1 x = up x. Proof. move=> x. rewrite /nups /ncoins big_cons_dot /=. by rewrite big_nil bob_unitR. Qed. Lemma down_power1 : forall x, ndowns 1 x = down x. Proof. move=> x. rewrite /ndowns /ncoins big_cons_dot /=; by rewrite big_nil bob_unitR. Qed. Lemma updown1K : forall x, dot (nups 1 x) (ndowns 1 x) = bob. Proof. by move=> x; rewrite up_power1 down_power1 up_down_unitL. Qed. Example up3 : forall x, nups 3 x = ncoins' 3 (up x). Proof. move=>x. rewrite /nups /ncoins /ncoins'. do 3! rewrite big_cons_dot /=. (* big_cons is also ok. *) by rewrite big_nil bob_unitR. Qed. Example down3 : forall x, ndowns 3 x = ncoins' 3 (down x). Proof. move=>x. rewrite /ndowns /ncoins /ncoins'. do 3! rewrite big_cons/=. by rewrite big_nil bob_unitR. Qed. Lemma nups_eq : forall n x, nups n x = ncoins' n (up x). Proof. move=> n x. rewrite /nups /ncoins /ncoins' big_cons_dot /=. elim n. by rewrite big_nil bob_unitL /=. move=> m iH. rewrite big_cons_dot /=. rewrite iH /=. case m=> /=. by rewrite bob_unitR. by[]. Qed. Lemma ndowns_eq : forall n x, ndowns n x = ncoins' n (down x). Proof. move=> n x. rewrite /ndowns /ncoins /ncoins' big_cons_dot /=. elim n => /=. by rewrite big_nil bob_unitL /=. move=> m iH. rewrite big_cons_dot /= iH. case m =>/=. by rewrite bob_unitR /=. done. Qed. Lemma ncoins2_eq: forall n x, ncoins n x = ncoins' n x. Proof. move=> n x. rewrite /ncoins /ncoins' big_cons_dot /=. elim n =>/=. by rewrite big_nil bob_unitL /=. move=> m iH. rewrite big_cons_dot /= iH. case m =>/=. by rewrite bob_unitR. done. Qed. Lemma nupdownK : forall n x, dot (nups n x) (ndowns n x) = bob. Proof. move=> n x; rewrite nups_eq ndowns_eq. elim n. by rewrite /ncoins' /=; rewrite bob_unitL. move=> m iH. do 2! rewrite ncoins1'. have ac: forall a b, dot a b = bob -> dot (dot a (up x)) (dot b (down x)) = bob. - move=> a b ih. - by rewrite -!dotA [ dot _ (dot b _)] dotA [dot _ b] dotC -![dot (dot b _) _]dotA up_down_unitL bob_unitR ih. by rewrite ac. Qed. (* work from here *) (* 2015/3/27 *) (* working with integers using library [ssrint]. *) Require Import ssrint. (* addition of two integers *) Definition addz := intZmod.addz. (* negative numbers are denoted by [Negz n] == -(n+1). *) Eval compute in addz 1 2. Eval compute in addz 3 (-1). Eval compute in addz 1 (Negz 0). Eval compute in addz 1 (Negz 1). (* Opposite of an integer n, [oppz n] == -n. For instance, oppz Posz 0 == Posz 0, oppz Posz n.+1 == Neg n, oppz Negz 0 == Posz 1, oppz Negz n == Posz n.+1. *) Definition oppz := intZmod.oppz. Eval compute in addz 1 (oppz 1). Eval compute in addz (Negz 3) (oppz (Negz 3)). Goal forall n, addz n (oppz n) = Posz 0. Proof. (* FILL IN LINES HERE *) Admitted. (* Notations for integers, addition, and subtraction. (1) 1,2,3, etc. also stand for int, when coerced, eg. 1+1. (2) - 1%:Z, - 2%:Z, -3%:Z, stand for negative integers, -1, -2, -3, etc.. (3) m+n, integer addition for any m, n integers, e.g., 1+2, - 5%:Z + - 7%:Z, etc.. (4) m-n, integer subtraction for any m, n integers, e.g., 1-7%:Z, - 5%:Z - 7%:Z, etc.. *) (* 2015/3/27 *) Local Open Scope int_scope. Local Notation "0" := (Posz 0) : int_scope. Local Notation "-%Z" := (@oppz) : int_scope. Local Notation "- x" := (oppz x) : int_scope. Local Notation "+%Z" := (@addz) : int_scope. Local Notation "x + y" := (addz x y) : int_scope. Local Notation "x - y" := (x + - y) : int_scope. (* addition of two integers *) Eval compute in 0 + 0. Eval compute in 3+0. Eval compute in Negz 3 + 4. Eval compute in 4 + Negz 3. Eval compute in Negz 3 + Negz 3. Goal forall m n:nat, addz m n = addn m n. Proof. (* FILL IN LINES HERE *) Admitted. (* to confirm the useage of the notations *) (* the oppsite numbers *) Goal -(-0)=0. Proof. by[]. Qed. Goal -(-1) = 1. Proof. by[]. Qed. Goal -(-2%:Z) = 2%:Z. Proof. by[]. Qed. Goal -(-2%:Z) = 2. Proof. by[]. Qed. Goal - -2%:Z = 2. Proof. by[]. Qed. Goal --2%:Z = 2. Proof. by[]. Qed. Goal -------2%:Z = -2%:Z. Proof. by[]. Qed. Goal forall n, n - n =0. Proof. move => n; elim n. by[]. by case. by case. Qed. Goal forall n, oppz (oppz n) = n. Proof. by do 2! case. Qed. Goal forall n: int, - - n = n. Proof. by do 2! case. Qed. Goal forall n, - Negz n = n.+1. Proof. by []. Qed. (* Define integer powers of coins. *) Definition nupsz n x := match n with | Posz n' => nups n' x | Negz n' => ncoins n'.+1 (down x) end. Definition ndownsz n x := match n with | Posz n' => ndowns n' x | Negz n' => ncoins n'.+1 (up x) end. Lemma upz_power0_bob: forall x, nupsz 0 x = bob. Proof. move=> x /=. by rewrite up_power0_bob. Qed. Lemma upz_power1: forall x, nupsz 1 x = up x. Proof. move=> x /=. by rewrite up_power1. Qed. Lemma downz_power0_bob: forall x, ndownsz 0 x = bob. Proof. move=> x /=. by rewrite down_power0_bob. Qed. Lemma downz_power1: forall x, ndownsz 1 x = down x. Proof. move=> x /=. by rewrite down_power1. Qed. Lemma upz_power_m1: forall x, nupsz (-1%:Z) x = down x. Proof. move=> x /=. rewrite /ncoins big_cons_dot /=. by rewrite big_nil bob_unitR. Qed. Lemma downz_power_m1: forall x, ndownsz (-1%:Z) x = up x. Proof. move=> x /=. rewrite /ncoins big_cons_dot /=. by rewrite big_nil bob_unitR. Qed. Lemma nupsz_eq: forall (n:nat) x, nupsz n x = nups n x. Proof. by []. Qed. Lemma ndownsz_eq: forall (n:nat) x, ndownsz n x = ndowns n x. Proof. by []. Qed. Lemma nupszdown_eq: forall (n:nat) x, nupsz (-n%:Z) x = ndowns n x. Proof. case. by[]. by[]. Qed. Lemma ndownszup_eq: forall (n:nat) x, ndownsz (-n%:Z) x = nups n x. Proof. case. by[]. by[]. Qed. Lemma updownz_eq: forall n x, nupsz n x = ndownsz (-n) x. Proof. case; move=> n x /=. by rewrite /nups ndownszup_eq /= /ndowns. by[]. Qed. Lemma downupz_eq: forall n x, ndownsz n x = nupsz (-n) x. Proof. case; move=> n x. by rewrite nupszdown_eq. by[]. Qed. Lemma upzK: forall n x, dot (nupsz n x) (nupsz (-n) x) = bob. Proof. case; move=> n x. by rewrite nupsz_eq nupszdown_eq nupdownK /=. move=> /=. have tem: ndowns n.+1 x = ncoins n.+1 (down x). by[]. by rewrite -!tem dotC nupdownK. Qed. Lemma downzK: forall n x, dot (ndownsz n x) (ndownsz (-n) x) = bob. Proof. move=> n x; by rewrite -!updownz_eq downupz_eq dotC upzK. Qed. Lemma mix_up: forall x y, x != bot -> mix x y = dot (nupsz 1 (join x y)) (nupsz (-1) y). Proof. move=> x y iH; rewrite mix_up_down. by rewrite -!upz_power1 -!downz_power1 downupz_eq. by[]. Qed. Lemma atomic_up: forall x y, mix x y = if x==bot then down y else dot (nupsz 1 (join x y)) (nupsz (-1) y). Proof. move=> x y. case: ifPn; first by move/eqP => ->. exact: mix_up. Qed. (* Representation of coins in terms of raising coins. *) (* Lower coins can be expressed as powers of raising coins. *) Lemma down_up_ex: forall x, {n : int | down x = nupsz n x}. Proof. by exists (-1%:Z); rewrite upz_power_m1. Qed. (* Mixed coins can be decomposed as the product of powers of raising coins *) Lemma mix_up_ex: forall x y, x != bot -> {a: L*L | mix x y = dot (nupsz 1 a.1) (nupsz (-1) a.2)}. Proof. by move=> x y; exists (join x y, y); rewrite mix_up. Qed. (* >>> An example using dependent type *) Example ex_imp_ex A (f g: A -> Prop): (exists a: A, f a) -> (forall x: A, f x -> g x) -> exists b: A, g b. Proof. case => a Sa SiT. by exists a; apply: SiT. Qed. (* <<< An example using dependent type *) (* An important theorem says that any coin can be decomposed as the product of powers of raising coins. *) (* By definition, any coin is a product of mixed coins. *) Print coin_prod_atomics. (* ==== forall c : coins, {acs : seq (L * L) | c = \big[dot/bob]_(ac <- acs) mix ac.1 ac.2} ] *) (* Define coin products without using bigop *) Fixpoint coin_prod (l:seq coins) : coins := match l with | nil => bob | h :: t => dot h (coin_prod t) end. (* Parameters c d:coins. Eval compute in (coin_prod [::]). Eval compute in (coin_prod [::bob]). Eval compute in (coin_prod [:: c]). Eval compute in (coin_prod [:: c; d]). Eval compute in (coin_prod [::c; d; d]). Eval compute in (coin_prod (c :: [::d; d])). Eval compute in (coin_prod [:: c; c; d; d]). *) Lemma coin_prod_rec : forall a l, coin_prod (a :: l) = dot a (coin_prod l). Proof. move=> a l. case l. by rewrite /coin_prod bob_unitR. by rewrite /coin_prod //. Qed. (* Define coin products using bigop *) Definition coin_prod_bigop (l:seq coins) : coins := \big[dot/bob]_(c <- l) c. Lemma coin_prod_eq : forall l, coin_prod l = coin_prod_bigop l. Proof. elim. by rewrite /coin_prod /coin_prod_bigop big_nil //. move=>a l. rewrite /coin_prod_bigop =>h. by rewrite coin_prod_rec big_cons h. Qed. (* Define a list of mixed coins corresponding to a list of type [L*L]. *) Fixpoint seqL_to_seqC (l : seq (L * L)) : seq coins := match l with | nil => nil | h :: t => (mix h.1 h.2) :: (seqL_to_seqC t) end. Lemma seqL_to_seqC_rec : forall (a:L*L) (l: seq (L*L)), seqL_to_seqC (a :: l) = (mix a.1 a.2) :: (seqL_to_seqC l). Proof. by move=> a. Qed. (* Eval compute in (seqL_to_seqC [::]). Eval compute in (seqL_to_seqC [:: (bot,bot)]). Eval compute in (seqL_to_seqC [:: (bot,bot); (top, bot)]). *) Lemma seqL_to_seqC_eq : forall l : seq (L * L), coin_prod (seqL_to_seqC l) = \big[dot/bob]_(x <- l) mix x.1 x.2. Proof. - elim. by rewrite big_nil. - move=>a l h. by rewrite seqL_to_seqC_rec big_cons coin_prod_rec h. Qed. (* A list of type [seq (L * L)] produces a product of mixed coins, which can be rewritten as a product of interger powers. *) Fixpoint seqL_to_seqUp (l : seq (L * L)) : coins := match l with | nil => bob | h :: t => let c:= if (h.1==bot) then (down h.2) else dot (up (join h.1 h.2)) (down h.2) in dot c (seqL_to_seqUp t) end. Eval compute in (seqL_to_seqUp [::]). Eval compute in (seqL_to_seqUp [:: (bot, top)]). Lemma ref_eq (T: eqType) : forall x:T, (x == x) = true. Proof. move=> x. by apply /eqP. Qed. Goal forall x, seqL_to_seqUp [:: (bot, x)] = down x. Proof. by move=> x /=; rewrite ref_eq bob_unitR. Qed. Lemma double_not : forall P:Prop, ~ ~ P <-> P. Proof. move=> P. split. apply contradiction. by rewrite /not . by rewrite /not . Qed. Lemma negb_false_iff : forall (T:eqType) (x y: T), x != y <-> ((x == y) = false). Proof. split. rewrite /negb. destruct (x==y). by[]. by[]. move=> xny. rewrite /negb. by move: xny ->. Qed. Goal forall x y, x != bot -> seqL_to_seqUp [:: (x, y)] = mix x y. Proof. move=> x y h /=. rewrite mix_up_down; last by[]. move:h. rewrite negb_false_iff => ->. by rewrite bob_unitR //. Qed. Goal forall x y : L, {xns : seq (int*L) | seqL_to_seqUp [:: (x, y)] = \big[dot/bob]_(xn <- xns) nupsz xn.1 xn.2}. Proof. move=> x y. case: (altP (x =P bot)). exists [:: (-1%:Z, y)] =>/=. move: p; move /eqP ->. by rewrite bob_unitR /= big_cons /= big_nil bob_unitR ncoins2_eq /ncoins' . - exists [:: (1%:Z, join x y); (-1%:Z, y)] => /= . move:i; rewrite negb_false_iff =>->. do 2! rewrite big_cons //=. rewrite big_nil up_power1 /ncoins big_cons big_nil //=. by do 3! rewrite bob_unitR. Qed. (* <<<< selective induction *) Fixpoint evenb n := if n is n'.+2 then evenb n' else n == 0%N. Lemma evenb_plus n m : evenb n -> evenb m -> evenb (n + m). Proof. move: (leqnn n) . elim: n {1 3 4}n. (* --- among the 4 n's, do induction on the second one, the same as [elim: n {-2}n]. *) by case=>//. move =>n Hn. case=>//. case=>// n0. by move/ltnW /Hn=>//. Qed. (* Any coin can be written as the product of powers of raising coins. *) Theorem coin_prod_up : forall c : coins, {xns:seq (int*L) | c = \big[dot/bob]_(xn <- xns) nupsz xn.1 xn.2}. Proof. move=>c. move: (coin_prod_atomics c). case=> x. move:c. (* essential step for induction! *) elim: x. move=> c ca; exists nil; rewrite big_nil; by rewrite big_nil in ca. (* the second subgoal *) move=> a l H c. rewrite big_cons. rewrite atomic_up. case: ifPn => _. rewrite -upz_power_m1. set c1:= \big[dot/bob]_(j <- l) mix j.1 j.2. case: (H c1) => // il Hc1 Hc. exists ((-1%Z, a.2) :: il). by rewrite big_cons Hc Hc1. -set c1:= \big[dot/bob]_(j <- l) mix j.1 j.2. case: (H c1) => // il Hc1 Hc. exists ((1%:Z, (join a.1 a.2)) :: (-1%Z, a.2) :: il). do 2! rewrite big_cons. by rewrite Hc Hc1 dotA. Qed. (* return [true] if [seq L] has mutually distinct elements *) Fixpoint neqs (l:seq L) : bool := match l with | nil => true | h :: t => match t with | nil => true | h' :: t' => (h != h') && (neqs t') end end. Eval compute in neqs [::]. Eval compute in neqs [:: bot]. Eval compute in neqs [:: bot;bot]. Lemma ref: forall (T:eqType) (x:T), x == x. Proof. by[]. Qed. Lemma nnref: forall (T:eqType) (x:T), ~(x != x). Proof. move=> T x; by rewrite /not /negb ref. Qed. Lemma nref: forall (T:eqType) (x:T), (x != x) = false. Proof. by move=> T x; rewrite /negb ref. Qed. (* Return true if each element of [l:seq L] is smaller than [x:L]. *) Fixpoint seq_le (l:seq L) (x:L) : bool := match l with | nil => true | h :: t => if (ge x h) then (seq_le t x) else false end. (* this definition is equivalent to [all (ge x) l]. *) Goal all (ge bot) [::]. Proof. by[]. Qed. Eval compute in all (ge bot) [::]. Goal seq_le [::] bot. Proof. by[]. Qed. Eval compute in seq_le [::] bot. Lemma seq_le_all: forall x l, seq_le l x == all (ge x) l. Proof. move=> x l. elim l. by[]. move=>a l1 h. rewrite /seq_le /all. by case: ifP. Qed. (* Return true if each element of [l:seq L] is strictly smaller than [x:L]. *) Fixpoint seq_lt (l:seq L) (x:L) : bool := match l with | nil => true | h :: t => if gt x h then (seq_lt t x) else false end. (* this definition is equivalent to [all (gt x) l]. *) Lemma seq_lt_all: forall x l, seq_lt l x == all (gt x) l. Proof. move=> x l. elim l. by[]. move=>a l1 h. rewrite /seq_lt /all. by case: ifP. Qed. Goal seq_lt [::] bot. Proof. by[]. Qed. Eval compute in seq_lt [::] bot. (* Return true if each natural of a list is strictly smaller than a given natural. *) Fixpoint seqn_lt (l:seq nat) (x:nat) : bool := match l with | nil => true | h :: t => if (h < x) then (seqn_lt t x) else false end. (* this definition is equivalent to [all (fun z => z< x) l]. *) Lemma seqn_lt_all: forall (x:nat) l, seqn_lt l x == all (fun z => z< x) l. Proof. move=> x l. elim l. by[]. move=>a l1 h. rewrite /seqn_lt /all. by case: ifP. Qed. (* pick the first elements from [seq (A*B)] *) Fixpoint seq_1 {A B: Type} (l:seq (A*B)) : seq A:= match l with | nil => nil | h :: t => h.1 :: seq_1 t end. (* the same as [map (fun x => x.1) l] *) (* pick the second elements from [seq (A*B)] *) Fixpoint seq_2 {A B: Type} (l:seq (A*B)) : seq B:= match l with | nil => nil | h :: t => h.2 :: seq_2 t end. (* the same as [map (fun x => x.2) l] *) Lemma seq_1_map {A B: Type}: forall l:seq (A*B), seq_1 l = map (fun x => x.1) l. Proof. elim. by[]. move=> a l h. have t1: seq_1 (a :: l) = a.1::seq_1 l. by[]. have t2: [seq x.1 | x <- a :: l] = a.1::[seq x.1 | x <- l]. by[]. by rewrite t1 t2 h. Qed. Lemma seq_2_map {A B: Type}: forall l:seq (A*B), seq_2 l = map (fun x => x.2) l. Proof. elim. by[]. move=> a l h. have t1: seq_2 (a :: l) = a.2::seq_2 l. by[]. have t2: [seq x.2 | x <- a :: l] = a.2::[seq x.2 | x <- l]. by[]. by rewrite t1 t2 h. Qed. (*New fomalization of prime coins by Shimoyama.*) Lemma coin_decomp : forall x : L, exists y c xns, x != bot -> ge x y /\ c = \big[dot/bob]_(xn <- xns) nupsz xn.1 xn.2 /\ seq_lt (seq_2 xns) x /\ up x == dot c (up y). Proof. move=> x; exists x; exists bob; exists [::(1%:Z, bot)]; move=> H. apply/and_assoc. apply/(and_assoc _ _ (up x == dot bob (up x))). apply:conj. apply:conj. apply:conj. by apply:ge_reflexive. by rewrite big_cons big_nil upz_power1 up_bot_bob dot0r. rewrite /seq_2 /snd /seq_lt /gt; case:ifP. - done. - move/ andP; case; apply: conj. apply/ bot_minimum. apply/ H. by rewrite dot0r. Qed. (*formalization of cain*) (* Define ctext *) Parameter ctext : coins -> L. Fixpoint neq0_seq (l:seq int) : bool := match l with | nil => true | h :: t => match t with | nil => (h !=0) | h' :: t' => (h != h') && (neq0_seq t') end end. Axiom weak_ctext: forall (c:coins) (nx: seq(int*L)), c = \big[dot/bob]_(i <- nx) nupsz i.1 i.2 -> uniq [seq i.2 | i <- nx](*neqs (seq_2 nx)*) -> 0 \notin [seq i.1 | i <- nx] (*neq0_seq (seq_1 nx)*) -> ctext c = \big[join/bot]_(i <- nx) i.2. Lemma addnzE(n m:nat) : (addn n m)%:Z = addz n m. Proof. elim:n => //. Qed. Theorem addncoins n m c: dot (ncoins n c)(ncoins m c) = ncoins (n + m) c. Proof. elim: n => [|n Hn]. by rewrite add0n ncoins0_bob bob_unitL. by rewrite addSn !ncoins2_eq !ncoins1' dotrC dotrA -!ncoins2_eq [dot _ (ncoins n c)]dotrC Hn. Qed. (* move=> [[|n]|n] [[|m]|m] /=; rewrite ?NegzE ?oppzK ?addnS ?addn0 ?subn0 //; *) (* rewrite ?ltnS[m <= n]leqNgt [n <= m]leqNgt; case: ltngtP=> hmn /=; *) (* by rewrite ?hmn ?subnn // ?oppzK ?subSS ?subnS ?prednK // ?subn_gt0. *) Theorem neg_nupsz n x : ncoins n (down x) = nupsz (-n%:Z) x. Proof. by elim:n =>[|n Hn] /=;rewrite /nups ?ncoins0_bob. Qed. Theorem poz_nupsz n x : ncoins n (up x) = nupsz (n%:Z) x. Proof. by elim:n. Qed. Theorem nupszp_eq m x: (0 <= m) -> (nupsz m%:Z x) = nups m x. Proof. by elim:m => [h|m h1 h2] => //. Qed. Theorem nupszn_eq m x: (0 <= m) -> (ndownsz m%:Z x) = ndowns m x. Proof. by elim:m => [h|m h1 h2] => //. Qed. Lemma ncoins_subup n m x: m <= n -> ncoins n (up x) = dot (ncoins (n - m) (up x)) (ncoins m (up x)). Proof. move => h. by rewrite addncoins (subnK h). Qed. Lemma ncoins_subdown n m x: m <= n -> ncoins n (down x) = dot (ncoins (n - m) (down x)) (ncoins m (down x)). Proof. move => h. by rewrite addncoins (subnK h). Qed. Theorem addnupsz n m x: dot (nupsz n x)(nupsz m x) = nupsz (n + m) x. Proof. move: n m. move=> [[|n]|n] [[|m]|m] /= ; rewrite ?NegzE ?addn0 ?subn0 //; rewrite /nups ?ncoins0_bob ?bob_unitL ?bob_unitR; rewrite ?addncoins ?addSn ?addnS //; rewrite !ncoins2_eq !ncoins1' dotrACA ?up_down_unitL; rewrite ?down_up_unitL bob_unitR -!ncoins2_eq. rewrite subzSS. move:(leq_total m n) => /orP [] H. rewrite (subzn H) (@ncoins_subup n m x H) -dotA nupdownK bob_unitR. move/ (leq_sub2r m) in H; rewrite subnn in H. by rewrite (@nupszp_eq (n - m) x H). rewrite (@ncoins_subdown m n x H) dotC -dotA [dot (ncoins n (down x)) _]dotC; rewrite nupdownK bob_unitR updownz_eq oppz_add GRing.addrC GRing.opprK; rewrite (subzn H). move/ (leq_sub2r n) in H; rewrite subnn in H. by rewrite (@nupszn_eq (m - n) x H). rewrite GRing.addrC. rewrite subzSS. move:(leq_total n m) => /orP [] H. rewrite (subzn H). rewrite (@ncoins_subup m n x H) dotC -dotA nupdownK bob_unitR. move/ (leq_sub2r n) in H; rewrite subnn in H. by rewrite (@nupszp_eq (m - n) x H). rewrite (@ncoins_subdown n m x H) -dotA [dot (ncoins m (down x)) _]dotC nupdownK bob_unitR; rewrite updownz_eq oppz_add GRing.addrC GRing.opprK; rewrite (subzn H). move/ (leq_sub2r m) in H; rewrite subnn in H. by rewrite (@nupszn_eq (n - m) x H). Qed. (* 2016/07/20 *) Fixpoint head_in_tail (a:(int*L))(l:seq(int*L)):= match l with | nil => [::a] | h :: t => if a.2 == h.2 then ((a.1 + h.1),a.2)::t else h :: (head_in_tail a t) end. Fixpoint remove0L (xns:seq(int*L)):= match xns with | nil => nil | h::t => if h.1 == 0 then remove0L t else h ::(remove0L t) end. Theorem coin_prod_up_eq_non0 (xns:seq(int*L)): \big[dot/bob]_(xn <- xns) nupsz xn.1 xn.2 = \big[dot/bob]_(xn <- (remove0L xns)) nupsz xn.1 xn.2 . Proof. elim: xns => /=. -by[]. -move => a l H. case: ifP. move/eqP => a0. by rewrite big_cons a0 upz_power0_bob bob_unitL H. move => a0f. by rewrite !big_cons H. Qed. Theorem coin_prod_up_eq_hit (a:(int*L))(xns:seq(int*L)): \big[dot/bob]_(xn <- a :: xns) nupsz xn.1 xn.2 = \big[dot/bob]_(xn <- (head_in_tail a xns)) nupsz xn.1 xn.2 . Proof. elim: xns => /=. -by[]. -move => a0 l H. case: ifP; move/eqP => ha. rewrite !big_cons ha => /=. by rewrite -addnupsz dotA. by rewrite [in RHS] big_cons -H !big_cons dotC dotrAC dotA. Qed. Theorem zero_notin_rem (xns:seq (int*L)): 0 \in [seq i.1 | i <- (remove0L xns)] = false. Proof. elim:xns. by[]. move => a l H /=. case:ifP => a0. exact: H. rewrite in_cons eq_sym a0 Bool.orb_false_l. apply: H. Qed. Theorem hit_map_eq a xns: a.2 \in [seq i.2 | i <- xns] -> [seq i.2 | i <- xns] = [seq i.2 | i <- (head_in_tail a xns)]. Proof. elim: xns => /=. -by[ ]. -move => a0 l h1. rewrite in_cons => /orP [] /eqP h2. case:ifP => /eqP. by rewrite map_cons h2 => /=. by rewrite h2. move/eqP in h2. case:ifP => /eqP h3. by rewrite map_cons h3 => /=. rewrite map_cons. rewrite h2 in h1. by rewrite h1. Qed. Theorem coin_prod_seq_uniq xns: {uxns:seq (int*L) | \big[dot/bob]_(i <- xns) nupsz i.1 i.2 = \big[dot/bob]_(ui <- uxns)nupsz ui.1 ui.2 /\ uniq ([seq i.2 | i <- uxns]) }. Proof. elim: xns => /=. exists nil. by[]. move => a l. case => yms [] h1 h2. case H :(a.2 \notin [seq i.2 | i <- yms]). exists (a :: yms). split. by rewrite !big_cons -h1. apply/andP. exact: conj; last first => //. move:H;rewrite/negb. case:ifP => H _ //. exists (head_in_tail a yms). split. by rewrite -coin_prod_up_eq_hit !big_cons h1. by rewrite -(hit_map_eq H) h2. Qed. Lemma notin_rem_notin (a:(int*L))(l:seq(int*L)): a.2 \notin [seq i.2 | i <- l] -> a.2 \notin [seq i.2 | i <- (remove0L l)]. Proof. elim: l => /=. by[]. move => a' l h1 h2; case: ifP => // a'10. apply: h1. move:h2; rewrite in_cons /negb. case: ifP => // ;rewrite Bool.orb_false_iff. case => h2 h3 _ ; case:ifP => // h4. by rewrite -h3. move: h2. rewrite map_cons in_cons /negb. case: ifP => //. rewrite Bool.orb_false_iff. case => h2 h3 _. case:ifP => //. rewrite in_cons h2 Bool.orb_false_l. move:h1. rewrite /negb. case: ifP => h4; case:ifP => h5 _ // _. by rewrite -h3. Qed. Lemma rem_uniq (xns:seq (int*L)) : uniq ([seq i.2 | i <- xns]) -> uniq ([seq i.2 | i <- (remove0L xns)]). Proof. elim:xns => /=. by[]. move => a l h1. move/andP =>[] h2 h3. case:ifP => a0 /=. exact: h1. apply/andP. split; last first. exact: h1. exact: notin_rem_notin. Qed. Theorem coin_prod_up_strong c: {xns:seq (int*L) | c = \big[dot/bob]_(xn <- xns) nupsz xn.1 xn.2 /\ uniq ([seq i.2 | i <- xns]) /\ 0 \notin [seq i.1 | i <- xns] }. Proof. move: (@coin_prod_up c) => [] xns Hc. move: (@coin_prod_seq_uniq xns) => [] uxns [] uHc1 uHc2. exists (remove0L uxns). split. -by rewrite uHc1 in Hc ;rewrite -coin_prod_up_eq_non0. rewrite (coin_prod_up_eq_non0 uxns) in uHc1. split. by apply:rem_uniq. move : Hc uHc1 uHc2. elim: uxns => /=. by[]. move => a l h1 h2. case:ifP. move/eqP => a0 h3. move/andP => [] h4 h5. apply: h1 => //. move => a0f; rewrite big_cons /= => hc1; rewrite in_cons /negb. by case :ifP ;rewrite eq_sym a0f Bool.orb_false_l zero_notin_rem. Qed. (* 2016/07/13 *) Axiom ctext1 : forall x, ctext (up x) = x. Axiom ctext2 : forall x y, x != bot /\ ge y x -> ctext (mix x y) = bot. Axiom ctext3 : forall x y, x != bot /\ ~~ ge y x -> ctext (mix x y) = join x y. Axiom ctext4 : forall x, ctext (down x) = x. Lemma ctext1_1 x: {xns| up x = \big[dot/bob]_(xn <- xns) nupsz xn.1 xn.2 /\ uniq ([seq i.2 | i <- xns]) /\ 0 \notin ([seq i.1 | i <- xns]) /\ \big[join/bot]_(i <- xns) i.2 = x}. Proof. exists [::(1%:Z,x)] => //=. split. by rewrite big_cons big_nil bob_unitR -up_power1 => //=. rewrite big_cons big_nil join_commutative => //=. do 2 split => //. exact:join_bot_unitL. Qed. Lemma ctext1' x: ctext (up x) = x. Proof. move:(@ctext1_1 x). case => x0 [] h1 [] h2 [] h3 h4. move: (@weak_ctext (up x) x0)=> h5. rewrite h4 in h5. by rewrite (h5 h1 h2 h3). Qed. Lemma dot_inv_prod_up c nx: c = \big[dot/bob]_(i <- nx) nupsz i.1 i.2 -> dot_inv c = \big[dot/bob]_(i <- nx) nupsz (- i.1) i.2. Proof. Admitted. Theorem Th3_1 c: ctext c = ctext (dot_inv c). Proof. Admitted. Theorem Th3_2 c1 c2: ge (join (ctext c1) (ctext c2)) (ctext (dot c1 c2)). Proof. Admitted. Lemma not_bot_gt_bot x : x != bot = gt x bot. Proof. rewrite /gt; apply/eqP. case: ifP. case /andP => H1 H2; exact/eqP. rewrite (@bot_minimum x) /= ;by move/negbFE /eqP. Qed. Definition cintegrable x c := ge (ctext c) x. Parameter mcoin : L -> coins. Axiom mcoin_axiom : forall y, ge y (ctext (mcoin y)). Axiom mcoin_axiom':forall x c, ge x (ctext c)-> c = mcoin x. Lemma gt_joinL(*used in lemma5's proof*) a b : gt (join a b) b -> gt a bot. Proof. case: (altP (b =P bot)) => [-> | nbbot]. move: (@join_bot_unitL a)=> H. by rewrite join_commutative H. rewrite /gt. move /andP => [] gjabb njabb. apply /andP; apply conj. exact:bot_minimum. apply/negP. move=> /eqP abot. move: njabb; move /negP. case. by rewrite abot join_bot_unitL. Qed. Lemma ge_meet_def(*used in lemma5's proof*) a b: ge a b = (meet a b == b). Proof. rewrite /ge; apply/eqP;case: ifPn; move/eqP => H. by rewrite -{2}(@join_absorption a b) meet_distributive meet_idempotent H. rewrite /not. move => H1; move:H. rewrite /not => /eqP. by rewrite -H1 meet_commutative join_commutative join_absorption nref. Qed. Lemma meet_not_bot (*lemma5*)a b x: ge (join a b) x -> gt x b -> meet a x != bot. Proof. rewrite ge_meet_def meet_commutative meet_distributive;move /eqP => H1. rewrite /gt. move/andP =>[]; rewrite ge_meet_def;move/eqP => H2 H3. rewrite not_bot_gt_bot. apply: (@gt_joinL (meet a x) b). rewrite -{1}H2 [meet _ x] meet_commutative H1. rewrite /gt. apply/andP. split. by rewrite ge_meet_def;apply /eqP. by[]. Qed. Lemma also_integ x y c cy : cintegrable x c /\ meet y x = bot /\ ge y (ctext cy) -> cintegrable x (dot cy c). Proof. Admitted. Parameter coin_margin : L -> coins -> coins. Notation "c /d x" := (coin_margin x c) (at level 50). Axiom margin0 : forall x c, ctext (c /d x) = meet (ctext c) (com x). Axiom margin1 : forall x y, ge y x -> (up y) /d x = up (meet y (com x)). Axiom margin2 : forall x1 x2 c1 c2, meet x1 x2 = bot /\ meet x1 (ctext c2) = bot /\ meet x2 (ctext c1) = bot /\ ge (ctext c1) x1 /\ ge (ctext c2) x2 /\ cintegrable (join x1 x2) (dot c1 c2) -> (dot c1 c2) /d (join x1 x2) = dot (c1 /d x1) (c2 /d x2). Axiom margin3 : forall c, c /d bot = c. (*we define cain by this cainoid satisfying these properties*) (*Th4*) Theorem const_margin' x y c cx : cintegrable x cx /\ meet x y = bot /\ ge y (ctext c) -> dot c cx /d x = dot c (cx /d x). Proof. rewrite /cintegrable; move=> []=> H1 []=> H2 H3. rewrite -[in RHS](@margin3 c). rewrite -[in RHS]margin2; last first. apply :conj; first by rewrite meet_bot_unitL. apply :conj; first by rewrite meet_bot_unitL. apply :conj; last first. apply :conj; first by rewrite /ge join_bot_unitR. apply :conj; first by[]. apply /also_integ; first by[]. apply :conj; first by rewrite /cintegrable join_bot_unitL H1. apply :conj; first by rewrite join_bot_unitL meet_commutative. by[]. rewrite ge_meet_def in H3. move :H3; move /eqP => H3. by rewrite -H3 meet_associative H2 meet_bot_unitL. by rewrite join_bot_unitL. Qed. Theorem const_margin x c cx : cintegrable x cx /\ meet x (ctext c) = bot -> dot c cx /d x = dot c (cx /d x). Proof. rewrite /cintegrable; move=> []=> H1=> H2. rewrite -[in LHS](@join_bot_unitL x) margin2. rewrite margin3; first by[]. apply :conj; first by rewrite meet_bot_unitL. apply :conj; first by rewrite meet_bot_unitL. apply :conj; first by[]. apply :conj; first by rewrite /ge join_bot_unitR. apply :conj; first by[]. rewrite (@also_integ (join bot x) (ctext c) cx c); first by[]. apply :conj; first by rewrite /cintegrable join_bot_unitL H1. apply :conj; first by rewrite join_bot_unitL meet_commutative. by rewrite /ge join_idempotent. Qed. Lemma com_join_P x y : complement_P (join x y) (meet (com x) (com y)). Proof. rewrite/ complement_P; apply: conj. -rewrite meet_commutative meet_distributive [_ (com y)]meet_commutative -meet_associative [_ x]meet_commutative com_bot meet_bot_unitR [_ (com x)]meet_commutative -meet_associative [_ y]meet_commutative com_bot meet_bot_unitR; apply: join_bot_unitL. -by rewrite join_distributive {1}[_ y]join_commutative -join_associative com_top -join_associative com_top 2!join_top_unitR meet_idempotent. Qed. Lemma com_meet_P x y : complement_P (meet x y) (join (com x) (com y)). Proof. rewrite/ complement_P; apply: conj. -by rewrite meet_distributive {1}[_ y]meet_commutative -!meet_associative !com_bot !meet_bot_unitR join_bot. -by rewrite join_commutative join_distributive join_commutative !join_associative com_top -join_associative [_ _ y]join_commutative com_top join_top_unitL join_top_unitR meet_idempotent. Qed. Lemma com_join x y : com (join x y) = meet (com x) (com y). Proof. apply: (@complement_unique (join x y)). apply: conj. -apply: com_P. -apply: com_join_P. Qed. Lemma com_meet x y : com (meet x y) = join (com x) (com y). Proof. apply: (@complement_unique (meet x y)). apply: conj. -apply: com_P. -apply: com_meet_P. Qed. Lemma double_com x : com (com x) = x. Proof. apply: (@complement_unique (com x)). apply: conj. -apply: com_P. -rewrite /complement_P meet_commutative join_commutative; apply/ com_P. Qed. Lemma Th5_1 x y z : x != bot /\ mix x y = mix x z -> up (join x y) = dot (mix x z) (up y). Proof. case=> H1 H2. rewrite -H2 mix_up_down. by rewrite -dotA down_up_unitL dotr0. by[]. Qed. Lemma Th5_2 x y z : x != bot /\ mix x y = mix x z -> up (meet (join x y) (com (meet (meet y (com x)) (com z)))) = dot (mix x z) (up (meet y (com (meet (meet y (com x)) (com z))))). Proof. case=> H1 H2; rewrite -margin1. rewrite (@Th5_1 x y z). rewrite const_margin. rewrite margin1. by[]. rewrite/ ge. by rewrite -meet_associative meet_absorption. apply: conj. rewrite/ cintegrable ctext1. rewrite /ge; by rewrite -meet_associative meet_absorption. move: (@orbN (ge z x)). move/ orP. case. move=> H3. rewrite ctext2. by rewrite meet_bot_unitR. by split. move=> H3. rewrite ctext3. by rewrite meet_distributive meet_commutative meet_associative [_ y _]meet_commutative meet_associative com_bot !meet_bot_unitL -meet_associative [_ _ z]meet_commutative com_bot meet_bot_unitR join_bot. by split. by split. by rewrite/ ge 2!join_distributive -join_associative join_idempotent !join_absorption. Qed. Lemma Th5_3 x y z : meet (join x y) (com (meet (meet y (com x)) (com z))) = join x (meet y z). Proof. rewrite !com_meet !double_com !meet_distributive ![_ (join x y) _]meet_commutative 2!meet_distributive [_ _ y]meet_commutative com_bot. by rewrite [_ bot]join_commutative join_bot_unitL meet_idempotent meet_absorption [_ x]join_commutative [_ _ x]meet_commutative meet_absorption join_distributive join_associative join_idempotent meet_commutative -join_distributive. Qed. Lemma Th5_4 x y z : x != bot /\ mix x y = mix x z -> up (meet y (com (meet (meet y (com x)) (com z)))) = up (meet z (com (meet (meet z (com x)) (com y)))). Proof. move=> H1; move: (H1); move /Th5_2; rewrite Th5_3=> H2. have H3: dot (mix x z) (up (meet y (com (meet (meet y (com x)) (com z))))) = dot (mix x y) (up (meet z (com (meet (meet z (com x)) (com y))))). -by rewrite -H2 meet_commutative -Th5_3; apply: Th5_2; apply: conj; case: H1. case: H1=> H1' H1''; move: H3; rewrite H1'' mix_up_down. by rewrite -dotA [_ (down z) _]dotC dotA; move/ div_down_right; rewrite -[RHS]dotA [_ _ (up z)]dotC dotA -[_ _ (up z)]dotA down_up_unitL bob_unitR [RHS]dotC; move/ div_up_down; rewrite dotC dotA down_up_unitL bob_unitL. by[]. Qed. Lemma Th5_5 x y z : meet (com (meet (meet y (com x)) (com z))) (com (meet (meet z (com x)) (com y))) = join (join x (meet y z)) (meet (com z) (com y)). Proof. rewrite !com_meet !double_com; rewrite [_ _ y]join_commutative [_ (com z) _]join_commutative join_associative meet_distributive [_ _ (com z)]meet_commutative [_ (com z) _]meet_distributive [_ (com z) z]meet_commutative com_bot [_ _ bot]join_commutative join_bot_unitL meet_commutative [_ y x]join_commutative. have H: com (meet (meet y (com x)) (com z)) = join (join (com y) x) z. -by rewrite !com_meet !double_com. by rewrite -H Th5_3 meet_distributive join_associative -[_ (join x (meet y z)) (meet (com z) (com y))]join_associative join_commutative join_associative [_ _ x]join_commutative meet_commutative meet_absorption join_associative. Qed. Theorem Th5 x y z : mix x y = mix x z -> mix x y = mix x (meet y z). Proof. move=> H1. move: (excluded_middle_axiom (x = bot)). case. -by move=> h1; move: H1; rewrite h1; move/ down_injective=> h2; rewrite -h2 meet_idempotent. -move/ eqP=> H2. have H3: (meet y (com (meet (meet y (com x)) (com z)))) = (meet z (com (meet (meet z (com x)) (com y)))). +by apply /up_injective /Th5_4. have H4: meet y (com (meet (meet y (com x)) (com z))) = meet y z. +by rewrite -[_ y _]meet_idempotent {2}H3 meet_associative -[meet (meet y (com (meet (meet y (com x)) (com z)))) z]meet_associative [_ _ z]meet_commutative meet_associative -meet_associative Th5_5 meet_distributive [_ x _]join_commutative join_absorption meet_absorption. rewrite [in RHS]mix_up_down; first 1 [apply/ eqP|]. by rewrite eq_sym; apply/ eqP; rewrite div_up_down H1 -[in LHS]Th5_3 -H4 Th5_2. by[]. Qed. Lemma com_bot_top_P : complement_P bot top. Proof. rewrite/ complement_P; split. -apply /meet_bot_unitL. -apply /join_bot_unitL. Qed. Lemma com_bot_top : com bot = top. Proof. apply /complement_unique. exact: bot. split. -apply /com_P. -apply /com_bot_top_P. Qed. Lemma com_top_bot : com top = bot. Proof. apply /complement_unique. exact: top. split. -apply /com_P. -move: com_bot_top_P => H; rewrite/ complement_P meet_commutative join_commutative; apply /H. Qed. Lemma meet_eq_ge x y : meet x y = bot <-> ge (com x) y. Proof. split. -move=> H; rewrite/ ge; apply/ eqP; move: (com_meet x y); rewrite H com_bot_top; move=> H1; by rewrite -[in RHS](join_bot_unitL (com x)) -com_top_bot H1 com_join !double_com [in RHS]join_commutative join_distributive [_ _ x]join_commutative com_top meet_top_unitL. -by rewrite/ ge; move /eqP => H1; rewrite -(double_com x) -(double_com y) -com_join -H1 -join_associative com_top join_top_unitR com_top_bot. Qed. Theorem Th6 x y z : gt x z /\ meet y z = bot -> mix x y /d z = mix (meet x (com z)) y. Proof. case; rewrite /gt /ge; move /andP =>[] /eqP => H1 H2; move: (excluded_middle_axiom (x = bot)); case. -by move=> H3; rewrite H3; rewrite H3 join_bot_unitL in H1; rewrite H1 margin3 meet_bot_unitL. -move/ eqP=> H3 H4; rewrite mix_up_down ; last by[]; rewrite dotC const_margin; last first. -rewrite /cintegrable /ge ctext1 ctext4. apply: conj. -by rewrite [_ _ y]join_commutative -join_associative H1. -by rewrite meet_commutative. rewrite margin1; last first. -by rewrite /ge [_ _ y]join_commutative -join_associative H1. rewrite meet_commutative meet_distributive. rewrite meet_commutative in H4. move: H4; move/ meet_eq_ge; rewrite ge_meet_def; move/ eqP=> H4; rewrite H4. rewrite dotC -mix_up_down ; first by rewrite meet_commutative. apply: meet_not_bot. exact z. by rewrite /ge [_ _ z]join_commutative com_top join_top_unitL. by rewrite /gt; apply /andP; split; first by rewrite /ge; apply /eqP. Qed. Theorem Th7_1 x : up x /d x = bob. Proof. rewrite margin1; first by rewrite com_bot up_bot_bob. by rewrite /ge join_idempotent. Qed. Theorem Th7_2 x y : x != bot -> mix x y /d meet x (com y) = bob. Proof. move=> H; rewrite mix_up_down; last by[]. rewrite -(meet_top_unitR (join x y)) -(com_top y) join_commutative -join_distributive dotC const_margin; first rewrite margin1; first by rewrite com_meet double_com join_distributive com_top meet_top_unitR [_ _ y]join_commutative -join_distributive com_bot join_commutative join_bot_unitL dotC up_down_unitL. by rewrite /ge -join_associative join_idempotent. apply: conj. by rewrite /cintegrable ctext1 /ge -join_associative join_idempotent. by rewrite ctext4 -meet_associative [_ _ y]meet_commutative com_bot meet_bot_unitR. Qed. Corollary Co1_1 c y : meet (ctext c) y = bot -> dot c (up y) /d y = c. Proof. move=> H; rewrite const_margin; first rewrite margin1; first by rewrite com_bot up_bot_bob bob_unitR. apply: ge_reflexive. apply: conj; first rewrite/ cintegrable ctext1; first apply: ge_reflexive. by rewrite meet_commutative. Qed. Corollary Co1_2 y z c : meet (ctext c) z = bot /\ meet y z = bot -> dot c (up (join y z)) /d z = dot c (up y). Proof. case=> H1 H2; rewrite const_margin; first rewrite margin1; first rewrite meet_commutative meet_distributive [_ _ z]meet_commutative com_bot join_bot_unitR; move: H2; rewrite meet_commutative =>/meet_eq_ge; rewrite ge_meet_def=>/ eqP=> H2; first by rewrite H2. by rewrite /ge -join_associative join_idempotent. apply: conj; first by rewrite /cintegrable ctext1 /ge -join_associative join_idempotent. by rewrite meet_commutative H1. Qed. Corollary Co1_3 x y z c : meet x z = bot /\ meet y z = bot /\ meet (ctext c) z = bot -> dot c (up (join x (join y z))) /d z = dot c (up (join x y)). Proof. case=> H1 [] H2 H3; rewrite const_margin. rewrite margin1. rewrite join_associative meet_commutative meet_distributive [_ _ z]meet_commutative com_bot join_bot_unitR meet_commutative. have H: meet z (join x y) = bot. -by rewrite meet_distributive meet_commutative [_ _ y]meet_commutative H1 H2 join_bot. by move: H; move /meet_eq_ge; rewrite ge_meet_def; move /eqP; rewrite meet_commutative=> H4; rewrite H4. by rewrite join_associative /ge -join_associative join_idempotent. rewrite meet_commutative in H3; apply: conj; last by[]. by rewrite /cintegrable ctext1 join_associative /ge -join_associative join_idempotent. Qed. Corollary Co1_4 x y z : x != bot /\ meet x y = bot /\ meet y z = bot -> mix (join x y) z /d y = mix x z. Proof. case => H1 [] H2 H3; rewrite mix_up_down; first rewrite dotC const_margin. rewrite margin1. rewrite -join_associative [_ _ z]join_commutative join_associative meet_commutative meet_distributive [_ _ y]meet_commutative com_bot join_bot_unitR meet_commutative. have H: meet y (join x z) = bot. -by rewrite meet_distributive meet_commutative H2 H3 join_bot. by move: H; move /meet_eq_ge; rewrite ge_meet_def; move /eqP; rewrite meet_commutative=> H4; rewrite H4 dotC -mix_up_down. by rewrite -join_associative [_ y _]join_commutative join_associative /ge -join_associative join_idempotent. apply: conj. -by rewrite /cintegrable ctext1 -join_associative [_ y _]join_commutative join_associative /ge -join_associative join_idempotent. -by rewrite ctext4. have H: (x != bot) || (y != bot) -> join x y != bot. -rewrite -negb_and; apply: contra; apply/join_eq_bot. by apply /H /orP /or_introl. Qed. Lemma meet_ge x y:ge x (meet x y). Proof. rewrite/ge. rewrite join_distributive. rewrite join_idempotent. apply/eqP. by apply:join_absorption. Qed. Lemma meet_ge' x y:ge x y <->meet x y = y. Proof. rewrite/ge. split. move=>H. move/eqP in H. rewrite meet_commutative -H meet_distributive. rewrite meet_idempotent join_commutative. apply/eqP. apply:meet_ge. move=>H. apply/eqP. by rewrite -H meet_absorption. Qed. Lemma ge_w_L x y z:ge x (join y z)-> ge x y. Proof. move=>H. apply:(@ge_transitive (join y z) x y)=>//. apply meet_ge'. by rewrite meet_commutative join_absorption. Qed. Lemma meet_ge_meet x y z:ge x y -> ge (meet x z) (meet y z). Proof. move=>H. rewrite meet_ge'=>//. move/meet_ge' in H. by rewrite (meet_commutative y _) meet_associative -(meet_associative x z z) meet_idempotent (meet_commutative x z) -meet_associative H. Qed. Theorem N_law1 x y z : x != bot /\ ge (com z) (ctext (mix x (join y z))) /\ meet x (com z)!=bot -> mix x (join y z) = mix (meet x (com z)) (meet y (com z)). Proof. case => H1 [] H2 H3. -move:(excluded_middle_axiom (ge (join y z) x));case=>Hyz. move:(le_mix_bob_eq)(Hyz)=>H Hyz'. rewrite/le in H. move/H in Hyz. rewrite Hyz=>//. move/(@meet_ge_meet _ _ (com z)) in Hyz'. rewrite meet_commutative meet_distributive (meet_commutative (com z) z) com_bot meet_commutative join_bot_unitR in Hyz'. move/H in Hyz'. by rewrite Hyz'. -rewrite ctext3 in H2=>//. move/negP in Hyz. rewrite [in RHS]mix_up_down=>//. move:(H2)=>H2';move:(H2)=>h2. move/ge_w_L in H2. move/meet_eq_ge in H2. rewrite join_associative (join_commutative x _) -join_associative in h2; move/ge_w_L in h2. move/meet_eq_ge in h2. rewrite meet_commutative {1}[(meet y (com z))]meet_commutative -meet_distributive meet_commutative -(join_bot_unitR (meet (join x y) (com z))) -(com_bot z) meet_commutative [_ z _]meet_commutative -meet_distributive meet_commutative -margin1. --have H: up (join (join x y) z) = dot (mix x (join y z)) (up (join y z)). -by rewrite mix_up_down; first rewrite -dotA down_up_unitL bob_unitR join_associative. rewrite H. --have h: ge (join y z) z. by rewrite join_commutative join_ge. move/margin1 in h. rewrite const_margin. rewrite meet_commutative meet_distributive (meet_commutative _ y) (meet_commutative _ z) com_bot join_bot_unitR in h. by rewrite h -dotrA up_down_unitL dotr0. apply:conj=>//. by rewrite /cintegrable ctext1 /ge -join_associative join_idempotent. rewrite ctext3=>//. move/meet_ge' in H2'. by rewrite -H2' meet_associative com_bot meet_bot_unitL. by rewrite join_commutative join_ge. by move/negP in Hyz. Qed. Lemma ctext_eq_ge x c : meet (ctext c) (com x) = bot <-> ge x (ctext c). Proof. split. by move=> H; apply /eqP; rewrite /ge -[in RHS](@join_bot_unitR x) -H join_distributive com_top meet_top_unitR. by rewrite ge_meet_def; move /eqP =>H; rewrite -H [_ x _]meet_commutative -meet_associative com_bot meet_bot_unitR. Qed. Lemma N_law2_1 x y z cx cy : meet (ctext cx) x = bot /\ meet (ctext cy) y = bot /\ up (join (join x y) z) = dot cy cx -> up (meet (join y z) (com x)) = dot cx (cy /d x). Proof. case=> H1 [] H2 H3. rewrite -(@join_bot_unitR (meet (join y z) (com x))) -(@com_bot x) meet_commutative [_ x _]meet_commutative -meet_distributive meet_commutative join_commutative join_associative -margin1; last first; first by rewrite /ge -join_associative join_commutative -join_associative join_commutative join_associative join_idempotent. rewrite H3 dotC const_margin; first by[]. apply: conj; last first; first by rewrite meet_commutative. rewrite /cintegrable /ge; move: (@Th3_2 cy cx); rewrite -H3 ctext1=> H4. move: (@join_ge x y) (@join_ge (join x y) z)=> H5 H6. have H: ge (join (join x y) z) x. -apply/ (@ge_transitive (join x y)); by[]. have H': ge (join (ctext cy) (ctext cx)) x. -apply/ (@ge_transitive (join (join x y) z)); by[]. move: H1; rewrite -{1}(double_com x) ctext_eq_ge ge_meet_def; move /eqP=> H1. rewrite ge_meet_def in H'; move /eqP in H'. by rewrite -H' -H1 meet_commutative meet_distributive meet_associative com_bot meet_bot_unitL join_bot_unitR meet_commutative meet_absorption. Qed. Lemma dot_eq c1 c2 c3 : c1 = c2 <-> dot c1 c3 = dot c2 c3. Proof. split. by move=> H; rewrite H. by move=> H; rewrite -(dotr0 c1) -(dotr0 c2) -(dotNr c3) [_ _ c3]dotC !dotA H. Qed. Lemma N_law2_2 x y z cx cy : ge (com x) y /\ meet (ctext cx) x = bot /\ meet (ctext cy) y = bot /\ up (join (join x y) z) = dot cy cx -> up (meet z (meet (com x) (com y))) = dot (cx /d y) (cy /d x). Proof. case=> H1 [] H2 [] H3 H4. rewrite (@dot_eq _ _ (up (meet (join x z) (com y)))) -(@join_bot_unitL (meet z (meet (com x) (com y)))) -(@meet_bot_unitL (com x)) -(com_bot y) -meet_associative [_ (com y) (com x)]meet_commutative meet_commutative [_ z _]meet_commutative -meet_distributive meet_commutative meet_associative -margin1; first rewrite dotC -[in LHS]const_margin; first rewrite (@N_law2_1 x y z cx cy); first rewrite [in LHS](@N_law2_1 y x z cy cx); first rewrite dotA [_ _ cx]dotC dotA [_ cx _]dotC -H4 -dotA dotC const_margin; first rewrite margin1; first by rewrite [_ _ y]join_commutative -join_associative meet_commutative meet_distributive [_ _ y]meet_commutative com_bot join_bot_unitL meet_commutative. by rewrite /ge join_commutative join_associative [_ x _]join_commutative join_associative join_idempotent. split. by rewrite /cintegrable /ge ctext1 join_commutative join_associative [_ x _]join_commutative join_associative join_idempotent; first last. move: (@Th3_2 (cx /d y) (cy /d x)); rewrite ge_meet_def; move /eqP=> H5. by rewrite -H5 meet_associative meet_distributive !margin0 [_ _ (com y)]meet_commutative meet_associative com_bot meet_bot_unitL meet_associative [_ y _]meet_commutative H3 meet_bot_unitL join_idempotent meet_bot_unitL. by rewrite [_ y _]join_commutative dotC. by[]. split; first rewrite /cintegrable /ge join_commutative ctext1 join_distributive join_associative join_idempotent; rewrite /ge in H1; move: H1; move /eqP=> H1. by rewrite [_ _ (com x)]join_commutative H1. by rewrite ctext1 [_ _ (com y)]meet_commutative meet_associative com_bot meet_bot_unitL. by rewrite /ge in H1; move: H1; move /eqP=> H1; rewrite /ge join_commutative join_distributive join_associative join_idempotent [_ _ (com x)]join_commutative H1. Qed. Theorem N_law2 x y z cx cy : ge (com x) y /\ meet (ctext cx) x = bot /\ meet (ctext cy) y = bot /\ up (join (join x y) z) = dot cy cx -> up (join (join x y) z) = dot (dot (up (meet (join x z) (com y))) (up (meet (join y z) (com x)))) (down (meet (meet z (com x)) (com y))). Proof. case=> H1 [] H2 [] H3 H4. rewrite (@N_law2_1 y x z cy cx); last by rewrite [_ y _]join_commutative dotC. rewrite (@N_law2_1 x y z cx cy); last by[]. rewrite [_ cy _]dotC dotA -[_ _ cx]dotA [_ (cx /d y) _]dotC -2!dotA -H4 [_ (cx /d y) _]dotA -meet_associative -(@N_law2_2 x y z cx cy); last by[]. by rewrite (@up_down_unitL (meet z (meet (com x) (com y)))) dotr0. Qed. Section conditional_independence. (*def 10*) Definition co_ind x y z:= (mix x (join y z))=(mix x z). Definition ind x y:= (co_ind x y bot). (*Notation "x._y|z":=(@co_ind _ _ _). Notation "x._y":=(@ind _ _).*) Lemma join_bot_bot x y: x!=bot-> y!=bot -> (join x y)!=bot. Proof. move=>XH YH. apply/eqP. case. move/eqP=>H0. move:(@join_eq_bot x y H0). move/andP. case. move=>X. move/eqP. by apply/eqP. Qed. Theorem co_ind_eq_1 x y z: x!=bot -> y!=bot -> (co_ind x y z <-> (mix (join x y) z)=dot (mix x z) (mix y z)). Proof. move=> XH YH . split. -rewrite/ co_ind=>H. rewrite -H. rewrite[in RHS] mix_up_down=>//. rewrite[in RHS] mix_up_down=>//. rewrite -dotrAC dotrA -dotrA dotrACA dotrA dotr_perm down_up_unitL dot0r dotC join_associative mix_up_down=>//. by apply join_bot_bot=>//. -rewrite/co_ind mix_up_down. rewrite div_up_down. move=>H. rewrite mix_up_down=>//. rewrite join_associative H. rewrite [mix y _]mix_up_down=>//. rewrite dotrA div_up_down dotr_perm up_down_unitL dot0r dotrC=>//. by apply join_bot_bot=>//. Qed. Theorem co_ind_eq_2 x y z: x!=bot -> y!=bot -> (co_ind x y z <-> (up (join (join x y) z)=dot (up (join y z)) (mix x z))). Proof. move=>XH YH. rewrite/co_ind. rewrite mix_up_down=>//. by rewrite div_up_down -join_associative dotrC. Qed. Theorem ind_eq x y: x!=bot -> y!=bot -> (ind x y <-> up (join x y) = dot (up x) (up y)). Proof. move=>XH YH. rewrite/ind/co_ind join_commutative. move:(join_bot_unitL y)=>->. rewrite mix_up_down=>//. by rewrite div_up_down. Qed. (*co_ind is symmetry*) Theorem co_sym x y z:x!=bot->y!=bot-> (co_ind x y z <-> co_ind y x z). Proof. move=>X Y. by split;move=>H; apply co_ind_eq_1 in H=>//; rewrite co_ind_eq_1=>//; rewrite join_commutative dotrC=>//. Qed. (*Prop6*) Proposition eq_co_ge x y: x!=bot -> y!=bot ->(co_ind x x y <-> ge y x). Proof. move=>X Y. rewrite (@co_ind_eq_1 x x y)=>//. rewrite join_idempotent. rewrite mix_up_down=>//. rewrite div_up_down. rewrite dotrA. rewrite dotr_perm. rewrite up_down_unitL dot0r. rewrite dotrC -div_up_down=>//. rewrite up_down_unitL. rewrite dotrC -div_up_down bob_unitL. split. move=>H. apply down_injective in H. rewrite/ge. rewrite join_commutative. by apply/eqP. rewrite/ge=>H. rewrite join_commutative. move/eqP in H. by rewrite H. Qed. Proposition ge_co_1 x y z : ge z y -> co_ind x y z. Proof. rewrite/ge/co_ind. move=>H. move/eqP in H. rewrite join_commutative H. by[]. Qed. Proposition ge_co_2 x y z : x!=bot -> ge z x -> co_ind x y z. Proof. rewrite/ge/co_ind. move=>X H. rewrite mix_up_down=>//. rewrite join_commutative. rewrite -join_associative. move/eqP in H. rewrite H up_down_unitL. rewrite mix_up_down=>//. by rewrite join_commutative H up_down_unitL. Qed. Lemma co_mc0 x y b:meet x y = bot->meet y b!=bot-> x = meet x (join (com y) b). Proof. move=>A H. rewrite meet_commutative in A;apply meet_eq_ge in A=>//. apply meet_ge' in A;rewrite meet_commutative in A. by rewrite meet_distributive A meet_absorption. Qed. Lemma co_mc00 x y b:meet x y = bot->meet y b!=bot-> (com x)=join (com x) (meet y (com b)). Proof. move=>A B. rewrite [in LHS](@co_mc0 x y b)=>//. by rewrite com_meet com_join double_com. Qed. Lemma gt_0 x y z:gt x y -> gt x (meet y z). Proof. rewrite/gt. move/andP=>[h1 h2]. move:(h1)=>h. apply/andP;split. move/eqP in h1. apply/eqP. by rewrite join_distributive h1 join_absorption. apply/negP; move=> /eqP h3. move/eqP in h1;apply meet_ge' in h. rewrite h3 join_commutative join_distributive join_idempotent -h3 join_absorption in h1. move:h2;move/negP. case. by rewrite h1. Qed. Lemma co_mc1 x y z b:x!=bot->y!=bot->meet x y = bot->meet y b!=bot-> (mix (join x y) z) /d (meet y (meet (com b) (com z)))=mix (join x (meet y b)) z. Proof. move=>X Y A H. rewrite Th6. rewrite com_meet -com_join double_com (join_associative (com y) _ _). rewrite meet_distributive. rewrite meet_commutative meet_distributive meet_commutative -co_mc0=>//. rewrite meet_commutative meet_distributive com_bot join_bot_unitL. apply/eqP;rewrite eq_sym;apply/eqP. apply:(@lemma1_3 (join x (meet y b)) z (meet (join x y) z)). apply:join_bot_bot=>//. -apply:(@ge_transitive z (join (join x (meet y b)) z) (meet (join x y) z)). rewrite join_commutative join_ge=>//. rewrite meet_commutative meet_ge=>//. split. -rewrite meet_associative. apply:gt_0. rewrite/gt;apply/andP;split. apply:(@ge_transitive y (join x y) (meet y (com b))). rewrite join_commutative join_ge=>//. apply meet_ge. apply/negP. move=>/eqP h. move:(A)=>a. apply meet_eq_ge in a. apply meet_ge' in a. move:(A)=>c. apply meet_eq_ge in c;move/eqP in c. move:H;move/negP. case. apply/eqP. rewrite meet_commutative. apply (@meet_eq_ge b y). apply meet_ge'. rewrite meet_commutative -h. rewrite-[in RHS](@join_bot_unitL y). rewrite -(@com_bot x) (join_commutative (meet _ _) _) join_distributive. rewrite meet_commutative (join_commutative y x) h (join_commutative y _) c. by rewrite meet_associative a. --rewrite meet_commutative -meet_associative -(meet_associative (com b) _ _) (meet_commutative (com _) z) com_bot. by rewrite meet_commutative (meet_commutative _ bot) meet_bot_unitL meet_bot_unitL. Qed. Lemma meet_join x y:(join x y = x)<->(meet x y = y). Proof. split=>H. apply meet_ge'. by apply/eqP. apply meet_ge' in H. by move/eqP in H. Qed. Lemma ge_mix_bob_eq x y:x!=bot-> (ge y x <-> (mix x y = bob)). Proof. move=>X. move:(@le_mix_bob_eq x y)=>H. rewrite/le in H. by apply H. Qed. Lemma co_mc2 x y z b:x!=bot->y!=bot->meet x y = bot->meet y b!=bot->~~(ge z y)->~~ (ge z x)-> (dot (mix x z) (mix y z))/d (meet y (meet (com b) (com z)))= dot (mix x z) (mix (meet y b) z). Proof. move=>X Y A B C D. rewrite const_margin. rewrite Th6. rewrite com_meet -com_join double_com meet_distributive. rewrite com_bot join_bot_unitL meet_distributive. rewrite -(@lemma1_3 (meet y b) z (meet y z))=>//. -apply:(@ge_transitive z (join (meet y b) z) (meet y z)). by rewrite join_commutative join_ge. by rewrite meet_commutative meet_ge. split. -rewrite meet_associative. apply:gt_0=>//. rewrite/gt;apply/andP;split. by rewrite meet_ge. apply/negP; move=> /eqP H. move:B;move/negP. case. by rewrite H -meet_associative (meet_commutative _ b) com_bot meet_commutative meet_bot_unitL. --rewrite meet_commutative -meet_associative -(meet_associative (com b) _ _) (meet_commutative (com _) z) com_bot. by rewrite meet_commutative (meet_commutative _ bot) meet_bot_unitL meet_bot_unitL. ---split. +rewrite/cintegrable. rewrite ctext3=>//. apply/eqP. rewrite join_distributive (join_commutative _ y) join_associative join_idempotent. by rewrite join_distributive -(join_associative y z (com z)) com_top join_top_unitR meet_top_unitR join_absorption. rewrite ctext3=>//. rewrite meet_distributive (meet_commutative _ x) meet_associative A meet_bot_unitL -meet_associative -meet_associative (meet_commutative _ z) com_bot meet_associative meet_bot_unitR join_idempotent=>//. Qed. Lemma margin_eq x y z:(x = y)-> (x /d z) = (y /d z). Proof. by move=>->. Qed. Theorem M_law x y z a b: (meet x y)=bot ->(meet x a)!=bot ->(meet y b)!=bot -> co_ind x y z ->co_ind (meet x a) (meet y b) z. Proof. move=> H1 H2 H3 H. move:(excluded_middle_axiom (x = bot));case=>Hx. rewrite co_sym=>//. rewrite Hx meet_bot_unitL. apply: ge_co_1. by apply bot_minimum. move:(excluded_middle_axiom (y = bot));case=>Hy. rewrite Hy meet_bot_unitL. by apply:ge_co_1; apply bot_minimum. move/eqP in Hx; move/eqP in Hy. move:(excluded_middle_axiom (ge z x));case=>Hzx. apply:ge_co_2=>//. apply:(@ge_transitive x z (meet x a))=>//. by rewrite meet_ge. move:(excluded_middle_axiom (ge z y));case=>Hzy. apply:ge_co_1. apply:(@ge_transitive y z (meet y b))=>//. by rewrite meet_ge. move:(excluded_middle_axiom (ge z (meet y b)));case=>Hzy'. by apply:ge_co_1. move/negP in Hzx;move/negP in Hzy;move/negP in Hzy'. -apply co_ind_eq_1 in H=>//. rewrite co_ind_eq_1=>//. apply (@margin_eq _ _ (meet y (meet (com b) (com z)))) in H. rewrite co_mc1 in H=>//. rewrite co_mc2 in H=>//. rewrite join_commutative dotrC in H. apply (@margin_eq _ _ (meet x (meet (com a) (com z)))) in H. rewrite co_mc1 in H=>//. rewrite co_mc2 in H=>//. by rewrite join_commutative dotrC. by rewrite meet_commutative meet_associative H1 meet_bot_unitL. by rewrite meet_commutative meet_associative H1 meet_bot_unitL. Qed. Theorem N_law1' x y z: meet x y = bot -> meet y z = bot -> meet x z = bot -> x != bot /\ ge (com z) (ctext (mix x (join y z)))/\ meet x (com z)!=bot-> mix x (join y z) = mix x y. Proof. move=> A B C H. apply N_law1 in H. rewrite meet_commutative in B;rewrite meet_commutative in C. apply meet_eq_ge in B;apply meet_eq_ge in C. apply meet_ge' in B;apply meet_ge' in C. rewrite meet_commutative in B;rewrite meet_commutative in C. by rewrite B C in H. Qed. Theorem N_law2' x y z cx cy : meet x y = bot -> meet y z = bot -> meet x z = bot -> ge (com x) y /\ meet (ctext cx) x = bot /\ meet (ctext cy) y = bot /\ up (join (join x y) z) = dot cy cx -> up (join (join x y) z) = dot (dot (up (join x z)) (up (join y z))) (down z). Proof. move=>a b c H. move:(a)(b)(c)=>A B C. apply N_law2 in H. rewrite meet_commutative in A. apply meet_eq_ge in A;apply meet_eq_ge in B;apply meet_eq_ge in C. apply meet_ge' in A;apply meet_ge' in B;apply meet_ge' in C. apply meet_eq_ge in a;apply meet_ge' in a. rewrite meet_commutative meet_distributive A B in H. rewrite meet_commutative meet_distributive a C in H. by rewrite (meet_commutative z _) C meet_commutative B in H. Qed. Theorem co_fact x y z cx cy:x!=bot->y!=bot->z!=bot-> meet x y = bot -> meet y z = bot -> meet x z = bot -> ge (com x) y /\ meet (ctext cx) x = bot /\ meet (ctext cy) y = bot /\ up (join x (join y z)) = dot cx cy -> co_ind x y z . Proof. move=>X Y Z A B C. case=>Ha [] Hb [] Hc Hd. apply co_ind_eq_2=>//. rewrite mix_up_down//. rewrite dotrA (dotrC (up (join y z)) _). move:(A)=>a;apply meet_eq_ge in A. apply (@N_law2' x y z cx cy)=>//. split=>//. split=>//. split=>//. by rewrite -join_associative dotrC. Qed. Theorem co_fact' x y z:x!=bot->y!=bot->z!=bot-> meet x y = bot -> meet y z = bot -> meet x z = bot -> co_ind x y z -> exists cx cy,ge (com x) (ctext cx) /\ ge (com y) (ctext cy) /\ up (join x (join y z)) = dot cx cy. Proof. move=>X Y Z A B C H. apply co_ind_eq_2 in H=>//. exists (up (join y z)), (mix x z). split. apply/meet_eq_ge. by rewrite ctext1 meet_distributive A C join_idempotent. split. apply/meet_eq_ge. move:(excluded_middle_axiom (ge z x));case=>Hzx. apply ge_mix_bob_eq in Hzx=>//. by rewrite Hzx ctext1 meet_bot_unitR. move/negP in Hzx. rewrite ctext3=>//. by rewrite meet_distributive B meet_commutative A join_idempotent. by rewrite join_associative. Qed. Theorem co_decomp x y z a b: a!=bot -> b!=bot -> meet x y = bot -> co_ind x y z -> ge x a -> ge y b -> co_ind a b z. Proof. move=> A B H0 H1 Ha Hb. apply meet_ge' in Ha. apply meet_ge' in Hb. rewrite -Ha -Hb. apply:M_law=>//. rewrite Ha=>//. rewrite Hb=>//. Qed. Theorem co_w_u x y z w:x!=bot -> y!=bot -> z!=bot -> w!=bot-> meet x y = bot -> meet x z = bot -> meet x w = bot -> meet y z = bot -> meet y w = bot -> meet w z = bot -> co_ind x (join y z) w -> co_ind x y (join z w). Proof. move=>X Y Z W A B C D E F H. move:(H)=>H'. apply co_ind_eq_2 in H=>//. rewrite co_ind_eq_2=>//. rewrite join_associative in H. rewrite join_associative H. rewrite[in RHS]dotrC -div_up_down. rewrite dotrC join_associative. rewrite dotrA (@dotrC (down (join (join y z) w)) _). rewrite up_down_unitL dot0r=>//. apply/eqP. rewrite eq_sym. apply/eqP. apply (@M_law x (join y z) w x (join z w)) in H'=>//. rewrite/co_ind in H'. rewrite meet_idempotent in H'. rewrite meet_distributive in H'. rewrite (join_commutative y _) in H'. rewrite (meet_commutative _ z) join_absorption in H'. rewrite (meet_commutative _ w) in H'. rewrite meet_distributive in H'. rewrite (meet_commutative _ y) F E in H'. rewrite join_idempotent in H'. move:(bot_minimum z)=>I. rewrite/ge in I. move/eqP in I. rewrite I in H'=>//. rewrite meet_distributive A B join_idempotent=>//. rewrite meet_idempotent=>//. rewrite (join_commutative y _) -join_distributive E. move:(bot_minimum z)=>I;rewrite/ge in I;move/eqP in I. rewrite I=>//. apply join_bot_bot=>//. Qed. Corollary M_l x y z w:x!=bot -> y!=bot -> z!=bot -> w!=bot-> meet x y = bot -> meet x z = bot -> meet x w = bot -> meet y z = bot -> meet y w = bot -> meet w z = bot -> co_ind x (join y z) w -> co_ind x z w. Proof. move=>X Y Z W A B C D E F H'. rewrite/co_ind. apply (@M_law x (join y z) w x (join z w)) in H'=>//. rewrite/co_ind in H'. rewrite meet_idempotent in H'. rewrite meet_distributive in H'. rewrite (join_commutative y _) in H'. rewrite (meet_commutative _ z) join_absorption in H'. rewrite (meet_commutative _ w) in H'. rewrite meet_distributive in H'. rewrite (meet_commutative _ y) F E in H'. rewrite join_idempotent in H'. move:(bot_minimum z)=>I. rewrite/ge in I. move/eqP in I. rewrite I in H'=>//. rewrite meet_distributive A B join_idempotent=>//. rewrite meet_idempotent=>//. rewrite (join_commutative y _) -join_distributive E. move:(bot_minimum z)=>I;rewrite/ge in I;move/eqP in I. rewrite I=>//. Qed. Theorem co_contr x y z w:x!=bot -> y!=bot -> z!=bot -> w!=bot -> meet x y = bot -> meet x z = bot -> meet x w = bot -> meet y z = bot -> meet y w = bot -> meet w z = bot -> (co_ind x y (join z w) /\ co_ind x z w <-> co_ind x (join y z) w). Proof. move=>X Y Z W A B C D E F. split. move=>[Ha Hb]. apply co_sym in Ha=>//. apply co_sym in Hb=>//. apply co_ind_eq_2 in Ha=>//. apply co_ind_eq_2 in Hb=>//. rewrite (join_commutative z x) -join_associative in Hb. rewrite Hb in Ha. rewrite co_sym=>//. rewrite co_ind_eq_2=>//. rewrite (join_commutative _ x) join_associative (join_commutative x y). rewrite -join_associative Ha. rewrite[in RHS]dotrC. rewrite -div_up_down. rewrite dotrC -(dotrA (up (join x w)) _ _). rewrite dotrA (dotrC (down (join x w)) (up (join x w))). rewrite up_down_unitL dot0r. rewrite mix_up_down=>//. rewrite mix_up_down=>//. rewrite dotrA. rewrite (dotrC (dot (dot (up (join z w)) (down w)) (up (join y (join z w))))). rewrite dotrA dotrA. rewrite (dotrC _ (up (join z w))). rewrite up_down_unitL dot0r. rewrite dotrC join_associative mix_up_down=>//. apply:join_bot_bot=>//. apply:join_bot_bot=>//. apply:join_bot_bot=>//. -move=>H. split. apply:co_w_u=>//. apply: (@M_l x y z w)=>//. Qed. Corollary co_con x y z:x!=bot -> y!=bot -> z!=bot -> meet x y = bot -> meet x z = bot -> meet y z = bot->((co_ind x y z /\ ind x z)<->ind x (join y z)). Proof. move=>X Y Z A B C. split. move=>[Ha Hb]. rewrite ind_eq=>//. apply ind_eq in Hb=>//. apply co_sym in Ha=>//. apply co_ind_eq_2 in Ha=>//. rewrite Hb in Ha. rewrite (join_commutative y x) -join_associative in Ha. rewrite Ha. apply/eqP. rewrite eq_sym. apply/eqP. rewrite[in RHS] dotrC (dotrC (up x) (up z)) dotrA. rewrite dotrC -div_up_down. rewrite -dotrA dotrC up_down_unitL bob_unitL -div_up_down=>//. rewrite -mix_up_down=>//. apply:join_bot_bot=>//. move=>H. move:(H)=>H'. split. apply ind_eq in H=>//. rewrite co_ind_eq_2=>//. rewrite -join_associative H. rewrite[in RHS]dotrC. rewrite -div_up_down. rewrite -dotrA (dotrC (up x) _). rewrite up_down_unitL bob_unitL. rewrite/ind in H'. apply (@M_law x (join y z) bot x z) in H'. rewrite meet_idempotent in H'. rewrite meet_commutative join_commutative join_absorption in H'. rewrite/co_ind in H'. rewrite join_commutative join_bot_unitL in H'. rewrite H'=>//. rewrite meet_distributive. rewrite A B join_bot=>//. rewrite meet_idempotent=>//. rewrite meet_commutative join_commutative join_absorption=>//. apply:join_bot_bot=>//. apply (@M_law x (join y z) bot x z) in H'. rewrite meet_idempotent in H'. rewrite meet_commutative join_commutative join_absorption in H'. rewrite/ind=>//. rewrite meet_distributive. rewrite A B join_bot=>//. rewrite meet_idempotent=>//. rewrite meet_commutative join_commutative join_absorption=>//. Qed. Theorem co_inter x y z w:x!=bot -> y!=bot -> z!=bot -> w!=bot->meet x (com z)!=bot-> meet x y = bot -> meet x z = bot -> meet x w = bot -> meet y z = bot -> meet y w = bot -> meet w z = bot -> (co_ind x (join y z) w <-> (co_ind x y (join z w)/\co_ind x z (join y w))). Proof. move=>X Y Z W XZ A B C D E F. split. -move=>H. apply:conj. apply:co_w_u=>//. rewrite join_commutative in H;apply:co_w_u=>//. by rewrite meet_commutative. by rewrite meet_commutative. by rewrite meet_commutative. -move=>[HA HB]. move:(HA)(HB)=>Ha Hb. move/co_ind_eq_2 in Ha=>//; move/co_ind_eq_2 in Hb=>//. rewrite dotrC in Ha; rewrite dotrC in Hb. rewrite (join_associative y _ _) (join_commutative y z) -(join_associative z _ _)in Ha. apply div_up_down in Ha=>//;apply div_up_down in Hb=>//. rewrite -join_associative (join_associative y z w) (join_commutative y z) (join_associative x _ w) (join_associative x z y) -join_associative in Ha. rewrite Ha in Hb. ---have Hm: mix x (join z w)=mix x w. rewrite join_commutative. apply:N_law1'=>//. split;first by[]. split;last by[]. rewrite join_commutative Hb. move: (excluded_middle_axiom (ge (join y w) x)); case=>Hyw. rewrite ctext2=>//. by rewrite bot_minimum. move/negP in Hyw. rewrite ctext3=>//. by rewrite -meet_eq_ge meet_distributive meet_distributive meet_commutative B meet_commutative D meet_commutative F join_bot_unitL join_bot_unitL. apply div_up_down in Ha. rewrite dotrC Hm in Ha. rewrite co_ind_eq_2=>//. by rewrite (join_commutative y z) -join_associative -join_associative join_associative. by apply:join_bot_bot. Qed. End conditional_independence. Section separoid. Parameter sep:L -> L -> L -> bool. Axiom sep_id :forall x y, sep x y x. Axiom sep_co : forall x y z, sep x y z -> sep y x z. Axiom sep_decomp : forall x y z w, sep x y z -> ge y w -> sep x w z. Axiom sep_w_u : forall x y z w, sep x y z -> ge y w -> sep x y (join z w). Axiom sep_contr : forall x y z w, sep x y z -> sep x w (join y z) -> sep x (join y w) z. Axiom sep_strong : forall x y z w, ge y z -> ge y w -> sep x y z -> sep x y w -> sep x y (meet z w). Lemma sep_idL x y: sep x y y. Proof. apply:sep_co. by apply:sep_id. Qed. (* Lemma sep_xx x y: sep x x y -> sep x (join x y) y. Proof. move:(@sep_idL x y). move=>Ha Hb ;move:Ha Hb. move:(@sep_contr x y y x)=>H. by rewrite join_idempotent join_commutative in H. Qed. *) Lemma ge_sep_eq x y: ge y x -> sep x x y. Proof. (*move: (sep_idL x y).*) apply:sep_decomp. by apply:sep_idL. Qed. Proposition ge_sep_1 x y z: ge z y -> sep x y z. Proof. move:(@sep_idL x z). apply:(@sep_decomp x z z y). Qed. Proposition ge_sep_2 x y z: x!=bot -> ge z x -> sep x y z. Proof. move=>H h. apply sep_co. by apply:(@ge_sep_1 y x z). Qed. Lemma sep_de x y z w: sep x (join y w) z -> sep x y z. Proof. move=>H. move:H (@join_ge y w). apply:(@sep_decomp x (join y w) z y). Qed. Lemma sep_join x y z:sep x y z -> sep x (join y z) z. Proof. move=>H. move:(sep_idL x z)=>Ha. rewrite -(@join_idempotent z) in H. rewrite join_commutative. apply:sep_contr=>//. Qed. Lemma sep_join' x y z:sep x y z -> sep x y (join y z). Proof. move=>H. rewrite join_commutative. apply:(@sep_w_u x y z y)=>//. by rewrite ge_reflexive. Qed. Lemma sep_join'2 x y z:sep x y z -> sep x y (join x z). Proof. move=>H. apply:sep_co. apply:sep_join'. by apply sep_co. Qed. Lemma sep_join'3 x y z:sep x y z -> sep x y (join x (join y z)). Proof. move=>H. move:(sep_join' H)=>H'. apply:sep_join'2=>//. Qed. Theorem M_law_sep x y z a b: (meet x y)=bot ->(meet x a)!=bot ->(meet y b)!=bot -> sep x y z ->sep (meet x a) (meet y b) z. Proof. move=>H1 H2 H3 H. rewrite(@sep_decomp (meet x a) y z (meet y b))=>//. rewrite sep_co=>//. rewrite (@sep_decomp y x z (meet x a))=>//. rewrite sep_co=>//. by apply meet_ge. by apply meet_ge. Qed. Proposition mar_sep x1 x2 x3 x4 x5: sep x3 x1 x2 -> sep x4 (join x1 x2) x3 -> sep x5 (join (join x1 x2) x3) x4 -> sep x3 (join x1 x5) (join x2 x4). Proof. move=>Ha Hb Hc. move:(Hc)=>Hc'. apply (@sep_w_u x5 (join (join x1 x2) x3) x4 x2) in Hc'. rewrite (join_commutative x4 _) join_commutative in Hc'. apply sep_de in Hc'. rewrite join_commutative sep_contr=>//. rewrite sep_co=>//. -rewrite join_commutative -join_associative. rewrite sep_co=>//. rewrite(@sep_decomp x1 (join x3 (join x4 x5)) (join x2 (join x4 x5)) x3)=>//. rewrite sep_w_u=>//. rewrite sep_contr=>//. rewrite sep_co=>//. rewrite sep_contr=>//. -move:(Hb)=>Hb'. apply(@sep_w_u x4 (join x1 x2) x3 x2) in Hb'. rewrite sep_co=>//. rewrite (@sep_decomp x4 (join x1 x2) (join x3 x2) x1)=>//. rewrite join_ge=>//. rewrite join_commutative join_ge=>//. -rewrite sep_co=>//. move:(Hc)=>HC. rewrite -join_associative in HC. apply(@sep_w_u x5 (join x1 (join x2 x3)) x4 (join x2 x3)) in HC. rewrite (@sep_decomp x5 (join x1 (join x2 x3)) (join x4 (join x3 x2)) x1)=>//. rewrite (join_commutative x3 _)=>//. rewrite join_ge=>//. rewrite join_commutative join_ge=>//. rewrite join_commutative join_ge=>//. rewrite join_ge=>//. rewrite (join_commutative x1 _) -join_associative join_ge=>//. Qed. (*conditional independence => separoid*) Theorem co_id x y:x!=bot -> co_ind x y x. Proof. move=>X. apply ge_co_2=>//. Print ge_co_2. by rewrite/le ge_reflexive. Qed. Theorem co_ind_sep x y z w:x!=bot -> y!=bot -> z!=bot -> w!=bot -> meet x y = bot -> meet x z = bot -> meet x w = bot -> meet y z = bot -> meet y w = bot -> meet w z = bot -> (co_ind x y x /\ (co_ind x y z -> co_ind y x z) /\(co_ind x y z -> ge y w -> co_ind x w z) /\(co_ind x y z -> ge y w -> co_ind x y (join z w)) /\ (co_ind x y z -> co_ind x w (join y z) -> co_ind x (join y w) z) /\(ge y z -> ge y w -> co_ind x y z -> co_ind x y w -> co_ind x y (meet z w))). Proof. move=>X Y Z W A B C D E F. split. -by apply co_id. split. --by apply co_sym. split. ---move=>H H'. apply:(@co_decomp x y z x w)=>//. by rewrite ge_reflexive. split. ----move=>H H'. rewrite/ge/le in H'. move/eqP in H'. rewrite -H' in H. move/co_w_u in H=>//. rewrite join_commutative. apply:H=>//. by rewrite meet_commutative. split. -----move=>H1 H2. rewrite join_commutative. apply (@co_contr x w y z)=>//. by rewrite meet_commutative. by rewrite meet_commutative. ------rewrite/co_ind. move=>H1 H2 H H'. move:( H1)=>H3;move:(H2)=>H4. apply meet_ge' in H3;apply meet_ge' in H4. move/eqP in H1;move/eqP in H2. rewrite join_distributive H1 H2 meet_idempotent. rewrite H1 in H; rewrite H2 in H'. rewrite H in H'. rewrite H. by apply Th5. Qed. End separoid. Section graphoid. Parameter grap: L -> L -> L -> bool. Axiom grap_sym:forall x y z, grap x y z -> grap y x z. Axiom grap_decomp:forall x y z w, grap x (join y w) z -> grap x y z. Axiom grap_w_u:forall x y z w, grap x (join y z) w -> grap x y (join z w). Axiom grap_contr:forall x y z w, grap x y (join z w) /\ grap x z w -> grap x (join y z) w. Axiom grap_int:forall x y z w, grap x y (join z w) /\ grap x z (join y w) -> grap x (join y z) w.