weblib/tutorial/chapter2.ma

   1 include "basics/logic.ma".
   2
   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 *)
  11
  12 inductive nat : Type[0] ≝
  13 | O :nat
  14 | S: nat →nat.
  15
  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.
  20
  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 *)
  27
  28 let rec add n m ≝
  29 match n with
  30 [ O ⇒ m
  31 | S a ⇒ \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (add a m)
  32 ].
  33
  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.
  40
  41 The elim tactic, allow you to apply induction in a vcery simple way. If your
  42 goal is P(n), the invocation of
  43   elim n
  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 *)
  46
  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.
  48 #a elim a
  49
  50 (* If you stop the computation here, you will see on the right the two subgoals
  51     - add O O = O
  52     - ∀x. add x 0 = x → add (S x) O = S x
  53 After normalization, both goals are trivial.
  54 *)
  55
  56 normalize // qed.
  57
  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. *)
  60
  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).
  62
  63 (* In the same way as before, we proceed by induction over a. *)
  64
  65 #a #b elim a normalize //
  66 qed.
  67
  68 (* We are now in the position to prove the commutativity of the sum *)
  69
  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.
  71 #a elim a normalize
  72
  73 (* We have two sub goals:
  74   G1: ∀b. b = add b O
  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 // *)
  79
  80 // qed.
  81
  82 (* Let us now define the following function: *)
  83
  84 definition twice ≝ λn.\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 n n.
  85
  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. *)
  91
  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).
  93
  94
  95
  96  include "basics.ma".
  97 include "basics/list.ma".
  98
  99 interpretation "iff" 'iff a b = (iff a b).
 100
 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)
 104 }.
 105
 106 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
 107 interpretation "eqb" 'eqb a b = (eqb ? a b).
 108
 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.
 110
 111 inductive re (S: \ 5a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) : Type[0] ≝
 112    z: re S
 113  | e: re S
 114  | s: S → re S
 115  | c: re S → re S → re S
 116  | o: re S → re S → re S
 117  | k: re S → re S.
 118
 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).
 123
 124 notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
 125 interpretation "cat" 'pc a b = (c ? a b).
 126
 127 (* to get rid of \middot
 128 coercion c  : ∀S:Alpha.∀p:re S.  re S →  re S   ≝ c  on _p : re ?  to ∀_:?.?. *)
 129
 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).
 133
 134 notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
 135 interpretation "epsilon" 'epsilon = (e ?).
 136
 137 notation "∅" non associative with precedence 90 for @{ 'empty }.
 138 interpretation "empty" 'empty = (z ?).
 139
 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 ].
 142
 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 ].
 145
 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 ?).
 149
 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).
 153
 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).
 156
 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).
 160
 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).
 163
 164 notation > "𝐋 term 70 E" non associative with precedence 75 for @{in_l ? $E}.
 165
 166 let rec in_l (S : Alpha) (r : re S) on r : word S → Prop ≝
 167 match r with
 168 [ z ⇒ {}
 169 | e ⇒ { [ ] }
 170 | s x ⇒ { [x] }
 171 | c r1 r2 ⇒ 𝐋 r1 · 𝐋 r2
 172 | o r1 r2 ⇒  𝐋 r1 ∪ 𝐋 r2
 173 | k r1 ⇒ (𝐋 r1) ^*].
 174
 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).
 178
 179 notation "a || b" left associative with precedence 30 for @{'orb $a $b}.
 180 interpretation "orb" 'orb a b = (orb a b).
 181
 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).
 186
 187 ninductive pitem (S: Alpha) : Type[0] ≝
 188    pz: pitem S
 189  | pe: pitem S
 190  | ps: S → pitem S
 191  | pp: S → pitem S
 192  | pc: pitem S → pitem S → pitem S
 193  | po: pitem S → pitem S → pitem S
 194  | pk: pitem S → pitem S.
 195
 196 ndefinition pre ≝ λS.pitem S × bool.
 197
 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 ?).
 209
 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 ≝
 212  match l with
 213   [ pz ⇒ ∅
 214   | pe ⇒ ϵ
 215   | ps x ⇒ `x
 216   | pp x ⇒ `x
 217   | pc E1 E2 ⇒ (|E1| · |E2|)
 218   | po E1 E2 ⇒ (|E1| + |E2|)
 219   | pk E ⇒ |E|^* ].
 220 notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.
 221 interpretation "forget" 'forget a = (forget ? a).
 222
 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).
 227
 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 ≝
 230 match r with
 231 [ pz ⇒ {}
 232 | pe ⇒ {}
 233 | ps _ ⇒ {}
 234 | pp x ⇒ { [x] }
 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).
 242
 243 ndefinition epsilon ≝ λS,b.if b then { ([ ] : word S) } else {}.
 244
 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).
 248
 249 ndefinition in_prl ≝ λS : Alpha.λp:pre S.  𝐋\p (\fst p) ∪ ϵ (\snd p).
 250
 251 interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
 252 interpretation "in_prl" 'in_pl E = (in_prl ? E).
 253
 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.
 256
 257 (* lemma 12 *)
 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 {};//;
 265 nqed.
 266
 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/;##]
 275 nqed.
 276
 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).
 280
 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 ⇒
 283    match b1 with
 284    [ false ⇒ 〈e1 · \fst b, \snd b〉
 285    | true ⇒ 〈e1 · \fst (bcast ? (\fst b)),\snd b || \snd (bcast ? (\fst b))〉]].
 286
 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}.
 290
 291 ndefinition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa:pre S.
 292    match a with [ mk_pair e1 b1 ⇒
 293    match b1 with
 294    [ false ⇒ 〈e1^*, false〉
 295    | true ⇒ 〈(\fst (bcast ? e1))^*, true〉]].
 296
 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}.
 300
 301 notation > "•" non associative with precedence 60 for @{eclose ?}.
 302 nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝
 303  match E with
 304   [ pz ⇒ 〈 ∅, false 〉
 305   | pe ⇒ 〈 ϵ,  true 〉
 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}.
 314
 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).
 317
 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).
 322
 323 naxiom extP : ∀S.∀p,q:word S → Prop.(p =1 q) → p = q.
 324
 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/; *; //; *;
 327 nqed.
 328
 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.
 331
 332 nlemma cupC : ∀S. ∀a,b:word S → Prop.a ∪ b = b ∪ a.
 333 #S a b; napply extP; #w; @; *; nnormalize; /2/; nqed.
 334
 335 (* theorem 16: 2 *)
 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 …); //;
 344 nqed.
 345
 346 nlemma odotEt :
 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.
 349
 350 nlemma LcatE : ∀S.∀e1,e2:pitem S.𝐋\p (e1 · e2) =  𝐋\p e1 · 𝐋 |e2| ∪ 𝐋\p e2. //; nqed.
 351
 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; ##]
 356 nqed.
 357
 358 nlemma cup0 :∀S.∀p:word S → Prop.p ∪ {} = p.
 359 #S p; napply extP; #w; nnormalize; @; /2/; *; //; *; nqed.
 360
 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;
 363 nqed.
 364
 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.
 367
 368 nlemma erase_star : ∀S.∀e1:pitem S.𝐋 |e1|^* = 𝐋 |e1^*|. //; nqed.
 369
 370 ndefinition substract := λS.λp,q:word S → Prop.λw.p w ∧ ¬ q w.
 371 interpretation "substract" 'minus a b = (substract ? a b).
 372
 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.
 375
 376 nlemma sub0 : ∀S.∀a:word S → Prop. a - {} = a.
 377 #S a; napply extP; #w; nnormalize; @; /3/; *; //; nqed.
 378
 379 nlemma subK : ∀S.∀a:word S → Prop. a - a = {}.
 380 #S a; napply extP; #w; nnormalize; @; *; /2/; nqed.
 381
 382 nlemma subW : ∀S.∀a,b:word S → Prop.∀w.(a - b) w → a w.
 383 #S a b w; nnormalize; *; //; nqed.
 384
 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))^*; //; ##]
 398 nqed.
 399
 400 nlemma eta_lp : ∀S.∀p:pre S.𝐋\p p = 𝐋\p 〈\fst p, \snd p〉.
 401 #S p; ncases p; //; nqed.
 402
 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;
 406 napply Hw2; nqed.
 407
 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 (?∪?);
 433     nrewrite > (cup0…);
 434     nrewrite > (cupA…); //;##]
 435 nqed.
 436
 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]
 455                    @wl'; @; //; ##] ##]
 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]
 460                 @[]; @; //;
 461             ##| @; @w'; @[]; nrewrite > (append_nil…); @; ##[##2: @[]; @; //]
 462                 @; //; @; //; @; *;##]##]##]
 463 nqed.
 464
 465 (* theorem 16: 1 *)
 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|.
 471 #S e; nelim e; //;
 472   ##[ #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl, or_intror;
 473   ##| #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl; *;
 474   ##| #e1 e2 IH1 IH2;
 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 …); //;
 481   ##| #e1 e2 IH1 IH2;
 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;##]
 501  nqed.
 502
 503 (* theorem 16: 3 *)
 504 nlemma odot_dot:
 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.
 507
 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;
 515     @; /2/; @xs; /2/;##]
 516  nqed.
 517
 518 nlemma nil_star : ∀S.∀e:re S. [ ] ∈ e^*.
 519 #S e; @[]; /2/; nqed.
 520
 521 nlemma cupID : ∀S.∀l:word S → Prop.l ∪ l = l.
 522 #S l; napply extP; #w; @; ##[*]//; #; @; //; nqed.
 523
 524 nlemma cup_star_nil : ∀S.∀l:word S → Prop. l^* ∪ {[]} = l^*.
 525 #S a; napply extP; #w; @; ##[*; //; #H; nrewrite < H; @[]; @; //] #;@; //;nqed.
 526
 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); *]
 531 nqed.
 532
 533 (* theorem 16: 4 *)
 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 (?∪?);
 551     nrewrite > (cup0…);
 552     nchange in ⊢ (??%?) with (𝐋\p e · 𝐋 |e|^* );
 553     nrewrite < (cup0 ? (𝐋\p e)); //;##]
 554 nqed.
 555
 556 nlet rec pre_of_re (S : Alpha) (e : re S) on e : pitem S ≝
 557   match e with
 558   [ z ⇒ pz ?
 559   | e ⇒ pe ?
 560   | s x ⇒ ps ? x
 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)].
 564
 565 nlemma notFalse : ¬False. @; //; nqed.
 566
 567 nlemma dot0 : ∀S.∀A:word S → Prop. {} · A = {}.
 568 #S A; nnormalize; napply extP; #w; @; ##[##2: *]
 569 *; #w1; *; #w2; *; *; //; nqed.
 570
 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; ##]
 579 nqed.
 580
 581 nlemma erase_pre_of_reK : ∀S.∀e. 𝐋 |pre_of_re S e| = 𝐋 e.
 582 #S A; nelim A; //;
 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)^* );
 588     nrewrite < H1; //]
 589 nqed.
 590
 591 (* corollary 17 *)
 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…); //;
 595 nqed.
 596
 597 nlemma Pext : ∀S.∀f,g:word S → Prop. f = g → ∀w.f w → g w.
 598 #S f g H; nrewrite > H; //; nqed.
 599
 600 (* corollary 18 *)
 601 ntheorem bull_true_epsilon : ∀S.∀e:pitem S. \snd (•e) = true ↔ [ ] ∈ |e|.
 602 #S e; @;
 603 ##[ #defsnde; nlapply (bull_cup ? e); nchange in match (𝐋\p (•e)) with (?∪?);
 604     nrewrite > defsnde; #H;
 605     nlapply (Pext ??? H [ ] ?); ##[ @2; //] *; //;
 606
 607 STOP
 608
 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 ≝
 612  match E with
 613   [ pz ⇒ 〈 ∅, false 〉
 614   | pe ⇒ 〈 ϵ, false 〉
 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).
 623
 624 ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e).
 625 interpretation "rmove" 'move x E = (rmove ? x E).
 626
 627 nlemma XXz :  ∀S:Alpha.∀w:word S. w ∈ ∅ → False.
 628 #S w abs; ninversion abs; #; ndestruct;
 629 nqed.
 630
 631
 632 nlemma XXe :  ∀S:Alpha.∀w:word S. w .∈ ϵ → False.
 633 #S w abs; ninversion abs; #; ndestruct;
 634 nqed.
 635
 636 nlemma XXze :  ∀S:Alpha.∀w:word S. w .∈ (∅ · ϵ)  → False.
 637 #S w abs; ninversion abs; #; ndestruct; /2/ by XXz,XXe;
 638 nqed.
 639
 640
 641 naxiom in_move_cat:
 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]
 660     ...
 661 nqed.
 662
 663 ntheorem move_ok:
 664  ∀S:Alpha.∀E:pre S.∀a,w.w .∈ \move a E ↔ (a :: w) .∈ E.
 665 #S E; ncases E; #r b; nelim r;
 666 ##[##1,2: #a w; @;
 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] //.
 683       ##|
 684       ...
 685 ##|
 686 ##|
 687 ##]
 688 nqed.
 689
 690
 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) ≝
 693  match w with
 694   [ nil ⇒ E
 695   | cons x w' ⇒ w' ↦* (x ↦ \snd E)].
 696
 697 ndefinition in_moves ≝ λS:decidable.λw.λE:bool × (pre S). \fst(w ↦* E).
 698
 699 ncoinductive equiv (S:decidable) : bool × (pre S) → bool × (pre S) → Prop ≝
 700  mk_equiv:
 701   ∀E1,E2: bool × (pre S).
 702    \fst E1  = \fst E2 →
 703     (∀x. equiv S (x ↦ \snd E1) (x ↦ \snd E2)) →
 704      equiv S E1 E2.
 705
 706 ndefinition NAT: decidable.
 707  @ nat eqb; /2/.
 708 nqed.
 709
 710 include "hints_declaration.ma".
 711
 712 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
 713 unification hint 0 ≔ ; X ≟ NAT ⊢ carr X ≡ nat.
 714
 715 ninductive unit: Type[0] ≝ I: unit.
 716
 717 nlet corec foo_nop (b: bool):
 718  equiv ?
 719   〈 b, pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0))) 〉
 720   〈 b, pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0) 〉 ≝ ?.
 721  @; //; #x; ncases x
 722   [ nnormalize in ⊢ (??%%); napply (foo_nop false)
 723   | #y; ncases y
 724      [ nnormalize in ⊢ (??%%); napply (foo_nop false)
 725      | #w; nnormalize in ⊢ (??%%); napply (foo_nop false) ]##]
 726 nqed.
 727
 728 (*
 729 nlet corec foo (a: unit):
 730  equiv NAT
 731   (eclose NAT (pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0)))))
 732   (eclose NAT (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0)))
 733 ≝ ?.
 734  @;
 735   ##[ nnormalize; //
 736   ##| #x; ncases x
 737        [ nnormalize in ⊢ (??%%);
 738          nnormalize in foo: (? → ??%%);
 739          @; //; #y; ncases y
 740            [ nnormalize in ⊢ (??%%); napply foo_nop
 741            | #y; ncases y
 742               [ nnormalize in ⊢ (??%%);
 743
 744             ##| #z; nnormalize in ⊢ (??%%); napply foo_nop ]##]
 745      ##| #y; nnormalize in ⊢ (??%%); napply foo_nop
 746   ##]
 747 nqed.
 748 *)
 749
 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)^*.
 753
 754
 755 nlemma foo: in_moves ? [0;0;1;0;1;1] (ɛ test3) = true.
 756  nnormalize in match test3;
 757  nnormalize;
 758 //;
 759 nqed.
 760
 761 (**********************************************************)
 762
 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').
 774
 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.
 778 nqed.
 779
 780 nlemma append1: ∀A.∀a:A.∀l. [a] @ l = a::l. //. nqed.
 781
 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
 784   [ #K; ninversion K
 785   | #H1; #H2; napply (in_c ? []); //
 786   | (* tutti casi assurdi *) *)
 787
 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.
 791
 792 ncoinductive eq_re (S: Type[0]) : re S → re S → CProp[0] ≝
 793    mk_eq_re: ∀E1,E2.
 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') →
 797       eq_re S E1 E2.
 798
 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 ⊢ %
 802   [ #r; #K (* ok *)
 803   | #a; #w; #R1; #R2; #K1; #K2; #K3; #R3; #K4; @2 R2; //; ncases K4;
 804
 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
 808   [ //
 809   | #a; #w'; #r; #r'; #H1; (* e si cade qua sotto! *)
 810   ]
 811 nqed. *)
 812
 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
 824      [ //
 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;