interpretation "empty" 'empty_r = (z ?).
notation > "'lang' S" non associative with precedence 90 for @{ Ω^(list $S) }.
-notation > "'Elang' S" non associative with precedence 90 for @{ 𝛀^(list $S) }.
+notation > "'Elang' S" non associative with precedence 90 for @{ 𝛀^(LIST $S) }.
(* setoid support for re *)
(*-----------------------------------------------------------------------*) ⊢
carr X ≡ re T.
-unification hint 0 ≔ A:Alpha,a,b:re A;
+unification hint 0 ≔ A:Alpha, a,b:re (carr (acarr A));
R ≟ eq0 (RE A),
- L ≟ re A
+ L ≟ re (carr (acarr A))
(* -------------------------------------------- *) ⊢
eq_re A a b ≡ eq_rel L R a b.
(* XXX This is the good format for hints about morphisms, fix the others *)
alias symbol "hint_decl" (instance 1) = "hint_decl_Type0".
-unification hint 0 ≔ S:Alpha, A,B:re S;
- MM ≟ mk_unary_morphism ??
- (λA:re S.mk_unary_morphism ?? (λB.A · B) (prop1 ?? (c_is_morph S A)))
- (prop1 ?? (c_is_morph S)),
+unification hint 0 ≔ S:Alpha, A,B:re (carr (acarr S));
+ SS ≟ carr (acarr S),
+ MM ≟ mk_unary_morphism ?? (λA.
+ mk_unary_morphism ??
+ (λB.A · B) (prop1 ?? (fun1 ?? (c_is_morph S) A)))
+ (prop1 ?? (c_is_morph S)),
T ≟ RE S
(*--------------------------------------------------------------------------*) ⊢
- fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ A · B.
+ fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ c SS A B.
nlemma o_is_morph : ∀A:Alpha.(re A) ⇒_0 (re A) ⇒_0 (re A).
#A; napply (mk_binary_morphism … (λs1,s2:re A. s1 + s2));
##|#r IH a'; ncases a'; nnormalize; /2/ by conj; ##]
nqed.
-unification hint 0 ≔ S:Alpha, A,B:re S;
- MM ≟ mk_unary_morphism ??
- (λA:re S.mk_unary_morphism ?? (λB.A + B) (prop1 ?? (o_is_morph S A)))
- (prop1 ?? (o_is_morph S)),
+unification hint 0 ≔ S:Alpha, A,B:re (carr (acarr S));
+ SS ≟ carr (acarr S),
+ MM ≟ mk_unary_morphism ?? (λA.
+ mk_unary_morphism ??
+ (λB.A + B) (prop1 ?? (fun1 ?? (o_is_morph S) A)))
+ (prop1 ?? (o_is_morph S)),
T ≟ RE S
(*--------------------------------------------------------------------------*) ⊢
- fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ A + B.
+ fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ o SS A B.
(* end setoids support for re *)
nqed.
alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ≔ A : setoid, B,C : Elang A;
+unification hint 0 ≔ A : setoid, B,C : Elang A;
AA ≟ LIST A,
- R ≟ mk_ext_powerclass ?
- (ext_carr ? B · ext_carr ? C) (ext_prop ? (cat_is_ext ? B C))
-(*--------------------------------------------------------------------*) ⊢
- ext_carr AA R ≡ cat A (ext_carr AA B) (ext_carr AA C).
+ BB ≟ ext_carr AA B,
+ CC ≟ ext_carr AA C,
+ R ≟ mk_ext_powerclass AA
+ (cat A (ext_carr AA B) (ext_carr AA C))
+ (ext_prop AA (cat_is_ext A B C))
+(*----------------------------------------------------------*) ⊢
+ ext_carr AA R ≡ cat A BB CC.
-unification hint 0 ≔ S:setoid, A,B:lang S;
- T ≟ powerclass_setoid (list S),
+unification hint 0 ≔ S:setoid, A,B:lang (carr S);
+ T ≟ powerclass_setoid (list (carr S)),
MM ≟ mk_unary_morphism1 T (unary_morphism1_setoid1 T T)
- (λA:lang S.
+ (λA:lang (carr S).
mk_unary_morphism1 T T
- (λB:lang S.cat S A B) (prop11 T T (cat_is_morph S A)))
+ (λB:lang (carr S).cat S A B)
+ (prop11 T T (fun11 ?? (cat_is_morph S) A)))
(prop11 T (unary_morphism1_setoid1 T T) (cat_is_morph S))
(*--------------------------------------------------------------------------*) ⊢
fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ cat S A B.
unification hint 1 ≔ AA : setoid, B,C : Elang AA;
AAS ≟ LIST AA,
- T ≟ ext_powerclass_setoid (list AA),
- R ≟ mk_unary_morphism1 T (unary_morphism1_setoid1 T T)
- (λS:Elang AA.
- mk_unary_morphism1 T T
- (λS':Elang AA.
- mk_ext_powerclass (list AA) (cat AA (ext_carr ? S) (ext_carr ? S'))
- (ext_prop (list AA) (cat_is_ext AA S S')))
- (prop11 T T (cat_is_ext_morph AA S)))
- (prop11 T (unary_morphism1_setoid1 T T) (cat_is_ext_morph AA)),
+ T ≟ ext_powerclass_setoid AAS,
+ R ≟ mk_unary_morphism1 T (unary_morphism1_setoid1 T T) (λX:Elang AA.
+ mk_unary_morphism1 T T (λY:Elang AA.
+ mk_ext_powerclass AAS
+ (cat AA (ext_carr ? X) (ext_carr ? Y))
+ (ext_prop AAS (cat_is_ext AA X Y)))
+ (prop11 T T (fun11 ?? (cat_is_ext_morph AA) X)))
+ (prop11 T (unary_morphism1_setoid1 T T) (cat_is_ext_morph AA)),
BB ≟ ext_carr ? B,
CC ≟ ext_carr ? C
(*------------------------------------------------------*) ⊢
λS.λl.{ w ∈ list S | ∃lw.flatten ? lw = w ∧ conjunct ? lw l}.
interpretation "star lang" 'pk l = (star ? l).
+(* hints for star *)
+nlemma star_is_morph : ∀A:setoid. (lang A) ⇒_1 (lang A).
+#X; @(λA:lang X.A^* ); #a1 a2 E; @; #x; *; #wl; *; #defx Px; @wl; @; //;
+nelim wl in Px; //; #s tl IH; *; #a1s a1tl; /4/; nqed.
+
+nlemma star_is_ext: ∀A:setoid. (Elang A) → (Elang A).
+ #S A; @ ((ext_carr … A) ^* ); #w1 w2 E; @; *; #wl; *; #defw1 Pwl;
+ @wl; @; //; napply (.=_0 defw1); /2/; nqed.
+
+alias symbol "hint_decl" = "hint_decl_Type1".
+unification hint 0 ≔ A : setoid, B : Elang A;
+ AA ≟ LIST A,
+ BB ≟ ext_carr AA B,
+ R ≟ mk_ext_powerclass ?
+ ((ext_carr ? B)^* ) (ext_prop ? (star_is_ext ? B))
+(*--------------------------------------------------------------------*) ⊢
+ ext_carr AA R ≡ star A BB.
+
+unification hint 0 ≔ S:setoid, A:lang (carr S);
+ T ≟ powerclass_setoid (list (carr S)),
+ MM ≟ mk_unary_morphism1 T T
+ (λB:lang (carr S).star S B) (prop11 T T (star_is_morph S))
+(*--------------------------------------------------------------------------*) ⊢
+ fun11 T T MM A ≡ star S A.
+
+nlemma star_is_ext_morph:∀A:setoid.(Elang A) ⇒_1 (Elang A).
+#A; @(star_is_ext …);
+#x1 x2 Ex; napply (prop11 … (star_is_morph A)); nassumption.
+nqed.
+
+unification hint 1 ≔ AA : setoid, B : Elang AA;
+ AAS ≟ LIST AA,
+ T ≟ ext_powerclass_setoid AAS,
+ R ≟ mk_unary_morphism1 T T
+ (λS:Elang AA.
+ mk_ext_powerclass AAS (star AA (ext_carr ? S))
+ (ext_prop AAS (star_is_ext AA S)))
+ (prop11 T T (star_is_ext_morph AA)),
+ BB ≟ ext_carr ? B
+(*------------------------------------------------------*) ⊢
+ ext_carr AAS (fun11 T T R B) ≡ star AA BB.
+
+(* end hints for star *)
+
notation > "𝐋 term 70 E" non associative with precedence 75 for @{L_re ? $E}.
nlet rec L_re (S : Alpha) (r : re S) on r : lang S ≝
match r with
##| #e H; @; *; #l; *; #defw1 Pl; @l; @; //; napply (.=_1 defw1); /2/; ##]
nqed.
-unification hint 0 ≔ S : Alpha,e : re S;
- SS ≟ LIST S,
+unification hint 0 ≔ S : Alpha,e : re (carr (acarr S));
+ SS ≟ LIST (acarr S),
X ≟ mk_ext_powerclass SS (𝐋 e) (ext_prop SS (L_re_is_ext S e))
(*-----------------------------------------------------------------*)⊢
ext_carr SS X ≡ L_re S e.
@; ##[##1,3: nassumption] /2/; ##]
nqed.
-unification hint 0 ≔ A:Alpha, a:re A;
+unification hint 0 ≔ A:Alpha, a:re (carr (acarr A));
T ≟ setoid1_of_setoid (RE A),
- T1 ≟ LIST A,
- T2 ≟ powerclass_setoid T1,
+ T2 ≟ powerclass_setoid (list (carr (acarr A))),
MM ≟ mk_unary_morphism1 ??
- (λa:setoid1_of_setoid (RE A).𝐋 a) (prop11 ?? (L_re_is_morph A))
+ (λa:carr1 (setoid1_of_setoid (RE A)).𝐋 a) (prop11 ?? (L_re_is_morph A))
(*--------------------------------------------------------------------------*) ⊢
- fun11 T T2 MM a ≡ 𝐋 a.
+ fun11 T T2 MM a ≡ L_re A a.
nlemma L_re_is_ext_morph:∀A:Alpha.(setoid1_of_setoid (re A)) ⇒_1 𝛀^(list A).
#A; @; ##[ #a; napply (L_re_is_ext ? a); ##] #a b E;
##| napply (. (# ╪_1 ?)); ##[##3: napply H |##2: ##skip ] napply (EL^-1)]
nqed.
-unification hint 1 ≔ AA : Alpha, a: re AA;
- T ≟ RE AA, T1 ≟ LIST AA, TT ≟ ext_powerclass_setoid T1,
- R ≟ mk_unary_morphism1 ??
- (λa:setoid1_of_setoid T.
- mk_ext_powerclass ? (𝐋 a) (ext_prop ? (L_re_is_ext AA a)))
- (prop11 ?? (L_re_is_ext_morph AA))
+unification hint 1 ≔ AA : Alpha, a: re (carr (acarr AA));
+ T ≟ RE AA, T1 ≟ LIST (acarr AA), T2 ≟ setoid1_of_setoid T,
+ TT ≟ ext_powerclass_setoid T1,
+ R ≟ mk_unary_morphism1 T2 TT
+ (λa:carr1 (setoid1_of_setoid T).
+ mk_ext_powerclass T1 (𝐋 a) (ext_prop T1 (L_re_is_ext AA a)))
+ (prop11 T2 TT (L_re_is_ext_morph AA))
(*------------------------------------------------------*) ⊢
ext_carr T1 (fun11 (setoid1_of_setoid T) TT R a) ≡ L_re AA a.
P1 ≟ refl ? (eq0 (PITEM SS)),
P2 ≟ sym ? (eq0 (PITEM SS)),
P3 ≟ trans ? (eq0 (PITEM SS)),
- R ≟ mk_setoid (pitem S)
+ R ≟ mk_setoid (pitem (carr S))
(mk_equivalence_relation (pitem A) (eq_pitem SS) P1 P2 P3)
(*-----------------------------------------------------------------*)⊢
carr R ≡ pitem A.
-unification hint 0 ≔ S:Alpha,a,b:pitem S;
- R ≟ PITEM S, L ≟ (pitem S)
+unification hint 0 ≔ S:Alpha,a,b:pitem (carr (acarr S));
+ R ≟ PITEM S, L ≟ pitem (carr (acarr S))
(* -------------------------------------------- *) ⊢
eq_pitem S a b ≡ eq_rel L (eq0 R) a b.
##]
nqed.
-unification hint 0 ≔ S : Alpha,e : pitem S;
- SS ≟ (list S),
- X ≟ (mk_ext_powerclass SS (𝐋\p e) (ext_prop SS (L_pi_ext S e)))
+unification hint 0 ≔ S : Alpha,e : pitem (carr (acarr S));
+ SS ≟ LIST (acarr S),
+ X ≟ mk_ext_powerclass SS (𝐋\p e) (ext_prop SS (L_pi_ext S e))
(*-----------------------------------------------------------------*)⊢
ext_carr SS X ≡ 𝐋\p e.
nlemma erase_bull : ∀S:Alpha.∀a:pitem S. |\fst (•a)| = |a|.
#S a; nelim a; // by {};
##[ #e1 e2 IH1 IH2;
- napply (?^-1);
+ napply (?^-1);
napply (.=_0 (IH1^-1)╪_0 (IH2^-1));
nchange in match (•(e1 · ?)) with (?⊙?);
ncases (•e1); #e3 b; ncases b; ##[ nnormalize; ncases (•e2); /3/ by refl, conj]
(* XXX This seems to be a pattern for equations *)
alias symbol "hint_decl" (instance 1) = "hint_decl_CProp2".
-unification hint 0 ≔ S : Alpha, x,y: re S;
+unification hint 0 ≔ S : Alpha, x,y: re (carr (acarr S));
SS ≟ RE S,
TT ≟ setoid1_of_setoid SS,
T ≟ carr1 TT
//]
nqed.
-STOP
+
nlemma sub_dot_star :
- ∀S.∀X:word S → Prop.∀b. (X - ϵ b) · X^* ∪ {[]} = X^*.
-#S X b; napply extP; #w; @;
-##[ *; ##[##2: nnormalize; #defw; nrewrite < defw; @[]; @; //]
+ ∀S:Alpha.∀X:Elang S.∀b. (X - ϵ b) · (ext_carr … X)^* ∪ {[]} = (ext_carr … X)^*.
+#S X b; napply ext_set; #w; @;
+##[ *; ##[##2: #defw; @[]; @; //]
*; #w1; *; #w2; *; *; #defw sube; *; #lw; *; #flx cj;
- @ (w1 :: lw); nrewrite < defw; nrewrite < flx; @; //;
+ @ (w1 :: lw); @; ##[ napply (.=_0 # ╪_0 flx); napply (?^-1); //]
@; //; napply (subW … sube);
-##| *; #wl; *; #defw Pwl; nrewrite < defw; nelim wl in Pwl; ##[ #_; @2; //]
+##| *; #wl; *; #defw Pwl; (* STOP manca ext_carr vs epsilon. *)
+ncases b; ##[ nchange in match (ϵtrue) with {[]}.
+napply (. (defw^-1 ╪_1 #)); nelim wl in Pwl; /2/;
+#s tl IH; *; #Xs Ptl; ncases s in Xs; ##[ #; napply IH; //] #x xs Xxxs;
+@; @(x :: xs); @(flatten ? tl); @; ##[ @; ##[ napply #] @; //; nassumption; ##]
+nelim tl in Ptl; ##[ #; @[]; /2/] #w ws IH; *; #Xw Pws; @(w :: ws); @; ##[ napply #]
+@; //;
+
+
+
+ nrewrite < defw; nelim wl in Pwl; ##[ #_; @2; //]
#w' wl' IH; *; #Pw' IHp; nlapply (IH IHp); *;
##[ *; #w1; *; #w2; *; *; #defwl' H1 H2;
@; ncases b in H1; #H1;
projects / helm.git / blobdiff