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 ]
+ #S; #w; #H; ninversion H; #; ndestruct; //.
nqed.
naxiom in_l_inv_s:
let E1' ≝ eclose ? E1 in
let E1'' ≝ snd … E1' in
match fst … E1' with
- [ true =>
+ [ true ⇒
let E2' ≝ eclose ? E2 in
〈 fst … E2', pc ? E1'' (snd … E2') 〉
| false ⇒ 〈 false, pc ? E1'' E2 〉 ]
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; #H; ncases (?: False); /2/
| #x; #H; ncases (?: False); /2/
| #w1; #w2; ncases (fst … (eclose S w1)); nnormalize; /3/;
#_; #_; #H; ncases (?:False); /2/
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
+ [##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; //
- | #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 ]
+ ndestruct; // ]
nqed.
ntheorem eclose_true':
| #E1; #E2; ncases (fst … (eclose S E1)); nnormalize
[ #H1; #H2; #H3; ninversion H3; /3/;
##| #H1; #H2; #H3; ninversion H3
- [ #_; #K; ndestruct
- | #x; #K; ndestruct
+ [ ##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 ?); //
- | #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 ]##]
+ napply H1; nrewrite < (eq_append_nil_to_eq_nil1 … w1 w2 ?); //]##]
##| #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
+ [ ##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/
- | #w; #E1'; #E2'; #H1'; #H2'; #H3'; #H4; ndestruct; /2/
- | #a; #b; #c; ndestruct
- | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct]##]
+ /2/ ]##]
nqed.
(*
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.
-ndefinition test1 ≝
- pc ? (pk ? (po ? (ps ? 0) (ps ? 1))) (ps ? 0).
+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.
-ndefinition test2 ≝
- po ?
- (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0))
- (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 1)).
+(*
+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.
+*)
-ndefinition test3 ≝
- pk ? (pc ? (pc ? (ps ? 0) (pk ? (pc ? (ps ? 0) (ps ? 1)))) (ps ? 1)).
+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.
(**********************************************************)