(* *)
(**************************************************************************)
-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.
| 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.
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)
| 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
+ [ #a; #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.
+
+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)
| 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; 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
+ [ #_; #H2; ndestruct
+ | #x; #K; ndestruct
+ | #w1; #w2; #E1'; #E2'; #H1; #H2; #H3; #H4; #H5; #H6;
+ nrewrite < H5; nlapply (eq_append_nil_to_eq_nil2 … w1 w2 ?); //;
+ ndestruct; //
+ | #w; #E1'; #E2'; #H1; #H2; #H3; #H4; ndestruct
+ | #w; #E1'; #E2'; #H1; #H2; #H3; #H4; ndestruct
+ | #E; #_; #K; ndestruct
+ | #w1; #w2; #w3; #H1; #H2; #H3; #H4; #H5; #H6; 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
+ [ #_; #K; ndestruct
+ | #x; #K; ndestruct
+ | #w1; #w2; #E1'; #E2'; #H4; #H5; #K1; #K2; #K3; #K4; ndestruct;
+ napply H1; nrewrite < (eq_append_nil_to_eq_nil1 … w1 w2 ?); //
+ | #w1; #E1'; #E2'; #H4; #H5; #H6; #H7; ndestruct
+ | #w1; #E1'; #E2'; #H4; #H5; #H6; #H7; ndestruct
+ | #E'; #_; #K; ndestruct
+ | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct ]##]
+##| #E1; ncases (fst … (eclose S E1)); nnormalize; //;
+ #E2; #H1; #H2; #H3; ninversion H3
+ [ #_; #K; ndestruct
+ | #w; #_; #K; ndestruct
+ | #a; #b; #c; #d; #e; #f; #g; #h; #i; #l; ndestruct
+ | #w; #E1'; #E2'; #H1'; #H2'; #H3'; #H4; ndestruct;
+ ncases (?: False); napply (absurd ?? (not_eq_true_false …));
+ /2/
+ | #w; #E1'; #E2'; #H1'; #H2'; #H3'; #H4; ndestruct; /2/
+ | #a; #b; #c; ndestruct
+ | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct]##]
+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).
+
+ndefinition NAT: decidable.
+ @ nat eqb; /2/.
+nqed.
+
+ndefinition test1 ≝
+ pc ? (pk ? (po ? (ps ? 0) (ps ? 1))) (ps ? 0).
+
+ndefinition test2 ≝
+ po ?
+ (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0))
+ (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 1)).
+
+ndefinition test3 ≝
+ pk ? (pc ? (pc ? (ps ? 0) (pk ? (pc ? (ps ? 0) (ps ? 1)))) (ps ? 1)).
+
+nlemma foo: in_moves NAT
+ [0;0;1;0;1;1] (eclose ? test3) = true.
+ nnormalize;
+
(**********************************************************)
ninductive der (S: Type[0]) (a: S) : re S → re S → CProp[0] ≝
projects / helm.git / commitdiff