1 include "basics/logic.ma".
3 (* Most of the types we have seen so far are enumerated types, composed by
4 a finite set of alternatives, and records, composed by tuples of
5 heteregoneous elements. A more interesting case of type definition is
6 when some of the rules defining its elements are recursive, i.e. they
7 allow the formation of more elements of the type in terms of the already
8 defined ones. The most typical case is provided by the natural numbers,
9 that can be defined as the smallest set generated by a constant 0 and a
10 successor function from natural numbers to natural numbers *)
12 inductive nat : Type[0] ≝
16 (* The two terms O and S are called constructors: they define the
17 signature of the type, whose objects are the elements freely generated
18 by means of them. So, examples of natural numbers are O, S O, S (S O),
19 S (S (S O)) and so on.
21 The language of Matita allows the definition of well founded recursive functions
22 over inductive types; in order to guarantee termination of recursion you are
23 only allowed to make recursive calls on structurally smaller arguments than the
24 ones your received in input.
25 Most mathematical functions can be naturally defined in this way. For instance,
26 the sum of two natural numbers can be defined as follows *)
31 | S a ⇒
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 (add a m)
34 (* It is worth to observe that the previous algorithm works by recursion over the
35 first argument. This means that, for instance, (add 0 x) will reduce to x, as expected,
36 but (add x 0) is stack. How can we prove that, for a generic x, (add x 0) = x? The
37 mathematical tool do it is called induction. The induction principle states that,
38 given a property P(n) over natural numbers, if we prove P(0) and prove that, for any
39 m, P(m) implies P(S m), than we can conclude P(n) for any n.
41 The elim tactic, allow you to apply induction in a vcery simple way. If your
42 goal is P(n), the invocation of
44 will break down your task to prove the two subgoals P(0) and ∀m.P(m) → P(S m).
45 Let us apply it to our case *)
47 lemma add_0: ∀a.
\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"
\ 6add
\ 5/a
\ 6 a
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 a.
50 (* If you stop the computation here, you will see on the right the two subgoals
52 - ∀x. add x 0 = x → add (S x) O = S x
53 After normalization, both goals are trivial.
58 (* In a similar way, it is convenient to state a lemma about the behaviour of add when the
59 second argument is not zero. *)
61 lemma add_S : ∀a,b.
\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"
\ 6add
\ 5/a
\ 6 a (
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 b)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"
\ 6add
\ 5/a
\ 6 a b).
63 (* In the same way as before, we proceed by induction over a. *)
65 #a #b elim a normalize //
68 (* We are now in the position to prove the commutativity of the sum *)
70 theorem add_comm : ∀a,b.
\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"
\ 6add
\ 5/a
\ 6 a b
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"
\ 6add
\ 5/a
\ 6 b a.
73 (* We have two sub goals:
75 G2: ∀x.(∀b. add x b = add b x) → ∀b. S (add x b) = add b (S x).
76 G1 is just our lemma add_O. For G2, we start introducing x and the induction
77 hypothesis IH; then, the goal is proved by rewriting using add_S and IH.
78 For Matita, the task is trivial and we can simply close the goal with // *)
82 (* Let us now define the following function: *)
84 definition twice ≝ λn.
\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"
\ 6add
\ 5/a
\ 6 n n.
86 (* We are interested to prove that for any natural number m there
87 exists a natural number m that is the integer half of m. This
88 will give us the opportunity to introduce new connectives
89 and quantifiers, and later on to make some interesting consideration
90 on proofs and computations. *)
92 theorem ex_half: ∀n.
\ 5a title="exists" href="cic:/fakeuri.def(1)"
\ 6∃
\ 5/a
\ 6m. n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"
\ 6twice
\ 5/a
\ 6 m
\ 5a title="logical or" href="cic:/fakeuri.def(1)"
\ 6∨
\ 5/a
\ 6 n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"
\ 6twice
\ 5/a
\ 6 m).
97 include "basics/list.ma".
99 interpretation "iff" 'iff a b = (iff a b).
101 record Alpha : Type[1] ≝ { carr :> Type[0];
102 eqb: carr → carr →
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6;
103 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)
106 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
107 interpretation "eqb" 'eqb a b = (eqb ? a b).
109 definition word ≝ λS:
\ 5a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"
\ 6Alpha
\ 5/a
\ 6.
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 S.
111 inductive re (S:
\ 5a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"
\ 6Alpha
\ 5/a
\ 6) : Type[0] ≝
115 | c: re S → re S → re S
116 | o: re S → re S → re S
119 notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
120 notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}.
121 interpretation "star" 'pk a = (k ? a).
122 interpretation "or" 'plus a b = (o ? a b).
124 notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
125 interpretation "cat" 'pc a b = (c ? a b).
127 (* to get rid of \middot
128 coercion c : ∀S:Alpha.∀p:re S. re S → re S ≝ c on _p : re ? to ∀_:?.?. *)
130 notation < "a" non associative with precedence 90 for @{ 'ps $a}.
131 notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
132 interpretation "atom" 'ps a = (s ? a).
134 notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
135 interpretation "epsilon" 'epsilon = (e ?).
137 notation "∅" non associative with precedence 90 for @{ 'empty }.
138 interpretation "empty" 'empty = (z ?).
140 let rec flatten (S :
\ 5a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"
\ 6Alpha
\ 5/a
\ 6) (l :
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/re/word.def(3)"
\ 6word
\ 5/a
\ 6 S)) on l :
\ 5a href="cic:/matita/tutorial/re/word.def(3)"
\ 6word
\ 5/a
\ 6 S ≝
141 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 ].
143 let rec conjunct (S :
\ 5a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"
\ 6Alpha
\ 5/a
\ 6) (l :
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/re/word.def(3)"
\ 6word
\ 5/a
\ 6 S)) (r :
\ 5a href="cic:/matita/tutorial/re/word.def(3)"
\ 6word
\ 5/a
\ 6 S → Prop) on l: Prop ≝
144 match l with [ nil ⇒
\ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"
\ 6True
\ 5/a
\ 6 | cons w tl ⇒ r w
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 conjunct ? tl r ].
146 definition empty_lang ≝ λS.λw:
\ 5a href="cic:/matita/tutorial/re/word.def(3)"
\ 6word
\ 5/a
\ 6 S.
\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"
\ 6False
\ 5/a
\ 6.
147 notation "{}" non associative with precedence 90 for @{'empty_lang}.
148 interpretation "empty lang" 'empty_lang = (empty_lang ?).
150 definition sing_lang ≝ λS.λx,w:
\ 5a href="cic:/matita/tutorial/re/word.def(3)"
\ 6word
\ 5/a
\ 6 S.x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6w.
151 notation "{x}" non associative with precedence 90 for @{'sing_lang $x}.
152 interpretation "sing lang" 'sing_lang x = (sing_lang ? x).
154 definition union : ∀S,l1,l2,w.Prop ≝ λS.λl1,l2.λw:
\ 5a href="cic:/matita/tutorial/re/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.
155 interpretation "union lang" 'union a b = (union ? a b).
157 definition cat : ∀S,l1,l2,w.Prop ≝
158 λS.λl1,l2.λw:
\ 5a href="cic:/matita/tutorial/re/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.
159 interpretation "cat lang" 'pc a b = (cat ? a b).
161 definition star ≝ λS.λl.λw:
\ 5a href="cic:/matita/tutorial/re/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/re/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/re/conjunct.fix(0,1,4)"
\ 6conjunct
\ 5/a
\ 6 ? lw l.
162 interpretation "star lang" 'pk l = (star ? l).
164 notation > "𝐋 term 70 E" non associative with precedence 75 for @{in_l ? $E}.
166 let rec in_l (S : Alpha) (r : re S) on r : word S → Prop ≝
171 | c r1 r2 ⇒ 𝐋 r1 · 𝐋 r2
172 | o r1 r2 ⇒ 𝐋 r1 ∪ 𝐋 r2
175 notation "𝐋 term 70 E" non associative with precedence 75 for @{'in_l $E}.
176 interpretation "in_l" 'in_l E = (in_l ? E).
177 interpretation "in_l mem" 'mem w l = (in_l ? l w).
179 notation "a || b" left associative with precedence 30 for @{'orb $a $b}.
180 interpretation "orb" 'orb a b = (orb a b).
182 ndefinition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
183 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 }.
184 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 }.
185 interpretation "if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
187 ninductive pitem (S: Alpha) : Type[0] ≝
192 | pc: pitem S → pitem S → pitem S
193 | po: pitem S → pitem S → pitem S
194 | pk: pitem S → pitem S.
196 ndefinition pre ≝ λS.pitem S × bool.
198 interpretation "pstar" 'pk a = (pk ? a).
199 interpretation "por" 'plus a b = (po ? a b).
200 interpretation "pcat" 'pc a b = (pc ? a b).
201 notation < ".a" non associative with precedence 90 for @{ 'pp $a}.
202 notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}.
203 interpretation "ppatom" 'pp a = (pp ? a).
204 (* to get rid of \middot *)
205 ncoercion pc : ∀S.∀p:pitem S. pitem S → pitem S ≝ pc on _p : pitem ? to ∀_:?.?.
206 interpretation "patom" 'ps a = (ps ? a).
207 interpretation "pepsilon" 'epsilon = (pe ?).
208 interpretation "pempty" 'empty = (pz ?).
210 notation > "|term 19 e|" non associative with precedence 70 for @{forget ? $e}.
211 nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝
217 | pc E1 E2 ⇒ (|E1| · |E2|)
218 | po E1 E2 ⇒ (|E1| + |E2|)
220 notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.
221 interpretation "forget" 'forget a = (forget ? a).
223 notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.
224 interpretation "fst" 'fst x = (fst ? ? x).
225 notation > "\snd term 90 x" non associative with precedence 90 for @{'snd $x}.
226 interpretation "snd" 'snd x = (snd ? ? x).
228 notation > "𝐋\p\ term 70 E" non associative with precedence 75 for @{in_pl ? $E}.
229 nlet rec in_pl (S : Alpha) (r : pitem S) on r : word S → Prop ≝
235 | pc r1 r2 ⇒ 𝐋\p\ r1 · 𝐋 |r2| ∪ 𝐋\p\ r2
236 | po r1 r2 ⇒ 𝐋\p\ r1 ∪ 𝐋\p\ r2
237 | pk r1 ⇒ 𝐋\p\ r1 · 𝐋 (|r1|^* ) ].
238 notation > "𝐋\p term 70 E" non associative with precedence 75 for @{'in_pl $E}.
239 notation "𝐋\sub(\p) term 70 E" non associative with precedence 75 for @{'in_pl $E}.
240 interpretation "in_pl" 'in_pl E = (in_pl ? E).
241 interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
243 ndefinition epsilon ≝ λS,b.if b then { ([ ] : word S) } else {}.
245 interpretation "epsilon" 'epsilon = (epsilon ?).
246 notation < "ϵ b" non associative with precedence 90 for @{'app_epsilon $b}.
247 interpretation "epsilon lang" 'app_epsilon b = (epsilon ? b).
249 ndefinition in_prl ≝ λS : Alpha.λp:pre S. 𝐋\p (\fst p) ∪ ϵ (\snd p).
251 interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
252 interpretation "in_prl" 'in_pl E = (in_prl ? E).
254 nlemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = [ ] → w1 = [ ].
255 #S w1; nelim w1; //. #x tl IH w2; nnormalize; #abs; ndestruct; nqed.
258 nlemma epsilon_in_true : ∀S.∀e:pre S. [ ] ∈ e ↔ \snd e = true.
259 #S r; ncases r; #e b; @; ##[##2: #H; nrewrite > H; @2; /2/; ##] ncases b;//;
260 nnormalize; *; ##[##2:*] nelim e;
261 ##[ ##1,2: *; ##| #c; *; ##| #c; nnormalize; #; ndestruct; ##| ##7: #p H;
262 ##| #r1 r2 H G; *; ##[##2: /3/ by or_intror]
263 ##| #r1 r2 H1 H2; *; /3/ by or_intror, or_introl; ##]
264 *; #w1; *; #w2; *; *; #defw1; nrewrite > (append_eq_nil … w1 w2 …); /3/ by {};//;
267 nlemma not_epsilon_lp : ∀S:Alpha.∀e:pitem S. ¬ ((𝐋\p e) [ ]).
268 #S e; nelim e; nnormalize; /2/ by nmk;
269 ##[ #; @; #; ndestruct;
270 ##| #r1 r2 n1 n2; @; *; /2/; *; #w1; *; #w2; *; *; #H;
271 nrewrite > (append_eq_nil …H…); /2/;
272 ##| #r1 r2 n1 n2; @; *; /2/;
273 ##| #r n; @; *; #w1; *; #w2; *; *; #H;
274 nrewrite > (append_eq_nil …H…); /2/;##]
277 ndefinition lo ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a || \snd b〉.
278 notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
279 interpretation "oplus" 'oplus a b = (lo ? a b).
281 ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S.
282 match a with [ mk_pair e1 b1 ⇒
284 [ false ⇒ 〈e1 · \fst b, \snd b〉
285 | true ⇒ 〈e1 · \fst (bcast ? (\fst b)),\snd b || \snd (bcast ? (\fst b))〉]].
287 notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}.
288 interpretation "lc" 'lc op a b = (lc ? op a b).
289 notation > "a ⊙ b" left associative with precedence 60 for @{'lc eclose $a $b}.
291 ndefinition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa:pre S.
292 match a with [ mk_pair e1 b1 ⇒
294 [ false ⇒ 〈e1^*, false〉
295 | true ⇒ 〈(\fst (bcast ? e1))^*, true〉]].
297 notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $op $a}.
298 interpretation "lk" 'lk op a = (lk ? op a).
299 notation > "a^⊛" non associative with precedence 90 for @{'lk eclose $a}.
301 notation > "•" non associative with precedence 60 for @{eclose ?}.
302 nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝
306 | ps x ⇒ 〈 `.x, false 〉
307 | pp x ⇒ 〈 `.x, false 〉
308 | po E1 E2 ⇒ •E1 ⊕ •E2
309 | pc E1 E2 ⇒ •E1 ⊙ 〈 E2, false 〉
310 | pk E ⇒ 〈(\fst (•E))^*,true〉].
311 notation < "• x" non associative with precedence 60 for @{'eclose $x}.
312 interpretation "eclose" 'eclose x = (eclose ? x).
313 notation > "• x" non associative with precedence 60 for @{'eclose $x}.
315 ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉.
316 interpretation "reclose" 'eclose x = (reclose ? x).
318 ndefinition eq_f1 ≝ λS.λa,b:word S → Prop.∀w.a w ↔ b w.
319 notation > "A =1 B" non associative with precedence 45 for @{'eq_f1 $A $B}.
320 notation "A =\sub 1 B" non associative with precedence 45 for @{'eq_f1 $A $B}.
321 interpretation "eq f1" 'eq_f1 a b = (eq_f1 ? a b).
323 naxiom extP : ∀S.∀p,q:word S → Prop.(p =1 q) → p = q.
325 nlemma epsilon_or : ∀S:Alpha.∀b1,b2. ϵ(b1 || b2) = ϵ b1 ∪ ϵ b2. ##[##2: napply S]
326 #S b1 b2; ncases b1; ncases b2; napply extP; #w; nnormalize; @; /2/; *; //; *;
329 nlemma cupA : ∀S.∀a,b,c:word S → Prop.a ∪ b ∪ c = a ∪ (b ∪ c).
330 #S a b c; napply extP; #w; nnormalize; @; *; /3/; *; /3/; nqed.
332 nlemma cupC : ∀S. ∀a,b:word S → Prop.a ∪ b = b ∪ a.
333 #S a b; napply extP; #w; @; *; nnormalize; /2/; nqed.
336 nlemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S.𝐋\p (e1 ⊕ e2) = 𝐋\p e1 ∪ 𝐋\p e2.
337 #S r1; ncases r1; #e1 b1 r2; ncases r2; #e2 b2;
338 nwhd in ⊢ (??(??%)?);
339 nchange in ⊢(??%?) with (𝐋\p (e1 + e2) ∪ ϵ (b1 || b2));
340 nchange in ⊢(??(??%?)?) with (𝐋\p (e1) ∪ 𝐋\p (e2));
341 nrewrite > (epsilon_or S …); nrewrite > (cupA S (𝐋\p e1) …);
342 nrewrite > (cupC ? (ϵ b1) …); nrewrite < (cupA S (𝐋\p e2) …);
343 nrewrite > (cupC ? ? (ϵ b1) …); nrewrite < (cupA …); //;
347 ∀S.∀e1,e2:pitem S.∀b2. 〈e1,true〉 ⊙ 〈e2,b2〉 = 〈e1 · \fst (•e2),b2 || \snd (•e2)〉.
348 #S e1 e2 b2; nnormalize; ncases (•e2); //; nqed.
350 nlemma LcatE : ∀S.∀e1,e2:pitem S.𝐋\p (e1 · e2) = 𝐋\p e1 · 𝐋 |e2| ∪ 𝐋\p e2. //; nqed.
352 nlemma cup_dotD : ∀S.∀p,q,r:word S → Prop.(p ∪ q) · r = (p · r) ∪ (q · r).
353 #S p q r; napply extP; #w; nnormalize; @;
354 ##[ *; #x; *; #y; *; *; #defw; *; /7/ by or_introl, or_intror, ex_intro, conj;
355 ##| *; *; #x; *; #y; *; *; /7/ by or_introl, or_intror, ex_intro, conj; ##]
358 nlemma cup0 :∀S.∀p:word S → Prop.p ∪ {} = p.
359 #S p; napply extP; #w; nnormalize; @; /2/; *; //; *; nqed.
361 nlemma erase_dot : ∀S.∀e1,e2:pitem S.𝐋 |e1 · e2| = 𝐋 |e1| · 𝐋 |e2|.
362 #S e1 e2; napply extP; nnormalize; #w; @; *; #w1; *; #w2; *; *; /7/ by ex_intro, conj;
365 nlemma erase_plus : ∀S.∀e1,e2:pitem S.𝐋 |e1 + e2| = 𝐋 |e1| ∪ 𝐋 |e2|.
366 #S e1 e2; napply extP; nnormalize; #w; @; *; /4/ by or_introl, or_intror; nqed.
368 nlemma erase_star : ∀S.∀e1:pitem S.𝐋 |e1|^* = 𝐋 |e1^*|. //; nqed.
370 ndefinition substract := λS.λp,q:word S → Prop.λw.p w ∧ ¬ q w.
371 interpretation "substract" 'minus a b = (substract ? a b).
373 nlemma cup_sub: ∀S.∀a,b:word S → Prop. ¬ (a []) → a ∪ (b - {[]}) = (a ∪ b) - {[]}.
374 #S a b c; napply extP; #w; nnormalize; @; *; /4/; *; /4/; nqed.
376 nlemma sub0 : ∀S.∀a:word S → Prop. a - {} = a.
377 #S a; napply extP; #w; nnormalize; @; /3/; *; //; nqed.
379 nlemma subK : ∀S.∀a:word S → Prop. a - a = {}.
380 #S a; napply extP; #w; nnormalize; @; *; /2/; nqed.
382 nlemma subW : ∀S.∀a,b:word S → Prop.∀w.(a - b) w → a w.
383 #S a b w; nnormalize; *; //; nqed.
385 nlemma erase_bull : ∀S.∀a:pitem S. |\fst (•a)| = |a|.
386 #S a; nelim a; // by {};
387 ##[ #e1 e2 IH1 IH2; nchange in ⊢ (???%) with (|e1| · |e2|);
388 nrewrite < IH1; nrewrite < IH2;
389 nchange in ⊢ (??(??%)?) with (\fst (•e1 ⊙ 〈e2,false〉));
390 ncases (•e1); #e3 b; ncases b; nnormalize;
391 ##[ ncases (•e2); //; ##| nrewrite > IH2; //]
392 ##| #e1 e2 IH1 IH2; nchange in ⊢ (???%) with (|e1| + |e2|);
393 nrewrite < IH2; nrewrite < IH1;
394 nchange in ⊢ (??(??%)?) with (\fst (•e1 ⊕ •e2));
395 ncases (•e1); ncases (•e2); //;
396 ##| #e IH; nchange in ⊢ (???%) with (|e|^* ); nrewrite < IH;
397 nchange in ⊢ (??(??%)?) with (\fst (•e))^*; //; ##]
400 nlemma eta_lp : ∀S.∀p:pre S.𝐋\p p = 𝐋\p 〈\fst p, \snd p〉.
401 #S p; ncases p; //; nqed.
403 nlemma epsilon_dot: ∀S.∀p:word S → Prop. {[]} · p = p.
404 #S e; napply extP; #w; nnormalize; @; ##[##2: #Hw; @[]; @w; /3/; ##]
405 *; #w1; *; #w2; *; *; #defw defw1 Hw2; nrewrite < defw; nrewrite < defw1;
408 (* theorem 16: 1 → 3 *)
409 nlemma odot_dot_aux : ∀S.∀e1,e2: pre S.
410 𝐋\p (•(\fst e2)) = 𝐋\p (\fst e2) ∪ 𝐋 |\fst e2| →
411 𝐋\p (e1 ⊙ e2) = 𝐋\p e1 · 𝐋 |\fst e2| ∪ 𝐋\p e2.
412 #S e1 e2 th1; ncases e1; #e1' b1'; ncases b1';
413 ##[ nwhd in ⊢ (??(??%)?); nletin e2' ≝ (\fst e2); nletin b2' ≝ (\snd e2);
414 nletin e2'' ≝ (\fst (•(\fst e2))); nletin b2'' ≝ (\snd (•(\fst e2)));
415 nchange in ⊢ (??%?) with (?∪?);
416 nchange in ⊢ (??(??%?)?) with (?∪?);
417 nchange in match (𝐋\p 〈?,?〉) with (?∪?);
418 nrewrite > (epsilon_or …); nrewrite > (cupC ? (ϵ ?)…);
419 nrewrite > (cupA …);nrewrite < (cupA ?? (ϵ?)…);
420 nrewrite > (?: 𝐋\p e2'' ∪ ϵ b2'' = 𝐋\p e2' ∪ 𝐋 |e2'|); ##[##2:
421 nchange with (𝐋\p 〈e2'',b2''〉 = 𝐋\p e2' ∪ 𝐋 |e2'|);
422 ngeneralize in match th1;
423 nrewrite > (eta_lp…); #th1; nrewrite > th1; //;##]
424 nrewrite > (eta_lp ? e2);
425 nchange in match (𝐋\p 〈\fst e2,?〉) with (𝐋\p e2'∪ ϵ b2');
426 nrewrite > (cup_dotD …); nrewrite > (epsilon_dot…);
427 nrewrite > (cupC ? (𝐋\p e2')…); nrewrite > (cupA…);nrewrite > (cupA…);
428 nrewrite < (erase_bull S e2') in ⊢ (???(??%?)); //;
429 ##| ncases e2; #e2' b2'; nchange in match (〈e1',false〉⊙?) with 〈?,?〉;
430 nchange in match (𝐋\p ?) with (?∪?);
431 nchange in match (𝐋\p (e1'·?)) with (?∪?);
432 nchange in match (𝐋\p 〈e1',?〉) with (?∪?);
434 nrewrite > (cupA…); //;##]
437 nlemma sub_dot_star :
438 ∀S.∀X:word S → Prop.∀b. (X - ϵ b) · X^* ∪ {[]} = X^*.
439 #S X b; napply extP; #w; @;
440 ##[ *; ##[##2: nnormalize; #defw; nrewrite < defw; @[]; @; //]
441 *; #w1; *; #w2; *; *; #defw sube; *; #lw; *; #flx cj;
442 @ (w1 :: lw); nrewrite < defw; nrewrite < flx; @; //;
443 @; //; napply (subW … sube);
444 ##| *; #wl; *; #defw Pwl; nrewrite < defw; nelim wl in Pwl; ##[ #_; @2; //]
445 #w' wl' IH; *; #Pw' IHp; nlapply (IH IHp); *;
446 ##[ *; #w1; *; #w2; *; *; #defwl' H1 H2;
447 @; ncases b in H1; #H1;
448 ##[##2: nrewrite > (sub0…); @w'; @(w1@w2);
449 nrewrite > (associative_append ? w' w1 w2);
450 nrewrite > defwl'; @; ##[@;//] @(wl'); @; //;
451 ##| ncases w' in Pw';
452 ##[ #ne; @w1; @w2; nrewrite > defwl'; @; //; @; //;
453 ##| #x xs Px; @(x::xs); @(w1@w2);
454 nrewrite > (defwl'); @; ##[@; //; @; //; @; nnormalize; #; ndestruct]
456 ##| #wlnil; nchange in match (flatten ? (w'::wl')) with (w' @ flatten ? wl');
457 nrewrite < (wlnil); nrewrite > (append_nil…); ncases b;
458 ##[ ncases w' in Pw'; /2/; #x xs Pxs; @; @(x::xs); @([]);
459 nrewrite > (append_nil…); @; ##[ @; //;@; //; nnormalize; @; #; ndestruct]
461 ##| @; @w'; @[]; nrewrite > (append_nil…); @; ##[##2: @[]; @; //]
462 @; //; @; //; @; *;##]##]##]
466 alias symbol "pc" (instance 13) = "cat lang".
467 alias symbol "in_pl" (instance 23) = "in_pl".
468 alias symbol "in_pl" (instance 5) = "in_pl".
469 alias symbol "eclose" (instance 21) = "eclose".
470 ntheorem bull_cup : ∀S:Alpha. ∀e:pitem S. 𝐋\p (•e) = 𝐋\p e ∪ 𝐋 |e|.
472 ##[ #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl, or_intror;
473 ##| #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl; *;
475 nchange in ⊢ (??(??(%))?) with (•e1 ⊙ 〈e2,false〉);
476 nrewrite > (odot_dot_aux S (•e1) 〈e2,false〉 IH2);
477 nrewrite > (IH1 …); nrewrite > (cup_dotD …);
478 nrewrite > (cupA …); nrewrite > (cupC ?? (𝐋\p ?) …);
479 nchange in match (𝐋\p 〈?,?〉) with (𝐋\p e2 ∪ {}); nrewrite > (cup0 …);
480 nrewrite < (erase_dot …); nrewrite < (cupA …); //;
482 nchange in match (•(?+?)) with (•e1 ⊕ •e2); nrewrite > (oplus_cup …);
483 nrewrite > (IH1 …); nrewrite > (IH2 …); nrewrite > (cupA …);
484 nrewrite > (cupC ? (𝐋\p e2)…);nrewrite < (cupA ??? (𝐋\p e2)…);
485 nrewrite > (cupC ?? (𝐋\p e2)…); nrewrite < (cupA …);
486 nrewrite < (erase_plus …); //.
487 ##| #e; nletin e' ≝ (\fst (•e)); nletin b' ≝ (\snd (•e)); #IH;
488 nchange in match (𝐋\p ?) with (𝐋\p 〈e'^*,true〉);
489 nchange in match (𝐋\p ?) with (𝐋\p (e'^* ) ∪ {[ ]});
490 nchange in ⊢ (??(??%?)?) with (𝐋\p e' · 𝐋 |e'|^* );
491 nrewrite > (erase_bull…e);
492 nrewrite > (erase_star …);
493 nrewrite > (?: 𝐋\p e' = 𝐋\p e ∪ (𝐋 |e| - ϵ b')); ##[##2:
494 nchange in IH : (??%?) with (𝐋\p e' ∪ ϵ b'); ncases b' in IH;
495 ##[ #IH; nrewrite > (cup_sub…); //; nrewrite < IH;
496 nrewrite < (cup_sub…); //; nrewrite > (subK…); nrewrite > (cup0…);//;
497 ##| nrewrite > (sub0 …); #IH; nrewrite < IH; nrewrite > (cup0 …);//; ##]##]
498 nrewrite > (cup_dotD…); nrewrite > (cupA…);
499 nrewrite > (?: ((?·?)∪{[]} = 𝐋 |e^*|)); //;
500 nchange in match (𝐋 |e^*|) with ((𝐋 |e|)^* ); napply sub_dot_star;##]
505 ∀S.∀e1,e2: pre S. 𝐋\p (e1 ⊙ e2) = 𝐋\p e1 · 𝐋 |\fst e2| ∪ 𝐋\p e2.
506 #S e1 e2; napply odot_dot_aux; napply (bull_cup S (\fst e2)); nqed.
508 nlemma dot_star_epsilon : ∀S.∀e:re S.𝐋 e · 𝐋 e^* ∪ {[]} = 𝐋 e^*.
509 #S e; napply extP; #w; nnormalize; @;
510 ##[ *; ##[##2: #H; nrewrite < H; @[]; /3/] *; #w1; *; #w2;
511 *; *; #defw Hw1; *; #wl; *; #defw2 Hwl; @(w1 :: wl);
512 nrewrite < defw; nrewrite < defw2; @; //; @;//;
513 ##| *; #wl; *; #defw Hwl; ncases wl in defw Hwl; ##[#defw; #; @2; nrewrite < defw; //]
514 #x xs defw; *; #Hx Hxs; @; @x; @(flatten ? xs); nrewrite < defw;
518 nlemma nil_star : ∀S.∀e:re S. [ ] ∈ e^*.
519 #S e; @[]; /2/; nqed.
521 nlemma cupID : ∀S.∀l:word S → Prop.l ∪ l = l.
522 #S l; napply extP; #w; @; ##[*]//; #; @; //; nqed.
524 nlemma cup_star_nil : ∀S.∀l:word S → Prop. l^* ∪ {[]} = l^*.
525 #S a; napply extP; #w; @; ##[*; //; #H; nrewrite < H; @[]; @; //] #;@; //;nqed.
527 nlemma rcanc_sing : ∀S.∀A,C:word S → Prop.∀b:word S .
528 ¬ (A b) → A ∪ { (b) } = C → A = C - { (b) }.
529 #S A C b nbA defC; nrewrite < defC; napply extP; #w; @;
530 ##[ #Aw; /3/| *; *; //; #H nH; ncases nH; #abs; nlapply (abs H); *]
534 nlemma star_dot: ∀S.∀e:pre S. 𝐋\p (e^⊛) = 𝐋\p e · (𝐋 |\fst e|)^*.
535 #S p; ncases p; #e b; ncases b;
536 ##[ nchange in match (〈e,true〉^⊛) with 〈?,?〉;
537 nletin e' ≝ (\fst (•e)); nletin b' ≝ (\snd (•e));
538 nchange in ⊢ (??%?) with (?∪?);
539 nchange in ⊢ (??(??%?)?) with (𝐋\p e' · 𝐋 |e'|^* );
540 nrewrite > (?: 𝐋\p e' = 𝐋\p e ∪ (𝐋 |e| - ϵ b' )); ##[##2:
541 nlapply (bull_cup ? e); #bc;
542 nchange in match (𝐋\p (•e)) in bc with (?∪?);
543 nchange in match b' in bc with b';
544 ncases b' in bc; ##[##2: nrewrite > (cup0…); nrewrite > (sub0…); //]
545 nrewrite > (cup_sub…); ##[napply rcanc_sing] //;##]
546 nrewrite > (cup_dotD…); nrewrite > (cupA…);nrewrite > (erase_bull…);
547 nrewrite > (sub_dot_star…);
548 nchange in match (𝐋\p 〈?,?〉) with (?∪?);
549 nrewrite > (cup_dotD…); nrewrite > (epsilon_dot…); //;
550 ##| nwhd in match (〈e,false〉^⊛); nchange in match (𝐋\p 〈?,?〉) with (?∪?);
552 nchange in ⊢ (??%?) with (𝐋\p e · 𝐋 |e|^* );
553 nrewrite < (cup0 ? (𝐋\p e)); //;##]
556 nlet rec pre_of_re (S : Alpha) (e : re S) on e : pitem S ≝
561 | c e1 e2 ⇒ pc ? (pre_of_re ? e1) (pre_of_re ? e2)
562 | o e1 e2 ⇒ po ? (pre_of_re ? e1) (pre_of_re ? e2)
563 | k e1 ⇒ pk ? (pre_of_re ? e1)].
565 nlemma notFalse : ¬False. @; //; nqed.
567 nlemma dot0 : ∀S.∀A:word S → Prop. {} · A = {}.
568 #S A; nnormalize; napply extP; #w; @; ##[##2: *]
569 *; #w1; *; #w2; *; *; //; nqed.
571 nlemma Lp_pre_of_re : ∀S.∀e:re S. 𝐋\p (pre_of_re ? e) = {}.
572 #S e; nelim e; ##[##1,2,3: //]
573 ##[ #e1 e2 H1 H2; nchange in match (𝐋\p (pre_of_re S (e1 e2))) with (?∪?);
574 nrewrite > H1; nrewrite > H2; nrewrite > (dot0…); nrewrite > (cupID…);//
575 ##| #e1 e2 H1 H2; nchange in match (𝐋\p (pre_of_re S (e1+e2))) with (?∪?);
576 nrewrite > H1; nrewrite > H2; nrewrite > (cupID…); //
577 ##| #e1 H1; nchange in match (𝐋\p (pre_of_re S (e1^* ))) with (𝐋\p (pre_of_re ??) · ?);
578 nrewrite > H1; napply dot0; ##]
581 nlemma erase_pre_of_reK : ∀S.∀e. 𝐋 |pre_of_re S e| = 𝐋 e.
583 ##[ #e1 e2 H1 H2; nchange in match (𝐋 (e1 · e2)) with (𝐋 e1·?);
584 nrewrite < H1; nrewrite < H2; //
585 ##| #e1 e2 H1 H2; nchange in match (𝐋 (e1 + e2)) with (𝐋 e1 ∪ ?);
586 nrewrite < H1; nrewrite < H2; //
587 ##| #e1 H1; nchange in match (𝐋 (e1^* )) with ((𝐋 e1)^* );
592 nlemma L_Lp_bull : ∀S.∀e:re S.𝐋 e = 𝐋\p (•pre_of_re ? e).
593 #S e; nrewrite > (bull_cup…); nrewrite > (Lp_pre_of_re…);
594 nrewrite > (cupC…); nrewrite > (cup0…); nrewrite > (erase_pre_of_reK…); //;
597 nlemma Pext : ∀S.∀f,g:word S → Prop. f = g → ∀w.f w → g w.
598 #S f g H; nrewrite > H; //; nqed.
601 ntheorem bull_true_epsilon : ∀S.∀e:pitem S. \snd (•e) = true ↔ [ ] ∈ |e|.
603 ##[ #defsnde; nlapply (bull_cup ? e); nchange in match (𝐋\p (•e)) with (?∪?);
604 nrewrite > defsnde; #H;
605 nlapply (Pext ??? H [ ] ?); ##[ @2; //] *; //;
609 notation > "\move term 90 x term 90 E"
610 non associative with precedence 60 for @{move ? $x $E}.
611 nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝
615 | ps y ⇒ 〈 `y, false 〉
616 | pp y ⇒ 〈 `y, x == y 〉
617 | po e1 e2 ⇒ \move x e1 ⊕ \move x e2
618 | pc e1 e2 ⇒ \move x e1 ⊙ \move x e2
619 | pk e ⇒ (\move x e)^⊛ ].
620 notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}.
621 notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}.
622 interpretation "move" 'move x E = (move ? x E).
624 ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e).
625 interpretation "rmove" 'move x E = (rmove ? x E).
627 nlemma XXz : ∀S:Alpha.∀w:word S. w ∈ ∅ → False.
628 #S w abs; ninversion abs; #; ndestruct;
632 nlemma XXe : ∀S:Alpha.∀w:word S. w .∈ ϵ → False.
633 #S w abs; ninversion abs; #; ndestruct;
636 nlemma XXze : ∀S:Alpha.∀w:word S. w .∈ (∅ · ϵ) → False.
637 #S w abs; ninversion abs; #; ndestruct; /2/ by XXz,XXe;
642 ∀S.∀w:word S.∀x.∀E1,E2:pitem S. w .∈ \move x (E1 · E2) →
643 (∃w1.∃w2. w = w1@w2 ∧ w1 .∈ \move x E1 ∧ w2 ∈ .|E2|) ∨ w .∈ \move x E2.
644 #S w x e1 e2 H; nchange in H with (w .∈ \move x e1 ⊙ \move x e2);
645 ncases e1 in H; ncases e2;
646 ##[##1: *; ##[*; nnormalize; #; ndestruct]
647 #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
648 nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze;
649 ##|##2: *; ##[*; nnormalize; #; ndestruct]
650 #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
651 nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze;
652 ##| #r; *; ##[ *; nnormalize; #; ndestruct]
653 #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
654 ##[##2: nnormalize; #; ndestruct; @2; @2; //.##]
655 nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz;
656 ##| #y; *; ##[ *; nnormalize; #defw defx; ndestruct; @2; @1; /2/ by conj;##]
657 #H; ninversion H; nnormalize; #; ndestruct;
658 ##[ncases (?:False); /2/ by XXz] /3/ by or_intror;
659 ##| #r1 r2; *; ##[ *; #defw]
664 ∀S:Alpha.∀E:pre S.∀a,w.w .∈ \move a E ↔ (a :: w) .∈ E.
665 #S E; ncases E; #r b; nelim r;
667 ##[##1,3: nnormalize; *; ##[##1,3: *; #; ndestruct; ##| #abs; ncases (XXz … abs); ##]
668 #H; ninversion H; #; ndestruct;
669 ##|##*:nnormalize; *; ##[##1,3: *; #; ndestruct; ##| #H1; ncases (XXz … H1); ##]
670 #H; ninversion H; #; ndestruct;##]
671 ##|#a c w; @; nnormalize; ##[*; ##[*; #; ndestruct; ##] #abs; ninversion abs; #; ndestruct;##]
672 *; ##[##2: #abs; ninversion abs; #; ndestruct; ##] *; #; ndestruct;
673 ##|#a c w; @; nnormalize;
674 ##[ *; ##[ *; #defw; nrewrite > defw; #ca; @2; nrewrite > (eqb_t … ca); @; ##]
675 #H; ninversion H; #; ndestruct;
676 ##| *; ##[ *; #; ndestruct; ##] #H; ninversion H; ##[##2,3,4,5,6: #; ndestruct]
677 #d defw defa; ndestruct; @1; @; //; nrewrite > (eqb_true S d d); //. ##]
678 ##|#r1 r2 H1 H2 a w; @;
679 ##[ #H; ncases (in_move_cat … H);
680 ##[ *; #w1; *; #w2; *; *; #defw w1m w2m;
681 ncases (H1 a w1); #H1w1; #_; nlapply (H1w1 w1m); #good;
682 nrewrite > defw; @2; @2 (a::w1); //; ncases good; ##[ *; #; ndestruct] //.
691 notation > "x ↦* E" non associative with precedence 60 for @{move_star ? $x $E}.
692 nlet rec move_star (S : decidable) w E on w : bool × (pre S) ≝
695 | cons x w' ⇒ w' ↦* (x ↦ \snd E)].
697 ndefinition in_moves ≝ λS:decidable.λw.λE:bool × (pre S). \fst(w ↦* E).
699 ncoinductive equiv (S:decidable) : bool × (pre S) → bool × (pre S) → Prop ≝
701 ∀E1,E2: bool × (pre S).
703 (∀x. equiv S (x ↦ \snd E1) (x ↦ \snd E2)) →
706 ndefinition NAT: decidable.
710 include "hints_declaration.ma".
712 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
713 unification hint 0 ≔ ; X ≟ NAT ⊢ carr X ≡ nat.
715 ninductive unit: Type[0] ≝ I: unit.
717 nlet corec foo_nop (b: bool):
719 〈 b, pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0))) 〉
720 〈 b, pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0) 〉 ≝ ?.
722 [ nnormalize in ⊢ (??%%); napply (foo_nop false)
724 [ nnormalize in ⊢ (??%%); napply (foo_nop false)
725 | #w; nnormalize in ⊢ (??%%); napply (foo_nop false) ]##]
729 nlet corec foo (a: unit):
731 (eclose NAT (pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0)))))
732 (eclose NAT (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0)))
737 [ nnormalize in ⊢ (??%%);
738 nnormalize in foo: (? → ??%%);
740 [ nnormalize in ⊢ (??%%); napply foo_nop
742 [ nnormalize in ⊢ (??%%);
744 ##| #z; nnormalize in ⊢ (??%%); napply foo_nop ]##]
745 ##| #y; nnormalize in ⊢ (??%%); napply foo_nop
750 ndefinition test1 : pre ? ≝ ❨ `0 | `1 ❩^* `0.
751 ndefinition test2 : pre ? ≝ ❨ (`0`1)^* `0 | (`0`1)^* `1 ❩.
752 ndefinition test3 : pre ? ≝ (`0 (`0`1)^* `1)^*.
755 nlemma foo: in_moves ? [0;0;1;0;1;1] (ɛ test3) = true.
756 nnormalize in match test3;
761 (**********************************************************)
763 ninductive der (S: Type[0]) (a: S) : re S → re S → CProp[0] ≝
764 der_z: der S a (z S) (z S)
765 | der_e: der S a (e S) (z S)
766 | der_s1: der S a (s S a) (e ?)
767 | der_s2: ∀b. a ≠ b → der S a (s S b) (z S)
768 | der_c1: ∀e1,e2,e1',e2'. in_l S [] e1 → der S a e1 e1' → der S a e2 e2' →
769 der S a (c ? e1 e2) (o ? (c ? e1' e2) e2')
770 | der_c2: ∀e1,e2,e1'. Not (in_l S [] e1) → der S a e1 e1' →
771 der S a (c ? e1 e2) (c ? e1' e2)
772 | der_o: ∀e1,e2,e1',e2'. der S a e1 e1' → der S a e2 e2' →
773 der S a (o ? e1 e2) (o ? e1' e2').
775 nlemma eq_rect_CProp0_r:
776 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
777 #A; #a; #x; #p; ncases p; #P; #H; nassumption.
780 nlemma append1: ∀A.∀a:A.∀l. [a] @ l = a::l. //. nqed.
782 naxiom in_l1: ∀S,r1,r2,w. in_l S [ ] r1 → in_l S w r2 → in_l S w (c S r1 r2).
783 (* #S; #r1; #r2; #w; nelim r1
785 | #H1; #H2; napply (in_c ? []); //
786 | (* tutti casi assurdi *) *)
788 ninductive in_l' (S: Type[0]) : word S → re S → CProp[0] ≝
789 in_l_empty1: ∀E.in_l S [] E → in_l' S [] E
790 | in_l_cons: ∀a,w,e,e'. in_l' S w e' → der S a e e' → in_l' S (a::w) e.
792 ncoinductive eq_re (S: Type[0]) : re S → re S → CProp[0] ≝
794 (in_l S [] E1 → in_l S [] E2) →
795 (in_l S [] E2 → in_l S [] E1) →
796 (∀a,E1',E2'. der S a E1 E1' → der S a E2 E2' → eq_re S E1' E2') →
799 (* serve il lemma dopo? *)
800 ntheorem eq_re_is_eq: ∀S.∀E1,E2. eq_re S E1 E2 → ∀w. in_l ? w E1 → in_l ? w E2.
801 #S; #E1; #E2; #H1; #w; #H2; nelim H2 in E2 H1 ⊢ %
803 | #a; #w; #R1; #R2; #K1; #K2; #K3; #R3; #K4; @2 R2; //; ncases K4;
805 (* IL VICEVERSA NON VALE *)
806 naxiom in_l_to_in_l: ∀S,w,E. in_l' S w E → in_l S w E.
807 (* #S; #w; #E; #H; nelim H
809 | #a; #w'; #r; #r'; #H1; (* e si cade qua sotto! *)
813 ntheorem der1: ∀S,a,e,e',w. der S a e e' → in_l S w e' → in_l S (a::w) e.
814 #S; #a; #E; #E'; #w; #H; nelim H
815 [##1,2: #H1; ninversion H1
816 [##1,8: #_; #K; (* non va ndestruct K; *) ncases (?:False); (* perche' due goal?*) /2/
817 |##2,9: #X; #Y; #K; ncases (?:False); /2/
818 |##3,10: #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
819 |##4,11: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
820 |##5,12: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
821 |##6,13: #x; #y; #K; ncases (?:False); /2/
822 |##7,14: #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/]
823 ##| #H1; ninversion H1
825 | #X; #Y; #K; ncases (?:False); /2/
826 | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
827 | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
828 | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
829 | #x; #y; #K; ncases (?:False); /2/
830 | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
831 ##| #H1; #H2; #H3; ninversion H3
832 [ #_; #K; ncases (?:False); /2/
833 | #X; #Y; #K; ncases (?:False); /2/
834 | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
835 | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
836 | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
837 | #x; #y; #K; ncases (?:False); /2/
838 | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
839 ##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6;