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 "∅" 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" 'pc a b = (cat ? a b).
  71
  72 definition star ≝ λ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 ? 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: \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x]\ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6}
  82  | _ ⇒ \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
  83  ].
  84
  85
  86 (*
  87  | concat r1 r2 ⇒ 𝐋 r1 · 𝐋 r2
  88  | or r1 r2 ⇒  𝐋 r1 ∪ 𝐋 r2
  89  | star r1 ⇒ (𝐋 r1) ^*
  90  ].
  91
  92 *)
  93
  94  notation "𝐋 term 70 E" non associative with precedence 75 for @{'in_l $E}.
  95 interpretation "in_l" 'in_l E = (in_l ? E).
  96 interpretation "in_l mem" 'mem w l = (in_l ? l w).
  97
  98 notation "a || b" left associative with precedence 30 for @{'orb $a $b}.
  99 interpretation "orb" 'orb a b = (orb a b).
 100
 101 ndefinition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
 102 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 }.
 103 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 }.
 104 interpretation "if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
 105
 106 ninductive pitem (S: Alpha) : Type[0] ≝
 107    pz: pitem S
 108  | pe: pitem S
 109  | ps: S → pitem S
 110  | pp: S → pitem S
 111  | pc: pitem S → pitem S → pitem S
 112  | po: pitem S → pitem S → pitem S
 113  | pk: pitem S → pitem S.
 114
 115 ndefinition pre ≝ λS.pitem S × bool.
 116
 117 interpretation "pstar" 'pk a = (pk ? a).
 118 interpretation "por" 'plus a b = (po ? a b).
 119 interpretation "pcat" 'pc a b = (pc ? a b).
 120 notation < ".a" non associative with precedence 90 for @{ 'pp $a}.
 121 notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}.
 122 interpretation "ppatom" 'pp a = (pp ? a).
 123 (* to get rid of \middot *)
 124 ncoercion pc : ∀S.∀p:pitem S. pitem S → pitem S  ≝ pc on _p : pitem ? to ∀_:?.?.
 125 interpretation "patom" 'ps a = (ps ? a).
 126 interpretation "pepsilon" 'epsilon = (pe ?).
 127 interpretation "pempty" 'empty = (pz ?).
 128
 129 notation > "|term 19 e|" non associative with precedence 70 for @{forget ? $e}.
 130 nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝
 131  match l with
 132   [ pz ⇒ ∅
 133   | pe ⇒ ϵ
 134   | ps x ⇒ `x
 135   | pp x ⇒ `x
 136   | pc E1 E2 ⇒ (|E1| · |E2|)
 137   | po E1 E2 ⇒ (|E1| + |E2|)
 138   | pk E ⇒ |E|^* ].
 139 notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.
 140 interpretation "forget" 'forget a = (forget ? a).
 141
 142 notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.