helm/software/matita/nlibrary/re/re.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (*include "logic/connectives.ma".*)
  16 (*include "logic/equality.ma".*)
  17 include "datatypes/list.ma".
  18 include "datatypes/pairs.ma".
  19 include "arithmetics/nat.ma".
  20
  21 (*include "Plogic/equality.ma".*)
  22
  23 nrecord Alpha : Type[1] ≝
  24  { carr :> Type[0];
  25    eqb: carr → carr → bool;
  26    eqb_true: ∀x,y. (eqb x y = true) = (x=y);
  27    eqb_false: ∀x,y. (eqb x y = false) = (x≠y)
  28  }.
  29
  30 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
  31 interpretation "eqb" 'eqb a b = (eqb ? a b).
  32
  33 ndefinition word ≝ λS:Alpha.list S.
  34
  35 ninductive re (S: Alpha) : Type[0] ≝
  36    z: re S
  37  | e: re S
  38  | s: S → re S
  39  | c: re S → re S → re S
  40  | o: re S → re S → re S
  41  | k: re S → re S.
  42
  43 notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
  44 notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}.
  45 interpretation "star" 'pk a = (k ? a).
  46 interpretation "or" 'plus a b = (o ? a b).
  47
  48 notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
  49 interpretation "cat" 'pc a b = (c ? a b).
  50
  51 (* to get rid of \middot *)
  52 ncoercion c  : ∀S:Alpha.∀p:re S.  re S →  re S   ≝ c  on _p : re ?  to ∀_:?.?.
  53
  54 notation < "a" non associative with precedence 90 for @{ 'ps $a}.
  55 notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
  56 interpretation "atom" 'ps a = (s ? a).
  57
  58 notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
  59 interpretation "epsilon" 'epsilon = (e ?).
  60
  61 notation "∅" non associative with precedence 90 for @{ 'empty }.
  62 interpretation "empty" 'empty = (z ?).
  63
  64 notation > "w ∈ E" non associative with precedence 45 for @{in_l ? $w $E}.
  65 ninductive in_l (S : Alpha) : word S → re S → Prop ≝
  66  | in_e: [ ] ∈ ϵ
  67  | in_s: ∀x:S. [x] ∈ `x
  68  | in_c: ∀w1,w2,e1,e2. w1 ∈ e1 → w2 ∈ e2 → w1@w2 ∈ e1 · e2
  69  | in_o1: ∀w,e1,e2. w ∈ e1 → w ∈ e1 + e2
  70  | in_o2: ∀w,e1,e2. w ∈ e2 → w ∈ e1 + e2
  71  | in_ke: ∀e. [ ] ∈ e^*
  72  | in_ki: ∀w1,w2,e. w1 ∈ e → w2 ∈ e^* → w1@w2 ∈ e^*.
  73 interpretation "in_l" 'mem w l = (in_l ? w l).
  74
  75 (*
  76 notation "a || b" left associative with precedence 30 for @{'orb $a $b}.
  77 interpretation "orb" 'orb a b = (orb a b).
  78
  79 notation "a && b" left associative with precedence 40 for @{'andb $a $b}.
  80 interpretation "andb" 'andb a b = (andb a b).
  81
  82 nlet rec weq (S : Alpha) (l1, l2 : word S) on l1 : bool ≝
  83 match l1 with
  84 [ nil ⇒ match l2 with [ nil ⇒ true | cons _ _ ⇒ false ]
  85 | cons x xs ⇒ match l2 with [ nil ⇒ false | cons y ys ⇒ (x == y) && weq S xs ys]].
  86
  87 ndefinition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
  88 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 }.
  89 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 }.
  90 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
  91
  92 *)
  93
  94 nlemma in_l_inv_e:
  95  ∀S.∀w:word S. w ∈ ∅ → w = [].
  96  #S; #w; #H; ninversion H; #; ndestruct;
  97 nqed.
  98
  99 nlemma in_l_inv_s: ∀S.∀w:word S.∀x. w ∈ `x → w = [x].
 100 #S w x H; ninversion H; #; ndestruct; //.
 101 nqed.
 102
 103 nlemma in_l_inv_c:
 104  ∀S.∀w:word S.∀E1,E2. w ∈ E1 · E2 → ∃w1.∃w2. w = w1@w2 ∧ w1 ∈ E1 ∧ w2 ∈ E2.
 105 #S w e1 e2 H; ninversion  H; ##[##1,2,4,5,6,7: #; ndestruct; ##]
 106 #w1 w2 r1 r2 w1r1 w2r2; #_; #_; #defw defe; @w1; @w2; ndestruct; /3/.
 107 nqed.
 108
 109 ninductive pitem (S: Alpha) : Type[0] ≝
 110    pz: pitem S
 111  | pe: pitem S
 112  | ps: S → pitem S
 113  | pp: S → pitem S
 114  | pc: pitem S → pitem S → pitem S
 115  | po: pitem S → pitem S → pitem S
 116  | pk: pitem S → pitem S.
 117
 118 ndefinition pre ≝ λS.pitem S × bool.
 119
 120 interpretation "pstar" 'pk a = (pk ? a).
 121 interpretation "por" 'plus a b = (po ? a b).
 122 interpretation "pcat" 'pc a b = (pc ? a b).
 123 notation < ".a" non associative with precedence 90 for @{ 'pp $a}.
 124 notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}.
 125 interpretation "ppatom" 'pp a = (pp ? a).
 126 (* to get rid of \middot *)
 127 ncoercion pc : ∀S.∀p:pitem S. pitem S → pitem S  ≝ pc on _p : pitem ? to ∀_:?.?.
 128 interpretation "patom" 'ps a = (ps ? a).
 129 interpretation "pepsilon" 'epsilon = (pe ?).
 130 interpretation "pempty" 'empty = (pz ?).
 131
 132 notation > ".|term 19 e|" non associative with precedence 90 for @{forget ? $e}.
 133 nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝
 134  match l with
 135   [ pz ⇒ ∅
 136   | pe ⇒ ϵ
 137   | ps x ⇒ `x
 138   | pp x ⇒ `x
 139   | pc E1 E2 ⇒ .|E1| .|E2|
 140   | po E1 E2 ⇒ .|E1| + .|E2|
 141   | pk E ⇒ .|E|^* ].
 142 notation < ".|term 19 e|" non associative with precedence 90 for @{'forget $e}.
 143 interpretation "forget" 'forget a = (forget ? a).
 144
 145 notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.
 146 interpretation "fst" 'fst x = (fst ? ? x).
 147 notation > "\snd term 90 x" non associative with precedence 90 for @{'snd $x}.
 148 interpretation "snd" 'snd x = (snd ? ? x).
 149
 150 notation > "w .∈ E" non associative with precedence 40 for @{in_pl ? $w $E}.
 151 ninductive in_pl (S: Alpha): word S → pitem S → Prop ≝
 152  | in_pp:  ∀x:S.[x] .∈ `.x
 153  | in_pc1: ∀w1,w2:word S.∀e1,e2:pitem S.
 154              w1 .∈ e1 → w2 ∈ .|e2| → (w1@w2) .∈ e1 · e2
 155  | in_pc2: ∀w,e1,e2. w .∈ e2 → w .∈ e1 · e2
 156  | in_po1: ∀w,e1,e2. w .∈ e1 → w .∈ e1 + e2
 157  | in_po2: ∀w,e1,e2. w .∈ e2 → w .∈ e1 + e2
 158  | in_pki: ∀w1,w2,e. w1 .∈ e → w2 ∈ .|e|^* → (w1@w2) .∈ e^*.
 159
 160 interpretation "in_pl" 'in_pl w l = (in_pl ? w l).
 161
 162 ndefinition in_prl ≝ λS : Alpha.λw:word S.λp:pre S.
 163   (w = [ ] ∧ \snd p = true) ∨ w .∈ (\fst p).
 164
 165 notation > "w .∈ E" non associative with precedence 40 for @{'in_pl $w $E}.
 166 notation < "w\shy .∈\shy E" non associative with precedence 40 for @{'in_pl $w $E}.
 167 interpretation "in_prl" 'in_pl w l = (in_prl ? w l).
 168
 169 interpretation "iff" 'iff a b = (iff a b).
 170
 171 nlemma append_eq_nil :
 172   ∀S.∀w1,w2:word S. [ ] = w1 @ w2 → w1 = [ ].
 173 #S w1; nelim w1; //. #x tl IH w2; nnormalize; #abs; ndestruct;
 174 nqed.
 175
 176 nlemma append_eq_nil_r :
 177   ∀S.∀w1,w2:word S. [ ] = w1 @ w2 → w2 = [ ].
 178 #S w1; nelim w1; ##[ #w2 H; nrewrite > H; // ]
 179 #x tl IH w2; nnormalize; #abs; ndestruct;
 180 nqed.
 181
 182 nlemma lemma16 :
 183   ∀S.∀e:pre S. [ ] .∈ e ↔ \snd e = true.
 184 #S p; ncases p; #e b; @; ##[##2: #H; nrewrite > H; @; @; //. ##]
 185 ncases b; //; *; ##[*; //] nelim e;
 186 ##[##1,2: #abs; ninversion abs; #; ndestruct;
 187 ##|##3,4: #x abs; ninversion abs; #; ndestruct;
 188 ##|#p1 p2 H1 H2 H; ninversion H; ##[##1,3,4,5,6: #; ndestruct; /2/. ##]
 189    #w1 w2 r1 r2 w1r1 w2fr2 H3 H4 Ep1p2; ndestruct;
 190    nrewrite > (append_eq_nil … H4) in w1r1; /2/ by {};
 191 ##|#r1 r2 H1 H2 H; ninversion H; #; ndestruct; /2/ by {};
 192 ##|#r H1 H2; ninversion H2; ##[##1,2,3,4,5: #; ndestruct; ##]
 193    #w1 w2 r1 w1r1 w1er1 H11 H21 H31;
 194    nrewrite > (append_eq_nil … H21) in w1r1 H1;
 195    nrewrite > (?: r = r1); /2/ by {};
 196    ndestruct; //. ##]
 197 nqed.
 198
 199 ndefinition lo ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a || \snd b〉.
 200 notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
 201 interpretation "oplus" 'oplus a b = (lo ? a b).
 202
 203 ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S.
 204    match a with [ mk_pair e1 b1 ⇒
 205    match b with [ mk_pair e2 b2 ⇒
 206    match b1 with
 207    [ false ⇒ 〈e1 · e2, b2〉
 208    | true ⇒ match bcast ? e2 with [ mk_pair e2' b2' ⇒ 〈e1 · e2', b2 || b2'〉 ]]]].
 209
 210 notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}.
 211 interpretation "lc" 'lc op a b = (lc ? op a b).
 212 notation > "a ⊙ b" left associative with precedence 60 for @{'lc eclose $a $b}.
 213
 214 ndefinition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa:pre S.
 215    match a with [ mk_pair e1 b1 ⇒
 216    match b1 with
 217    [ false ⇒ 〈e1^*, false〉
 218    | true ⇒ match bcast ? e1 with [ mk_pair e1' b1' ⇒ 〈e1'^*, true〉 ]]].
 219
 220 notation < "a \sup ⊛" non associative with precedence 90 for @{'lk ? $a}.
 221 interpretation "lk" 'lk op a = (lk ? op a).
 222 notation > "a^⊛" non associative with precedence 90 for @{'lk eclose $a}.
 223
 224 notation > "•" non associative with precedence 60 for @{eclose ?}.
 225 nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝
 226  match E with
 227   [ pz ⇒ 〈 ∅, false 〉
 228   | pe ⇒ 〈 ϵ,  true 〉
 229   | ps x ⇒ 〈 `.x, false 〉
 230   | pp x ⇒ 〈 `.x, false 〉
 231   | po E1 E2 ⇒ •E1 ⊕ •E2
 232   | pc E1 E2 ⇒ •E1 ⊙ 〈 E2, false 〉
 233   | pk E ⇒ 〈E,true〉^⊛].
 234 notation < "• x" non associative with precedence 60 for @{'eclose $x}.
 235 interpretation "eclose" 'eclose x = (eclose ? x).
 236 notation > "• x" non associative with precedence 60 for @{'eclose $x}.
 237
 238 ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉.
 239 interpretation "reclose" 'eclose x = (reclose ? x).
 240
 241 nlemma lemma19_2 :
 242  ∀S:Alpha.∀e1,e2:pre S.∀w. w .∈ e1 ⊕ e2 → w .∈ e1 ∨ w .∈ e2.
 243 #S e1 e2 w H; nnormalize in H; ncases H;
 244 ##[ *; #defw; ncases e1; #p b; ncases b; nnormalize;
 245     ##[ #_; @1; @1; /2/ by conj;
 246     ##| #H1; @2; @1; /2/ by conj; ##]
 247 ##| #H1; ninversion H1; #; ndestruct; /4/ by or_introl, or_intror; ##]
 248 nqed.
 249
 250 notation > "\move term 90 x term 90 E"
 251 non associative with precedence 60 for @{move ? $x $E}.
 252 nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝
 253  match E with
 254   [ pz ⇒ 〈 ∅, false 〉
 255   | pe ⇒ 〈 ϵ, false 〉
 256   | ps y ⇒ 〈 `y, false 〉
 257   | pp y ⇒ 〈 `y, x == y 〉
 258   | po e1 e2 ⇒ \move x e1 ⊕ \move x e2
 259   | pc e1 e2 ⇒ \move x e1 ⊙ \move x e2
 260   | pk e ⇒ (\move x e)^⊛ ].
 261 notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}.
 262 notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}.
 263 interpretation "move" 'move x E = (move ? x E).
 264
 265 ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e).
 266 interpretation "rmove" 'move x E = (rmove ? x E).
 267
 268 nlemma XXz :  ∀S:Alpha.∀w:word S. w .∈ ∅ → False.
 269 #S w abs; ninversion abs; #; ndestruct;
 270 nqed.
 271
 272
 273 nlemma XXe :  ∀S:Alpha.∀w:word S. w .∈ ϵ → False.
 274 #S w abs; ninversion abs; #; ndestruct;
 275 nqed.
 276
 277 nlemma XXze :  ∀S:Alpha.∀w:word S. w .∈ (∅ · ϵ)  → False.
 278 #S w abs; ninversion abs; #; ndestruct; /2/ by XXz,XXe;
 279 nqed.
 280
 281 nlemma eqb_t : ∀S:Alpha.∀a,b:S.∀p:a == b = true. a = b.
 282 #S a b H; nrewrite < (eqb_true ? a b); //.
 283 nqed.
 284
 285 naxiom in_move_cat:
 286  ∀S.∀w:word S.∀x.∀E1,E2:pitem S. w .∈ \move x (E1 · E2) →
 287    (∃w1.∃w2. w = w1@w2 ∧ w1 .∈ \move x E1 ∧ w2 ∈ .|E2|) ∨ w .∈ \move x E2.
 288 #S w x e1 e2 H; nchange in H with (w .∈ \move x e1 ⊙ \move x e2);
 289 ncases e1 in H; ncases e2;
 290 ##[##1: *; ##[*; nnormalize; #; ndestruct]
 291    #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
 292    nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze;
 293 ##|##2: *; ##[*; nnormalize; #; ndestruct]
 294    #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
 295    nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze;
 296 ##| #r; *; ##[ *; nnormalize; #; ndestruct]
 297    #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
 298    ##[##2: nnormalize; #; ndestruct; @2; @2; //.##]
 299    nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz;
 300 ##| #y; *; ##[ *; nnormalize; #defw defx; ndestruct; @2; @1; /2/ by conj;##]
 301    #H; ninversion H; nnormalize; #; ndestruct;
 302    ##[ncases (?:False); /2/ by XXz] /3/ by or_intror;
 303 ##| #r1 r2; *; ##[ *; #defw]
 304     ...
 305 nqed.
 306
 307 ntheorem move_ok:
 308  ∀S:Alpha.∀E:pre S.∀a,w.w .∈ \move a E ↔ (a :: w) .∈ E.
 309 #S E; ncases E; #r b; nelim r;
 310 ##[##1,2: #a w; @;
 311    ##[##1,3: nnormalize; *; ##[##1,3: *; #; ndestruct; ##| #abs; ncases (XXz … abs); ##]
 312       #H; ninversion H; #; ndestruct;
 313    ##|##*:nnormalize; *; ##[##1,3: *; #; ndestruct; ##| #H1; ncases (XXz … H1); ##]
 314        #H; ninversion H; #; ndestruct;##]
 315 ##|#a c w; @; nnormalize; ##[*; ##[*; #; ndestruct; ##] #abs; ninversion abs; #; ndestruct;##]
 316    *; ##[##2: #abs; ninversion abs; #; ndestruct; ##] *; #; ndestruct;
 317 ##|#a c w; @; nnormalize;
 318    ##[ *; ##[ *; #defw; nrewrite > defw; #ca; @2;  nrewrite > (eqb_t … ca); @; ##]
 319        #H; ninversion H; #; ndestruct;
 320    ##| *; ##[ *; #; ndestruct; ##] #H; ninversion H; ##[##2,3,4,5,6: #; ndestruct]
 321               #d defw defa; ndestruct; @1; @; //; nrewrite > (eqb_true S d d); //. ##]
 322 ##|#r1 r2 H1 H2 a w; @;
 323    ##[ #H; ncases (in_move_cat … H);
 324       ##[ *; #w1; *; #w2; *; *; #defw w1m w2m;
 325           ncases (H1 a w1); #H1w1; #_; nlapply (H1w1 w1m); #good;
 326           nrewrite > defw; @2; @2 (a::w1); //; ncases good; ##[ *; #; ndestruct] //.
 327       ##|
 328       ...
 329 ##|
 330 ##|
 331 ##]
 332 nqed.
 333
 334
 335 notation > "x ↦* E" non associative with precedence 60 for @{move_star ? $x $E}.
 336 nlet rec move_star (S : decidable) w E on w : bool × (pre S) ≝
 337  match w with
 338   [ nil ⇒ E
 339   | cons x w' ⇒ w' ↦* (x ↦ \snd E)].
 340
 341 ndefinition in_moves ≝ λS:decidable.λw.λE:bool × (pre S). \fst(w ↦* E).
 342
 343 ncoinductive equiv (S:decidable) : bool × (pre S) → bool × (pre S) → Prop ≝
 344  mk_equiv:
 345   ∀E1,E2: bool × (pre S).
 346    \fst E1  = \fst E2 →
 347     (∀x. equiv S (x ↦ \snd E1) (x ↦ \snd E2)) →
 348      equiv S E1 E2.
 349
 350 ndefinition NAT: decidable.
 351  @ nat eqb; /2/.
 352 nqed.
 353
 354 include "hints_declaration.ma".
 355
 356 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
 357 unification hint 0 ≔ ; X ≟ NAT ⊢ carr X ≡ nat.
 358
 359 ninductive unit: Type[0] ≝ I: unit.
 360
 361 nlet corec foo_nop (b: bool):
 362  equiv ?
 363   〈 b, pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0))) 〉
 364   〈 b, pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0) 〉 ≝ ?.
 365  @; //; #x; ncases x
 366   [ nnormalize in ⊢ (??%%); napply (foo_nop false)
 367   | #y; ncases y
 368      [ nnormalize in ⊢ (??%%); napply (foo_nop false)
 369      | #w; nnormalize in ⊢ (??%%); napply (foo_nop false) ]##]
 370 nqed.
 371
 372 (*
 373 nlet corec foo (a: unit):
 374  equiv NAT
 375   (eclose NAT (pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0)))))
 376   (eclose NAT (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0)))
 377 ≝ ?.
 378  @;
 379   ##[ nnormalize; //
 380   ##| #x; ncases x
 381        [ nnormalize in ⊢ (??%%);
 382          nnormalize in foo: (? → ??%%);
 383          @; //; #y; ncases y
 384            [ nnormalize in ⊢ (??%%); napply foo_nop
 385            | #y; ncases y
 386               [ nnormalize in ⊢ (??%%);
 387
 388             ##| #z; nnormalize in ⊢ (??%%); napply foo_nop ]##]
 389      ##| #y; nnormalize in ⊢ (??%%); napply foo_nop
 390   ##]
 391 nqed.
 392 *)
 393
 394 ndefinition test1 : pre ? ≝ ❨ `0 | `1 ❩^* `0.
 395 ndefinition test2 : pre ? ≝ ❨ (`0`1)^* `0 | (`0`1)^* `1 ❩.
 396 ndefinition test3 : pre ? ≝ (`0 (`0`1)^* `1)^*.
 397
 398
 399 nlemma foo: in_moves ? [0;0;1;0;1;1] (ɛ test3) = true.
 400  nnormalize in match test3;
 401  nnormalize;
 402 //;
 403 nqed.
 404
 405 (**********************************************************)
 406
 407 ninductive der (S: Type[0]) (a: S) : re S → re S → CProp[0] ≝
 408    der_z: der S a (z S) (z S)
 409  | der_e: der S a (e S) (z S)
 410  | der_s1: der S a (s S a) (e ?)
 411  | der_s2: ∀b. a ≠ b → der S a (s S b) (z S)
 412  | der_c1: ∀e1,e2,e1',e2'. in_l S [] e1 → der S a e1 e1' → der S a e2 e2' →
 413             der S a (c ? e1 e2) (o ? (c ? e1' e2) e2')
 414  | der_c2: ∀e1,e2,e1'. Not (in_l S [] e1) → der S a e1 e1' →
 415             der S a (c ? e1 e2) (c ? e1' e2)
 416  | der_o: ∀e1,e2,e1',e2'. der S a e1 e1' → der S a e2 e2' →
 417     der S a (o ? e1 e2) (o ? e1' e2').
 418
 419 nlemma eq_rect_CProp0_r:
 420  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
 421  #A; #a; #x; #p; ncases p; #P; #H; nassumption.
 422 nqed.
 423
 424 nlemma append1: ∀A.∀a:A.∀l. [a] @ l = a::l. //. nqed.
 425
 426 naxiom in_l1: ∀S,r1,r2,w. in_l S [ ] r1 → in_l S w r2 → in_l S w (c S r1 r2).
 427 (* #S; #r1; #r2; #w; nelim r1
 428   [ #K; ninversion K
 429   | #H1; #H2; napply (in_c ? []); //
 430   | (* tutti casi assurdi *) *)
 431
 432 ninductive in_l' (S: Type[0]) : word S → re S → CProp[0] ≝
 433    in_l_empty1: ∀E.in_l S [] E → in_l' S [] E
 434  | in_l_cons: ∀a,w,e,e'. in_l' S w e' → der S a e e' → in_l' S (a::w) e.
 435
 436 ncoinductive eq_re (S: Type[0]) : re S → re S → CProp[0] ≝
 437    mk_eq_re: ∀E1,E2.
 438     (in_l S [] E1 → in_l S [] E2) →
 439     (in_l S [] E2 → in_l S [] E1) →
 440     (∀a,E1',E2'. der S a E1 E1' → der S a E2 E2' → eq_re S E1' E2') →
 441       eq_re S E1 E2.
 442
 443 (* serve il lemma dopo? *)
 444 ntheorem eq_re_is_eq: ∀S.∀E1,E2. eq_re S E1 E2 → ∀w. in_l ? w E1 → in_l ? w E2.
 445  #S; #E1; #E2; #H1; #w; #H2; nelim H2 in E2 H1 ⊢ %
 446   [ #r; #K (* ok *)
 447   | #a; #w; #R1; #R2; #K1; #K2; #K3; #R3; #K4; @2 R2; //; ncases K4;
 448
 449 (* IL VICEVERSA NON VALE *)
 450 naxiom in_l_to_in_l: ∀S,w,E. in_l' S w E → in_l S w E.
 451 (* #S; #w; #E; #H; nelim H
 452   [ //
 453   | #a; #w'; #r; #r'; #H1; (* e si cade qua sotto! *)
 454   ]
 455 nqed. *)
 456
 457 ntheorem der1: ∀S,a,e,e',w. der S a e e' → in_l S w e' → in_l S (a::w) e.
 458  #S; #a; #E; #E'; #w; #H; nelim H
 459   [##1,2: #H1; ninversion H1
 460      [##1,8: #_; #K; (* non va ndestruct K; *) ncases (?:False); (* perche' due goal?*) /2/
 461      |##2,9: #X; #Y; #K; ncases (?:False); /2/
 462      |##3,10: #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
 463      |##4,11: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 464      |##5,12: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 465      |##6,13: #x; #y; #K; ncases (?:False); /2/
 466      |##7,14: #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/]
 467 ##| #H1; ninversion H1
 468      [ //
 469      | #X; #Y; #K; ncases (?:False); /2/
 470      | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
 471      | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 472      | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 473      | #x; #y; #K; ncases (?:False); /2/
 474      | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
 475 ##| #H1; #H2; #H3; ninversion H3
 476      [ #_; #K; ncases (?:False); /2/
 477      | #X; #Y; #K; ncases (?:False); /2/
 478      | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
 479      | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 480      | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 481      | #x; #y; #K; ncases (?:False); /2/
 482      | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
 483 ##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6;
 484