X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fre%2Fre.ma;h=300812ce89ccff39d7be66f2b507ad6097496684;hb=ef98db5ff416ef53004e57cc054e28abd1bf871e;hp=10f446bc5f9a7572b610a92c33fb463e876b16a1;hpb=85521efd364ec494e4cc024bbf87182a312e1b7b;p=helm.git

diff --git a/helm/software/matita/nlibrary/re/re.ma b/helm/software/matita/nlibrary/re/re.ma
index 10f446bc5..300812ce8 100644
--- a/helm/software/matita/nlibrary/re/re.ma
+++ b/helm/software/matita/nlibrary/re/re.ma
@@ -12,13 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "logic/connectives.ma".
+(*include "logic/connectives.ma".*)
 (*include "logic/equality.ma".*)
 include "datatypes/list.ma".
-include "datatypes/bool.ma".
 include "datatypes/pairs.ma".
 
-include "Plogic/equality.ma".
+(*include "Plogic/equality.ma".*)
 
 ndefinition word ≝ λS:Type[0].list S.
 
@@ -30,6 +29,8 @@ ninductive re (S: Type[0]) : Type[0] ≝
  | o: re S → re S → re S
  | k: re S → re S.
 
+(*
+alias symbol "not" (instance 1) = "Clogical not".
 nlemma foo1: ∀S. ¬ (z S = e S). #S; @; #H; ndestruct. nqed.
 nlemma foo2: ∀S,x. ¬ (z S = s S x). #S; #x; @; #H; ndestruct. nqed.
 nlemma foo3: ∀S,x1,x2. ¬ (z S = c S x1 x2). #S; #x1; #x2; @; #H; ndestruct. nqed.
@@ -39,8 +40,9 @@ nlemma foo6: ∀S,x. ¬ (e S = s S x). #S; #x; @; #H; ndestruct. nqed.
 nlemma foo7: ∀S,x1,x2. ¬ (e S = c S x1 x2). #S; #x1; #x2; @; #H; ndestruct. nqed.
 nlemma foo8: ∀S,x1,x2. ¬ (e S = o S x1 x2). #S; #x1; #x2; @; #H; ndestruct. nqed.
 nlemma foo9: ∀S,x. ¬ (e S = k S x). #S; #x; @; #H; ndestruct. nqed.
+*)
 
-ninductive in_l (S: Type[0]): word S → re S → CProp[0] ≝
+ninductive in_l (S: Type[0]): word S → re S → Prop ≝
    in_e: in_l S [] (e ?)
  | in_s: ∀x. in_l S [x] (s ? x)
  | in_c: ∀w1,w2,e1,e2. in_l ? w1 e1 → in_l ? w2 e2 → in_l S (w1@w2) (c ? e1 e2)
@@ -49,27 +51,50 @@ ninductive in_l (S: Type[0]): word S → re S → CProp[0] ≝
  | in_ke: ∀e. in_l S [] (k ? e)
  | in_ki: ∀w1,w2,e. in_l ? w1 e → in_l ? w2 (k ? e) → in_l S (w1@w2) (k ? e).
 
+naxiom in_l_inv_z:
+ ∀S,w. ¬ (in_l S w (z ?)).
+(* #S; #w; #H; ninversion H
+  [ #_; #b; ndestruct
+  | #a; #b; #c; ndestruct
+  | #a; #b; #c; #d; #e; #f; #g; #h; #i; #l; ndestruct
+  | #a; #b; #c; #d; #e; #f; #g; ndestruct
+  | #a; #b; #c; #d; #e; #f; #g; ndestruct
+  | #a; #b; #c; ndestruct
+  | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct ]
+nqed. *)
+
+nlemma in_l_inv_e:
+ ∀S,w. in_l S w (e ?) → w = [].
+ #S; #w; #H; ninversion H; #; ndestruct; //.
+nqed.
+
+naxiom in_l_inv_s: 
+ ∀S,w,x. in_l S w (s ? x) → w = [x].
+
+naxiom in_l_inv_c:
+ ∀S,w,E1,E2. in_l S w (c S E1 E2) → ∃w1.∃w2. w = w1@w2 ∧ in_l S w1 E1 ∧ in_l S w2 E2.
+
 ninductive pre (S: Type[0]) : Type[0] ≝
-   pp: pre S → pre S
- | pz: pre S
+   pz: pre S
  | pe: pre S
  | ps: S → pre S
+ | pp: S → pre S
  | pc: pre S → pre S → pre S
  | po: pre S → pre S → pre S
  | pk: pre S → pre S.
 
 nlet rec forget (S: Type[0]) (l : pre S) on l: re S ≝
  match l with
-  [ pp E ⇒ forget S E
-  | pz ⇒ z S
+  [ pz ⇒ z S
   | pe ⇒ e S
   | ps x ⇒ s S x
+  | pp x ⇒ s S x
   | pc E1 E2 ⇒ c S (forget ? E1) (forget ? E2)
   | po E1 E2 ⇒ o S (forget ? E1) (forget ? E2)
   | pk E ⇒ k S (forget ? E) ].
 
-ninductive in_pl (S: Type[0]): word S → pre S → CProp[0] ≝
-   in_pp: ∀w,E. in_l S w (forget ? E) → in_pl S w (pp S E) 
+ninductive in_pl (S: Type[0]): word S → pre S → Prop ≝
+   in_pp: ∀x. in_pl S [x] (pp S x) 
  | in_pc1: ∀w1,w2,e1,e2. in_pl ? w1 e1 → in_l ? w2 (forget ? e2) →
             in_pl S (w1@w2) (pc ? e1 e2)
  | in_pc2: ∀w,e1,e2. in_pl ? w e2 → in_pl S w (pc ? e1 e2)
@@ -78,24 +103,244 @@ ninductive in_pl (S: Type[0]): word S → pre S → CProp[0] ≝
  | in_pki: ∀w1,w2,e. in_pl ? w1 e → in_l ? w2 (k ? (forget ? e)) →
            in_pl S (w1@w2) (pk ? e).
 
-nlet rec eclose (S: Type[0]) (b: bool) (E: pre S) on E ≝
+nlet rec eclose (S: Type[0]) (E: pre S) on E ≝
  match E with
-  [ pp E' ⇒ eclose ? true E'
-  | pz ⇒ 〈 false, pz ? 〉
-  | pe ⇒ 〈 b, pe ? 〉
-  | ps x ⇒ 〈 false, ps ? x 〉
+  [ pz ⇒ 〈 false, pz ? 〉
+  | pe ⇒ 〈 true, pe ? 〉
+  | ps x ⇒ 〈 false, pp ? x 〉
+  | pp x ⇒ 〈 false, pp ? x 〉
   | pc E1 E2 ⇒
-     let E1' ≝ eclose ? b E1 in
+     let E1' ≝ eclose ? E1 in
      let E1'' ≝ snd … E1' in
-     let E2' ≝ eclose ? (fst … E1') E2 in
-      〈 fst … E2', pc ? E1'' (snd … E2') 〉
+      match fst … E1' with
+       [ true ⇒ 
+          let E2' ≝ eclose ? E2 in
+           〈 fst … E2', pc ? E1'' (snd … E2') 〉
+       | false ⇒ 〈 false, pc ? E1'' E2 〉 ]
   | po E1 E2 ⇒
-     let E1' ≝ eclose ? b E1 in
-     let E2' ≝ eclose ? b E2 in
+     let E1' ≝ eclose ? E1 in
+     let E2' ≝ eclose ? E2 in
+      〈 fst … E1' ∨ fst … E2', po ? (snd … E1') (snd … E2') 〉
+  | pk E ⇒ 〈 true, pk ? (snd … (eclose S E)) 〉 ].
+
+ntheorem forget_eclose:
+ ∀S,E. forget S (snd … (eclose … E)) = forget ? E.
+ #S; #E; nelim E; nnormalize; //;
+ #p; ncases (fst … (eclose S p)); nnormalize; //.
+nqed.
+
+ntheorem eclose_true:
+ ∀S,E. (* bug refiner se si scambia true con il termine *)
+  true = fst bool (pre S) (eclose S E) → in_l S [] (forget S E).
+ #S; #E; nelim E; nnormalize; //
+  [ #H; ncases (?: False); /2/
+  | #x H; #H; ncases (?: False); /2/
+  | #x; #H; ncases (?: False); /2/
+  | #w1; #w2; ncases (fst … (eclose S w1)); nnormalize; /3/;
+    #_; #_; #H; ncases (?:False); /2/
+  | #w1; #w2; ncases (fst … (eclose S w1)); nnormalize; /3/]
+nqed.
+
+(* to be moved *)
+nlemma eq_append_nil_to_eq_nil1:
+ ∀A.∀l1,l2:list A. l1 @ l2 = [] → l1 = [].
+ #A; #l1; nelim l1; nnormalize; /2/;
+ #x; #tl; #_; #l3; #K; ndestruct.
+nqed.
+
+(* to be moved *)
+nlemma eq_append_nil_to_eq_nil2:
+ ∀A.∀l1,l2:list A. l1 @ l2 = [] → l2 = [].
+ #A; #l1; nelim l1; nnormalize; /2/;
+ #x; #tl; #_; #l3; #K; ndestruct.
+nqed.
+
+ntheorem in_l_empty_c:
+ ∀S,E1,E2. in_l S [] (c … E1 E2) → in_l S [] E2.
+ #S; #E1; #E2; #H; ninversion H
+  [##1,2,4,5,6,7: #; ndestruct
+  | #w1; #w2; #E1'; #E2'; #H1; #H2; #H3; #H4; #H5; #H6;
+    nrewrite < H5; nlapply (eq_append_nil_to_eq_nil2 … w1 w2 ?); //;
+    ndestruct; // ]
+nqed.
+
+ntheorem eclose_true':
+ ∀S,E. (* bug refiner se si scambia true con il termine *)
+  in_l S [] (forget S E) → true = fst bool (pre S) (eclose S E).
+ #S; #E; nelim E; nnormalize; //
+  [ #H; ncases (?:False); /2/
+  |##2,3: #x; #H; ncases (?:False); nlapply (in_l_inv_s ??? H); #K; ndestruct
+  | #E1; #E2; ncases (fst … (eclose S E1)); nnormalize
+     [ #H1; #H2; #H3; ninversion H3; /3/;
+   ##| #H1; #H2; #H3; ninversion H3
+        [ ##1,2,4,5,6,7: #; ndestruct
+        | #w1; #w2; #E1'; #E2'; #H4; #H5; #K1; #K2; #K3; #K4; ndestruct;
+          napply H1; nrewrite < (eq_append_nil_to_eq_nil1 … w1 w2 ?); //]##]
+##| #E1; ncases (fst … (eclose S E1)); nnormalize; //;
+    #E2; #H1; #H2; #H3; ninversion H3
+     [ ##1,2,3,5,6,7: #; ndestruct; /2/
+     | #w; #E1'; #E2'; #H1'; #H2'; #H3'; #H4; ndestruct;
+       ncases (?: False); napply (absurd ?? (not_eq_true_false …));
+       /2/ ]##]
+nqed.     
+
+(*
+ntheorem eclose_superset:
+ ∀S,E.
+  ∀w. in_l S w (forget … E) ∨ in_pl ? w E → 
+       let E' ≝ eclose … E in
+       in_pl ? w (snd … E') ∨ fst … E' = true ∧ w = [].
+ #S; #E; #w; *
+  [ ngeneralize in match w; nelim E; nnormalize
+     [ #w'; #H; ncases (? : False); /2/
+   ##| #w'; #H; @2; @; //; napply in_l_inv_e; //; (* auto non va *)
+   ##|##3,4: #x; #w'; #H; @1; nrewrite > (in_l_inv_s … H); //;
+   ##| #E1; #E2; #H1; #H2; #w'; #H3;
+       ncases (in_l_inv_c … H3); #w1; *; #w2; *; *; #H4; #H5; #H6;
+       ncases (fst … (eclose S E1)) in H1 H2 ⊢ %; nnormalize
+        [ #H1; #H2; ncases (H1 … H5); ncases (H2 … H6)
+          [ #K1; #K2; nrewrite > H4; /3/;
+        ##| *; #_; #K1; #K2; nrewrite > H4; /3/;
+        ##| #K1; *; #_; #K2; nrewrite > H4; @1; nrewrite > K2;
+            /3/ ]
+   
+    @2; @; //; ninversion H; //;
+##| #H; nwhd; @1; (* manca intro per letin*)
+    (* LEMMA A PARTE? *) (* manca clear E' *)
+    nelim H; nnormalize; /2/
+     [ #w1; #w2; #p; ncases (fst … (eclose S p));
+       nnormalize; /2/
+     | #w; #p; ncases (fst … (eclose S p));
+       nnormalize; /2/ ]
+nqed.
+*)
+
+nrecord decidable : Type[1] ≝
+ { carr :> Type[0];
+   eqb: carr → carr → bool;
+   eqb_true: ∀x,y. eqb x y = true → x=y;
+   eqb_false: ∀x,y. eqb x y = false → x≠y
+ }.
+
+nlet rec move (S: decidable) (x:S) (E: pre S) on E ≝
+ match E with
+  [ pz ⇒ 〈 false, pz ? 〉
+  | pe ⇒ 〈 false, pe ? 〉
+  | ps y ⇒ 〈false, ps ? y 〉
+  | pp y ⇒ 〈 eqb … x y, ps ? y 〉
+  | pc E1 E2 ⇒
+     let E1' ≝ move ? x E1 in
+     let E2' ≝ move ? x E2 in
+     let E1'' ≝ snd … E1' in
+     let E2'' ≝ snd ?? E2' in
+      match fst … E1' with
+       [ true =>
+          let E2''' ≝ eclose S E2'' in
+           〈 fst … E2' ∨ fst … E2''', pc ? E1'' (snd … E2''') 〉
+       | false ⇒ 〈 fst … E2', pc ? E1'' E2'' 〉 ]
+  | po E1 E2 ⇒
+     let E1' ≝ move ? x E1 in
+     let E2' ≝ move ? x E2 in
       〈 fst … E1' ∨ fst … E2', po ? (snd … E1') (snd … E2') 〉
   | pk E ⇒
-     〈 true, pk ? (snd … (eclose S b E)) 〉 ].
-      
+     let E' ≝ move S x E in
+     let E'' ≝ snd bool (pre S) E' in
+      match fst … E' with
+       [ true ⇒ 〈 true, pk ? (snd … (eclose … E'')) 〉
+       | false ⇒ 〈 false, pk ? E'' 〉 ]].
+
+(*
+ntheorem move_ok:
+ ∀S:decidable.∀E,a,w.
+  in_pl S w (snd … (move S a E)) → in_pl S (a::w) E.
+ #S; #E; #a; #w;
+nqed.
+*)
+
+nlet rec move_star S w E on w ≝
+ match w with
+  [ nil ⇒ E
+  | cons x w' ⇒ move_star S w' (move S x (snd … E))].
+
+ndefinition in_moves ≝ λS,w,E. fst … (move_star S w E).
+
+ncoinductive equiv (S:decidable) : bool × (pre S) → bool × (pre S) → Prop ≝
+ mk_equiv:
+  ∀E1,E2: bool × (pre S).
+   fst ?? E1  = fst ?? E2 →
+    (∀x. equiv S (move S x (snd … E1)) (move S x (snd … E2))) →
+     equiv S E1 E2.
+
+ndefinition NAT: decidable.
+ @ nat eqb; /2/.
+nqed.
+
+ninductive unit: Type[0] ≝ I: unit.
+
+nlet corec foo_nop (b: bool):
+ equiv NAT
+  〈 b, pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0))) 〉
+  〈 b, pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0) 〉 ≝ ?.
+ @; //; #x; ncases x
+  [ nnormalize in ⊢ (??%%); napply (foo_nop false)
+  | #y; ncases y
+     [ nnormalize in ⊢ (??%%); napply (foo_nop false)
+     | #w; nnormalize in ⊢ (??%%); napply (foo_nop false) ]##]
+nqed.
+
+(*
+nlet corec foo (a: unit):
+ equiv NAT
+  (eclose NAT (pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0)))))
+  (eclose NAT (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0)))
+≝ ?.
+ @;
+  ##[ nnormalize; //
+  ##| #x; ncases x
+       [ nnormalize in ⊢ (??%%);
+         nnormalize in foo: (? → ??%%);
+         @; //; #y; ncases y
+           [ nnormalize in ⊢ (??%%); napply foo_nop
+           | #y; ncases y
+              [ nnormalize in ⊢ (??%%);
+                
+            ##| #z; nnormalize in ⊢ (??%%); napply foo_nop ]##]
+     ##| #y; nnormalize in ⊢ (??%%); napply foo_nop
+  ##]
+nqed.
+*)
+
+notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
+notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}.
+interpretation "star" 'pk a = (pk ? a).
+                      
+notation "❨a|b❩" non associative with precedence 90 for @{ 'po $a $b}.
+interpretation "or" 'po a b = (po ? a b).
+           
+notation < "a b" non associative with precedence 60 for @{ 'pc $a $b}.
+notation > "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
+interpretation "cat" 'pc a b = (pc ? a b).
+
+notation < "a" non associative with precedence 90 for @{ 'pp $a}.
+notation > "` term 90 a" non associative with precedence 90 for @{ 'pp $a}.
+interpretation "atom" 'pp a = (pp ? a).
+
+(* to get rid of \middot *)
+ncoercion rex_concat : ∀S:Type[0].∀p:pre S. pre S → pre S  ≝ pc
+on _p : pre ? to ∀_:?.?.
+(* we could also get rid of ` with a coercion from nat → pre nat *) 
+
+ndefinition test1 ≝ ❨ `0 | `1 ❩^* `0.
+ndefinition test2 ≝ ❨ (`0`1)^* `0 | (`0`1)^* `1 ❩.
+ndefinition test3 ≝ (`0 (`0`1)^* `1)^*.
+
+nlemma foo: in_moves NAT
+  [0;0;1;0;1;1] (eclose ? test3) = true.
+ nnormalize in match test3;
+ nnormalize;
+//;
+nqed.
+
 (**********************************************************)
 
 ninductive der (S: Type[0]) (a: S) : re S → re S → CProp[0] ≝