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 interpretation "iff" 'iff a b = (iff a b).
  24
  25 nrecord Alpha : Type[1] ≝
  26  { carr :> Type[0];
  27    eqb: carr → carr → bool;
  28    eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
  29  }.
  30
  31 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
  32 interpretation "eqb" 'eqb a b = (eqb ? a b).
  33
  34 ndefinition word ≝ λS:Alpha.list S.
  35
  36 ninductive re (S: Alpha) : Type[0] ≝
  37    z: re S
  38  | e: re S
  39  | s: S → re S
  40  | c: re S → re S → re S
  41  | o: re S → re S → re S
  42  | k: re S → re S.
  43
  44 notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
  45 notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}.
  46 interpretation "star" 'pk a = (k ? a).
  47 interpretation "or" 'plus a b = (o ? a b).
  48
  49 notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
  50 interpretation "cat" 'pc a b = (c ? a b).
  51
  52 (* to get rid of \middot *)
  53 ncoercion c  : ∀S:Alpha.∀p:re S.  re S →  re S   ≝ c  on _p : re ?  to ∀_:?.?.
  54
  55 notation < "a" non associative with precedence 90 for @{ 'ps $a}.
  56 notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
  57 interpretation "atom" 'ps a = (s ? a).
  58
  59 notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
  60 interpretation "epsilon" 'epsilon = (e ?).
  61
  62 notation "∅" non associative with precedence 90 for @{ 'empty }.
  63 interpretation "empty" 'empty = (z ?).
  64
  65 notation > "w ∈ E" non associative with precedence 45 for @{in_l ? $w $E}.
  66 ninductive in_l (S : Alpha) : word S → re S → Prop ≝
  67  | in_e: [ ] ∈ ϵ
  68  | in_s: ∀x:S. [x] ∈ `x
  69  | in_c: ∀w1,w2,e1,e2. w1 ∈ e1 → w2 ∈ e2 → w1@w2 ∈ e1 · e2
  70  | in_o1: ∀w,e1,e2. w ∈ e1 → w ∈ e1 + e2
  71  | in_o2: ∀w,e1,e2. w ∈ e2 → w ∈ e1 + e2
  72  | in_ke: ∀e. [ ] ∈ e^*
  73  | in_ki: ∀w1,w2,e. w1 ∈ e → w2 ∈ e^* → w1@w2 ∈ e^*.
  74 interpretation "in_l" 'mem w l = (in_l ? w l).
  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 notation "~~ a" non associative with precedence 40 for @{'notb $a}.
  83 interpretation "notb" 'notb a = (notb a).
  84
  85 nlet rec weq (S : Alpha) (l1, l2 : word S) on l1 : bool ≝
  86 match l1 with
  87 [ nil ⇒ match l2 with [ nil ⇒ true | cons _ _ ⇒ false ]
  88 | cons x xs ⇒ match l2 with [ nil ⇒ false | cons y ys ⇒ (x == y) && weq S xs ys]].
  89
  90 ndefinition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
  91 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 }.
  92 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 }.
  93 interpretation "if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
  94
  95 interpretation "qew" 'eqb a b = (weq ? a b).
  96
  97 ndefinition is_epsilon ≝ λA.λw:word A. w == [ ].
  98 ndefinition is_empty ≝ λA.λw:word A.false.
  99 ndefinition is_char ≝ λA,x.λw:word A. w == [ x ].
 100
 101 nlemma andP : ∀a,b.(a && b) = true ↔ (a = true ∧ b = true).
 102 #a b; ncases a; ncases b; nnormalize; @; ##[##2,4,6,8: *] /2/;
 103 nqed.
 104
 105 nlemma orP : ∀a,b.(a || b) = true ↔ (a = true ∨ b = true).
 106 #a b; ncases a; ncases b; nnormalize; @; ##[##2,4,6,8: *] /2/;
 107 nqed.
 108
 109 nlemma iff_l2r : ∀a,p.a = true ↔ p → a = true → p.
 110 #a p; *; /2/;
 111 nqed.
 112
 113 nlemma iff_r2l : ∀a,p.a = true ↔ p → p → a = true.
 114 #a p; *; /2/;
 115 nqed.
 116
 117 ncoercion xx : ∀a,p.∀H:a = true ↔ p. a = true → p ≝ iff_l2r
 118 on _H : (? = true) ↔ ? to ∀_:?. ?.
 119
 120 ncoercion yy : ∀a,p.∀H:a = true ↔ p. p → a = true ≝ iff_r2l
 121 on _H : (? = true) ↔ ? to ∀_:?. ?.
 122
 123 ndefinition wAlpha : Alpha → Alpha. #A; @ (word A) (weq A).
 124 #x; nelim x; ##[ #y; ncases y; /2/; #x xs; @; nnormalize; #; ndestruct; ##]
 125 #x xs; #IH y; nelim y; ##[ @; nnormalize; #; ndestruct; ##]
 126 #y ys; *; #H1 H2; @; #H3;
 127 ##[ ##2: ncases (IH ys); #_; #H; ndestruct; nrewrite > (iff_r2l ?? (eqb_true ???) ?); //; napply H; //]
 128 nrewrite > (iff_l2r ?? (eqb_true ? x y) ?); nnormalize in H3; ncases (x == y) in H3; nnormalize; /2/;
 129 ##[ #H; ncases (IH ys); #E; #_; nrewrite > (E H); //] #; ndestruct;
 130 nqed.
 131
 132 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
 133 unification hint 0 ≔ T; Y ≟ T, X ≟  (wAlpha T) ⊢ carr X ≡ word Y.
 134 unification hint 0 ≔ T; Y ≟ T, X ≟  (wAlpha T) ⊢ carr X ≡ list Y.
 135 unification hint 0 ≔ T,x,y; Y ≟ T, X ≟ (wAlpha T) ⊢ eqb X x y ≡ weq Y x y.
 136
 137 nlet rec ex_split (A : Alpha) (p1,p2 : word A → bool) (w : word A) on w : bool ≝
 138   match w with
 139   [ nil ⇒ p1 [ ] && p2 [ ]
 140   | cons x xs ⇒ p1 [ ] && p2 (x::xs) || ex_split … (λw.p1 (x :: w)) p2 xs].
 141
 142 nlemma ex_splitP :
 143   ∀A,w,p1,p2. ex_split A p1 p2 w = true ↔
 144               ∃w1,w2. w = w1 @ w2 ∧ p1 w1 = true ∧ p2 w2 = true.
 145 #A w; nelim w;
 146 ##[ #p1 p2; @;
 147    ##[ #H; @[ ]; @[ ]; ncases (iff_l2r ?? (andP ??) H); (* bug coercions *)
 148        #E1 E2; nrewrite > E1; nrewrite > E2; /3/;
 149    ##| *; #w1; *;#w2; *; *; ncases w1; ncases w2; nnormalize; #abs H1 H2; #;
 150        ndestruct; nrewrite > H1 ; nrewrite > H2; //]
 151 ##| #x xs IH p1 p2; @;
 152    ##[ #H; ncases (iff_l2r ?? (orP ??) H);
 153       ##[ #H1; ncases (iff_l2r ?? (andP ??) H1); #p1T p2T;
 154           @[ ]; @(x::xs); nnormalize; /3/;
 155       ##| #E; ncases (iff_l2r ?? (IH ??) E); #l1; *; #l2; *; *; #defxs p1T p2T;
 156           @(x :: l1); @l2; ndestruct; /3/; ##]
 157     ##| *; #w1; *; #w2; *; *; ncases w1;
 158        ##[ nnormalize in ⊢ (% → ?); ncases w2; ##[ #; ndestruct] #y ys defw2 p1T p2T;
 159            nchange with ((p1 [ ] && p2 (x::xs) || ex_split ? (λw0.p1 (x::w0)) p2 xs) = true);
 160            napply (iff_r2l ?? (orP ??)); @1; napply (iff_r2l ?? (andP ??));
 161            ndestruct; /2/;
 162        ##| #y ys; nnormalize in ⊢ (% → ?); #E p1T p2T;
 163            nchange with ((p1 [ ] && p2 (x::xs) || ex_split ? (λw0.p1 (x::w0)) p2 xs) = true);
 164            napply (iff_r2l ?? (orP ??)); @2; napply (iff_r2l ?? (IH ??));
 165            @ys; @w2; ndestruct; /3/; ##]##]##]
 166 nqed.
 167
 168 nlet rec allb (A : Alpha) (p,fresh_p : word A → bool) (w : word A) on w : bool ≝
 169   match w with
 170   [ nil ⇒ p [ ]
 171   | cons x xs ⇒ p [x] && (xs == [ ] || allb … fresh_p fresh_p xs)
 172                 || allb … (λw.p (x :: w)) fresh_p xs].
 173
 174 nlemma allbP :
 175   ∀A,w,p.allb A p p w = true ↔
 176     ∃w1,w2.w = w1 @ w2 ∧ p w1 = true ∧ (w2 = [ ] ∨ allb ? p p w2 = true).
 177 #A w; nelim w;
 178 ##[ #p; @;
 179    ##[ #H; @[ ]; @[ ]; nnormalize in H; /4/ by conj, or_introl;
 180    ##| *; #w1; *; #w2; ncases w1;
 181        ##[ *; *; nnormalize in ⊢ (% → ?); #defw2 pnil; *; ##[ #; ndestruct] //;
 182        ##| #y ys; *; *; nnormalize in ⊢ (% → ?); #; ndestruct; ##]##]
 183 ##| #y ys IH p; @;
 184    ##[ #E; ncases (iff_l2r ?? (orP ??) E);
 185        ##[ #H; ncases (iff_l2r ?? (andP ??) H); #px allys;
 186            nlapply (iff_l2r ?? (orP ??) allys); *;
 187            ##[ #defys; @[y]; @[ ]; nrewrite > (iff_l2r ?? (eqb_true ? ys ?) defys);
 188                /4/ by conj, or_introl;
 189            ##| #IHa; ncases (iff_l2r ?? (IH ?) IHa); #z; *; #zs; *; *;
 190                #defys pz; *;
 191                ##[ #; ndestruct; @[y]; @z;
 192                    nrewrite > (append_nil ? z) in IHa; /4/ by or_intror, conj;
 193                ##| #allzs; @[y]; @(z@zs); nrewrite > defys; /3/ by or_intror, conj;##]##]
 194        ##| #allbp;
 195                ;
 196
 197
 198
 199 nlet rec in_lb (A : Alpha) (e : re A) on e : word A → bool ≝
 200   match e with
 201   [ e ⇒ is_epsilon …
 202   | z ⇒ is_empty …
 203   | s x ⇒ is_char … x
 204   | o e1 e2 ⇒ λw.in_lb … e1 w || in_lb … e2 w
 205   | c e1 e2 ⇒ ex_split … (in_lb A e1) (in_lb A e2)
 206   | k e ⇒ allb … (in_lb A e) (in_lb A e)].
 207
 208
 209 nlemma equiv_l_lb : ∀A,e,w. w ∈ e ↔ in_lb A e w = true.
 210 #A e; nelim e; nnormalize;
 211 ##[ #w; @; ##[##2: #; ndestruct] #H; ninversion H; #; ndestruct;
 212 ##| #w; @; ##[##2: #H; nrewrite > (l2r ??? H); //; ##]
 213     #H; ninversion H; #; ndestruct; //;
 214 ##| #x w; @; ##[ #H; ninversion H; #; ndestruct; nrewrite > (r2l ????); //; ##]
 215     #H; nrewrite > (l2r ??? H); @2;
 216 ##| #e1 e2 IH1 IH2 w; @; #E;
 217     ##[ ninversion E; ##[##1,2,4,5,6,7: #; ndestruct]
 218         #w1 w2 e1 e2 w1r1 w2r2 H1 H2 defw defr1r2; ndestruct;
 219         nlapply (IH1 w1); *; #IH1; #_; nlapply (IH1 w1r1);
 220         nlapply (IH2 w2); *; #IH2; #_; nlapply (IH2 w2r2);
 221         nelim w1;nnormalize; ncases w2; //; nnormalize;
 222
 223     ##[ nelim w; ##[ nnormalize; //] #x xs IH E; nnormalize;
 224     nlapply (IH1 [x]); nlapply (IH2 xs);
 225     ncases (in_lb A e1 [x]); ncases (in_lb A e2 xs); nnormalize; *; #E1 E2; *; #E3 E4; /2/;
 226     ##[ ncases xs in IH E3 E4; nnormalize; //; #xx xs H; #_;
 227
 228      *; nnormalize;
 229
 230
 231 nlemma in_l_inv_e:
 232  ∀S.∀w:word S. w ∈ ∅ → w = [].
 233  #S; #w; #H; ninversion H; #; ndestruct;
 234 nqed.
 235
 236 nlemma in_l_inv_s: ∀S.∀w:word S.∀x. w ∈ `x → w = [x].
 237 #S w x H; ninversion H; #; ndestruct; //.
 238 nqed.
 239
 240 nlemma in_l_inv_c:
 241  ∀S.∀w:word S.∀E1,E2. w ∈ E1 · E2 → ∃w1.∃w2. w = w1@w2 ∧ w1 ∈ E1 ∧ w2 ∈ E2.
 242 #S w e1 e2 H; ninversion  H; ##[##1,2,4,5,6,7: #; ndestruct; ##]
 243 #w1 w2 r1 r2 w1r1 w2r2; #_; #_; #defw defe; @w1; @w2; ndestruct; /3/.
 244 nqed.
 245
 246 ninductive pitem (S: Alpha) : Type[0] ≝
 247    pz: pitem S
 248  | pe: pitem S
 249  | ps: S → pitem S
 250  | pp: S → pitem S
 251  | pc: pitem S → pitem S → pitem S
 252  | po: pitem S → pitem S → pitem S
 253  | pk: pitem S → pitem S.
 254
 255 ndefinition pre ≝ λS.pitem S × bool.
 256
 257 interpretation "pstar" 'pk a = (pk ? a).
 258 interpretation "por" 'plus a b = (po ? a b).
 259 interpretation "pcat" 'pc a b = (pc ? a b).
 260 notation < ".a" non associative with precedence 90 for @{ 'pp $a}.
 261 notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}.
 262 interpretation "ppatom" 'pp a = (pp ? a).
 263 (* to get rid of \middot *)
 264 ncoercion pc : ∀S.∀p:pitem S. pitem S → pitem S  ≝ pc on _p : pitem ? to ∀_:?.?.
 265 interpretation "patom" 'ps a = (ps ? a).
 266 interpretation "pepsilon" 'epsilon = (pe ?).
 267 interpretation "pempty" 'empty = (pz ?).
 268
 269 notation > ".|term 19 e|" non associative with precedence 90 for @{forget ? $e}.
 270 nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝
 271  match l with
 272   [ pz ⇒ ∅
 273   | pe ⇒ ϵ
 274   | ps x ⇒ `x
 275   | pp x ⇒ `x
 276   | pc E1 E2 ⇒ .|E1| .|E2|
 277   | po E1 E2 ⇒ .|E1| + .|E2|
 278   | pk E ⇒ .|E|^* ].
 279 notation < ".|term 19 e|" non associative with precedence 90 for @{'forget $e}.
 280 interpretation "forget" 'forget a = (forget ? a).
 281
 282 notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.
 283 interpretation "fst" 'fst x = (fst ? ? x).
 284 notation > "\snd term 90 x" non associative with precedence 90 for @{'snd $x}.
 285 interpretation "snd" 'snd x = (snd ? ? x).
 286
 287 notation > "w .∈ E" non associative with precedence 40 for @{in_pl ? $w $E}.
 288 ninductive in_pl (S: Alpha): word S → pitem S → Prop ≝
 289  | in_pp:  ∀x:S.[x] .∈ `.x
 290  | in_pc1: ∀w1,w2:word S.∀e1,e2:pitem S.
 291              w1 .∈ e1 → w2 ∈ .|e2| → (w1@w2) .∈ e1 · e2
 292  | in_pc2: ∀w,e1,e2. w .∈ e2 → w .∈ e1 · e2
 293  | in_po1: ∀w,e1,e2. w .∈ e1 → w .∈ e1 + e2
 294  | in_po2: ∀w,e1,e2. w .∈ e2 → w .∈ e1 + e2
 295  | in_pki: ∀w1,w2,e. w1 .∈ e → w2 ∈ .|e|^* → (w1@w2) .∈ e^*.
 296
 297 interpretation "in_pl" 'in_pl w l = (in_pl ? w l).
 298
 299 ndefinition in_prl ≝ λS : Alpha.λw:word S.λp:pre S.
 300   (w = [ ] ∧ \snd p = true) ∨ w .∈ (\fst p).
 301
 302 notation > "w .∈ E" non associative with precedence 40 for @{'in_pl $w $E}.
 303 notation < "w\shy .∈\shy E" non associative with precedence 40 for @{'in_pl $w $E}.
 304 interpretation "in_prl" 'in_pl w l = (in_prl ? w l).
 305
 306
 307
 308 nlemma append_eq_nil :
 309   ∀S.∀w1,w2:word S. [ ] = w1 @ w2 → w1 = [ ].
 310 #S w1; nelim w1; //. #x tl IH w2; nnormalize; #abs; ndestruct;
 311 nqed.
 312
 313 nlemma append_eq_nil_r :
 314   ∀S.∀w1,w2:word S. [ ] = w1 @ w2 → w2 = [ ].
 315 #S w1; nelim w1; ##[ #w2 H; nrewrite > H; // ]
 316 #x tl IH w2; nnormalize; #abs; ndestruct;
 317 nqed.
 318
 319 nlemma lemma16 :
 320   ∀S.∀e:pre S. [ ] .∈ e ↔ \snd e = true.
 321 #S p; ncases p; #e b; @; ##[##2: #H; nrewrite > H; @; @; //. ##]
 322 ncases b; //; *; ##[*; //] nelim e;
 323 ##[##1,2: #abs; ninversion abs; #; ndestruct;
 324 ##|##3,4: #x abs; ninversion abs; #; ndestruct;
 325 ##|#p1 p2 H1 H2 H; ninversion H; ##[##1,3,4,5,6: #; ndestruct; /2/. ##]
 326    #w1 w2 r1 r2 w1r1 w2fr2 H3 H4 Ep1p2; ndestruct;
 327    nrewrite > (append_eq_nil … H4) in w1r1; /2/ by {};
 328 ##|#r1 r2 H1 H2 H; ninversion H; #; ndestruct; /2/ by {};
 329 ##|#r H1 H2; ninversion H2; ##[##1,2,3,4,5: #; ndestruct; ##]
 330    #w1 w2 r1 w1r1 w1er1 H11 H21 H31;
 331    nrewrite > (append_eq_nil … H21) in w1r1 H1;
 332    nrewrite > (?: r = r1); /2/ by {};
 333    ndestruct; //. ##]
 334 nqed.
 335
 336 ndefinition lo ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a || \snd b〉.
 337 notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
 338 interpretation "oplus" 'oplus a b = (lo ? a b).
 339
 340 ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S.
 341    match a with [ mk_pair e1 b1 ⇒
 342    match b with [ mk_pair e2 b2 ⇒
 343    match b1 with
 344    [ false ⇒ 〈e1 · e2, b2〉
 345    | true ⇒ match bcast ? e2 with [ mk_pair e2' b2' ⇒ 〈e1 · e2', b2 || b2'〉 ]]]].
 346
 347 notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}.
 348 interpretation "lc" 'lc op a b = (lc ? op a b).
 349 notation > "a ⊙ b" left associative with precedence 60 for @{'lc eclose $a $b}.
 350
 351 ndefinition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa:pre S.
 352    match a with [ mk_pair e1 b1 ⇒
 353    match b1 with
 354    [ false ⇒ 〈e1^*, false〉
 355    | true ⇒ match bcast ? e1 with [ mk_pair e1' b1' ⇒ 〈e1'^*, true〉 ]]].
 356
 357 notation < "a \sup ⊛" non associative with precedence 90 for @{'lk ? $a}.
 358 interpretation "lk" 'lk op a = (lk ? op a).
 359 notation > "a^⊛" non associative with precedence 90 for @{'lk eclose $a}.
 360
 361 notation > "•" non associative with precedence 60 for @{eclose ?}.
 362 nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝
 363  match E with
 364   [ pz ⇒ 〈 ∅, false 〉
 365   | pe ⇒ 〈 ϵ,  true 〉
 366   | ps x ⇒ 〈 `.x, false 〉
 367   | pp x ⇒ 〈 `.x, false 〉
 368   | po E1 E2 ⇒ •E1 ⊕ •E2
 369   | pc E1 E2 ⇒ •E1 ⊙ 〈 E2, false 〉
 370   | pk E ⇒ 〈E,true〉^⊛].
 371 notation < "• x" non associative with precedence 60 for @{'eclose $x}.
 372 interpretation "eclose" 'eclose x = (eclose ? x).
 373 notation > "• x" non associative with precedence 60 for @{'eclose $x}.
 374
 375 ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉.
 376 interpretation "reclose" 'eclose x = (reclose ? x).
 377
 378 nlemma lemma19_2 :
 379  ∀S:Alpha.∀e1,e2:pre S.∀w. w .∈ e1 ⊕ e2 → w .∈ e1 ∨ w .∈ e2.
 380 #S e1 e2 w H; nnormalize in H; ncases H;
 381 ##[ *; #defw; ncases e1; #p b; ncases b; nnormalize;
 382     ##[ #_; @1; @1; /2/ by conj;
 383     ##| #H1; @2; @1; /2/ by conj; ##]
 384 ##| #H1; ninversion H1; #; ndestruct; /4/ by or_introl, or_intror; ##]
 385 nqed.
 386
 387 notation > "\move term 90 x term 90 E"
 388 non associative with precedence 60 for @{move ? $x $E}.
 389 nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝
 390  match E with
 391   [ pz ⇒ 〈 ∅, false 〉
 392   | pe ⇒ 〈 ϵ, false 〉
 393   | ps y ⇒ 〈 `y, false 〉
 394   | pp y ⇒ 〈 `y, x == y 〉
 395   | po e1 e2 ⇒ \move x e1 ⊕ \move x e2
 396   | pc e1 e2 ⇒ \move x e1 ⊙ \move x e2
 397   | pk e ⇒ (\move x e)^⊛ ].
 398 notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}.
 399 notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}.
 400 interpretation "move" 'move x E = (move ? x E).
 401
 402 ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e).
 403 interpretation "rmove" 'move x E = (rmove ? x E).
 404
 405 nlemma XXz :  ∀S:Alpha.∀w:word S. w .∈ ∅ → False.
 406 #S w abs; ninversion abs; #; ndestruct;
 407 nqed.
 408
 409
 410 nlemma XXe :  ∀S:Alpha.∀w:word S. w .∈ ϵ → False.
 411 #S w abs; ninversion abs; #; ndestruct;
 412 nqed.
 413
 414 nlemma XXze :  ∀S:Alpha.∀w:word S. w .∈ (∅ · ϵ)  → False.
 415 #S w abs; ninversion abs; #; ndestruct; /2/ by XXz,XXe;
 416 nqed.
 417
 418
 419 naxiom in_move_cat:
 420  ∀S.∀w:word S.∀x.∀E1,E2:pitem S. w .∈ \move x (E1 · E2) →
 421    (∃w1.∃w2. w = w1@w2 ∧ w1 .∈ \move x E1 ∧ w2 ∈ .|E2|) ∨ w .∈ \move x E2.
 422 #S w x e1 e2 H; nchange in H with (w .∈ \move x e1 ⊙ \move x e2);
 423 ncases e1 in H; ncases e2;
 424 ##[##1: *; ##[*; nnormalize; #; ndestruct]
 425    #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
 426    nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze;
 427 ##|##2: *; ##[*; nnormalize; #; ndestruct]
 428    #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
 429    nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze;
 430 ##| #r; *; ##[ *; nnormalize; #; ndestruct]
 431    #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
 432    ##[##2: nnormalize; #; ndestruct; @2; @2; //.##]
 433    nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz;
 434 ##| #y; *; ##[ *; nnormalize; #defw defx; ndestruct; @2; @1; /2/ by conj;##]
 435    #H; ninversion H; nnormalize; #; ndestruct;
 436    ##[ncases (?:False); /2/ by XXz] /3/ by or_intror;
 437 ##| #r1 r2; *; ##[ *; #defw]
 438     ...
 439 nqed.
 440
 441 ntheorem move_ok:
 442  ∀S:Alpha.∀E:pre S.∀a,w.w .∈ \move a E ↔ (a :: w) .∈ E.
 443 #S E; ncases E; #r b; nelim r;
 444 ##[##1,2: #a w; @;
 445    ##[##1,3: nnormalize; *; ##[##1,3: *; #; ndestruct; ##| #abs; ncases (XXz … abs); ##]
 446       #H; ninversion H; #; ndestruct;
 447    ##|##*:nnormalize; *; ##[##1,3: *; #; ndestruct; ##| #H1; ncases (XXz … H1); ##]
 448        #H; ninversion H; #; ndestruct;##]
 449 ##|#a c w; @; nnormalize; ##[*; ##[*; #; ndestruct; ##] #abs; ninversion abs; #; ndestruct;##]
 450    *; ##[##2: #abs; ninversion abs; #; ndestruct; ##] *; #; ndestruct;
 451 ##|#a c w; @; nnormalize;
 452    ##[ *; ##[ *; #defw; nrewrite > defw; #ca; @2;  nrewrite > (eqb_t … ca); @; ##]
 453        #H; ninversion H; #; ndestruct;
 454    ##| *; ##[ *; #; ndestruct; ##] #H; ninversion H; ##[##2,3,4,5,6: #; ndestruct]
 455               #d defw defa; ndestruct; @1; @; //; nrewrite > (eqb_true S d d); //. ##]
 456 ##|#r1 r2 H1 H2 a w; @;
 457    ##[ #H; ncases (in_move_cat … H);
 458       ##[ *; #w1; *; #w2; *; *; #defw w1m w2m;
 459           ncases (H1 a w1); #H1w1; #_; nlapply (H1w1 w1m); #good;
 460           nrewrite > defw; @2; @2 (a::w1); //; ncases good; ##[ *; #; ndestruct] //.
 461       ##|
 462       ...
 463 ##|
 464 ##|
 465 ##]
 466 nqed.
 467
 468
 469 notation > "x ↦* E" non associative with precedence 60 for @{move_star ? $x $E}.
 470 nlet rec move_star (S : decidable) w E on w : bool × (pre S) ≝
 471  match w with
 472   [ nil ⇒ E
 473   | cons x w' ⇒ w' ↦* (x ↦ \snd E)].
 474
 475 ndefinition in_moves ≝ λS:decidable.λw.λE:bool × (pre S). \fst(w ↦* E).
 476
 477 ncoinductive equiv (S:decidable) : bool × (pre S) → bool × (pre S) → Prop ≝
 478  mk_equiv:
 479   ∀E1,E2: bool × (pre S).
 480    \fst E1  = \fst E2 →
 481     (∀x. equiv S (x ↦ \snd E1) (x ↦ \snd E2)) →
 482      equiv S E1 E2.
 483
 484 ndefinition NAT: decidable.
 485  @ nat eqb; /2/.
 486 nqed.
 487
 488 include "hints_declaration.ma".
 489
 490 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
 491 unification hint 0 ≔ ; X ≟ NAT ⊢ carr X ≡ nat.
 492
 493 ninductive unit: Type[0] ≝ I: unit.
 494
 495 nlet corec foo_nop (b: bool):
 496  equiv ?
 497   〈 b, pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0))) 〉
 498   〈 b, pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0) 〉 ≝ ?.
 499  @; //; #x; ncases x
 500   [ nnormalize in ⊢ (??%%); napply (foo_nop false)
 501   | #y; ncases y
 502      [ nnormalize in ⊢ (??%%); napply (foo_nop false)
 503      | #w; nnormalize in ⊢ (??%%); napply (foo_nop false) ]##]
 504 nqed.
 505
 506 (*
 507 nlet corec foo (a: unit):
 508  equiv NAT
 509   (eclose NAT (pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0)))))
 510   (eclose NAT (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0)))
 511 ≝ ?.
 512  @;
 513   ##[ nnormalize; //
 514   ##| #x; ncases x
 515        [ nnormalize in ⊢ (??%%);
 516          nnormalize in foo: (? → ??%%);
 517          @; //; #y; ncases y
 518            [ nnormalize in ⊢ (??%%); napply foo_nop
 519            | #y; ncases y
 520               [ nnormalize in ⊢ (??%%);
 521
 522             ##| #z; nnormalize in ⊢ (??%%); napply foo_nop ]##]
 523      ##| #y; nnormalize in ⊢ (??%%); napply foo_nop
 524   ##]
 525 nqed.
 526 *)
 527
 528 ndefinition test1 : pre ? ≝ ❨ `0 | `1 ❩^* `0.
 529 ndefinition test2 : pre ? ≝ ❨ (`0`1)^* `0 | (`0`1)^* `1 ❩.
 530 ndefinition test3 : pre ? ≝ (`0 (`0`1)^* `1)^*.
 531
 532
 533 nlemma foo: in_moves ? [0;0;1;0;1;1] (ɛ test3) = true.
 534  nnormalize in match test3;
 535  nnormalize;
 536 //;
 537 nqed.
 538
 539 (**********************************************************)
 540
 541 ninductive der (S: Type[0]) (a: S) : re S → re S → CProp[0] ≝
 542    der_z: der S a (z S) (z S)
 543  | der_e: der S a (e S) (z S)
 544  | der_s1: der S a (s S a) (e ?)
 545  | der_s2: ∀b. a ≠ b → der S a (s S b) (z S)
 546  | der_c1: ∀e1,e2,e1',e2'. in_l S [] e1 → der S a e1 e1' → der S a e2 e2' →
 547             der S a (c ? e1 e2) (o ? (c ? e1' e2) e2')
 548  | der_c2: ∀e1,e2,e1'. Not (in_l S [] e1) → der S a e1 e1' →
 549             der S a (c ? e1 e2) (c ? e1' e2)
 550  | der_o: ∀e1,e2,e1',e2'. der S a e1 e1' → der S a e2 e2' →
 551     der S a (o ? e1 e2) (o ? e1' e2').
 552
 553 nlemma eq_rect_CProp0_r:
 554  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
 555  #A; #a; #x; #p; ncases p; #P; #H; nassumption.
 556 nqed.
 557
 558 nlemma append1: ∀A.∀a:A.∀l. [a] @ l = a::l. //. nqed.
 559
 560 naxiom in_l1: ∀S,r1,r2,w. in_l S [ ] r1 → in_l S w r2 → in_l S w (c S r1 r2).
 561 (* #S; #r1; #r2; #w; nelim r1
 562   [ #K; ninversion K
 563   | #H1; #H2; napply (in_c ? []); //
 564   | (* tutti casi assurdi *) *)
 565
 566 ninductive in_l' (S: Type[0]) : word S → re S → CProp[0] ≝
 567    in_l_empty1: ∀E.in_l S [] E → in_l' S [] E
 568  | in_l_cons: ∀a,w,e,e'. in_l' S w e' → der S a e e' → in_l' S (a::w) e.
 569
 570 ncoinductive eq_re (S: Type[0]) : re S → re S → CProp[0] ≝
 571    mk_eq_re: ∀E1,E2.
 572     (in_l S [] E1 → in_l S [] E2) →
 573     (in_l S [] E2 → in_l S [] E1) →
 574     (∀a,E1',E2'. der S a E1 E1' → der S a E2 E2' → eq_re S E1' E2') →
 575       eq_re S E1 E2.
 576
 577 (* serve il lemma dopo? *)
 578 ntheorem eq_re_is_eq: ∀S.∀E1,E2. eq_re S E1 E2 → ∀w. in_l ? w E1 → in_l ? w E2.
 579  #S; #E1; #E2; #H1; #w; #H2; nelim H2 in E2 H1 ⊢ %
 580   [ #r; #K (* ok *)
 581   | #a; #w; #R1; #R2; #K1; #K2; #K3; #R3; #K4; @2 R2; //; ncases K4;
 582
 583 (* IL VICEVERSA NON VALE *)
 584 naxiom in_l_to_in_l: ∀S,w,E. in_l' S w E → in_l S w E.
 585 (* #S; #w; #E; #H; nelim H
 586   [ //
 587   | #a; #w'; #r; #r'; #H1; (* e si cade qua sotto! *)
 588   ]
 589 nqed. *)
 590
 591 ntheorem der1: ∀S,a,e,e',w. der S a e e' → in_l S w e' → in_l S (a::w) e.
 592  #S; #a; #E; #E'; #w; #H; nelim H
 593   [##1,2: #H1; ninversion H1
 594      [##1,8: #_; #K; (* non va ndestruct K; *) ncases (?:False); (* perche' due goal?*) /2/
 595      |##2,9: #X; #Y; #K; ncases (?:False); /2/
 596      |##3,10: #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
 597      |##4,11: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 598      |##5,12: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 599      |##6,13: #x; #y; #K; ncases (?:False); /2/
 600      |##7,14: #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/]
 601 ##| #H1; ninversion H1
 602      [ //
 603      | #X; #Y; #K; ncases (?:False); /2/
 604      | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
 605      | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 606      | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 607      | #x; #y; #K; ncases (?:False); /2/
 608      | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
 609 ##| #H1; #H2; #H3; ninversion H3
 610      [ #_; #K; ncases (?:False); /2/
 611      | #X; #Y; #K; ncases (?:False); /2/
 612      | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
 613      | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 614      | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 615      | #x; #y; #K; ncases (?:False); /2/
 616      | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
 617 ##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6;
 618