Moozonian
Web Images Developer News Books Maps Shopping Moo-AI
Showing results for basic need HD HD
GitHub Repo https://github.com/kenkinn/cain_conditionalindependence-

kenkinn/cain_conditionalindependence-

(* 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.
GitHub Repo https://github.com/chrisneagu/FTC-Skystone-Dark-Angels-Romania-2020

chrisneagu/FTC-Skystone-Dark-Angels-Romania-2020

NOTICE This repository contains the public FTC SDK for the SKYSTONE (2019-2020) competition season. If you are looking for the current season's FTC SDK software, please visit the new and permanent home of the public FTC SDK: FtcRobotController repository Welcome! This GitHub repository contains the source code that is used to build an Android app to control a FIRST Tech Challenge competition robot. To use this SDK, download/clone the entire project to your local computer. Getting Started If you are new to robotics or new to the FIRST Tech Challenge, then you should consider reviewing the FTC Blocks Tutorial to get familiar with how to use the control system: FTC Blocks Online Tutorial Even if you are an advanced Java programmer, it is helpful to start with the FTC Blocks tutorial, and then migrate to the OnBot Java Tool or to Android Studio afterwards. Downloading the Project If you are an Android Studio programmer, there are several ways to download this repo. Note that if you use the Blocks or OnBot Java Tool to program your robot, then you do not need to download this repository. If you are a git user, you can clone the most current version of the repository: git clone https://github.com/FIRST-Tech-Challenge/SKYSTONE.git Or, if you prefer, you can use the "Download Zip" button available through the main repository page. Downloading the project as a .ZIP file will keep the size of the download manageable. You can also download the project folder (as a .zip or .tar.gz archive file) from the Downloads subsection of the Releases page for this repository. Once you have downloaded and uncompressed (if needed) your folder, you can use Android Studio to import the folder ("Import project (Eclipse ADT, Gradle, etc.)"). Getting Help User Documentation and Tutorials FIRST maintains online documentation with information and tutorials on how to use the FIRST Tech Challenge software and robot control system. You can access this documentation using the following link: SKYSTONE Online Documentation Note that the online documentation is an "evergreen" document that is constantly being updated and edited. It contains the most current information about the FIRST Tech Challenge software and control system. Javadoc Reference Material The Javadoc reference documentation for the FTC SDK is now available online. Click on the following link to view the FTC SDK Javadoc documentation as a live website: FTC Javadoc Documentation Documentation for the FTC SDK is also included with this repository. There is a subfolder called "doc" which contains several subfolders: The folder "apk" contains the .apk files for the FTC Driver Station and FTC Robot Controller apps. The folder "javadoc" contains the JavaDoc user documentation for the FTC SDK. Online User Forum For technical questions regarding the Control System or the FTC SDK, please visit the FTC Technology forum: FTC Technology Forum Release Information Version 5.5 (20200824-090813) Version 5.5 requires Android Studio 4.0 or later. New features Adds support for calling custom Java classes from Blocks OpModes (fixes SkyStone issue #161). Classes must be in the org.firstinspires.ftc.teamcode package. Methods must be public static and have no more than 21 parameters. Parameters declared as OpMode, LinearOpMode, Telemetry, and HardwareMap are supported and the argument is provided automatically, regardless of the order of the parameters. On the block, the sockets for those parameters are automatically filled in. Parameters declared as char or java.lang.Character will accept any block that returns text and will only use the first character in the text. Parameters declared as boolean or java.lang.Boolean will accept any block that returns boolean. Parameters declared as byte, java.lang.Byte, short, java.lang.Short, int, java.lang.Integer, long, or java.lang.Long, will accept any block that returns a number and will round that value to the nearest whole number. Parameters declared as float, java.lang.Float, double, java.lang.Double will accept any block that returns a number. Adds telemetry API method for setting display format Classic Monospace HTML (certain tags only) Adds blocks support for switching cameras. Adds Blocks support for TensorFlow Object Detection with a custom model. Adds support for uploading a custom TensorFlow Object Detection model in the Manage page, which is especially useful for Blocks and OnBotJava users. Shows new Control Hub blink codes when the WiFi band is switched using the Control Hub's button (only possible on Control Hub OS 1.1.2) Adds new warnings which can be disabled in the Advanced RC Settings Mismatched app versions warning Unnecessary 2.4 GHz WiFi usage warning REV Hub is running outdated firmware (older than version 1.8.2) Adds support for Sony PS4 gamepad, and reworks how gamepads work on the Driver Station Removes preference which sets gamepad type based on driver position. Replaced with menu which allows specifying type for gamepads with unknown VID and PID Attempts to auto-detect gamepad type based on USB VID and PID If gamepad VID and PID is not known, use type specified by user for that VID and PID If gamepad VID and PID is not known AND the user has not specified a type for that VID and PID, an educated guess is made about how to map the gamepad Driver Station will now attempt to automatically recover from a gamepad disconnecting, and re-assign it to the position it was assigned to when it dropped If only one gamepad is assigned and it drops: it can be recovered If two gamepads are assigned, and have different VID/PID signatures, and only one drops: it will be recovered If two gamepads are assigned, and have different VID/PID signatures, and BOTH drop: both will be recovered If two gamepads are assigned, and have the same VID/PID signatures, and only one drops: it will be recovered If two gamepads are assigned, and have the same VID/PID signatures, and BOTH drop: neither will be recovered, because of the ambiguity of the gamepads when they re-appear on the USB bus. There is currently one known edge case: if there are two gamepads with the same VID/PID signature plugged in, but only one is assigned, and they BOTH drop, it's a 50-50 chance of which one will be chosen for automatic recovery to the assigned position: it is determined by whichever one is re-enumerated first by the USB bus controller. Adds landscape user interface to Driver Station New feature: practice timer with audio cues New feature (Control Hub only): wireless network connection strength indicator (0-5 bars) New feature (Control Hub only): tapping on the ping/channel display will switch to an alternate display showing radio RX dBm and link speed (tap again to switch back) The layout will NOT autorotate. You can switch the layout from the Driver Station's settings menu. Breaking changes Removes support for Android versions 4.4 through 5.1 (KitKat and Lollipop). The minSdkVersion is now 23. Removes the deprecated LinearOpMode methods waitOneFullHardwareCycle() and waitForNextHardwareCycle() Enhancements Handles RS485 address of Control Hub automatically The Control Hub is automatically given a reserved address Existing configuration files will continue to work All addresses in the range of 1-10 are still available for Expansion Hubs The Control Hub light will now normally be solid green, without blinking to indicate the address The Control Hub will not be shown on the Expansion Hub Address Change settings page Improves REV Hub firmware updater The user can now choose between all available firmware update files Version 1.8.2 of the REV Hub firmware is bundled into the Robot Controller app. Text was added to clarify that Expansion Hubs can only be updated via USB. Firmware update speed was reduced to improve reliability Allows REV Hub firmware to be updated directly from the Manage webpage Improves log viewer on Robot Controller Horizontal scrolling support (no longer word wrapped) Supports pinch-to-zoom Uses a monospaced font Error messages are highlighted New color scheme Attempts to force-stop a runaway/stuck OpMode without restarting the entire app Not all types of runaway conditions are stoppable, but if the user code attempts to talk to hardware during the runaway, the system should be able to capture it. Makes various tweaks to the Self Inspect screen Renames "OS version" entry to "Android version" Renames "WiFi Direct Name" to "WiFi Name" Adds Control Hub OS version, when viewing the report of a Control Hub Hides the airplane mode entry, when viewing the report of a Control Hub Removes check for ZTE Speed Channel Changer Shows firmware version for all Expansion and Control Hubs Reworks network settings portion of Manage page All network settings are now applied with a single click The WiFi Direct channel of phone-based Robot Controllers can now be changed from the Manage page WiFi channels are filtered by band (2.4 vs 5 GHz) and whether they overlap with other channels The current WiFi channel is pre-selected on phone-based Robot Controllers, and Control Hubs running OS 1.1.2 or later. On Control Hubs running OS 1.1.2 or later, you can choose to have the system automatically select a channel on the 5 GHz band Improves OnBotJava New light and dark themes replace the old themes (chaos, github, chrome,...) the new default theme is light and will be used when you first update to this version OnBotJava now has a tabbed editor Read-only offline mode Improves function of "exit" menu item on Robot Controller and Driver Station Now guaranteed to be fully stopped and unloaded from memory Shows a warning message if a LinearOpMode exists prematurely due to failure to monitor for the start condition Improves error message shown when the Driver Station and Robot Controller are incompatible with each other Driver Station OpMode Control Panel now disabled while a Restart Robot is in progress Disables advanced settings related to WiFi direct when the Robot Controller is a Control Hub. Tint phone battery icons on Driver Station when low/critical. Uses names "Control Hub Portal" and "Control Hub" (when appropriate) in new configuration files Improve I2C read performance Very large improvement on Control Hub; up to ~2x faster with small (e.g. 6 byte) reads Not as apparent on Expansion Hubs connected to a phone Update/refresh build infrastructure Update to 'androidx' support library from 'com.android.support:appcompat', which is end-of-life Update targetSdkVersion and compileSdkVersion to 28 Update Android Studio's Android plugin to latest Fix reported build timestamp in 'About' screen Add sample illustrating manual webcam use: ConceptWebcam Bug fixes Fixes SkyStone issue #248 Fixes SkyStone issue #232 and modifies bulk caching semantics to allow for cache-preserving MANUAL/AUTO transitions. Improves performance when REV 2M distance sensor is unplugged Improves readability of Toast messages on certain devices Allows a Driver Station to connect to a Robot Controller after another has disconnected Improves generation of fake serial numbers for UVC cameras which do not provide a real serial number Previously some devices would assign such cameras a serial of 0:0 and fail to open and start streaming Fixes ftc_app issue #638. Fixes a slew of bugs with the Vuforia camera monitor including: Fixes bug where preview could be displayed with a wonky aspect ratio Fixes bug where preview could be cut off in landscape Fixes bug where preview got totally messed up when rotating phone Fixes bug where crosshair could drift off target when using webcams Fixes issue in UVC driver on some devices (ftc_app 681) if streaming was started/stopped multiple times in a row Issue manifested as kernel panic on devices which do not have this kernel patch. On affected devices which do have the patch, the issue was manifest as simply a failure to start streaming. The Tech Team believes that the root cause of the issue is a bug in the Linux kernel XHCI driver. A workaround was implemented in the SDK UVC driver. Fixes bug in UVC driver where often half the frames from the camera would be dropped (e.g. only 15FPS delivered during a streaming session configured for 30FPS). Fixes issue where TensorFlow Object Detection would show results whose confidence was lower than the minimum confidence parameter. Fixes a potential exploitation issue of CVE-2019-11358 in OnBotJava Fixes changing the address of an Expansion Hub with additional Expansion Hubs connected to it Preserves the Control Hub's network connection when "Restart Robot" is selected Fixes issue where device scans would fail while the Robot was restarting Fix RenderScript usage Use androidx.renderscript variant: increased compatibility Use RenderScript in Java mode, not native: simplifies build Fixes webcam-frame-to-bitmap conversion problem: alpha channel wasn't being initialized, only R, G, & B Fixes possible arithmetic overflow in Deadline Fixes deadlock in Vuforia webcam support which could cause 5-second delays when stopping OpMode Version 5.4 (20200108-101156) Fixes SkyStone issue #88 Adds an inspection item that notes when a robot controller (Control Hub) is using the factory default password. Fixes SkyStone issue #61 Fixes SkyStone issue #142 Fixes ftc_app issue #417 by adding more current and voltage monitoring capabilities for REV Hubs. Fixes a crash sometimes caused by OnBotJava activity Improves OnBotJava autosave functionality ftc_app #738 Fixes system responsiveness issue when an Expansion Hub is disconnected Fixes issue where IMU initialization could prevent Op Modes from stopping Fixes issue where AndroidTextToSpeech.speak() would fail if it was called too early Adds telemetry.speak() methods and blocks, which cause the Driver Station (if also updated) to speak text Adds and improves Expansion Hub-related warnings Improves Expansion Hub low battery warning Displays the warning immediately after the hub reports it Specifies whether the condition is current or occurred temporarily during an OpMode run Displays which hubs reported low battery Displays warning when hub loses and regains power during an OpMode run Fixes the hub's LED pattern after this condition Displays warning when Expansion Hub is not responding to commands Specifies whether the condition is current or occurred temporarily during an OpMode run Clarifies warning when Expansion Hub is not present at startup Specifies that this condition requires a Robot Restart before the hub can be used. The hub light will now accurately reflect this state Improves logging and reduces log spam during these conditions Syncs the Control Hub time and timezone to a connected web browser programming the robot, if a Driver Station is not available. Adds bulk read functionality for REV Hubs A bulk caching mode must be set at the Hub level with LynxModule#setBulkCachingMode(). This applies to all relevant SDK hardware classes that reference that Hub. The following following Hub bulk caching modes are available: BulkCachingMode.OFF (default): All hardware calls operate as usual. Bulk data can read through LynxModule#getBulkData() and processed manually. BulkCachingMode.AUTO: Applicable hardware calls are served from a bulk read cache that is cleared/refreshed automatically to ensure identical commands don't hit the same cache. The cache can also be cleared manually with LynxModule#clearBulkCache(), although this is not recommended. (advanced users) BulkCachingMode.MANUAL: Same as BulkCachingMode.AUTO except the cache is never cleared automatically. To avoid getting stale data, the cache must be manually cleared at the beginning of each loop body or as the user deems appropriate. Removes PIDF Annotation values added in Rev 5.3 (to AndyMark, goBILDA and TETRIX motor configurations). The new motor types will still be available but their Default control behavior will revert back to Rev 5.2 Adds new ConceptMotorBulkRead sample Opmode to demonstrate and compare Motor Bulk-Read modes for reducing I/O latencies. Version 5.3 (20191004-112306) Fixes external USB/UVC webcam support Makes various bugfixes and improvements to Blocks page, including but not limited to: Many visual tweaks Browser zoom and window resize behave better Resizing the Java preview pane works better and more consistently across browsers The Java preview pane consistently gets scrollbars when needed The Java preview pane is hidden by default on phones Internet Explorer 11 should work Large dropdown lists display properly on lower res screens Disabled buttons are now visually identifiable as disabled A warning is shown if a user selects a TFOD sample, but their device is not compatible Warning messages in a Blocks op mode are now visible by default. Adds goBILDA 5201 and 5202 motors to Robot Configurator Adds PIDF Annotation values to AndyMark, goBILDA and TETRIX motor configurations. This has the effect of causing the RUN_USING_ENCODERS and RUN_TO_POSITION modes to use PIDF vs PID closed loop control on these motors. This should provide more responsive, yet stable, speed control. PIDF adds Feedforward control to the basic PID control loop. Feedforward is useful when controlling a motor's speed because it "anticipates" how much the control voltage must change to achieve a new speed set-point, rather than requiring the integrated error to change sufficiently. The PIDF values were chosen to provide responsive, yet stable, speed control on a lightly loaded motor. The more heavily a motor is loaded (drag or friction), the more noticable the PIDF improvement will be. Fixes startup crash on Android 10 Fixes ftc_app issue #712 (thanks to FROGbots-4634) Fixes ftc_app issue #542 Allows "A" and lowercase letters when naming device through RC and DS apps. Version 5.2 (20190905-083277) Fixes extra-wide margins on settings activities, and placement of the new configuration button Adds Skystone Vuforia image target data. Includes sample Skystone Vuforia Navigation op modes (Java). Includes sample Skystone Vuforia Navigation op modes (Blocks). Adds TensorFlow inference model (.tflite) for Skystone game elements. Includes sample Skystone TensorFlow op modes (Java). Includes sample Skystone TensorFlow op modes (Blocks). Removes older (season-specific) sample op modes. Includes 64-bit support (to comply with Google Play requirements). Protects against Stuck OpModes when a Restart Robot is requested. (Thanks to FROGbots-4634) (ftc_app issue #709) Blocks related changes: Fixes bug with blocks generated code when hardware device name is a java or javascript reserved word. Shows generated java code for blocks, even when hardware items are missing from the active configuration. Displays warning icon when outdated Vuforia and TensorFlow blocks are used (SkyStone issue #27) Version 5.1 (20190820-222104) Defines default PIDF parameters for the following motors: REV Core Hex Motor REV 20:1 HD Hex Motor REV 40:1 HD Hex Motor Adds back button when running on a device without a system back button (such as a Control Hub) Allows a REV Control Hub to update the firmware on a REV Expansion Hub via USB Fixes SkyStone issue #9 Fixes ftc_app issue #715 Prevents extra DS User clicks by filtering based on current state. Prevents incorrect DS UI state changes when receiving new OpMode list from RC Adds support for REV Color Sensor V3 Adds a manual-refresh DS Camera Stream for remotely viewing RC camera frames. To show the stream on the DS, initialize but do not run a stream-enabled opmode, select the Camera Stream option in the DS menu, and tap the image to refresh. This feature is automatically enabled when using Vuforia or TFOD—no additional RC configuration is required for typical use cases. To hide the stream, select the same menu item again. Note that gamepads are disabled and the selected opmode cannot be started while the stream is open as a safety precaution. To use custom streams, consult the API docs for CameraStreamServer#setSource and CameraStreamSource. Adds many Star Wars sounds to RobotController resources. Added SKYSTONE Sounds Chooser Sample Program. Switches out startup, connect chimes, and error/warning sounds for Star Wars sounds Updates OnBot Java to use a WebSocket for communication with the robot The OnBot Java page no longer has to do a full refresh when a user switches from editing one file to another Known issues: Camera Stream The Vuforia camera stream inherits the issues present in the phone preview (namely ftc_app issue #574). This problem does not affect the TFOD camera stream even though it receives frames from Vuforia. The orientation of the stream frames may not always match the phone preview. For now, these frames may be rotated manually via a custom CameraStreamSource if desired. OnBotJava Browser back button may not always work correctly It's possible for a build to be queued, but not started. The OnBot Java build console will display a warning if this occurs. A user might not realize they are editing a different file if the user inadvertently switches from one file to another since this switch is now seamless. The name of the currently open file is displayed in the browser tab. Version 5.0 (built on 19.06.14) Support for the REV Robotics Control Hub. Adds a Java preview pane to the Blocks editor. Adds a new offline export feature to the Blocks editor. Display wifi channel in Network circle on Driver Station. Adds calibration for Logitech C270 Updates build tooling and target SDK. Compliance with Google's permissions infrastructure (Required after build tooling update). Keep Alives to mitigate the Motorola wifi scanning problem. Telemetry substitute no longer necessary. Improves Vuforia error reporting. Fixes ftctechnh/ftc_app issues 621, 713. Miscellaneous bug fixes and improvements. Version 4.3 (built on 18.10.31) Includes missing TensorFlow-related libraries and files. Version 4.2 (built on 18.10.30) Includes fix to avoid deadlock situation with WatchdogMonitor which could result in USB communication errors. Comm error appeared to require that user disconnect USB cable and restart the Robot Controller app to recover. robotControllerLog.txt would have error messages that included the words "E RobotCore: lynx xmit lock: #### abandoning lock:" Includes fix to correctly list the parent module address for a REV Robotics Expansion Hub in a configuration (.xml) file. Bug in versions 4.0 and 4.1 would incorrect list the address module for a parent REV Robotics device as "1". If the parent module had a higher address value than the daisy-chained module, then this bug would prevent the Robot Controller from communicating with the downstream Expansion Hub. Added requirement for ACCESS_COARSE_LOCATION to allow a Driver Station running Android Oreo to scan for Wi-Fi Direct devices. Added google() repo to build.gradle because aapt2 must be downloaded from the google() repository beginning with version 3.2 of the Android Gradle Plugin. Important Note: Android Studio users will need to be connected to the Internet the first time build the ftc_app project. Internet connectivity is required for the first build so the appropriate files can be downloaded from the Google repository. Users should not need to be connected to the Internet for subsequent builds. This should also fix buid issue where Android Studio would complain that it "Could not find com.android.tools.lint:lint-gradle:26.1.4" (or similar). Added support for REV Spark Mini motor controller as part of the configuration menu for a servo/PWM port on the REV Expansion Hub. Provide examples for playing audio files in an Op Mode. Block Development Tool Changes Includes a fix for a problem with the Velocity blocks that were reported in the FTC Technology forum (Blocks Programming subforum). Change the "Save completed successfully." message to a white color so it will contrast with a green background. Fixed the "Download image" feature so it will work if there are text blocks in the op mode. Introduce support for Google's TensorFlow Lite technology for object detetion for 2018-2019 game. TensorFlow lite can recognize Gold Mineral and Silver Mineral from 2018-2019 game. Example Java and Block op modes are included to show how to determine the relative position of the gold block (left, center, right). Version 4.1 (released on 18.09.24) Changes include: Fix to prevent crash when deprecated configuration annotations are used. Change to allow FTC Robot Controller APK to be auto-updated using FIRST Global Control Hub update scripts. Removed samples for non supported / non legal hardware. Improvements to Telemetry.addData block with "text" socket. Updated Blocks sample op mode list to include Rover Ruckus Vuforia example. Update SDK library version number. Version 4.0 (released on 18.09.12) Changes include: Initial support for UVC compatible cameras If UVC camera has a unique serial number, RC will detect and enumerate by serial number. If UVC camera lacks a unique serial number, RC will only support one camera of that type connected. Calibration settings for a few cameras are included (see TeamCode/src/main/res/xml/teamwebcamcalibrations.xml for details). User can upload calibration files from Program and Manage web interface. UVC cameras seem to draw a fair amount of electrical current from the USB bus. This does not appear to present any problems for the REV Robotics Control Hub. This does seem to create stability problems when using some cameras with an Android phone-based Robot Controller. FTC Tech Team is investigating options to mitigate this issue with the phone-based Robot Controllers. Updated sample Vuforia Navigation and VuMark Op Modes to demonstrate how to use an internal phone-based camera and an external UVC webcam. Support for improved motor control. REV Robotics Expansion Hub firmware 1.8 and greater will support a feed forward mechanism for closed loop motor control. FTC SDK has been modified to support PIDF coefficients (proportional, integral, derivative, and feed forward). FTC Blocks development tool modified to include PIDF programming blocks. Deprecated older PID-related methods and variables. REV's 1.8.x PIDF-related changes provide a more linear and accurate way to control a motor. Wireless Added 5GHz support for wireless channel changing for those devices that support it. Tested with Moto G5 and E4 phones. Also tested with other (currently non-approved) phones such as Samsung Galaxy S8. Improved Expansion Hub firmware update support in Robot Controller app Changes to make the system more robust during the firmware update process (when performed through Robot Controller app). User no longer has to disconnect a downstream daisy-chained Expansion Hub when updating an Expansion Hub's firmware. If user is updating an Expansion Hub's firmware through a USB connection, he/she does not have to disconnect RS485 connection to other Expansion Hubs. The user still must use a USB connection to update an Expansion Hub's firmware. The user cannot update the Expansion Hub firmware for a downstream device that is daisy chained through an RS485 connection. If an Expansion Hub accidentally gets "bricked" the Robot Controller app is now more likely to recognize the Hub when it scans the USB bus. Robot Controller app should be able to detect an Expansion Hub, even if it accidentally was bricked in a previous update attempt. Robot Controller app should be able to install the firmware onto the Hub, even if if accidentally was bricked in a previous update attempt. Resiliency FTC software can detect and enable an FTDI reset feature that is available with REV Robotics v1.8 Expansion Hub firmware and greater. When enabled, the Expansion Hub can detect if it hasn't communicated with the Robot Controller over the FTDI (USB) connection. If the Hub hasn't heard from the Robot Controller in a while, it will reset the FTDI connection. This action helps system recover from some ESD-induced disruptions. Various fixes to improve reliability of FTC software. Blocks Fixed errors with string and list indices in blocks export to java. Support for USB connected UVC webcams. Refactored optimized Blocks Vuforia code to support Rover Ruckus image targets. Added programming blocks to support PIDF (proportional, integral, derivative and feed forward) motor control. Added formatting options (under Telemetry and Miscellaneous categories) so user can set how many decimal places to display a numerical value. Support to play audio files (which are uploaded through Blocks web interface) on Driver Station in addition to the Robot Controller. Fixed bug with Download Image of Blocks feature. Support for REV Robotics Blinkin LED Controller. Support for REV Robotics 2m Distance Sensor. Added support for a REV Touch Sensor (no longer have to configure as a generic digital device). Added blocks for DcMotorEx methods. These are enhanced methods that you can use when supported by the motor controller hardware. The REV Robotics Expansion Hub supports these enhanced methods. Enhanced methods include methods to get/set motor velocity (in encoder pulses per second), get/set PIDF coefficients, etc.. Modest Improvements in Logging Decrease frequency of battery checker voltage statements. Removed non-FTC related log statements (wherever possible). Introduced a "Match Logging" feature. Under "Settings" a user can enable/disable this feature (it's disabled by default). If enabled, user provides a "Match Number" through the Driver Station user interface (top of the screen). The Match Number is used to create a log file specifically with log statements from that particular Op Mode run. Match log files are stored in /sdcard/FIRST/matlogs on the Robot Controller. Once an op mode run is complete, the Match Number is cleared. This is a convenient way to create a separate match log with statements only related to a specific op mode run. New Devices Support for REV Robotics Blinkin LED Controller. Support for REV Robotics 2m Distance Sensor. Added configuration option for REV 20:1 HD Hex Motor. Added support for a REV Touch Sensor (no longer have to configure as a generic digital device). Miscellaneous Fixed some errors in the definitions for acceleration and velocity in our javadoc documentation. Added ability to play audio files on Driver Station When user is configuring an Expansion Hub, the LED on the Expansion Hub will change blink pattern (purple-cyan) to indicate which Hub is currently being configured. Renamed I2cSensorType to I2cDeviceType. Added an external sample Op Mode that demonstrates localization using 2018-2019 (Rover Ruckus presented by QualComm) Vuforia targets. Added an external sample Op Mode that demonstrates how to use the REV Robotics 2m Laser Distance Sensor. Added an external sample Op Mode that demonstrates how to use the REV Robotics Blinkin LED Controller. Re-categorized external Java sample Op Modes to "TeleOp" instead of "Autonomous". Known issues: Initial support for UVC compatible cameras UVC cameras seem to draw significant amount of current from the USB bus. This does not appear to present any problems for the REV Robotics Control Hub. This does seem to create stability problems when using some cameras with an Android phone-based Robot Controller. FTC Tech Team is investigating options to mitigate this issue with the phone-based Robot Controllers. There might be a possible deadlock which causes the RC to become unresponsive when using a UVC webcam with a Nougat Android Robot Controller. Wireless When user selects a wireless channel, this channel does not necessarily persist if the phone is power cycled. Tech Team is hoping to eventually address this issue in a future release. Issue has been present since apps were introduced (i.e., it is not new with the v4.0 release). Wireless channel is not currently displayed for WiFi Direct connections. Miscellaneous The blink indication feature that shows which Expansion Hub is currently being configured does not work for a newly created configuration file. User has to first save a newly created configuration file and then close and re-edit the file in order for blink indicator to work. Version 3.6 (built on 17.12.18) Changes include: Blocks Changes Uses updated Google Blockly software to allow users to edit their op modes on Apple iOS devices (including iPad and iPhone). Improvement in Blocks tool to handle corrupt op mode files. Autonomous op modes should no longer get switched back to tele-op after re-opening them to be edited. The system can now detect type mismatches during runtime and alert the user with a message on the Driver Station. Updated javadoc documentation for setPower() method to reflect correct range of values (-1 to +1). Modified VuforiaLocalizerImpl to allow for user rendering of frames Added a user-overrideable onRenderFrame() method which gets called by the class's renderFrame() method. Version 3.5 (built on 17.10.30) Changes with version 3.5 include: Introduced a fix to prevent random op mode stops, which can occur after the Robot Controller app has been paused and then resumed (for example, when a user temporarily turns off the display of the Robot Controller phone, and then turns the screen back on). Introduced a fix to prevent random op mode stops, which were previously caused by random peer disconnect events on the Driver Station. Fixes issue where log files would be closed on pause of the RC or DS, but not re-opened upon resume. Fixes issue with battery handler (voltage) start/stop race. Fixes issue where Android Studio generated op modes would disappear from available list in certain situations. Fixes problem where OnBot Java would not build on REV Robotics Control Hub. Fixes problem where OnBot Java would not build if the date and time on the Robot Controller device was "rewound" (set to an earlier date/time). Improved error message on OnBot Java that occurs when renaming a file fails. Removed unneeded resources from android.jar binaries used by OnBot Java to reduce final size of Robot Controller app. Added MR_ANALOG_TOUCH_SENSOR block to Blocks Programming Tool. Version 3.4 (built on 17.09.06) Changes with version 3.4 include: Added telemetry.update() statement for BlankLinearOpMode template. Renamed sample Block op modes to be more consistent with Java samples. Added some additional sample Block op modes. Reworded OnBot Java readme slightly. Version 3.3 (built on 17.09.04) This version of the software includes improves for the FTC Blocks Programming Tool and the OnBot Java Programming Tool. Changes with verion 3.3 include: Android Studio ftc_app project has been updated to use Gradle Plugin 2.3.3. Android Studio ftc_app project is already using gradle 3.5 distribution. Robot Controller log has been renamed to /sdcard/RobotControllerLog.txt (note that this change was actually introduced w/ v3.2). Improvements in I2C reliability. Optimized I2C read for REV Expansion Hub, with v1.7 firmware or greater. Updated all external/samples (available through OnBot and in Android project folder). Vuforia Added support for VuMarks that will be used for the 2017-2018 season game. Blocks Update to latest Google Blockly release. Sample op modes can be selected as a template when creating new op mode. Fixed bug where the blocks would disappear temporarily when mouse button is held down. Added blocks for Range.clip and Range.scale. User can now disable/enable Block op modes. Fix to prevent occasional Blocks deadlock. OnBot Java Significant improvements with autocomplete function for OnBot Java editor. Sample op modes can be selected as a template when creating new op mode. Fixes and changes to complete hardware setup feature. Updated (and more useful) onBot welcome message. Known issues: Android Studio After updating to the new v3.3 Android Studio project folder, if you get error messages indicating "InvalidVirtualFileAccessException" then you might need to do a File->Invalidate Caches / Restart to clear the error. OnBot Java Sometimes when you push the build button to build all op modes, the RC returns an error message that the build failed. If you press the build button a second time, the build typically suceeds. Version 3.2 (built on 17.08.02) This version of the software introduces the "OnBot Java" Development Tool. Similar to the FTC Blocks Development Tool, the FTC OnBot Java Development Tool allows a user to create, edit and build op modes dynamically using only a Javascript-enabled web browser. The OnBot Java Development Tool is an integrated development environment (IDE) that is served up by the Robot Controller. Op modes are created and edited using a Javascript-enabled browser (Google Chromse is recommended). Op modes are saved on the Robot Controller Android device directly. The OnBot Java Development Tool provides a Java programming environment that does NOT need Android Studio. Changes with version 3.2 include: Enhanced web-based development tools Introduction of OnBot Java Development Tool. Web-based programming and management features are "always on" (user no longer needs to put Robot Controller into programming mode). Web-based management interface (where user can change Robot Controller name and also easily download Robot Controller log file). OnBot Java, Blocks and Management features available from web based interface. Blocks Programming Development Tool: Changed "LynxI2cColorRangeSensor" block to "REV Color/range sensor" block. Fixed tooltip for ColorSensor.isLightOn block. Added blocks for ColorSensor.getNormalizedColors and LynxI2cColorRangeSensor.getNormalizedColors. Added example op modes for digital touch sensor and REV Robotics Color Distance sensor. User selectable color themes. Includes many minor enhancements and fixes (too numerous to list). Known issues: Auto complete function is incomplete and does not support the following (for now): Access via this keyword Access via super keyword Members of the super cloass, not overridden by the class Any methods provided in the current class Inner classes Can't handle casted objects Any objects coming from an parenthetically enclosed expression Version 3.10 (built on 17.05.09) This version of the software provides support for the REV Robotics Expansion Hub. This version also includes improvements in the USB communication layer in an effort to enhance system resiliency. If you were using a 2.x version of the software previously, updating to version 3.1 requires that you also update your Driver Station software in addition to updating the Robot Controller software. Also note that in version 3.10 software, the setMaxSpeed and getMaxSpeed methods are no longer available (not deprecated, they have been removed from the SDK). Also note that the the new 3.x software incorporates motor profiles that a user can select as he/she configures the robot. Changes include: Blocks changes Added VuforiaTrackableDefaultListener.getPose and Vuforia.trackPose blocks. Added optimized blocks support for Vuforia extended tracking. Added atan2 block to the math category. Added useCompetitionFieldTargetLocations parameter to Vuforia.initialize block. If set to false, the target locations are placed at (0,0,0) with target orientation as specified in https://github.com/gearsincorg/FTCVuforiaDemo/blob/master/Robot_Navigation.java tutorial op mode. Incorporates additional improvements to USB comm layer to improve system resiliency (to recover from a greater number of communication disruptions). Additional Notes Regarding Version 3.00 (built on 17.04.13) In addition to the release changes listed below (see section labeled "Version 3.00 (built on 17.04.013)"), version 3.00 has the following important changes: Version 3.00 software uses a new version of the FTC Robocol (robot protocol). If you upgrade to v3.0 on the Robot Controller and/or Android Studio side, you must also upgrade the Driver Station software to match the new Robocol. Version 3.00 software removes the setMaxSpeed and getMaxSpeed methods from the DcMotor class. If you have an op mode that formerly used these methods, you will need to remove the references/calls to these methods. Instead, v3.0 provides the max speed information through the use of motor profiles that are selected by the user during robot configuration. Version 3.00 software currently does not have a mechanism to disable extra i2c sensors. We hope to re-introduce this function with a release in the near future. Version 3.00 (built on 17.04.13) *** Use this version of the software at YOUR OWN RISK!!! *** This software is being released as an "alpha" version. Use this version at your own risk! This pre-release software contains SIGNIFICANT changes, including changes to the Wi-Fi Direct pairing mechanism, rewrites of the I2C sensor classes, changes to the USB/FTDI layer, and the introduction of support for the REV Robotics Expansion Hub and the REV Robotics color-range-light sensor. These changes were implemented to improve the reliability and resiliency of the FTC control system. Please note, however, that version 3.00 is considered "alpha" code. This code is being released so that the FIRST community will have an opportunity to test the new REV Expansion Hub electronics module when it becomes available in May. The developers do not recommend using this code for critical applications (i.e., competition use). *** Use this version of the software at YOUR OWN RISK!!! *** Changes include: Major rework of sensor-related infrastructure. Includes rewriting sensor classes to implement synchronous I2C communication. Fix to reset Autonomous timer back to 30 seconds. Implementation of specific motor profiles for approved 12V motors (includes Tetrix, AndyMark, Matrix and REV models). Modest improvements to enhance Wi-Fi P2P pairing. Fixes telemetry log addition race. Publishes all the sources (not just a select few). Includes Block programming improvements Addition of optimized Vuforia blocks. Auto scrollbar to projects and sounds pages. Fixed blocks paste bug. Blocks execute after while-opModeIsActive loop (to allow for cleanup before exiting op mode). Added gyro integratedZValue block. Fixes bug with projects page for Firefox browser. Added IsSpeaking block to AndroidTextToSpeech. Implements support for the REV Robotics Expansion Hub Implements support for integral REV IMU (physically installed on I2C bus 0, uses same Bosch BNO055 9 axis absolute orientation sensor as Adafruit 9DOF abs orientation sensor). - Implements support for REV color/range/light sensor. Provides support to update Expansion Hub firmware through FTC SDK. Detects REV firmware version and records in log file. Includes support for REV Control Hub (note that the REV Control Hub is not yet approved for FTC use). Implements FTC Blocks programming support for REV Expansion Hub and sensor hardware. Detects and alerts when I2C device disconnect. Version 2.62 (built on 17.01.07) Added null pointer check before calling modeToByte() in finishModeSwitchIfNecessary method for ModernRoboticsUsbDcMotorController class. Changes to enhance Modern Robotics USB protocol robustness. Version 2.61 (released on 16.12.19) Blocks Programming mode changes: Fix to correct issue when an exception was thrown because an OpticalDistanceSensor object appears twice in the hardware map (the second time as a LightSensor). Version 2.6 (released on 16.12.16) Fixes for Gyro class: Improve (decrease) sensor refresh latency. fix isCalibrating issues. Blocks Programming mode changes: Blocks now ignores a device in the configuration xml if the name is empty. Other devices work in configuration work fine. Version 2.5 (internal release on released on 16.12.13) Blocks Programming mode changes: Added blocks support for AdafruitBNO055IMU. Added Download Op Mode button to FtcBocks.html. Added support for copying blocks in one OpMode and pasting them in an other OpMode. The clipboard content is stored on the phone, so the programming mode server must be running. Modified Utilities section of the toolbox. In Programming Mode, display information about the active connections. Fixed paste location when workspace has been scrolled. Added blocks support for the android Accelerometer. Fixed issue where Blocks Upload Op Mode truncated name at first dot. Added blocks support for Android SoundPool. Added type safety to blocks for Acceleration. Added type safety to blocks for AdafruitBNO055IMU.Parameters. Added type safety to blocks for AnalogInput. Added type safety to blocks for AngularVelocity. Added type safety to blocks for Color. Added type safety to blocks for ColorSensor. Added type safety to blocks for CompassSensor. Added type safety to blocks for CRServo. Added type safety to blocks for DigitalChannel. Added type safety to blocks for ElapsedTime. Added type safety to blocks for Gamepad. Added type safety to blocks for GyroSensor. Added type safety to blocks for IrSeekerSensor. Added type safety to blocks for LED. Added type safety to blocks for LightSensor. Added type safety to blocks for LinearOpMode. Added type safety to blocks for MagneticFlux. Added type safety to blocks for MatrixF. Added type safety to blocks for MrI2cCompassSensor. Added type safety to blocks for MrI2cRangeSensor. Added type safety to blocks for OpticalDistanceSensor. Added type safety to blocks for Orientation. Added type safety to blocks for Position. Added type safety to blocks for Quaternion. Added type safety to blocks for Servo. Added type safety to blocks for ServoController. Added type safety to blocks for Telemetry. Added type safety to blocks for Temperature. Added type safety to blocks for TouchSensor. Added type safety to blocks for UltrasonicSensor. Added type safety to blocks for VectorF. Added type safety to blocks for Velocity. Added type safety to blocks for VoltageSensor. Added type safety to blocks for VuforiaLocalizer.Parameters. Added type safety to blocks for VuforiaTrackable. Added type safety to blocks for VuforiaTrackables. Added type safety to blocks for enums in AdafruitBNO055IMU.Parameters. Added type safety to blocks for AndroidAccelerometer, AndroidGyroscope, AndroidOrientation, and AndroidTextToSpeech. Version 2.4 (released on 16.11.13) Fix to avoid crashing for nonexistent resources. Blocks Programming mode changes: Added blocks to support OpenGLMatrix, MatrixF, and VectorF. Added blocks to support AngleUnit, AxesOrder, AxesReference, CameraDirection, CameraMonitorFeedback, DistanceUnit, and TempUnit. Added blocks to support Acceleration. Added blocks to support LinearOpMode.getRuntime. Added blocks to support MagneticFlux and Position. Fixed typos. Made blocks for ElapsedTime more consistent with other objects. Added blocks to support Quaternion, Velocity, Orientation, AngularVelocity. Added blocks to support VuforiaTrackables, VuforiaTrackable, VuforiaLocalizer, VuforiaTrackableDefaultListener. Fixed a few blocks. Added type checking to new blocks. Updated to latest blockly. Added default variable blocks to navigation and matrix blocks. Fixed toolbox entry for openGLMatrix_rotation_withAxesArgs. When user downloads Blocks-generated op mode, only the .blk file is downloaded. When user uploads Blocks-generated op mode (.blk file), Javascript code is auto generated. Added DbgLog support. Added logging when a blocks file is read/written. Fixed bug to properly render blocks even if missing devices from configuration file. Added support for additional characters (not just alphanumeric) for the block file names (for download and upload). Added support for OpMode flavor (“Autonomous” or “TeleOp”) and group. Changes to Samples to prevent tutorial issues. Incorporated suggested changes from public pull 216 (“Replace .. paths”). Remove Servo Glitches when robot stopped. if user hits “Cancels” when editing a configuration file, clears the unsaved changes and reverts to original unmodified configuration. Added log info to help diagnose why the Robot Controller app was terminated (for example, by watch dog function). Added ability to transfer log from the controller. Fixed inconsistency for AngularVelocity Limit unbounded growth of data for telemetry. If user does not call telemetry.update() for LinearOpMode in a timely manner, data added for telemetry might get lost if size limit is exceeded. Version 2.35 (released on 16.10.06) Blockly programming mode - Removed unnecesary idle() call from blocks for new project. Version 2.30 (released on 16.10.05) Blockly programming mode: Mechanism added to save Blockly op modes from Programming Mode Server onto local device To avoid clutter, blocks are displayed in categorized folders Added support for DigitalChannel Added support for ModernRoboticsI2cCompassSensor Added support for ModernRoboticsI2cRangeSensor Added support for VoltageSensor Added support for AnalogInput Added support for AnalogOutput Fix for CompassSensor setMode block Vuforia Fix deadlock / make camera data available while Vuforia is running. Update to Vuforia 6.0.117 (recommended by Vuforia and Google to close security loophole). Fix for autonomous 30 second timer bug (where timer was in effect, even though it appeared to have timed out). opModeIsActive changes to allow cleanup after op mode is stopped (with enforced 2 second safety timeout). Fix to avoid reading i2c twice. Updated sample Op Modes. Improved logging and fixed intermittent freezing. Added digital I/O sample. Cleaned up device names in sample op modes to be consistent with Pushbot guide. Fix to allow use of IrSeekerSensorV3. Version 2.20 (released on 16.09.08) Support for Modern Robotics Compass Sensor. Support for Modern Robotics Range Sensor. Revise device names for Pushbot templates to match the names used in Pushbot guide. Fixed bug so that IrSeekerSensorV3 device is accessible as IrSeekerSensor in hardwareMap. Modified computer vision code to require an individual Vuforia license (per legal requirement from PTC). Minor fixes. Blockly enhancements: Support for Voltage Sensor. Support for Analog Input. Support for Analog Output. Support for Light Sensor. Support for Servo Controller. Version 2.10 (released on 16.09.03) Support for Adafruit IMU. Improvements to ModernRoboticsI2cGyro class Block on reset of z axis. isCalibrating() returns true while gyro is calibration. Updated sample gyro program. Blockly enhancements support for android.graphics.Color. added support for ElapsedTime. improved look and legibility of blocks. support for compass sensor. support for ultrasonic sensor. support for IrSeeker. support for LED. support for color sensor. support for CRServo prompt user to configure robot before using programming mode. Provides ability to disable audio cues. various bug fixes and improvements. Version 2.00 (released on 16.08.19) This is the new release for the upcoming 2016-2017 FIRST Tech Challenge Season. Channel change is enabled in the FTC Robot Controller app for Moto G 2nd and 3rd Gen phones. Users can now use annotations to register/disable their Op Modes. Changes in the Android SDK, JDK and build tool requirements (minsdk=19, java 1.7, build tools 23.0.3). Standardized units in analog input. Cleaned up code for existing analog sensor classes. setChannelMode and getChannelMode were REMOVED from the DcMotorController class. This is important - we no longer set the motor modes through the motor controller. setMode and getMode were added to the DcMotor class. ContinuousRotationServo class has been added to the FTC SDK. Range.clip() method has been overloaded so it can support this operation for int, short and byte integers. Some changes have been made (new methods added) on how a user can access items from the hardware map. Users can now set the zero power behavior for a DC motor so that the motor will brake or float when power is zero. Prototype Blockly Programming Mode has been added to FTC Robot Controller. Users can place the Robot Controller into this mode, and then use a device (such as a laptop) that has a Javascript enabled browser to write Blockly-based Op Modes directly onto the Robot Controller. Users can now configure the robot remotely through the FTC Driver Station app. Android Studio project supports Android Studio 2.1.x and compile SDK Version 23 (Marshmallow). Vuforia Computer Vision SDK integrated into FTC SDK. Users can use sample vision targets to get localization information on a standard FTC field. Project structure has been reorganized so that there is now a TeamCode package that users can use to place their local/custom Op Modes into this package. Inspection function has been integrated into the FTC Robot Controller and Driver Station Apps (Thanks Team HazMat… 9277 & 10650!). Audio cues have been incorporated into FTC SDK. Swap mechanism added to FTC Robot Controller configuration activity. For example, if you have two motor controllers on a robot, and you misidentified them in your configuration file, you can use the Swap button to swap the devices within the configuration file (so you do not have to manually re-enter in the configuration info for the two devices). Fix mechanism added to all user to replace an electronic module easily. For example, suppose a servo controller dies on your robot. You replace the broken module with a new module, which has a different serial number from the original servo controller. You can use the Fix button to automatically reconfigure your configuration file to use the serial number of the new module. Improvements made to fix resiliency and responsiveness of the system. For LinearOpMode the user now must for a telemetry.update() to update the telemetry data on the driver station. This update() mechanism ensures that the driver station gets the updated data properly and at the same time. The Auto Configure function of the Robot Controller is now template based. If there is a commonly used robot configuration, a template can be created so that the Auto Configure mechanism can be used to quickly configure a robot of this type. The logic to detect a runaway op mode (both in the LinearOpMode and OpMode types) and to abort the run, then auto recover has been improved/implemented. Fix has been incorporated so that Logitech F310 gamepad mappings will be correct for Marshmallow users. Release 16.07.08 For the ftc_app project, the gradle files have been modified to support Android Studio 2.1.x. Release 16.03.30 For the MIT App Inventor, the design blocks have new icons that better represent the function of each design component. Some changes were made to the shutdown logic to ensure the robust shutdown of some of our USB services. A change was made to LinearOpMode so as to allow a given instance to be executed more than once, which is required for the App Inventor. Javadoc improved/updated. Release 16.03.09 Changes made to make the FTC SDK synchronous (significant change!) waitOneFullHardwareCycle() and waitForNextHardwareCycle() are no longer needed and have been deprecated. runOpMode() (for a LinearOpMode) is now decoupled from the system's hardware read/write thread. loop() (for an OpMode) is now decoupled from the system's hardware read/write thread. Methods are synchronous. For example, if you call setMode(DcMotorController.RunMode.RESET_ENCODERS) for a motor, the encoder is guaranteed to be reset when the method call is complete. For legacy module (NXT compatible), user no longer has to toggle between read and write modes when reading from or writing to a legacy device. Changes made to enhance reliability/robustness during ESD event. Changes made to make code thread safe. Debug keystore added so that user-generated robot controller APKs will all use the same signed key (to avoid conflicts if a team has multiple developer laptops for example). Firmware version information for Modern Robotics modules are now logged. Changes made to improve USB comm reliability and robustness. Added support for voltage indicator for legacy (NXT-compatible) motor controllers. Changes made to provide auto stop capabilities for op modes. A LinearOpMode class will stop when the statements in runOpMode() are complete. User does not have to push the stop button on the driver station. If an op mode is stopped by the driver station, but there is a run away/uninterruptible thread persisting, the app will log an error message then force itself to crash to stop the runaway thread. Driver Station UI modified to display lowest measured voltage below current voltage (12V battery). Driver Station UI modified to have color background for current voltage (green=good, yellow=caution, red=danger, extremely low voltage). javadoc improved (edits and additional classes). Added app build time to About activity for driver station and robot controller apps. Display local IP addresses on Driver Station About activity. Added I2cDeviceSynchImpl. Added I2cDeviceSync interface. Added seconds() and milliseconds() to ElapsedTime for clarity. Added getCallbackCount() to I2cDevice. Added missing clearI2cPortActionFlag. Added code to create log messages while waiting for LinearOpMode shutdown. Fix so Wifi Direct Config activity will no longer launch multiple times. Added the ability to specify an alternate i2c address in software for the Modern Robotics gyro. Release 16.02.09 Improved battery checker feature so that voltage values get refreshed regularly (every 250 msec) on Driver Station (DS) user interface. Improved software so that Robot Controller (RC) is much more resilient and “self-healing” to USB disconnects: If user attempts to start/restart RC with one or more module missing, it will display a warning but still start up. When running an op mode, if one or more modules gets disconnected, the RC & DS will display warnings,and robot will keep on working in spite of the missing module(s). If a disconnected module gets physically reconnected the RC will auto detect the module and the user will regain control of the recently connected module. Warning messages are more helpful (identifies the type of module that’s missing plus its USB serial number). Code changes to fix the null gamepad reference when users try to reference the gamepads in the init() portion of their op mode. NXT light sensor output is now properly scaled. Note that teams might have to readjust their light threshold values in their op modes. On DS user interface, gamepad icon for a driver will disappear if the matching gamepad is disconnected or if that gamepad gets designated as a different driver. Robot Protocol (ROBOCOL) version number info is displayed in About screen on RC and DS apps. Incorporated a display filter on pairing screen to filter out devices that don’t use the “-“ format. This filter can be turned off to show all WiFi Direct devices. Updated text in License file. Fixed formatting error in OpticalDistanceSensor.toString(). Fixed issue on with a blank (“”) device name that would disrupt WiFi Direct Pairing. Made a change so that the WiFi info and battery info can be displayed more quickly on the DS upon connecting to RC. Improved javadoc generation. Modified code to make it easier to support language localization in the future. Release 16.01.04 Updated compileSdkVersion for apps Prevent Wifi from entering power saving mode removed unused import from driver station Corrrected "Dead zone" joystick code. LED.getDeviceName and .getConnectionInfo() return null apps check for ROBOCOL_VERSION mismatch Fix for Telemetry also has off-by-one errors in its data string sizing / short size limitations error User telemetry output is sorted. added formatting variants to DbgLog and RobotLog APIs code modified to allow for a long list of op mode names. changes to improve thread safety of RobocolDatagramSocket Fix for "missing hardware leaves robot controller disconnected from driver station" error fix for "fast tapping of Init/Start causes problems" (toast is now only instantiated on UI thread). added some log statements for thread life cycle. moved gamepad reset logic inside of initActiveOpMode() for robustness changes made to mitigate risk of race conditions on public methods. changes to try and flag when WiFi Direct name contains non-printable characters. fix to correct race condition between .run() and .close() in ReadWriteRunnableStandard. updated FTDI driver made ReadWriteRunnableStanard interface public. fixed off-by-one errors in Command constructor moved specific hardware implmentations into their own package. moved specific gamepad implemnatations to the hardware library. changed LICENSE file to new BSD version. fixed race condition when shutting down Modern Robotics USB devices. methods in the ColorSensor classes have been synchronized. corrected isBusy() status to reflect end of motion. corrected "back" button keycode. the notSupported() method of the GyroSensor class was changed to protected (it should not be public). Release 15.11.04.001 Added Support for Modern Robotics Gyro. The GyroSensor class now supports the MR Gyro Sensor. Users can access heading data (about Z axis) Users can also access raw gyro data (X, Y, & Z axes). Example MRGyroTest.java op mode included. Improved error messages More descriptive error messages for exceptions in user code. Updated DcMotor API Enable read mode on new address in setI2cAddress Fix so that driver station app resets the gamepads when switching op modes. USB-related code changes to make USB comm more responsive and to display more explicit error messages. Fix so that USB will recover properly if the USB bus returns garbage data. Fix USB initializtion race condition. Better error reporting during FTDI open. More explicit messages during USB failures. Fixed bug so that USB device is closed if event loop teardown method was not called. Fixed timer UI issue Fixed duplicate name UI bug (Legacy Module configuration). Fixed race condition in EventLoopManager. Fix to keep references stable when updating gamepad. For legacy Matrix motor/servo controllers removed necessity of appending "Motor" and "Servo" to controller names. Updated HT color sensor driver to use constants from ModernRoboticsUsbLegacyModule class. Updated MR color sensor driver to use constants from ModernRoboticsUsbDeviceInterfaceModule class. Correctly handle I2C Address change in all color sensors Updated/cleaned up op modes. Updated comments in LinearI2cAddressChange.java example op mode. Replaced the calls to "setChannelMode" with "setMode" (to match the new of the DcMotor method). Removed K9AutoTime.java op mode. Added MRGyroTest.java op mode (demonstrates how to use MR Gyro Sensor). Added MRRGBExample.java op mode (demonstrates how to use MR Color Sensor). Added HTRGBExample.java op mode (demonstrates how to use HT legacy color sensor). Added MatrixControllerDemo.java (demonstrates how to use legacy Matrix controller). Updated javadoc documentation. Updated release .apk files for Robot Controller and Driver Station apps. Release 15.10.06.002 Added support for Legacy Matrix 9.6V motor/servo controller. Cleaned up build.gradle file. Minor UI and bug fixes for driver station and robot controller apps. Throws error if Ultrasonic sensor (NXT) is not configured for legacy module port 4 or 5. Release 15.08.03.001 New user interfaces for FTC Driver Station and FTC Robot Controller apps. An init() method is added to the OpMode class. For this release, init() is triggered right before the start() method. Eventually, the init() method will be triggered when the user presses an "INIT" button on driver station. The init() and loop() methods are now required (i.e., need to be overridden in the user's op mode). The start() and stop() methods are optional. A new LinearOpMode class is introduced. Teams can use the LinearOpMode mode to create a linear (not event driven) program model. Teams can use blocking statements like Thread.sleep() within a linear op mode. The API for the Legacy Module and Core Device Interface Module have been updated. Support for encoders with the Legacy Module is now working. The hardware loop has been updated for better performance.
GitHub Repo https://github.com/atabeyaydi/Intel-Verilog-HDL-Basics

atabeyaydi/Intel-Verilog-HDL-Basics

This instructor-led class is taught in a virtual classroom over 2 half days of instruction. You will use a remote computer connected through webex for labs. No setup is needed. The remote computer connection does require that you are logged in using a computer running Windows.
GitHub Repo https://github.com/keshavbhatt/kmusicplay

keshavbhatt/kmusicplay

Your entire music and video collection in one place. Play any audio / video file without any obstacle. kMusicplay support literally any type of music file, from HD or lossless files (like FLAC, ALAC, WAV, etc), to popular compressed or lossy files (like MP3, AAC, etc). kMusicplay also support all video formats and play them seamlessly with the all new Video mode. kMusicplay is elegant ,powerful, with so many controls . Most Important feature kMusicplay is lightweight app is totally written in Qml and uses Ubuntu touch UI components to draw GUI hence most lightweight and fast GUI based media player ever . In App animation and transitions takes the media player to new level . You can save Last Played Tracks so you never need to load tracks again and again , kMusicplay grabs Album art , Lyrics and other details of currently playing song on the fly with its all new metadata interpretor Klyric Engine beta , so many other features like slide to remove song from play-list , Playlist Quick Filter, with all basic features a music player have are available. If you love app and want more features please give five stars and provide your features request and feedbacks by commenting after installing app. If for some reasons app didn't work properly then provide the feedbacks by emailing me. Thanks,
GitHub Repo https://github.com/ZulqarnainZilli/-9-Email-Marketing-Tips-For-Content-Marketers

ZulqarnainZilli/-9-Email-Marketing-Tips-For-Content-Marketers

9 Email Marketing Tips For Content Marketers Even “agnostics” regarding email marketing can't hash out the following evidence - the average ROI from this promotional practice is close to 3,800%. Measureless opportunities to scale up and relative cheapness, compared to other reaching-out channels, are the two reasons why the email marketing is fair-haired by businesses. However, this is not about the price and physical extent alone. The chief advantage is a better alignment of communication with customers. If you hope a certain content strategy brings desirable results, overlooking the quality of mailing messages will be a sorry pitfall. Always keep in mind that newsletters, welcome, retention, and other emails are not just a brand's facade - but a powerful tool for generating conversions. By joining sides of email and content strategies, you can come up with synergy from both. In this guide, we’ll cover a few recommendations for content marketers on how to write email messages that work. Tips for email marketing Segment your list Split the batch of email recipients into smaller groups based on chosen criteria, and mail distinct relevant messages - for each. You can use recipients' GEO, demographic characteristics, or purchase history to distinguish homogeneous clusters and proceed with the content planning. Segmentation is the basic premise for personalization, and if you still doubt why bothering about the latter - here are just a few numbers we took from Instapage: 52% of customers claim they do care if the message was tailor-made or not 82% of marketers say that mail personalization increases the open ratio custom emails have 41% more unique clicks than mass-produced ones. To avoid a fragmented approach, use data from CRMs, website analytics tools, and other sources to define segments. Concerning phrasings, a good idea is to create Buyer personas profiles. Thus, you'll be able to choose the appropriate message length and wording. Say, design a newsletter to promote paid subscription for an email validator service. You've decided to distinguish corporate clients based on their company size and determined the following groups: #1 - B2Bs and #2 - sole entrepreneurs. Possible messages for the two: #1. Our "XXL" plan is perfect for agencies and enterprises. One can add unlimited users and conduct up to 100,000 checks per month. #2. With our "S" you get 1,000 credits and 5,000 unique recipients - for only $33 per month. Plus - a 7-days free trial. Use interactive content The best content marketers know that interactive content came into vogue a long time ago. As to emails, here are the most common examples: CSS animated buttons If you include CTAs buttons (that we hope you do) - liven them up a bit. Add an animated hover effect, so that every time a recipient puts a cursor on a button, it changes shape, shade, color, or text. “Add hover to emphasise objects”, source This shouldn’t necessarily be something dramatic - add tiny accents that will yet grab the user's attention. starring “Add a star rating component to engage readers with content”, source Including ranking or reviewing widgets in the email body is one of the most working ways to engage the reader with the message. Ask recipients to assess your product or service with stars. Add the link to Google Forms if you want to receive an extended opinion on overall customer satisfaction. pictures' rollovers “Use animated images to describe goods better”, source The effect is eagerly used by the ones who promote online stores. Using The rollover allows to show goods from different angles or even play with recipients, if relevant. Take into account that this feature only works on desktops - mobile mail users will see the very first picture only. images carousel “Add pieces of text directly on images”, source If you want to enhance goods cards with descriptive content, say - price and shipping details, use a carousel instead of a rollover. As so, you can add more info pictures to the email body and, hopefully, convert more recipients into customers. a countdown “Countdowns work well for limited in time offers”, source Again, this type of interactive content fits the online shopping niche. Animated clocks amplify urgency and theoretically increase conversions. But it's important to stay extremely careful and not to sound desperate - otherwise, the newsletter will end up in the recipient's "Spam". Improve design The attractiveness of an email is something granted on certain terms, indeed. Not all emails need to be flashy or include expensive designs. However, there are some prevailing common trends in the matter. By following them, you seem to show the recipient that your company is moving in step with the times, and not stuck in the 2000s. Here's the shortlist from the TOP email design trends list that a 99designs provides - as of 2021: magazine-styled “Make newsletters to look a bit editorial”, source More and more newsletters tend to look like a centerfold from good old printed media. With a strict following to the "Less is more" principle - clear fonts, short phrases, HD-quality images with a few objects on them, and short CTAs. hand-made illustrations “Unique pictures create a distinct flavour of your brand”, source Tailored icons or sketchy images - whatever fits your mailing purpose, just make sure it's not too bright, contrast, or overloaded with details. Give preference to clean colors. skeuomorphic objects This is when a design resembles a real object. To see an example - just open a reader App on your smartphone. “A skeuomorphic bookshelf”, source HD photographies “If you operate in the luxury segment, do not skimp on email visuals”, source These are expensive content, but if you work in fashion or other chick industries - it may be worth the effort. animated content Yeap, we've covered this in a previous tip. single scroll “Looks especially good on smartphones”, source Place the entire email content, including buttons, on the endless-looking long frame. Focus on conversions Stay focused on what's your mailing purpose. Don't forget that everybody expects to see a good ROI from email actions at the end of the reporting period. Craft effective CTAs - perceive these not as a sole button with a "Download now" text or so, but as an entire sense of a message that you write. To create a captivating CTA copy, adhere to the below advices: include win-win propositions Even though you’re not providing a customer with a discount or cash refund at the moment, your proposition may include a non-monetary incentive. New arrivals, selection of the latest news, free copies, advice from experts - the only rule here is to offer what’ll hold in high esteem. trigger on emotions Don't long-windedly list benefits. Instead, simulate a life situation and show how your product or service can help. use several CTAs throughout the email Email body may be viewed in several scrolls, especially when via small mobile devices’ screens. If you add a call to action at the beginning of the message, a mere number of users will get back to it after finishing reading the content. Thus, you may lose potential conversion. Include several buttons throughout the email body, but don’t sound repeatedly - change calls’ forms and wording. Encourage readers to reply Driving recipients to reply is challenging yet able to be done. First, choose the proper writing tone. According to an extensive study of emails that didn’t get a response, the most preferable is a 3rd-grade reading level. “Too elementary or too proficient tone may scare away readers”, source Of course, you must apply this recommendation with an eye on the recipient. If you mail to a professor or a government agency, a “3rd-grade” rule isn’t applicable. But all else being equal - simplify the lexicon to the level a schoolchild can understand it. Another trick is to sound overall happy. Emails that are enhanced with positive emotions get 10-15% more replies, on average than neutral ones. The best manner is to choose a slightly warm tone. Exaggerated excitement may look weird and even suspicious, especially when reaching out to business partners. And don’t forget about courtesy. A rare person will respond if you address him or her with a hair-raising “To whom it may concern” phrase. Make it personal Personification shouldn’t be confused with personalization. The second is rather about mailing fitting content from a commercial perspective, while the first term - about addressing the recipient as a one-off personality. Personal emails start with the recipient’s name - and no other way. They include references to the user's interests or past actions. For example, if your tourist agency’s client is interested in island vacations - you shall approach him or her with respective offers. They also shall contain personalized promotions, if any. The best way to expand this approach on hundreds or thousands of recipients is to launch trigger-based email campaigns. Create delivery scenarios for different segments or stages of a sales pipeline. Then prepare a fitting sequence of relevant content - for every single scenario. To give a human face to mailing, one can practice greetings, as well. Birthdays, state holidays, anniversaries, a new status in the loyalty system - there are a lot of examples of what one may congratulate the customer with. Keep your emails out of spam folders It is better not to launch mailing at all than to use an untrustworthy emails’ database. The risks are much higher than a slew of undelivered messages - from harming a sender's reputation to being banned by mailing systems. So it's better to stay proactive: tidy away broken, misspelled, temporary, or other worrisome emails from the database - either manually or with the help of software collect a valid email address only - through email finders avoid spam-trigger words establish a double opt-in validation set the correct mailing frequency. Make sure your emails look clean and crisp Newsletters shall afterall bring revenues - whether you want it or not. But in a bid of quantity, don’t lose the overall content integrity and sense: a subject line, pre-header, header, email body, and calls shall be consistent with one another the copy must be of the proper size; although the length depends on many factors, stick to an “ideal” interval - 50 to 125 words if can, don’t attach too many files or links to external websites - mailing filters are suspicious to these adapt the layout to fit smaller screens - nothing looks worse than broken email elements when you open it on mobile. Wrapping up It doesn't make much difference whether you create mailing content for personal or business purposes - these email marketing tips will serve both. No strains here - the recipient’s interest should be at your forefront. If you can hook him or her with the content by using tricks we've covered, you’ll never fail with enough conversions.