(*include "logic/equality.ma".*)
include "datatypes/list.ma".
include "datatypes/pairs.ma".
+include "arithmetics/nat.ma".
(*include "Plogic/equality.ma".*)
-ndefinition word ≝ λS:Type[0].list S.
+nrecord Alpha : 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)
+ }.
+
+notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
+interpretation "eqb" 'eqb a b = (eqb ? a b).
+
+ndefinition word ≝ λS:Alpha.list S.
-ninductive re (S: Type[0]) : Type[0] ≝
+ninductive re (S: Alpha) : Type[0] ≝
z: re S
| e: re S
| s: S → re S
| c: re S → re S → re S
| o: re S → re S → re S
| k: re S → re S.
+
+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 = (k ? a).
+interpretation "or" 'plus a b = (o ? a b).
+
+notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
+interpretation "cat" 'pc a b = (c ? a b).
+
+(* to get rid of \middot *)
+ncoercion c : ∀S:Alpha.∀p:re S. re S → re S ≝ c on _p : re ? to ∀_:?.?.
+
+notation < "a" non associative with precedence 90 for @{ 'ps $a}.
+notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
+interpretation "atom" 'ps a = (s ? a).
+
+notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
+interpretation "epsilon" 'epsilon = (e ?).
+
+notation "∅" non associative with precedence 90 for @{ 'empty }.
+interpretation "empty" 'empty = (z ?).
+
+notation > "w ∈ E" non associative with precedence 45 for @{in_l ? $w $E}.
+ninductive in_l (S : Alpha) : word S → re S → Prop ≝
+ | in_e: [ ] ∈ ϵ
+ | in_s: ∀x:S. [x] ∈ `x
+ | in_c: ∀w1,w2,e1,e2. w1 ∈ e1 → w2 ∈ e2 → w1@w2 ∈ e1 · e2
+ | in_o1: ∀w,e1,e2. w ∈ e1 → w ∈ e1 + e2
+ | in_o2: ∀w,e1,e2. w ∈ e2 → w ∈ e1 + e2
+ | in_ke: ∀e. [ ] ∈ e^*
+ | in_ki: ∀w1,w2,e. w1 ∈ e → w2 ∈ e^* → w1@w2 ∈ e^*.
+interpretation "in_l" 'mem w l = (in_l ? w l).
(*
-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 foo4: ∀S,x1,x2. ¬ (z S = o S x1 x2). #S; #x1; #x2; @; #H; ndestruct. nqed.
-nlemma foo5: ∀S,x. ¬ (z S = k S x). #S; #x; @; #H; ndestruct. nqed.
-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.
-*)
+notation "a || b" left associative with precedence 30 for @{'orb $a $b}.
+interpretation "orb" 'orb a b = (orb a b).
-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_o1: ∀w,e1,e2. in_l ? w e1 → in_l S w (o ? e1 e2)
- | in_o2: ∀w,e1,e2. in_l ? w e2 → in_l S w (o ? 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. *)
+notation "a && b" left associative with precedence 40 for @{'andb $a $b}.
+interpretation "andb" 'andb a b = (andb a b).
+
+nlet rec weq (S : Alpha) (l1, l2 : word S) on l1 : bool ≝
+match l1 with
+[ nil ⇒ match l2 with [ nil ⇒ true | cons _ _ ⇒ false ]
+| cons x xs ⇒ match l2 with [ nil ⇒ false | cons y ys ⇒ (x == y) && weq S xs ys]].
+
+ndefinition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
+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 }.
+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 }.
+interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
+
+*)
nlemma in_l_inv_e:
- ∀S,w. in_l S w (e ?) → w = [].
- #S; #w; #H; ninversion H; #; ndestruct; //.
+ ∀S.∀w:word S. w ∈ ∅ → w = [].
+ #S; #w; #H; ninversion H; #; ndestruct;
nqed.
-naxiom in_l_inv_s:
- ∀S,w,x. in_l S w (s ? x) → w = [x].
+nlemma in_l_inv_s: ∀S.∀w:word S.∀x. w ∈ `x → w = [x].
+#S w x H; ninversion H; #; ndestruct; //.
+nqed.
-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.
+nlemma in_l_inv_c:
+ ∀S.∀w:word S.∀E1,E2. w ∈ E1 · E2 → ∃w1.∃w2. w = w1@w2 ∧ w1 ∈ E1 ∧ w2 ∈ E2.
+#S w e1 e2 H; ninversion H; ##[##1,2,4,5,6,7: #; ndestruct; ##]
+#w1 w2 r1 r2 w1r1 w2r2; #_; #_; #defw defe; @w1; @w2; ndestruct; /3/.
+nqed.
-ninductive pre (S: Type[0]) : Type[0] ≝
- 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.
+ninductive pitem (S: Alpha) : Type[0] ≝
+ pz: pitem S
+ | pe: pitem S
+ | ps: S → pitem S
+ | pp: S → pitem S
+ | pc: pitem S → pitem S → pitem S
+ | po: pitem S → pitem S → pitem S
+ | pk: pitem S → pitem S.
+
+ndefinition pre ≝ λS.pitem S × bool.
+
+interpretation "pstar" 'pk a = (pk ? a).
+interpretation "por" 'plus a b = (po ? a b).
+interpretation "pcat" '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 "ppatom" 'pp a = (pp ? a).
+(* to get rid of \middot *)
+ncoercion pc : ∀S.∀p:pitem S. pitem S → pitem S ≝ pc on _p : pitem ? to ∀_:?.?.
+interpretation "patom" 'ps a = (ps ? a).
+interpretation "pepsilon" 'epsilon = (pe ?).
+interpretation "pempty" 'empty = (pz ?).
-nlet rec forget (S: Type[0]) (l : pre S) on l: re S ≝
+notation > ".|term 19 e|" non associative with precedence 90 for @{forget ? $e}.
+nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝
match l with
- [ 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 → 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_po1: ∀w,e1,e2. in_pl ? w e1 → in_pl S w (po ? e1 e2)
- | in_po2: ∀w,e1,e2. in_pl ? w e2 → in_pl S w (po ? 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]) (E: pre S) on E ≝
- match E with
- [ pz ⇒ 〈 false, pz ? 〉
- | pe ⇒ 〈 true, pe ? 〉
- | ps x ⇒ 〈 false, pp ? x 〉
- | pp x ⇒ 〈 false, pp ? x 〉
- | pc E1 E2 ⇒
- let E1' ≝ eclose ? E1 in
- let E1'' ≝ snd … E1' in
- 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 ? 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; //.
+ [ pz ⇒ ∅
+ | pe ⇒ ϵ
+ | ps x ⇒ `x
+ | pp x ⇒ `x
+ | pc E1 E2 ⇒ .|E1| .|E2|
+ | po E1 E2 ⇒ .|E1| + .|E2|
+ | pk E ⇒ .|E|^* ].
+notation < ".|term 19 e|" non associative with precedence 90 for @{'forget $e}.
+interpretation "forget" 'forget a = (forget ? a).
+
+notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.
+interpretation "fst" 'fst x = (fst ? ? x).
+notation > "\snd term 90 x" non associative with precedence 90 for @{'snd $x}.
+interpretation "snd" 'snd x = (snd ? ? x).
+
+notation > "w .∈ E" non associative with precedence 40 for @{in_pl ? $w $E}.
+ninductive in_pl (S: Alpha): word S → pitem S → Prop ≝
+ | in_pp: ∀x:S.[x] .∈ `.x
+ | in_pc1: ∀w1,w2:word S.∀e1,e2:pitem S.
+ w1 .∈ e1 → w2 ∈ .|e2| → (w1@w2) .∈ e1 · e2
+ | in_pc2: ∀w,e1,e2. w .∈ e2 → w .∈ e1 · e2
+ | in_po1: ∀w,e1,e2. w .∈ e1 → w .∈ e1 + e2
+ | in_po2: ∀w,e1,e2. w .∈ e2 → w .∈ e1 + e2
+ | in_pki: ∀w1,w2,e. w1 .∈ e → w2 ∈ .|e|^* → (w1@w2) .∈ e^*.
+
+interpretation "in_pl" 'in_pl w l = (in_pl ? w l).
+
+ndefinition in_prl ≝ λS : Alpha.λw:word S.λp:pre S.
+ (w = [ ] ∧ \snd p = true) ∨ w .∈ (\fst p).
+
+notation > "w .∈ E" non associative with precedence 40 for @{'in_pl $w $E}.
+notation < "w\shy .∈\shy E" non associative with precedence 40 for @{'in_pl $w $E}.
+interpretation "in_prl" 'in_pl w l = (in_prl ? w l).
+
+interpretation "iff" 'iff a b = (iff a b).
+
+nlemma append_eq_nil :
+ ∀S.∀w1,w2:word S. [ ] = w1 @ w2 → w1 = [ ].
+#S w1; nelim w1; //. #x tl IH w2; nnormalize; #abs; ndestruct;
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/]
+nlemma append_eq_nil_r :
+ ∀S.∀w1,w2:word S. [ ] = w1 @ w2 → w2 = [ ].
+#S w1; nelim w1; ##[ #w2 H; nrewrite > H; // ]
+#x tl IH w2; nnormalize; #abs; ndestruct;
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.
+nlemma lemma16 :
+ ∀S.∀e:pre S. [ ] .∈ e ↔ \snd e = true.
+#S p; ncases p; #e b; @; ##[##2: #H; nrewrite > H; @; @; //. ##]
+ncases b; //; *; ##[*; //] nelim e;
+##[##1,2: #abs; ninversion abs; #; ndestruct;
+##|##3,4: #x abs; ninversion abs; #; ndestruct;
+##|#p1 p2 H1 H2 H; ninversion H; ##[##1,3,4,5,6: #; ndestruct; /2/. ##]
+ #w1 w2 r1 r2 w1r1 w2fr2 H3 H4 Ep1p2; ndestruct;
+ nrewrite > (append_eq_nil … H4) in w1r1; /2/ by {};
+##|#r1 r2 H1 H2 H; ninversion H; #; ndestruct; /2/ by {};
+##|#r H1 H2; ninversion H2; ##[##1,2,3,4,5: #; ndestruct; ##]
+ #w1 w2 r1 w1r1 w1er1 H11 H21 H31;
+ nrewrite > (append_eq_nil … H21) in w1r1 H1;
+ nrewrite > (?: r = r1); /2/ by {};
+ 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.
+ndefinition lo ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a || \snd b〉.
+notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
+interpretation "oplus" 'oplus a b = (lo ? a b).
+
+ndefinition lc ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa,b:pre S.
+ match a with [ mk_pair e1 b1 ⇒
+ match b with [ mk_pair e2 b2 ⇒
+ match b1 with
+ [ false ⇒ 〈e1 · e2, b2〉
+ | true ⇒ match bcast ? e2 with [ mk_pair e2' b2' ⇒ 〈e1 · e2', b2 || b2'〉 ]]]].
+
+notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}.
+interpretation "lc" 'lc op a b = (lc ? op a b).
+notation > "a ⊙ b" left associative with precedence 60 for @{'lc eclose $a $b}.
+
+ndefinition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λa:pre S.
+ match a with [ mk_pair e1 b1 ⇒
+ match b1 with
+ [ false ⇒ 〈e1^*, false〉
+ | true ⇒ match bcast ? e1 with [ mk_pair e1' b1' ⇒ 〈e1'^*, true〉 ]]].
+
+notation < "a \sup ⊛" non associative with precedence 90 for @{'lk ? $a}.
+interpretation "lk" 'lk op a = (lk ? op a).
+notation > "a^⊛" non associative with precedence 90 for @{'lk eclose $a}.
+
+notation > "•" non associative with precedence 60 for @{eclose ?}.
+nlet rec eclose (S: Alpha) (E: pitem S) on E : pre S ≝
+ match E with
+ [ pz ⇒ 〈 ∅, false 〉
+ | pe ⇒ 〈 ϵ, true 〉
+ | ps x ⇒ 〈 `.x, false 〉
+ | pp x ⇒ 〈 `.x, false 〉
+ | po E1 E2 ⇒ •E1 ⊕ •E2
+ | pc E1 E2 ⇒ •E1 ⊙ 〈 E2, false 〉
+ | pk E ⇒ 〈E,true〉^⊛].
+notation < "• x" non associative with precedence 60 for @{'eclose $x}.
+interpretation "eclose" 'eclose x = (eclose ? x).
+notation > "• x" non associative with precedence 60 for @{'eclose $x}.
+
+ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉.
+interpretation "reclose" 'eclose x = (reclose ? x).
+
+nlemma lemma19_2 :
+ ∀S:Alpha.∀e1,e2:pre S.∀w. w .∈ e1 ⊕ e2 → w .∈ e1 ∨ w .∈ e2.
+#S e1 e2 w H; nnormalize in H; ncases H;
+##[ *; #defw; ncases e1; #p b; ncases b; nnormalize;
+ ##[ #_; @1; @1; /2/ by conj;
+ ##| #H1; @2; @1; /2/ by conj; ##]
+##| #H1; ninversion H1; #; ndestruct; /4/ by or_introl, or_intror; ##]
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; // ]
+notation > "\move term 90 x term 90 E"
+non associative with precedence 60 for @{move ? $x $E}.
+nlet rec move (S: Alpha) (x:S) (E: pitem S) on E : pre S ≝
+ match E with
+ [ pz ⇒ 〈 ∅, false 〉
+ | pe ⇒ 〈 ϵ, false 〉
+ | ps y ⇒ 〈 `y, false 〉
+ | pp y ⇒ 〈 `y, x == y 〉
+ | po e1 e2 ⇒ \move x e1 ⊕ \move x e2
+ | pc e1 e2 ⇒ \move x e1 ⊙ \move x e2
+ | pk e ⇒ (\move x e)^⊛ ].
+notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}.
+notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}.
+interpretation "move" 'move x E = (move ? x E).
+
+ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e).
+interpretation "rmove" 'move x E = (rmove ? x E).
+
+nlemma XXz : ∀S:Alpha.∀w:word S. w .∈ ∅ → False.
+#S w abs; ninversion abs; #; 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/ ]
+nlemma XXe : ∀S:Alpha.∀w:word S. w .∈ ϵ → False.
+#S w abs; ninversion abs; #; ndestruct;
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
- }.
+nlemma XXze : ∀S:Alpha.∀w:word S. w .∈ (∅ · ϵ) → False.
+#S w abs; ninversion abs; #; ndestruct; /2/ by XXz,XXe;
+nqed.
-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 ⇒
- 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'' 〉 ]].
+nlemma eqb_t : ∀S:Alpha.∀a,b:S.∀p:a == b = true. a = b.
+#S a b H; nrewrite < (eqb_true ? a b); //.
+nqed.
+
+naxiom in_move_cat:
+ ∀S.∀w:word S.∀x.∀E1,E2:pitem S. w .∈ \move x (E1 · E2) →
+ (∃w1.∃w2. w = w1@w2 ∧ w1 .∈ \move x E1 ∧ w2 ∈ .|E2|) ∨ w .∈ \move x E2.
+#S w x e1 e2 H; nchange in H with (w .∈ \move x e1 ⊙ \move x e2);
+ncases e1 in H; ncases e2;
+##[##1: *; ##[*; nnormalize; #; ndestruct]
+ #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
+ nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze;
+##|##2: *; ##[*; nnormalize; #; ndestruct]
+ #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
+ nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze;
+##| #r; *; ##[ *; nnormalize; #; ndestruct]
+ #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
+ ##[##2: nnormalize; #; ndestruct; @2; @2; //.##]
+ nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz;
+##| #y; *; ##[ *; nnormalize; #defw defx; ndestruct; @2; @1; /2/ by conj;##]
+ #H; ninversion H; nnormalize; #; ndestruct;
+ ##[ncases (?:False); /2/ by XXz] /3/ by or_intror;
+##| #r1 r2; *; ##[ *; #defw]
+ ...
+nqed.
-(*
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;
+ ∀S:Alpha.∀E:pre S.∀a,w.w .∈ \move a E ↔ (a :: w) .∈ E.
+#S E; ncases E; #r b; nelim r;
+##[##1,2: #a w; @;
+ ##[##1,3: nnormalize; *; ##[##1,3: *; #; ndestruct; ##| #abs; ncases (XXz … abs); ##]
+ #H; ninversion H; #; ndestruct;
+ ##|##*:nnormalize; *; ##[##1,3: *; #; ndestruct; ##| #H1; ncases (XXz … H1); ##]
+ #H; ninversion H; #; ndestruct;##]
+##|#a c w; @; nnormalize; ##[*; ##[*; #; ndestruct; ##] #abs; ninversion abs; #; ndestruct;##]
+ *; ##[##2: #abs; ninversion abs; #; ndestruct; ##] *; #; ndestruct;
+##|#a c w; @; nnormalize;
+ ##[ *; ##[ *; #defw; nrewrite > defw; #ca; @2; nrewrite > (eqb_t … ca); @; ##]
+ #H; ninversion H; #; ndestruct;
+ ##| *; ##[ *; #; ndestruct; ##] #H; ninversion H; ##[##2,3,4,5,6: #; ndestruct]
+ #d defw defa; ndestruct; @1; @; //; nrewrite > (eqb_true S d d); //. ##]
+##|#r1 r2 H1 H2 a w; @;
+ ##[ #H; ncases (in_move_cat … H);
+ ##[ *; #w1; *; #w2; *; *; #defw w1m w2m;
+ ncases (H1 a w1); #H1w1; #_; nlapply (H1w1 w1m); #good;
+ nrewrite > defw; @2; @2 (a::w1); //; ncases good; ##[ *; #; ndestruct] //.
+ ##|
+ ...
+##|
+##|
+##]
nqed.
-*)
-nlet rec move_star S w E on w ≝
+
+notation > "x ↦* E" non associative with precedence 60 for @{move_star ? $x $E}.
+nlet rec move_star (S : decidable) w E on w : bool × (pre S) ≝
match w with
[ nil ⇒ E
- | cons x w' ⇒ move_star S w' (move S x (snd … E))].
+ | cons x w' ⇒ w' ↦* (x ↦ \snd E)].
-ndefinition in_moves ≝ λS,w,E. fst … (move_star S w E).
+ndefinition in_moves ≝ λS:decidable.λw.λE:bool × (pre S). \fst(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))) →
+ \fst E1 = \fst E2 →
+ (∀x. equiv S (x ↦ \snd E1) (x ↦ \snd E2)) →
equiv S E1 E2.
ndefinition NAT: decidable.
@ nat eqb; /2/.
nqed.
+include "hints_declaration.ma".
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+unification hint 0 ≔ ; X ≟ NAT ⊢ carr X ≡ nat.
+
ninductive unit: Type[0] ≝ I: unit.
nlet corec foo_nop (b: bool):
- equiv NAT
+ equiv ?
〈 b, pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0))) 〉
〈 b, pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0) 〉 ≝ ?.
@; //; #x; ncases x
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 : pre ? ≝ ❨ `0 | `1 ❩^* `0.
+ndefinition test2 : pre ? ≝ ❨ (`0`1)^* `0 | (`0`1)^* `1 ❩.
+ndefinition test3 : pre ? ≝ (`0 (`0`1)^* `1)^*.
-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.
+nlemma foo: in_moves ? [0;0;1;0;1;1] (ɛ test3) = true.
nnormalize in match test3;
nnormalize;
//;
projects / helm.git / commitdiff