weblib/tutorial/chapter4.ma

   1 include "tutorial/chapter3.ma".
   2
   3 (* As a simple application of lists, let us now consider strings of characters
   4 over a given alphabet Alpha. We shall assume to have a decidable equality between
   5 characters, that is a (computable) function eqb associating a boolean value true
   6 or false to each pair of characters; eqb is correct, in the sense that (eqb x y)
   7 if and only if (x = y). The type Alpha of alphabets is hence defined by the
   8 following record *)
   9
  10 interpretation "iff" 'iff a b = (iff a b).
  11
  12 record Alpha : Type[1] ≝ { carr :> Type[0];
  13    eqb: carr → carr → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6;
  14    eqb_true: ∀x,y. (eqb x y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 (x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y)
  15 }.
  16
  17 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
  18 interpretation "eqb" 'eqb a b = (eqb ? a b).
  19
  20 definition word ≝ λS: \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S.
  21
  22 inductive re (S: \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) : Type[0] ≝
  23    zero: re S
  24  | epsilon: re S
  25  | char: S → re S
  26  | concat: re S → re S → re S
  27  | or: re S → re S → re S
  28  | star: re S → re S.
  29
  30 (* notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}. *)
  31 notation "a ^ *" non associative with precedence 90 for @{ 'kstar $a}.
  32 interpretation "star" 'kstar a = (star ? a).
  33 interpretation "or" 'plus a b = (or ? a b).
  34
  35 notation "a · b" non associative with precedence 60 for @{ 'concat $a $b}.
  36 interpretation "cat" 'concat a b = (concat ? a b).
  37
  38 (* to get rid of \middot
  39 coercion c  : ∀S:Alpha.∀p:re S.  re S →  re S   ≝ c  on _p : re ?  to ∀_:?.?. *)
  40
  41 (* notation < "a" non associative with precedence 90 for @{ 'ps $a}. *)
  42 notation "` term 90 a" non associative with precedence 90 for @{ 'atom $a}.
  43 interpretation "atom" 'atom a = (char ? a).
  44
  45 notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
  46 interpretation "epsilon" 'epsilon = (epsilon ?).
  47
  48 notation "∅" (* slash emptyv *) non associative with precedence 90 for @{ 'empty }.
  49 interpretation "empty" 'empty = (zero ?).
  50
  51 let rec flatten (S : \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) (l : \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S)) on l : \ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S ≝
  52 match l with [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] | cons w tl ⇒ w \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 flatten ? tl ].
  53
  54 let rec conjunct (S : \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) (l : \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S)) (L :\ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S → Prop) on l: Prop ≝
  55 match l with [ nil ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 | cons w tl ⇒ L w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 conjunct ? tl L ].
  56
  57 definition empty_lang ≝ λS.λw:\ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S.\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
  58 (* notation "{}" non associative with precedence 90 for @{'empty_lang}. *)
  59 interpretation "empty lang" 'empty = (empty_lang ?).
  60
  61 definition sing_lang ≝ λS.λx,w:\ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S.x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 w.
  62 notation "{: x }" non associative with precedence 90 for @{'sing_lang $x}.
  63 interpretation "sing lang" 'sing_lang x = (sing_lang ? x).
  64
  65 definition union : ∀S,L1,L2,w.Prop ≝ λS,L1,L2.λw: \ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S.L1 w \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 L2 w.
  66 interpretation "union lang" 'union a b = (union ? a b).
  67
  68 definition cat : ∀S,l1,l2,w.Prop ≝
  69   λS.λl1,l2.λw:\ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6w1,w2.w1 \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 w2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l1 w1 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 w2.
  70 interpretation "cat lang" 'concat a b = (cat ? a b).
  71
  72 definition star_lang ≝ λS.λl.λw:\ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6lw. \ 5a href="cic:/matita/tutorial/chapter4/flatten.fix(0,1,4)"\ 6flatten\ 5/a\ 6 ? lw \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/conjunct.fix(0,1,4)"\ 6conjunct\ 5/a\ 6 ? lw l.
  73 interpretation "star lang" 'kstar l = (star_lang ? l).
  74
  75 (* notation "ℓ term 70 E" non associative with precedence 75 for @{in_l ? $E}. *)
  76
  77 let rec in_l (S : \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) (r : \ 5a href="cic:/matita/tutorial/chapter4/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S) on r : \ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S → Prop ≝
  78 match r with
  79  [ zero ⇒ \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
  80  | epsilon ⇒ \ 5a title="sing lang" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6: \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] }
  81  | char x ⇒ \ 5a title="sing lang" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6: x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] }
  82  | concat r1 r2 ⇒ in_l ? r1 \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 in_l ? r2
  83  | or r1 r2 ⇒ in_l ? r1 \ 5a title="union lang" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 in_l ? r2
  84  | star r1 ⇒ (in_l ? r1)\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*
  85  ].
  86
  87 notation "ℓ term 70 E" non associative with precedence 75 for @{'in_l $E}.
  88 interpretation "in_l" 'in_l E = (in_l ? E).
  89 interpretation "in_l mem" 'mem w l = (in_l ? l w).
  90
  91 notation "a ∨ b" left associative with precedence 30 for @{'orb $a $b}.
  92 interpretation "orb" 'orb a b = (orb a b).
  93
  94 (* ndefinition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
  95 notation > "'if' term 19 e 'then' term 19 t 'else' term 19 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
  96 notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
  97 interpretation "if_then_else" 'if_then_else e t f = (if_then_else ? e t f). *)
  98
  99 inductive pitem (S: \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) : Type[0] ≝
 100  | pzero: pitem S
 101  | pepsilon: pitem S
 102  | pchar: S → pitem S
 103  | ppoint: S → pitem S
 104  | pconcat: pitem S → pitem S → pitem S
 105  | por: pitem S → pitem S → pitem S
 106  | pstar: pitem S → pitem S.
 107
 108 definition pre ≝ λS.\ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"\ 6bool\ 5/a\ 6.
 109
 110 interpretation "pstar" 'kstar a = (pstar ? a).
 111 interpretation "por" 'plus a b = (por ? a b).
 112 interpretation "pcat" 'concat a b = (pconcat ? a b).
 113
 114 notation "• a" non associative with precedence 90 for @{ 'ppoint $a}.
 115 (* notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}. *)
 116
 117 interpretation "ppatom" 'ppoint a = (ppoint ? a).
 118 (* to get rid of \middot
 119 ncoercion pc : ∀S.∀p:pitem S. pitem S → pitem S  ≝ pc on _p : pitem ? to ∀_:?.?. *)
 120 interpretation "patom" 'pchar a = (pchar ? a).
 121 interpretation "pepsilon" 'epsilon = (pepsilon ?).
 122 interpretation "pempty" 'empty = (pzero ?).
 123
 124 notation "\boxv term 19 e \boxv" (* slash boxv *) non associative with precedence 70 for @{forget ? $e}.
 125
 126 let rec forget (S: \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) (l : \ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on l: \ 5a href="cic:/matita/tutorial/chapter4/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S ≝
 127  match l with
 128   [ pzero ⇒ \ 5a title="empty" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
 129   | pepsilon ⇒ \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6
 130   | pchar x ⇒ \ 5a href="cic:/matita/tutorial/chapter4/re.con(0,3,1)"\ 6char\ 5/a\ 6 ? x
 131   | ppoint x ⇒ \ 5a href="cic:/matita/tutorial/chapter4/re.con(0,3,1)"\ 6char\ 5/a\ 6 ? x
 132   | pconcat e1 e2 ⇒ │e1│ \ 5a title="cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 │e2│
 133   | por e1 e2 ⇒ │e1│  \ 5a title="or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 │e2│
 134   | pstar e ⇒ │e│\ 5a title="star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*
 135   ].
 136
 137 notation "│ term 19 e │" non associative with precedence 70 for @{'forget $e}.
 138 interpretation "forget" 'forget a = (forget ? a).
 139
 140 notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.
 141 interpretation "fst" 'fst x = (fst ? ? x).
 142 notation "\snd term 90 x" non associative with precedence 90 for @{'snd $x}.
 143 interpretation "snd" 'snd x = (snd ? ? x).
 144
 145 notation "ℓ term 70 E" non associative with precedence 75 for @{in_pl ? $E}.
 146
 147 let rec in_pl (S : \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) (r : \ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on r : \ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S → Prop ≝
 148 match r with
 149   [ pzero ⇒ \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
 150   | pepsilon ⇒ \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
 151   | pchar _ ⇒ \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
 152   | ppoint x ⇒ \ 5a title="sing lang" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6: x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] }
 153   | pconcat pe1 pe2 ⇒ in_pl ? pe1 \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6ℓ\ 5/a\ 6 │pe2│  \ 5a title="union lang" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 in_pl ? pe2
 154   | por pe1 pe2 ⇒ in_pl ? pe1 \ 5a title="union lang" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 in_pl ? pe2
 155   | pstar pe ⇒ in_pl ? pe \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6ℓ\ 5/a\ 6 │pe│\ 5a title="star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*
 156   ].
 157
 158 interpretation "in_pl" 'in_l E = (in_pl ? E).
 159 interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
 160
 161 definition eps: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S → Prop
 162   ≝ λS,b. \ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"\ 6if_then_else\ 5/a\ 6 ? b \ 5a title="sing lang" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6: \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] } \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6.
 163
 164 (* interpretation "epsilon" 'epsilon = (epsilon ?). *)
 165 notation "ϵ _ b" non associative with precedence 90 for @{'app_epsilon $b}.
 166 interpretation "epsilon lang" 'app_epsilon b = (eps ? b).
 167
 168 definition in_prl ≝ λS : \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6.λp:\ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S.  \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6ℓ\ 5/a\ 6 (\ 5a title="fst" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p) \ 5a title="union lang" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="epsilon lang" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6_(\ 5a title="snd" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p).
 169
 170 interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
 171 interpretation "in_prl" 'in_l E = (in_prl ? E).
 172
 173 lemma not_epsilon_lp :∀S.∀pi:\ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S. \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 ((\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6ℓ\ 5/a\ 6 pi) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]).
 174 #S #pi (elim pi) normalize /2/
 175   [#pi1 #pi2 #H1 #H2 % * /2/ * #w1 * #w2 * * #appnil
 176    cases (\ 5a href="cic:/matita/tutorial/chapter3/nil_to_nil.def(5)"\ 6nil_to_nil\ 5/a\ 6 … appnil) /2/
 177   |#p11 #p12 #H1 #H2 % * /2/
 178   |#pi #H % * #w1 * #w2 * * #appnil (cases (\ 5a href="cic:/matita/tutorial/chapter3/nil_to_nil.def(5)"\ 6nil_to_nil\ 5/a\ 6 … appnil)) /2/
 179   ]
 180 qed.
 181
 182 lemma if_true_epsilon: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="snd" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → ((\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6ℓ\ 5/a\ 6 e) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]).
 183 #S #e #H %2 >H // qed.
 184
 185 lemma if_epsilon_true : ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter4/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] \ 5a title="in_prl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 e → \ 5a title="snd" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
 186 #S * #pi #b * [#abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /2/] cases b normalize // @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6
 187 qed.
 188
 189