P1 ≟ refl ? (eq0 (LIST S)),
P2 ≟ sym ? (eq0 (LIST S)),
P3 ≟ trans ? (eq0 (LIST S)),
- X ≟ mk_setoid (list S) (mk_equivalence_relation ? (eq_list T) P1 P2 P3)
+ X ≟ mk_setoid (list (carr S)) (mk_equivalence_relation ? (eq_list S) P1 P2 P3)
(*-----------------------------------------------------------------------*) ⊢
carr X ≡ list T.
-unification hint 0 ≔ S:setoid,a,b:list S;
+unification hint 0 ≔ S:setoid, a,b:list (carr S);
R ≟ eq0 (LIST S),
- L ≟ (list S)
+ L ≟ (list (carr S))
(* -------------------------------------------- *) ⊢
eq_list S a b ≡ eq_rel L R a b.
nqed.
alias symbol "hint_decl" (instance 1) = "hint_decl_Type0".
-unification hint 0 ≔ S:setoid, A,B:list S;
- MM ≟ mk_unary_morphism ??
- (λA:list S.mk_unary_morphism ?? (λB:list S.A @ B) (prop1 ?? (append_is_morph S A)))
+unification hint 0 ≔ S:setoid, A,B:list (carr S);
+ SS ≟ carr S,
+ MM ≟ mk_unary_morphism ?? (λA:list (carr S).
+ mk_unary_morphism ??
+ (λB:list (carr S).A @ B) (prop1 ?? (fun1 ??(append_is_morph S) A)))
(prop1 ?? (append_is_morph S)),
T ≟ LIST 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 ≡ append SS A B.
(* XXX to understand if are always needed or only if the coercion is active *)
unification hint 0 ≔ S1,S2,a,b;
R ≟ PAIR S1 S2,
- L ≟ (pair S1 S2)
+ L ≟ pair (carr S1) (carr S2)
(* -------------------------------------------- *) ⊢
eq_pair S1 S2 a b ≡ eq_rel L (eq0 R) a b.
unification hint 0 ≔ A,B:CProp[0];
T ≟ CPROP,
- MM ≟ mk_unary_morphism1 …
- (λX.mk_unary_morphism1 … (And X) (prop11 … (and_morphism X)))
- (prop11 … and_morphism)
+ MM ≟ mk_unary_morphism1 ??
+ (λX.mk_unary_morphism1 ?? (And X) (prop11 ?? (fun11 ?? and_morphism X)))
+ (prop11 ?? and_morphism)
(*-------------------------------------------------------------*) ⊢
fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ And A B.
unification hint 0 ≔ A,B:CProp[0];
T ≟ CPROP,
MM ≟ mk_unary_morphism1 …
- (λX.mk_unary_morphism1 … (Or X) (prop11 … (or_morphism X)))
+ (λX.mk_unary_morphism1 … (Or X) (prop11 … (fun11 ?? or_morphism X)))
(prop11 … or_morphism)
(*-------------------------------------------------------------*) ⊢
fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ Or A B.
#S; @(λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S P);
#P Q E; @; *; #x Px; @x; ncases (E x x #); /2/; nqed.
-unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CProp[0];
+unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CPROP;
A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP,
B ≟ CPROP,
- M ≟ mk_unary_morphism1 ?? (λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S P)
- (prop11 ?? (Ex_morphism S))
+ M ≟ mk_unary_morphism1 ??
+ (λP: (setoid1_of_setoid S) ⇒_1 CPROP.Ex (carr S) (fun11 ?? P))
+ (prop11 ?? (Ex_morphism S))
(*------------------------*)⊢
- fun11 A B M P ≡ Ex S (fun11 (setoid1_of_setoid S) CPROP P).
+ fun11 A B M P ≡ Ex (carr S) (fun11 (setoid1_of_setoid S) CPROP P).
nlemma Ex_morphism_eta : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CProp[0]) ⇒_1 CProp[0].
#S; @(λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S (λx.P x));
#P Q E; @; *; #x Px; @x; ncases (E x x #); /2/; nqed.
-unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CProp[0];
+unification hint 0 ≔ S : setoid, P : (setoid1_of_setoid S) ⇒_1 CPROP;
A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP,
B ≟ CPROP,
- M ≟ mk_unary_morphism1 ?? (λP: (setoid1_of_setoid S) ⇒_1 CProp[0].Ex S (λx.P x))
- (prop11 ?? (Ex_morphism_eta S))
+ M ≟ mk_unary_morphism1 ??
+ (λP: (setoid1_of_setoid S) ⇒_1 CPROP.Ex (carr S) (λx.fun11 ?? P x))
+ (prop11 ?? (Ex_morphism_eta S))
(*------------------------*)⊢
- fun11 A B M P ≡ Ex S (λx.fun11 (setoid1_of_setoid S) CPROP P x).
+ fun11 A B M P ≡ Ex (carr S) (λx.fun11 (setoid1_of_setoid S) CPROP P x).
nlemma Ex_setoid : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CPROP) → setoid.
#T P; @ (Ex T (λx:T.P x)); @; ##[ #H1 H2; napply True |##*: //; ##] nqed.
-unification hint 0 ≔ T,P ;
+unification hint 0 ≔ T : setoid,P ;
S ≟ (Ex_setoid T P)
(*---------------------------*) ⊢
- Ex T (λx:T.P x) ≡ carr S.
+ Ex (carr T) (λx:carr T.fun11 ?? P x) ≡ carr S.
(* couts how many Ex we are traversing *)
ninductive counter : Type[0] ≝
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;
nqed.
unification hint 0 ≔ o1,o2,o3:setoid,f:o2 ⇒_0 o3,g:o1 ⇒_0 o2;
- R ≟ mk_unary_morphism ?? (composition ??? f g)
- (prop1 ?? (comp_unary_morphisms o1 o2 o3 f g))
+ R ≟ mk_unary_morphism o1 o3
+ (composition ??? (fun1 o2 o3 f) (fun1 o1 o2 g))
+ (prop1 o1 o3 (comp_unary_morphisms o1 o2 o3 f g))
(* -------------------------------------------------------------------- *) ⊢
- fun1 o1 o3 R ≡ (composition o1 o2 o3 f g).
+ fun1 o1 o3 R ≡ composition ??? (fun1 o2 o3 f) (fun1 o1 o2 g).
ndefinition comp_binary_morphisms:
∀o1,o2,o3.(o2 ⇒_0 o3) ⇒_0 ((o1 ⇒_0 o2) ⇒_0 (o1 ⇒_0 o3)).
nqed.
unification hint 0 ≔ o1,o2,o3:setoid1,f:o2 ⇒_1 o3,g:o1 ⇒_1 o2;
- R ≟ (mk_unary_morphism1 ?? (composition1 ??? f g)
+ R ≟ (mk_unary_morphism1 ?? (composition1 ??? (fun11 ?? f) (fun11 ?? g))
(prop11 ?? (comp1_unary_morphisms o1 o2 o3 f g)))
(* -------------------------------------------------------------------- *) ⊢
- fun11 o1 o3 R ≡ (composition1 o1 o2 o3 f g).
+ fun11 o1 o3 R ≡ composition1 ??? (fun11 ?? f) (fun11 ?? g).
ndefinition comp1_binary_morphisms:
∀o1,o2,o3. (o2 ⇒_1 o3) ⇒_1 ((o1 ⇒_1 o2) ⇒_1 (o1 ⇒_1 o3)).
[ napply (. (ext_prop … Ha^-1)) | napply (. (ext_prop … Ha)) ] /2/.
nqed.
-unification hint 0 ≔ AA, x, S;
+unification hint 0 ≔ AA : setoid, S : 𝛀^AA, x : carr AA;
A ≟ carr AA,
SS ≟ (ext_carr ? S),
TT ≟ (mk_unary_morphism1 ??
- (λx:setoid1_of_setoid ?.
+ (λx:carr1 (setoid1_of_setoid ?).
mk_unary_morphism1 ??
- (λS:ext_powerclass_setoid ?. x ∈ S)
- (prop11 ?? (mem_ext_powerclass_setoid_is_morph AA x)))
+ (λS:carr1 (ext_powerclass_setoid ?). x ∈ (ext_carr ? S))
+ (prop11 ?? (fun11 ?? (mem_ext_powerclass_setoid_is_morph AA) x)))
(prop11 ?? (mem_ext_powerclass_setoid_is_morph AA))),
- XX ≟ (ext_powerclass_setoid AA)
- (*-------------------------------------*) ⊢
- fun11 (setoid1_of_setoid AA)
- (unary_morphism1_setoid1 XX CPROP) TT x S
- ≡ mem A SS x.
+ T2 ≟ (ext_powerclass_setoid AA)
+(*---------------------------------------------------------------------------*) ⊢
+ fun11 T2 CPROP (fun11 (setoid1_of_setoid AA) (unary_morphism1_setoid1 T2 CPROP) TT x) S ≡ mem A SS x.
nlemma set_ext : ∀S.∀A,B:Ω^S.A =_1 B → ∀x:S.(x ∈ A) =_1 (x ∈ B).
#S A B; *; #H1 H2 x; @; ##[ napply H1 | napply H2] nqed.
nqed.
alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ≔
- A : setoid, B,C : ext_powerclass A;
- R ≟ (mk_ext_powerclass ? (B ∩ C) (ext_prop ? (intersect_is_ext ? B C)))
+unification hint 0 ≔ A : setoid, B,C : 𝛀^A;
+ AA ≟ carr A,
+ BB ≟ ext_carr ? B,
+ CC ≟ ext_carr ? C,
+ R ≟ (mk_ext_powerclass ?
+ (ext_carr ? B ∩ ext_carr ? C)
+ (ext_prop ? (intersect_is_ext ? B C)))
(* ------------------------------------------*) ⊢
- ext_carr A R ≡ intersect ? (ext_carr ? B) (ext_carr ? C).
+ ext_carr A R ≡ intersect AA BB CC.
nlemma intersect_is_morph: ∀A. Ω^A ⇒_1 Ω^A ⇒_1 Ω^A.
#A; napply (mk_binary_morphism1 … (λS,S'. S ∩ S'));
unification hint 0 ≔ A : Type[0], B,C : Ω^A;
T ≟ powerclass_setoid A,
R ≟ mk_unary_morphism1 ??
- (λS. mk_unary_morphism1 ?? (λS'.S ∩ S') (prop11 ?? (intersect_is_morph A S)))
+ (λX. mk_unary_morphism1 ??
+ (λY.X ∩ Y) (prop11 ?? (fun11 ?? (intersect_is_morph A) X)))
(prop11 ?? (intersect_is_morph A))
(*------------------------------------------------------------------------*) ⊢
fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C ≡ intersect A B C.
AA : setoid, B,C : 𝛀^AA;
A ≟ carr AA,
T ≟ ext_powerclass_setoid AA,
- R ≟ (mk_unary_morphism1 ??
- (λS:𝛀^AA.
- mk_unary_morphism1 ??
- (λS':𝛀^AA.
- mk_ext_powerclass AA (S∩S') (ext_prop AA (intersect_is_ext ? S S')))
- (prop11 ?? (intersect_is_ext_morph AA S)))
+ R ≟ (mk_unary_morphism1 ?? (λX:𝛀^AA.
+ mk_unary_morphism1 ?? (λY:𝛀^AA.
+ mk_ext_powerclass AA
+ (ext_carr ? X ∩ ext_carr ? Y)
+ (ext_prop AA (intersect_is_ext ? X Y)))
+ (prop11 ?? (fun11 ?? (intersect_is_ext_morph AA) X)))
(prop11 ?? (intersect_is_ext_morph AA))) ,
BB ≟ (ext_carr ? B),
CC ≟ (ext_carr ? C)
nqed.
alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ≔
- A : setoid, B,C : 𝛀^A;
- R ≟ (mk_ext_powerclass ? (B ∪ C) (ext_prop ? (union_is_ext ? B C)))
+unification hint 0 ≔ A : setoid, B,C : 𝛀^A;
+ AA ≟ carr A,
+ BB ≟ ext_carr ? B,
+ CC ≟ ext_carr ? C,
+ R ≟ mk_ext_powerclass ?
+ (ext_carr ? B ∪ ext_carr ? C) (ext_prop ? (union_is_ext ? B C))
(*-------------------------------------------------------------------------*) ⊢
- ext_carr A R ≡ union ? (ext_carr ? B) (ext_carr ? C).
+ ext_carr A R ≡ union AA BB CC.
unification hint 0 ≔ S:Type[0], A,B:Ω^S;
T ≟ powerclass_setoid S,
MM ≟ mk_unary_morphism1 ??
- (λA.mk_unary_morphism1 ?? (λB.A ∪ B) (prop11 ?? (union_is_morph S A)))
+ (λA.mk_unary_morphism1 ??
+ (λB.A ∪ B) (prop11 ?? (fun11 ?? (union_is_morph S) A)))
(prop11 ?? (union_is_morph S))
(*--------------------------------------------------------------------------*) ⊢
fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ A ∪ B.
AA : setoid, B,C : 𝛀^AA;
A ≟ carr AA,
T ≟ ext_powerclass_setoid AA,
- R ≟ (mk_unary_morphism1 ??
- (λS:𝛀^AA.
- mk_unary_morphism1 ??
- (λS':𝛀^AA.
- mk_ext_powerclass AA (S ∪ S') (ext_prop AA (union_is_ext ? S S')))
- (prop11 ?? (union_is_ext_morph AA S)))
- (prop11 ?? (union_is_ext_morph AA))) ,
+ R ≟ mk_unary_morphism1 ?? (λX:𝛀^AA.
+ mk_unary_morphism1 ?? (λY:𝛀^AA.
+ mk_ext_powerclass AA
+ (ext_carr ? X ∪ ext_carr ? Y) (ext_prop AA (union_is_ext ? X Y)))
+ (prop11 ?? (fun11 ?? (union_is_ext_morph AA) X)))
+ (prop11 ?? (union_is_ext_morph AA)),
BB ≟ (ext_carr ? B),
CC ≟ (ext_carr ? C)
(*------------------------------------------------------*) ⊢
nqed.
alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ≔
- A : setoid, B,C : 𝛀^A;
- R ≟ (mk_ext_powerclass ? (B - C) (ext_prop ? (substract_is_ext ? B C)))
-(*-------------------------------------------------------------------------*) ⊢
- ext_carr A R ≡ substract ? (ext_carr ? B) (ext_carr ? C).
+unification hint 0 ≔ A : setoid, B,C : 𝛀^A;
+ AA ≟ carr A,
+ BB ≟ ext_carr ? B,
+ CC ≟ ext_carr ? C,
+ R ≟ mk_ext_powerclass ?
+ (ext_carr ? B - ext_carr ? C)
+ (ext_prop ? (substract_is_ext ? B C))
+(*---------------------------------------------------*) ⊢
+ ext_carr A R ≡ substract AA BB CC.
unification hint 0 ≔ S:Type[0], A,B:Ω^S;
T ≟ powerclass_setoid S,
MM ≟ mk_unary_morphism1 ??
- (λA.mk_unary_morphism1 ?? (λB.A - B) (prop11 ?? (substract_is_morph S A)))
+ (λA.mk_unary_morphism1 ??
+ (λB.A - B) (prop11 ?? (fun11 ?? (substract_is_morph S) A)))
(prop11 ?? (substract_is_morph S))
(*--------------------------------------------------------------------------*) ⊢
fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ A - B.
AA : setoid, B,C : 𝛀^AA;
A ≟ carr AA,
T ≟ ext_powerclass_setoid AA,
- R ≟ (mk_unary_morphism1 ??
- (λS:𝛀^AA.
- mk_unary_morphism1 ??
- (λS':𝛀^AA.
- mk_ext_powerclass AA (S - S') (ext_prop AA (substract_is_ext ? S S')))
- (prop11 ?? (substract_is_ext_morph AA S)))
- (prop11 ?? (substract_is_ext_morph AA))) ,
+ R ≟ mk_unary_morphism1 ?? (λX:𝛀^AA.
+ mk_unary_morphism1 ?? (λY:𝛀^AA.
+ mk_ext_powerclass AA
+ (ext_carr ? X - ext_carr ? Y)
+ (ext_prop AA (substract_is_ext ? X Y)))
+ (prop11 ?? (fun11 ?? (substract_is_ext_morph AA) X)))
+ (prop11 ?? (substract_is_ext_morph AA)),
BB ≟ (ext_carr ? B),
CC ≟ (ext_carr ? C)
(*------------------------------------------------------*) ⊢
#X a; @; ##[ napply ({(a)}); ##] #x y E; @; #H; /3/; nqed.
alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ≔ A : setoid, a:A;
+unification hint 0 ≔ A : setoid, a : carr A;
R ≟ (mk_ext_powerclass ? {(a)} (ext_prop ? (single_is_ext ? a)))
(*-------------------------------------------------------------------------*) ⊢
ext_carr A R ≡ singleton A a.
-unification hint 0 ≔ A:setoid, a:A;
+unification hint 0 ≔ A:setoid, a : carr A;
T ≟ setoid1_of_setoid A,
AA ≟ carr A,
MM ≟ mk_unary_morphism1 ??
- (λa:setoid1_of_setoid A.{(a)}) (prop11 ?? (single_is_morph A))
+ (λa:carr1 (setoid1_of_setoid A).{(a)}) (prop11 ?? (single_is_morph A))
(*--------------------------------------------------------------------------*) ⊢
fun11 T (powerclass_setoid AA) MM a ≡ {(a)}.
nlemma single_is_ext_morph:∀A:setoid.(setoid1_of_setoid A) ⇒_1 𝛀^A.
#A; @; ##[ #a; napply (single_is_ext ? a); ##] #a b E; @; #x; /3/; nqed.
-unification hint 1 ≔
- AA : setoid, a: AA;
+unification hint 1 ≔ AA : setoid, a: carr AA;
T ≟ ext_powerclass_setoid AA,
R ≟ mk_unary_morphism1 ??
- (λa:setoid1_of_setoid AA.
+ (λa:carr1 (setoid1_of_setoid AA).
mk_ext_powerclass AA {(a)} (ext_prop ? (single_is_ext AA a)))
(prop11 ?? (single_is_ext_morph AA))
(*------------------------------------------------------*) ⊢
ext_carr AA (fun11 (setoid1_of_setoid AA) T R a) ≡ singleton AA a.
-
-
-
-
(*
alias symbol "hint_decl" = "hint_decl_Type2".
unification hint 0 ≔
projects / helm.git / commitdiff