From 0c94f81f769d3c7377811a584f647553ebe7ceaf Mon Sep 17 00:00:00 2001 From: matitaweb Date: Mon, 8 Apr 2013 11:53:15 +0000 Subject: [PATCH] commit by user andrea --- weblib/While/syntax.ma | 58 +++++++++++++++++++++++++++++++++++++ weblib/prova.ma | 1 + weblib/tutorial/chapter9.ma | 50 ++++++++++++++++---------------- 3 files changed, 84 insertions(+), 25 deletions(-) create mode 100644 weblib/While/syntax.ma create mode 100644 weblib/prova.ma diff --git a/weblib/While/syntax.ma b/weblib/While/syntax.ma new file mode 100644 index 000000000..b55d89d43 --- /dev/null +++ b/weblib/While/syntax.ma @@ -0,0 +1,58 @@ +(* While Syntax *) + +include "basics/logic.ma". +include "basics/types.ma". +include "basics/bool.ma". +include "arithmetics/nat.ma". + +(* Variables *) + +inductive Var : Type[0] ≝ + Id : nat → Var. + +(* Arithmetic expressions *) + +inductive Aexp : Type[0] ≝ + | Const : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → Aexp + | Aid : span style="text-decoration: underline;"/spanVar → Aexp + | Add : Aexp → Aexp → Aexp + | Sub : Aexp → Aexp → Aexp + | Mul : Aexp → Aexp → Aexp + | Div : Aexp → Aexp → Aexp + | Mod : Aexp → Aexp → Aexp + . + +interpretation "Aexp plus" 'plus x y = (Add x y). +interpretation "Aexp minus" 'plus x y = (Sub x y). +interpretation "Aexp times" 'times x y = (Mul x y). + +(* Boolean expressions *) +inductive Bexp : Type[0] ≝ + | BFalse : Bexp + | BTtrue : Bexp + | BNot : Bexp → Bexp + | BAnd : Bexp → Bexp → Bexp + | BOr : Bexp → Bexp → Bexp + | Eq : a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → Bexp + | LE : a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → Bexp +. + +interpretation "Bexp not" 'not x = (BNot x). +interpretation "Bexp and" 'and x y = (BAnd x y). +interpretation "Bexp or" 'or x y = (BOr x y). +interpretation "Bexp 'less or equal to'" 'leq x y = (LE x y). + +(* Commands *) +inductive Cmd : Type[0] ≝ + | Skip : Cmd + | Assign : Var → a href="cic:/matita/While/syntax/Aexp.ind(1,0,0)"Aexp/a → Cmd + | Seq : Cmd → Cmd → Cmd + | If : a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"Bexp/a → Cmd → Cmd → Cmd + | While : a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"Bexp/a → Cmd → Cmd +. + +notation "hvbox(c1 break ; c2)" + left associative with precedence 47 for @{Seq $c1 $c2}. + +notation "hvbox(var break <- val)" + left associative with precedence 48 for @{Assign $var $val}. \ No newline at end of file diff --git a/weblib/prova.ma b/weblib/prova.ma new file mode 100644 index 000000000..5fe5dcee7 --- /dev/null +++ b/weblib/prova.ma @@ -0,0 +1 @@ +(* new script *) \ No newline at end of file diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma index 51fe4a402..ba759d47c 100644 --- a/weblib/tutorial/chapter9.ma +++ b/weblib/tutorial/chapter9.ma @@ -11,9 +11,9 @@ lifted operators of the previous section: include "tutorial/chapter8.ma". -img class="anchor" src="icons/tick.png" id="move"let rec move (S: a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (x:S) (E: a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S) on E : a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S ≝ +let rec move (S: a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (x:S) (E: a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S) on E : a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S ≝ match E with - [ pz ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"pz/a S, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a + [ pz ⇒ 〈a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"pz/a S, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a | pe ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem epsilon" href="cic:/fakeuri.def(1)"ϵ/a, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a | ps y ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem ps" href="cic:/fakeuri.def(1)"`/ay, a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a | pp y ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pitem ps" href="cic:/fakeuri.def(1)"`/ay, x a title="eqb" href="cic:/fakeuri.def(1)"=/aa title="eqb" href="cic:/fakeuri.def(1)"=/a y a title="Pair construction" href="cic:/fakeuri.def(1)"〉/a @@ -21,15 +21,15 @@ include "tutorial/chapter8.ma". | pc e1 e2 ⇒ (move ? x e1) a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a (move ? x e2) | pk e ⇒ (move ? x e)a title="lk" href="cic:/fakeuri.def(1)"^/aa title="lk" href="cic:/fakeuri.def(1)"⊛/a ]. -img class="anchor" src="icons/tick.png" id="move_plus"lemma move_plus: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀x:S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. +lemma move_plus: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀x:S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S x (i1 a title="pitem or" href="cic:/fakeuri.def(1)"+/a i2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? x i1) a title="oplus" href="cic:/fakeuri.def(1)"⊕/a (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? x i2). // qed. -img class="anchor" src="icons/tick.png" id="move_cat"lemma move_cat: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀x:S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. +lemma move_cat: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀x:S.∀i1,i2:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S x (i1 a title="pitem cat" href="cic:/fakeuri.def(1)"·/a i2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? x i1) a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? x i2). // qed. -img class="anchor" src="icons/tick.png" id="move_star"lemma move_star: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀x:S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. +lemma move_star: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀x:S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S x ia title="pitem star" href="cic:/fakeuri.def(1)"^/aa title="pitem star" href="cic:/fakeuri.def(1)"*/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? x i)a title="lk" href="cic:/fakeuri.def(1)"^/aa title="lk" href="cic:/fakeuri.def(1)"⊛/a. // qed. @@ -52,13 +52,13 @@ while the other point reaches the end of b* and must go back through b*a: *) -img class="anchor" src="icons/tick.png" id="pmove"definition pmove ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λx:S.λe:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? x (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e). +definition pmove ≝ λS:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λx:S.λe:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? x (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e). -img class="anchor" src="icons/tick.png" id="pmove_def"lemma pmove_def : ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀x:S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀b. +lemma pmove_def : ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀x:S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀b. a href="cic:/matita/tutorial/chapter9/pmove.def(7)"pmove/a ? x a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ai,ba title="Pair construction" href="cic:/fakeuri.def(1)"〉/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? x i. // qed. -img class="anchor" src="icons/tick.png" id="eq_to_eq_hd"lemma eq_to_eq_hd: ∀A.∀l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀a,b. +lemma eq_to_eq_hd: ∀A.∀l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀a,b. aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ba title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/al2 → a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b. #A #l1 #l2 #a #b #H destruct // qed. @@ -66,7 +66,7 @@ qed. (* Obviously, a move does not change the carrier of the item, as one can easily prove by induction on the item. *) -img class="anchor" src="icons/tick.png" id="same_kernel"lemma same_kernel: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀a:S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. +lemma same_kernel: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀a:S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? a i)a title="forget" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="forget" href="cic:/fakeuri.def(1)"|/aia title="forget" href="cic:/fakeuri.def(1)"|/a. #S #a #i elim i // [#i1 #i2 #H1 #H2 >a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"move_cat/a >a href="cic:/matita/tutorial/chapter8/erase_odot.def(7)"erase_odot/a // @@ -77,7 +77,7 @@ qed. (* Here is our first, major result, stating the correctness of the move operation. The proof is a simple induction on i. *) -img class="anchor" src="icons/tick.png" id="move_ok"theorem move_ok: +theorem move_ok: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀a:S.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S.∀w: a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S. a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a ? a ia title="in_prl" href="cic:/fakeuri.def(1)"}/a w a title="iff" href="cic:/fakeuri.def(1)"↔/a a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{ia title="in_pl" href="cic:/fakeuri.def(1)"}/a (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aw). #S #a #i elim i @@ -107,39 +107,39 @@ qed. notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}. -img class="anchor" src="icons/tick.png" id="moves"let rec moves (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) w e on w : a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S ≝ +let rec moves (S : a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) w e on w : a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S ≝ match w with [ nil ⇒ e | cons x w' ⇒ w' ↦* (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S x (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e))]. -img class="anchor" src="icons/tick.png" id="moves_empty"lemma moves_empty: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. +lemma moves_empty: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? a title="nil" href="cic:/fakeuri.def(1)"[/a a title="nil" href="cic:/fakeuri.def(1)"]/a e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a e. // qed. -img class="anchor" src="icons/tick.png" id="moves_cons"lemma moves_cons: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀a:S.∀w.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. +lemma moves_cons: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀a:S.∀w.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? (aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aw) e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w (a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e)). // qed. -img class="anchor" src="icons/tick.png" id="moves_left"lemma moves_left : ∀S,a,w,e. +lemma moves_left : ∀S,a,w,e. a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S (wa title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aa title="nil" href="cic:/fakeuri.def(1)"[/aa title="nil" href="cic:/fakeuri.def(1)"]/a)) e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e)). #S #a #w elim w // #x #tl #Hind #e >a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"moves_cons/a >a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"moves_cons/a // qed. -img class="anchor" src="icons/tick.png" id="not_epsilon_sem"lemma not_epsilon_sem: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀a:S.∀w: a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S. ∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. +lemma not_epsilon_sem: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀a:S.∀w: a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S. ∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. a href="cic:/matita/basics/logic/iff.def(1)"iff/a ((aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aw) a title="in_prl mem" href="cic:/fakeuri.def(1)"∈/a e) ((aa title="cons" href="cic:/fakeuri.def(1)":/aa title="cons" href="cic:/fakeuri.def(1)":/aw) a title="in_pl mem" href="cic:/fakeuri.def(1)"∈/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e). #S #a #w * #i #b cases b normalize [% /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/ * // #H destruct |% normalize /span class="autotactic"2span class="autotrace" trace /span/span/] qed. -img class="anchor" src="icons/tick.png" id="same_kernel_moves"lemma same_kernel_moves: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀w.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. +lemma same_kernel_moves: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀w.∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e)a title="forget" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a ea title="forget" href="cic:/fakeuri.def(1)"|/a. #S #w elim w // qed. -img class="anchor" src="icons/tick.png" id="decidable_sem"theorem decidable_sem: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀w: a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S. ∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. +theorem decidable_sem: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀w: a href="cic:/matita/tutorial/chapter6/word.def(3)"word/a S. ∀e:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a (a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a ? w e) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) a title="iff" href="cic:/fakeuri.def(1)"↔/a a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{ea title="in_prl" href="cic:/fakeuri.def(1)"}/a w. #S #w elim w - [* #i #b >a href="cic:/matita/tutorial/chapter9/moves_empty.def(8)"moves_empty/a cases b % /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter7/true_to_epsilon.def(9)"true_to_epsilon/a/span/span/span class="error" title="error location"/span #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ + [* #i #b >a href="cic:/matita/tutorial/chapter9/moves_empty.def(8)"moves_empty/a cases b % /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter7/true_to_epsilon.def(9)"true_to_epsilon/a/span/span/ #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ |#a #w1 #Hind #e >a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"moves_cons/a @a href="cic:/matita/basics/logic/iff_trans.def(2)"iff_trans/a [||@a href="cic:/matita/basics/logic/iff_sym.def(2)"iff_sym/a @a href="cic:/matita/tutorial/chapter9/not_epsilon_sem.def(9)"not_epsilon_sem/a] @a href="cic:/matita/basics/logic/iff_trans.def(2)"iff_trans/a [||@a href="cic:/matita/tutorial/chapter9/move_ok.def(14)"move_ok/a] @Hind @@ -188,12 +188,12 @@ are final, while 8 and 9 are not). We conclude this chapter with a few properties of the move opertions in relation with the pit state. *) -img class="anchor" src="icons/tick.png" id="pit_pre"definition pit_pre ≝ λS.λi.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"blank/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aia title="forget" href="cic:/fakeuri.def(1)"|/a), a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a. +definition pit_pre ≝ λS.λi.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"blank/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aia title="forget" href="cic:/fakeuri.def(1)"|/a), a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/aa title="Pair construction" href="cic:/fakeuri.def(1)"〉/a. (* The following function compute the list of characters occurring in a given item i. *) -img class="anchor" src="icons/tick.png" id="occur"let rec occur (S: a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (i: a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S) on i ≝ +let rec occur (S: a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a) (i: a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"re/a S) on i ≝ match i with [ z ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a a title="nil" href="cic:/fakeuri.def(1)"]/a | e ⇒ a title="nil" href="cic:/fakeuri.def(1)"[/a a title="nil" href="cic:/fakeuri.def(1)"]/a @@ -205,7 +205,7 @@ item i. *) (* If a symbol a does not occur in i, then move(i,a) gets to the pit state. *) -img class="anchor" src="icons/tick.png" id="not_occur_to_pit"lemma not_occur_to_pit: ∀S,a.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"occur/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aia title="forget" href="cic:/fakeuri.def(1)"|/a)) a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → +lemma not_occur_to_pit: ∀S,a.∀i:a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"pitem/a S. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"occur/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aia title="forget" href="cic:/fakeuri.def(1)"|/a)) a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i. #S #a #i elim i // [#x normalize cases (aa title="eqb" href="cic:/fakeuri.def(1)"=/aa title="eqb" href="cic:/fakeuri.def(1)"=/ax) normalize // #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ @@ -221,7 +221,7 @@ qed. (* We cannot escape form the pit state. *) -img class="anchor" src="icons/tick.png" id="move_pit"lemma move_pit: ∀S,a,i. a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i. +lemma move_pit: ∀S,a,i. a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"move/a S a (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a (a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i. #S #a #i elim i // [#i1 #i2 #Hind1 #Hind2 >a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"move_cat/a >Hind1 >Hind2 // |#i1 #i2 #Hind1 #Hind2 >a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"move_plus/a >Hind1 >Hind2 // @@ -229,14 +229,14 @@ qed. ] qed. -img class="anchor" src="icons/tick.png" id="moves_pit"lemma moves_pit: ∀S,w,i. a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w (a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i. +lemma moves_pit: ∀S,w,i. a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w (a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S i. #S #w #i elim w // qed. (* If any character in w does not occur in i, then moves(i,w) gets to the pit state. *) -img class="anchor" src="icons/tick.png" id="to_pit"lemma to_pit: ∀S,w,e. a title="logical not" href="cic:/fakeuri.def(1)"¬/a a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S w (a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"occur/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a ea title="forget" href="cic:/fakeuri.def(1)"|/a)) → +lemma to_pit: ∀S,w,e. a title="logical not" href="cic:/fakeuri.def(1)"¬/a a href="cic:/matita/tutorial/chapter5/sublist.def(5)"sublist/a S w (a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"occur/a S (a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a ea title="forget" href="cic:/fakeuri.def(1)"|/a)) → a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"moves/a S w e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"pit_pre/a S (a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e). #S #w elim w [#e * #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @H normalize #a #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ @@ -247,4 +247,4 @@ to the pit state. *) |#Hfalse >a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"moves_cons/a >a href="cic:/matita/tutorial/chapter9/not_occur_to_pit.def(8)"not_occur_to_pit/a // >Hfalse /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"eqnot_to_noteq/a/span/span/ ] ] -qed. +qed. \ No newline at end of file -- 2.39.2