1 include "tutorial/chapter3.ma".
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
10 interpretation "iff" 'iff a b = (iff a b).
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)
17 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
18 interpretation "eqb" 'eqb a b = (eqb ? a b).
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.
22 inductive re (S:
\ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"
\ 6Alpha
\ 5/a
\ 6) : Type[0] ≝
26 | concat: re S → re S → re S
27 | or: re S → re S → re S
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).
35 notation "a · b" non associative with precedence 60 for @{ 'concat $a $b}.
36 interpretation "cat" 'concat a b = (concat ? a b).
38 (* to get rid of \middot
39 coercion c : ∀S:Alpha.∀p:re S. re S → re S ≝ c on _p : re ? to ∀_:?.?. *)
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).
45 notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
46 interpretation "epsilon" 'epsilon = (epsilon ?).
48 notation "∅" non associative with precedence 90 for @{ 'empty }.
49 interpretation "empty" 'empty = (zero ?).
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 ].
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 ].
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 ?).
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).
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).
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).
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).
75 notation > "𝐋 term 70 E" non associative with precedence 75 for @{in_l ? $E}.
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 ≝
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
87 | concat r1 r2 ⇒ 𝐋 r1 · 𝐋 r2
88 | or r1 r2 ⇒ 𝐋 r1 ∪ 𝐋 r2
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).
98 notation "a || b" left associative with precedence 30 for @{'orb $a $b}.
99 interpretation "orb" 'orb a b = (orb a b).
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).
106 ninductive pitem (S: Alpha) : Type[0] ≝
111 | pc: pitem S → pitem S → pitem S
112 | po: pitem S → pitem S → pitem S
113 | pk: pitem S → pitem S.
115 ndefinition pre ≝ λS.pitem S × bool.
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 ?).
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 ≝
136 | pc E1 E2 ⇒ (|E1| · |E2|)
137 | po E1 E2 ⇒ (|E1| + |E2|)
139 notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.
140 interpretation "forget" 'forget a = (forget ? a).
142 notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.