mk_unary_morphism1 …
(λX:CProp[0].mk_unary_morphism1 … (λY:CProp[0]. X → Y) (prop11 … (if_morphism X)))
(prop11 … if_morphism)
- A B ≡ A → B.
\ No newline at end of file
+ A B ≡ A → B.
+
+(* not as morphism *)
+nlemma Not_morphism : CProp[0] ⇒_1 CProp[0].
+@(λx:CProp[0].¬ x); #a b; *; #; @; /3/; nqed.
+
+unification hint 0 ≔ P : CProp[0];
+ A ≟ CPROP,
+ B ≟ CPROP,
+ M ≟ mk_unary_morphism1 ?? (λP.¬ P) (prop11 ?? Not_morphism)
+(*------------------------*)⊢
+ fun11 A B M P ≡ ¬ P.
+
+(* Ex setoid support *)
+
+(* The caml, as some patches for it
+ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.
+*)
+
+(* simple case where the whole predicate can be rewritten *)
+nlemma Ex_morphism : ∀S:setoid.((setoid1_of_setoid S) ⇒_1 CProp[0]) ⇒_1 CProp[0].
+#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];
+ 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))
+(*------------------------*)⊢
+ fun11 A B M P ≡ Ex 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];
+ 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))
+(*------------------------*)⊢
+ fun11 A B M P ≡ Ex 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 ;
+ S ≟ (Ex_setoid T P)
+(*---------------------------*) ⊢
+ Ex T (λx:T.P x) ≡ carr S.
+
+(* couts how many Ex we are traversing *)
+ninductive counter : Type[0] ≝
+ | End : counter
+ | Next : (Prop → Prop) → (* dummy arg please the notation mechanism *)
+ counter → counter.
+
+(* to rewrite terms (live in setoid) *)
+nlet rec mk_P (S, T : setoid) (n : counter) on n ≝
+ match n with [ End ⇒ T → CProp[0] | Next _ m ⇒ S → (mk_P S T m) ].
+
+nlet rec mk_F (S, T : setoid) (n : counter) on n ≝
+ match n with [ End ⇒ T | Next _ m ⇒ S → (mk_F S T m) ].
+
+nlet rec mk_E (S, T : setoid) (n : counter) on n : ∀f,g : mk_F S T n. CProp[0] ≝
+ match n with
+ [ End ⇒ λf,g:T. f = g
+ | Next q m ⇒ λf,g: mk_F S T (Next q m). ∀x:S.mk_E S T m (f x) (g x) ].
+
+nlet rec mk_H (S, T : setoid) (n : counter) on n :
+∀P1,P2: mk_P S T n.∀f,g : mk_F S T n. CProp[1] ≝
+ match n with
+ [ End ⇒ λP1,P2:mk_P S T End.λf,g:T. f = g → P1 f =_1 P2 g
+ | Next q m ⇒ λP1,P2: mk_P S T (Next q m).λf,g: mk_F S T (Next q m).
+ ∀x:S.mk_H S T m (P1 x) (P2 x) (f x) (g x) ].
+
+nlet rec mk_Ex (S, T : setoid) (n : counter) on n :
+∀P: mk_P S T n.∀f : mk_F S T n. CProp[0] ≝
+ match n with
+ [ End ⇒ λP:mk_P S T End.λf:T. P f
+ | Next q m ⇒ λP: mk_P S T (Next q m).λf: mk_F S T (Next q m).
+ ∃x:S.mk_Ex S T m (P x) (f x) ].
+
+nlemma Sig_generic : ∀S,T.∀n:counter.∀P,f,g.
+ mk_E S T n f g → mk_H S T n P P f g → mk_Ex S T n P f =_1 mk_Ex S T n P g.
+#S T n; nelim n; nnormalize;
+##[ #P f g E H; /2/;
+##| #q m IH P f g E H; @; *; #x Px; @x; ncases (IH … (E x) (H x)); /3/; ##]
+nqed.
+
+(* to rewrite propositions (live in setoid1) *)
+nlet rec mk_P1 (S : setoid) (T : setoid1) (n : counter) on n ≝
+ match n with [ End ⇒ T → CProp[0] | Next _ m ⇒ S → (mk_P1 S T m) ].
+
+nlet rec mk_F1 (S : setoid) (T : setoid1) (n : counter) on n ≝
+ match n with [ End ⇒ T | Next _ m ⇒ S → (mk_F1 S T m) ].
+
+nlet rec mk_E1 (S : setoid) (T : setoid1) (n : counter) on n : ∀f,g : mk_F1 S T n. CProp[1] ≝
+ match n with
+ [ End ⇒ λf,g:T. f =_1 g
+ | Next q m ⇒ λf,g: mk_F1 S T (Next q m). ∀x:S.mk_E1 S T m (f x) (g x) ].
+
+nlet rec mk_H1 (S : setoid) (T : setoid1) (n : counter) on n :
+∀P1,P2: mk_P1 S T n.∀f,g : mk_F1 S T n. CProp[1] ≝
+ match n with
+ [ End ⇒ λP1,P2:mk_P1 S T End.λf,g:T. f = g → P1 f =_1 P2 g
+ | Next q m ⇒ λP1,P2: mk_P1 S T (Next q m).λf,g: mk_F1 S T (Next q m).
+ ∀x:S.mk_H1 S T m (P1 x) (P2 x) (f x) (g x) ].
+
+nlet rec mk_Ex1 (S : setoid) (T : setoid1) (n : counter) on n :
+∀P: mk_P1 S T n.∀f : mk_F1 S T n. CProp[0] ≝
+ match n with
+ [ End ⇒ λP:mk_P1 S T End.λf:T. P f
+ | Next q m ⇒ λP: mk_P1 S T (Next q m).λf: mk_F1 S T (Next q m).
+ ∃x:S.mk_Ex1 S T m (P x) (f x) ].
+
+nlemma Sig_generic1 : ∀S,T.∀n:counter.∀P,f,g.
+ mk_E1 S T n f g → mk_H1 S T n P P f g → mk_Ex1 S T n P f =_1 mk_Ex1 S T n P g.
+#S T n; nelim n; nnormalize;
+##[ #P f g E H; /2/;
+##| #q m IH P f g E H; @; *; #x Px; @x; ncases (IH … (E x) (H x)); /3/; ##]
+nqed.
+
+(* notation "∑x1,...,xn. E / H ; P" were:
+ - x1...xn are bound in E and P, H is bound in P
+ - H is an identifier that will have the type of E in P
+ - P is the proof that the two existentially quantified predicates are equal*)
+notation > "∑ list1 ident x sep , . term 56 E / ident nE ; term 19 H" with precedence 20
+for @{ 'Sig_gen
+ ${ fold right @{ 'End } rec acc @{ ('Next (λ${ident x}.${ident x}) $acc) } }
+ ${ fold right @{ $E } rec acc @{ λ${ident x}.$acc } }
+ ${ fold right @{ λ${ident nE}.$H } rec acc @{ λ${ident x}.$acc } }
+}.
+
+interpretation "next" 'Next x y = (Next x y).
+interpretation "end" 'End = End.
+interpretation "sig_gen" 'Sig_gen n E H = (Sig_generic ?? n ??? E H).
+interpretation "sig_gen1" 'Sig_gen n E H = (Sig_generic1 ?? n ??? E H).
+
+(*
+nlemma test0 : ∀S:setoid. ∀P: (setoid1_of_setoid S) ⇒_1 CPROP.∀f,g:S → S.
+ (∀x:S.f x = g x) → (Ex S (λw.P (f w))) =_1 (Ex S (λw.P (g w))).
+#S P f g E; napply (∑w. E w / H ; ┼_1H); nqed.
+
+nlemma test : ∀S:setoid. ∀P: (setoid1_of_setoid S) ⇒_1 CPROP.∀f,g:S → S.
+ (∀x:S.f x = g x) → (Ex S (λw.P (f w)∧ True)) =_1 (Ex S (λw.P (g w)∧ True)).
+#S P f g E; napply (∑w. E w / H ; (┼_1H)╪_1#); nqed.
+
+nlemma test_bound : ∀S:setoid. ∀e,f: (setoid1_of_setoid S) ⇒_1 CPROP. e = f →
+ (Ex S (λw.e w ∧ True)) =_1 (Ex S (λw.f w ∧ True)).
+#S f g E; napply (.=_1 ∑x. E x x # / H ; (H ╪_1 #)); //; nqed.
+
+nlemma test2 : ∀S:setoid. ∀ee: (setoid1_of_setoid S) ⇒_1 (setoid1_of_setoid S) ⇒_1 CPROP.
+ ∀x,y:setoid1_of_setoid S.x =_1 y →
+ (True ∧ (Ex S (λw.ee x w ∧ True))) =_1 (True ∧ (Ex S (λw.ee y w ∧ True))).
+#S m x y E; napply (.=_1 #╪_1(∑w. E / E ; ((E ╪_1 #) ╪_1 #))). //; nqed.
+
+nlemma test3 : ∀S:setoid. ∀ee: (setoid1_of_setoid S) ⇒_1 (setoid1_of_setoid S) ⇒_1 CPROP.
+ ∀x,y:setoid1_of_setoid S.x =_1 y →
+ ((Ex S (λw.ee x w ∧ True) ∨ True)) =_1 ((Ex S (λw.ee y w ∧ True) ∨ True)).
+#S m x y E; napply (.=_1 (∑w. E / E ; ((E ╪_1 #) ╪_1 #)) ╪_1 #). //; nqed.
+*)
+
\ No newline at end of file
(*-----------------------------------------------------------------------*) ⊢
carr X ≡ list T.
+unification hint 0 ≔ SS : setoid;
+ S ≟ carr SS,
+ TT ≟ setoid1_of_setoid (LIST SS)
+(*-----------------------------------------------------------------*) ⊢
+ list S ≡ carr1 TT.
+
unification hint 0 ≔ S:setoid,a,b:list S;
R ≟ eq0 (LIST S),
L ≟ (list S)
(* -------------------------------------------- *) ⊢
eq_list S a b ≡ eq_rel L R a b.
+alias symbol "hint_decl" (instance 1) = "hint_decl_CProp2".
+unification hint 0 ≔ S : setoid, x,y;
+ SS ≟ LIST S,
+ TT ≟ setoid1_of_setoid SS
+(*-----------------------------------------*) ⊢
+ eq_list S x y ≡ eq_rel1 ? (eq1 TT) x y.
+
notation "hvbox(hd break :: tl)"
right associative with precedence 47
for @{'cons $hd $tl}.
| o: re S → re S → re S
| k: re S → re S.
+(* setoid support for re *)
+
nlet rec eq_re (S:Alpha) (a,b : re S) on a : CProp[0] ≝
match a with
[ z ⇒ match b with [ z ⇒ True | _ ⇒ False]
(* -------------------------------------------- *) ⊢
eq_re A a b ≡ eq_rel L R a b.
+nlemma c_is_morph : ∀A:Alpha.(re A) ⇒_0 (re A) ⇒_0 (re A).
+#A; napply (mk_binary_morphism … (λs1,s2:re A. c A s1 s2));
+#a; nelim a;
+##[##1,2: #a' b b'; ncases a'; nnormalize; /2/ by conj;
+##|#x a' b b'; ncases a'; /2/ by conj;
+##|##4,5: #r1 r2 IH1 IH2 a'; ncases a'; nnormalize; /2/ by conj;
+##|#r IH a'; ncases a'; nnormalize; /2/ by conj; ##]
+nqed.
+
+(* XXX This is the good format for hints about morphisms, fix the others *)
+unification hint 0 ≔ S:Alpha, A,B:re S;
+ MM ≟ mk_unary_morphism ??
+ (λA:re S.mk_unary_morphism ?? (λB.c ? A B) (prop1 ?? (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 ≡ c S 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. o A s1 s2));
+#a; nelim a;
+##[##1,2: #a' b b'; ncases a'; nnormalize; /2/ by conj;
+##|#x a' b b'; ncases a'; /2/ by conj;
+##|##4,5: #r1 r2 IH1 IH2 a'; ncases a'; nnormalize; /2/ by conj;
+##|#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.o ? A B) (prop1 ?? (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 ≡ o S A B.
+
+
+(* end setoids support for re *)
+
notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
notation > "a ^ *" non associative with precedence 75 for @{ 'pk $a}.
interpretation "star" 'pk a = (k ? a).
notation "𝐋\sub(\p) term 70 E" non associative with precedence 75 for @{'L_pi $E}.
interpretation "in_pl" 'L_pi E = (L_pi ? E).
-(* The caml, as some patches for it *)
-ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.
-
-alias symbol "hint_decl" (instance 1) = "hint_decl_CProp2".
-unification hint 0 ≔ S : setoid, x,y;
- SS ≟ LIST S,
- TT ≟ setoid1_of_setoid SS
-(*-----------------------------------------*) ⊢
- eq_list S x y ≡ eq_rel1 ? (eq1 TT) x y.
-
-unification hint 0 ≔ SS : setoid;
- S ≟ carr SS,
- TT ≟ setoid1_of_setoid (LIST SS)
-(*-----------------------------------------------------------------*) ⊢
- list S ≡ carr1 TT.
-
-(* not as morphism *)
-nlemma Not_morphism : CProp[0] ⇒_1 CProp[0].
-@(λx:CProp[0].¬ x); #a b; *; #; @; /3/; nqed.
-
-unification hint 0 ≔ P : CProp[0];
- A ≟ CPROP,
- B ≟ CPROP,
- M ≟ mk_unary_morphism1 ?? (λP.¬ P) (prop11 ?? Not_morphism)
-(*------------------------*)⊢
- fun11 A B M P ≡ ¬ P.
-
-(* XXX Ex setoid support *)
-nlemma Ex_morphism : ∀S:setoid.(S ⇒_1 CProp[0]) ⇒_1 CProp[0].
-#S; @(λP: 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 : S ⇒_1 CProp[0];
- A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP,
- B ≟ CPROP,
- M ≟ mk_unary_morphism1 ?? (λP: S ⇒_1 CProp[0].Ex S P)
- (prop11 ?? (Ex_morphism S))
-(*------------------------*)⊢
- fun11 A B M P ≡ Ex S (fun11 S CPROP P).
-
-nlemma Ex_morphism_eta : ∀S:setoid.(S ⇒_1 CProp[0]) ⇒_1 CProp[0].
-#S; @(λP: 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 : S ⇒_1 CProp[0];
- A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP,
- B ≟ CPROP,
- M ≟ mk_unary_morphism1 ?? (λP: S ⇒_1 CProp[0].Ex S (λx.P x))
- (prop11 ?? (Ex_morphism_eta S))
-(*------------------------*)⊢
- fun11 A B M P ≡ Ex S (λx.fun11 S CPROP P x).
-
-nlemma Ex_setoid : ∀S:setoid.(S ⇒_1 CPROP) → setoid.
-#T P; @ (Ex T (λx:T.P x)); @; ##[ #H1 H2; napply True |##*: //; ##] nqed.
-
-unification hint 0 ≔ T,P ;
- S ≟ (Ex_setoid T P)
-(*---------------------------*) ⊢
- Ex T (λx:T.P x) ≡ carr S.
-
-(* couts how many Ex we are traversing *)
-ninductive counter : Type[0] ≝
- | End : counter
- | Next : (bool → bool) → (* dummy arg please the notation mechanism *)
- counter → counter.
-
-(* to rewrite terms (live in setoid) *)
-nlet rec mk_P (S, T : setoid) (n : counter) on n ≝
- match n with [ End ⇒ T → CProp[0] | Next _ m ⇒ S → (mk_P S T m) ].
-
-nlet rec mk_F (S, T : setoid) (n : counter) on n ≝
- match n with [ End ⇒ T | Next _ m ⇒ S → (mk_F S T m) ].
-
-nlet rec mk_E (S, T : setoid) (n : counter) on n : ∀f,g : mk_F S T n. CProp[0] ≝
- match n with
- [ End ⇒ λf,g:T. f = g
- | Next q m ⇒ λf,g: mk_F S T (Next q m). ∀x:S.mk_E S T m (f x) (g x) ].
-
-nlet rec mk_H (S, T : setoid) (n : counter) on n :
-∀P1,P2: mk_P S T n.∀f,g : mk_F S T n. CProp[1] ≝
- match n with
- [ End ⇒ λP1,P2:mk_P S T End.λf,g:T. f = g → P1 f =_1 P2 g
- | Next q m ⇒ λP1,P2: mk_P S T (Next q m).λf,g: mk_F S T (Next q m).
- ∀x:S.mk_H S T m (P1 x) (P2 x) (f x) (g x) ].
-
-nlet rec mk_Ex (S, T : setoid) (n : counter) on n :
-∀P: mk_P S T n.∀f : mk_F S T n. CProp[0] ≝
- match n with
- [ End ⇒ λP:mk_P S T End.λf:T. P f
- | Next q m ⇒ λP: mk_P S T (Next q m).λf: mk_F S T (Next q m).
- ∃x:S.mk_Ex S T m (P x) (f x) ].
-
-nlemma Sig_generic : ∀S,T.∀n:counter.∀P,f,g.
- mk_E S T n f g → mk_H S T n P P f g → mk_Ex S T n P f =_1 mk_Ex S T n P g.
-#S T n; nelim n; nnormalize;
-##[ #P f g E H; /2/;
-##| #q m IH P f g E H; @; *; #x Px; @x; ncases (IH … (E x) (H x)); /3/; ##]
-nqed.
-
-(* to rewrite propositions (live in setoid1) *)
-nlet rec mk_P1 (S : setoid) (T : setoid1) (n : counter) on n ≝
- match n with [ End ⇒ T → CProp[0] | Next _ m ⇒ S → (mk_P1 S T m) ].
-
-nlet rec mk_F1 (S : setoid) (T : setoid1) (n : counter) on n ≝
- match n with [ End ⇒ T | Next _ m ⇒ S → (mk_F1 S T m) ].
-
-nlet rec mk_E1 (S : setoid) (T : setoid1) (n : counter) on n : ∀f,g : mk_F1 S T n. CProp[1] ≝
- match n with
- [ End ⇒ λf,g:T. f =_1 g
- | Next q m ⇒ λf,g: mk_F1 S T (Next q m). ∀x:S.mk_E1 S T m (f x) (g x) ].
-
-nlet rec mk_H1 (S : setoid) (T : setoid1) (n : counter) on n :
-∀P1,P2: mk_P1 S T n.∀f,g : mk_F1 S T n. CProp[1] ≝
- match n with
- [ End ⇒ λP1,P2:mk_P1 S T End.λf,g:T. f = g → P1 f =_1 P2 g
- | Next q m ⇒ λP1,P2: mk_P1 S T (Next q m).λf,g: mk_F1 S T (Next q m).
- ∀x:S.mk_H1 S T m (P1 x) (P2 x) (f x) (g x) ].
-
-nlet rec mk_Ex1 (S : setoid) (T : setoid1) (n : counter) on n :
-∀P: mk_P1 S T n.∀f : mk_F1 S T n. CProp[0] ≝
- match n with
- [ End ⇒ λP:mk_P1 S T End.λf:T. P f
- | Next q m ⇒ λP: mk_P1 S T (Next q m).λf: mk_F1 S T (Next q m).
- ∃x:S.mk_Ex1 S T m (P x) (f x) ].
-
-nlemma Sig_generic1 : ∀S,T.∀n:counter.∀P,f,g.
- mk_E1 S T n f g → mk_H1 S T n P P f g → mk_Ex1 S T n P f =_1 mk_Ex1 S T n P g.
-#S T n; nelim n; nnormalize;
-##[ #P f g E H; /2/;
-##| #q m IH P f g E H; @; *; #x Px; @x; ncases (IH … (E x) (H x)); /3/; ##]
-nqed.
-
-(* notation "∑x1,...,xn. E / H ; P" were:
- - x1...xn are bound in E and P, H is bound in P
- - H is an identifier that will have the type of E in P
- - P is the proof that the two existentially quantified predicates are equal*)
-notation > "∑ list1 ident x sep , . term 56 E / ident nE ; term 19 H" with precedence 20
-for @{ 'Sig_gen
- ${ fold right @{ 'End } rec acc @{ ('Next (λ${ident x}.${ident x}) $acc) } }
- ${ fold right @{ $E } rec acc @{ λ${ident x}.$acc } }
- ${ fold right @{ λ${ident nE}.$H } rec acc @{ λ${ident x}.$acc } }
-}.
-
-interpretation "next" 'Next x y = (Next x y).
-interpretation "end" 'End = End.
-(*interpretation "sig_gen" 'Sig_gen n E H = (Sig_generic ?? n ??? E H).*)
-interpretation "sig_gen1" 'Sig_gen n E H = (Sig_generic1 ?? n ??? E H).
-
-nlemma test0 : ∀S:setoid. ∀P: S ⇒_1 CPROP.∀f,g:S → S.
- (∀x:S.f x = g x) → (Ex S (λw.P (f w))) =_1 (Ex S (λw.P (g w))).
-#S P f g E; napply (∑w. E w / H ; ┼_1H); nqed.
-
-nlemma test : ∀S:setoid. ∀P: S ⇒_1 CPROP.∀f,g:S → S.
- (∀x:S.f x = g x) → (Ex S (λw.P (f w)∧ True)) =_1 (Ex S (λw.P (g w)∧ True)).
-#S P f g E; napply (∑w. E w / H ; (┼_1H)╪_1#); nqed.
-
-nlemma test_bound : ∀S:setoid. ∀e,f: S ⇒_1 CPROP. e = f →
- (Ex S (λw.e w ∧ True)) =_1 (Ex S (λw.f w ∧ True)).
-#S f g E; napply (.=_1 ∑x. E x x # / H ; (H ╪_1 #)); //; nqed.
-
-nlemma test2 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
- ∀x,y:setoid1_of_setoid S.x =_1 y →
- (True ∧ (Ex S (λw.ee x w ∧ True))) =_1 (True ∧ (Ex S (λw.ee y w ∧ True))).
-#S m x y E; napply (.=_1 #╪_1(∑w. E / E ; ((E ╪_1 #) ╪_1 #))). //; nqed.
-
-nlemma test3 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
- ∀x,y:setoid1_of_setoid S.x =_1 y →
- ((Ex S (λw.ee x w ∧ True) ∨ True)) =_1 ((Ex S (λw.ee y w ∧ True) ∨ True)).
-#S m x y E; napply (.=_1 (∑w. E / E ; ((E ╪_1 #) ╪_1 #)) ╪_1 #). //; nqed.
-
-(* Ex setoid support end *)
-
ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
#S r; @(𝐋\p r); #w1 w2 E; nelim r;
##[ ##1,2: /2/;
nlemma mem_single : ∀S:setoid.∀a,b:S. a ∈ {(b)} → a = b.
#S a b; nnormalize; /2/; nqed.
-notation < "[\setoid\emsp\of\emsp term 19 x]" non associative with precedence 90 for @{'mk_setoid $x}.
-interpretation "mk_setoid" 'mk_setoid x = (mk_setoid x ?).
-
nlemma cup_sub: ∀S.∀A,B:𝛀^S.∀x. ¬ (x ∈ A) → A ∪ (B - {(x)}) = (A ∪ B) - {(x)}.
#S A B x H; napply ext_set; #w; @;
##[ *; ##[ #wa; @; ##[@;//] #H2; napply H; napply (. (mem_single ??? H2)^-1╪_1#); //]
nlemma erase_bull : ∀S:Alpha.∀a:pitem S. |\fst (•a)| = |a|.
#S a; nelim a; // by {};
-##[ #e1 e2 IH1 IH2; nchange in ⊢ (???%) with (|e1| · |e2|);
-
-finqui: manca · morfismo, oppure un lemma che dice che == è come Leibnitz.
-
- nrewrite < IH1; nrewrite < IH2;
- nchange in ⊢ (??(??%)?) with (\fst (•e1 ⊙ 〈e2,false〉));
- ncases (•e1); #e3 b; ncases b; nnormalize;
- ##[ ncases (•e2); //; ##| nrewrite > IH2; //]
-##| #e1 e2 IH1 IH2; nchange in ⊢ (???%) with (.|e1| + .|e2|);
- nrewrite < IH2; nrewrite < IH1;
- nchange in ⊢ (??(??%)?) with (\fst (•e1 ⊕ •e2));
+##[ #e1 e2 IH1 IH2;
+ 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]
+ napply (.=_0 #╪_0 (IH2)); //;
+##| #e1 e2 IH1 IH2; napply (?^-1);
+ napply (.=_0 (IH1^-1)╪_0(IH2^-1));
+ nchange in match (•(e1+?)) with (?⊕?);
ncases (•e1); ncases (•e2); //]
-##| #e IH; nchange in ⊢ (???%) with (.|e|^* ); nrewrite < IH;
- nchange in ⊢ (??(??%)?) with (\fst (•e))^*; //; ##]
nqed.
-nlemma eta_lp : ∀S.∀p:pre S.𝐋\p p = 𝐋\p 〈\fst p, \snd p〉.
+nlemma eta_lp : ∀S:Alpha.∀p:pre S. 𝐋\p p = 𝐋\p 〈\fst p, \snd p〉.
#S p; ncases p; //; nqed.
-nlemma epsilon_dot: ∀S.∀p:word S → Prop. {[]} · p = p.
-#S e; napply extP; #w; nnormalize; @; ##[##2: #Hw; @[]; @w; /3/; ##]
-*; #w1; *; #w2; *; *; #defw defw1 Hw2; nrewrite < defw; nrewrite < defw1;
+(* ext_carr non applica *)
+nlemma epsilon_dot: ∀S:Alpha.∀p:Elang S. {[]} · (ext_carr ? p) = p.
+#S e; napply ext_set; #w; @; ##[##2: #Hw; @[]; @w; @; //; @; //; napply #; (* XXX auto *) ##]
+*; #w1; *; #w2; *; *; #defw defw1 Hw2;
+napply (. defw╪_1#);
+napply (. (defw1^-1 ╪_0 #)╪_1#); (* manca @ morfismo *)
napply Hw2; nqed.
+STOP
+
(* theorem 16: 1 → 3 *)
nlemma odot_dot_aux : ∀S.∀e1,e2: pre S.
𝐋\p (•(\fst e2)) = 𝐋\p (\fst e2) ∪ 𝐋 .|\fst e2| →
(* ---------------------------------------- *) ⊢
setoid ≡ force1 ? MR lock.
+notation < "[\setoid\ensp\of term 19 x]" non associative with precedence 90 for @{'mk_setoid $x}.
+interpretation "mk_setoid" 'mk_setoid x = (mk_setoid x ?).
+
interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y).
notation > "hvbox(a break =_0 b)" non associative with precedence 45
nlemma mk_binary_morphism:
∀A,B,C: setoid. ∀f: A → B → C. (∀a,a',b,b'. a=a' → b=b' → f a b = f a' b') →
A ⇒_0 (unary_morph_setoid B C).
- #A; #B; #C; #f; #H; @ [ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph_eq; #y]
+ #A; #B; #C; #f; #H; @; ##[ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph_eq; #y]
/2/.
nqed.
nqed.
unification hint 0 ≔ o1,o2,o3:setoid,f:o2 ⇒_0 o3,g:o1 ⇒_0 o2;
- R ≟ mk_unary_morphism ?? (composition … f g)
+ R ≟ mk_unary_morphism ?? (composition ??? f g)
(prop1 ?? (comp_unary_morphisms o1 o2 o3 f g))
(* -------------------------------------------------------------------- *) ⊢
- fun1 ?? R ≡ (composition … f g).
+ fun1 ?? R ≡ (composition ??? f g).
ndefinition comp_binary_morphisms:
∀o1,o2,o3.(o2 ⇒_0 o3) ⇒_0 ((o1 ⇒_0 o2) ⇒_0 (o1 ⇒_0 o3)).
(* ---------------------------------------- *) ⊢
setoid1 ≡ force2 ? MR lock.
+notation < "[\setoid1\ensp\of term 19 x]" non associative with precedence 90 for @{'mk_setoid1 $x}.
+interpretation "mk_setoid1" 'mk_setoid1 x = (mk_setoid1 x ?).
+
+(* da capire se mettere come coercion *)
ndefinition setoid1_of_setoid: setoid → setoid1.
#s; @ (carr s); @ (eq0…) (refl…) (sym…) (trans…);
nqed.
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type2".
+unification hint 0 ≔ A,x,y
+(*-----------------------------------------------*) ⊢
+ eq_rel ? (eq0 A) x y ≡ eq_rel1 ? (eq1 (setoid1_of_setoid A)) x y.
+(* XXX capire come mai questa hint non funziona se porto su (setoid1_of_setoid A) *)
+
interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y).
interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y).
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 ??? f g)
(prop11 ?? (comp1_unary_morphisms o1 o2 o3 f g)))
(* -------------------------------------------------------------------- *) ⊢
- fun11 ?? R ≡ (composition1 … f g).
+ fun11 ?? R ≡ (composition1 ??? f g).
ndefinition comp1_binary_morphisms:
∀o1,o2,o3. (o2 ⇒_1 o3) ⇒_1 ((o1 ⇒_1 o2) ⇒_1 (o1 ⇒_1 o3)).
ndefinition union ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∨ x ∈ V }.
interpretation "union" 'union U V = (union ? U V).
+ndefinition substract ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∧ ¬ x ∈ V }.
+interpretation "substract" 'minus U V = (substract ? U V).
+
+
ndefinition big_union ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∃i. i ∈ T ∧ x ∈ f i }.
ndefinition big_intersection ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∀i. i ∈ T → x ∈ f i }.
include "sets/setoids1.ma".
+ndefinition singleton ≝ λA:setoid.λa:A.{ x | a = x }.
+interpretation "singl" 'singl a = (singleton ? a).
+
(* this has to be declared here, so that it is combined with carr *)
ncoercion full_set : ∀A:Type[0]. Ω^A ≝ full_set on A: Type[0] to (Ω^?).
#a; #a'; #b; #b'; *; #H1; #H2; *; /5/ by mk_iff, sym1, subseteq_trans;
nqed.
-alias symbol "hint_decl" (instance 1) = "hint_decl_Type2".
-unification hint 0 ≔ A,x,y
-(*-----------------------------------------------*) ⊢
- eq_rel ? (eq0 A) x y ≡ eq_rel1 ? (eq1 (setoid1_of_setoid A)) x y.
-
-(* XXX capire come mai questa hint non funziona se porto su (setoid1_of_setoid A) *)
-
+(* hints for ∩ *)
nlemma intersect_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
#S A B; @ (A ∩ B); #x y Exy; @; *; #H1 H2; @;
##[##1,2: napply (. Exy^-1‡#); nassumption;
(* ------------------------------------------------------*) ⊢
ext_carr AA (R B C) ≡ intersect A BB CC.
+
+(* hints for ∩ *)
nlemma union_is_morph : ∀A. Ω^A ⇒_1 (Ω^A ⇒_1 Ω^A).
#X; napply (mk_binary_morphism1 … (λA,B.A ∪ B));
#A1 A2 B1 B2 EA EB; napply ext_set; #x;
(*------------------------------------------------------*) ⊢
ext_carr AA (R B C) ≡ union A BB CC.
+
+(* hints for - *)
+nlemma substract_is_morph : ∀A. Ω^A ⇒_1 (Ω^A ⇒_1 Ω^A).
+#X; napply (mk_binary_morphism1 … (λA,B.A - B));
+#A1 A2 B1 B2 EA EB; napply ext_set; #x;
+nchange in match (x ∈ (A1 - B1)) with (?∧?);
+napply (.= (set_ext ??? EA x)‡#); @; *; #H H1; @; //; #H2; napply H1;
+##[ napply (. (set_ext ??? EB x)); ##| napply (. (set_ext ??? EB^-1 x)); ##] //;
+nqed.
+
+nlemma substract_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
+ #S A B; @ (A - B); #x y Exy; @; *; #H1 H2; @; ##[##2,4: #H3; napply H2]
+##[##1,4: napply (. Exy╪_1#); // ##|##2,3: napply (. Exy^-1╪_1#); //]
+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 ≔ S:Type[0], A,B:Ω^S;
+ MM ≟ mk_unary_morphism1 ??
+ (λA.mk_unary_morphism1 ?? (λB.A - B) (prop11 ?? (substract_is_morph S A)))
+ (prop11 ?? (substract_is_morph S))
+(*--------------------------------------------------------------------------*) ⊢
+ fun11 ?? (fun11 ?? MM A) B ≡ A - B.
+
+nlemma substract_is_ext_morph:∀A.𝛀^A ⇒_1 𝛀^A ⇒_1 𝛀^A.
+#A; napply (mk_binary_morphism1 … (substract_is_ext …));
+#x1 x2 y1 y2 Ex Ey; napply (prop11 … (substract_is_morph A)); nassumption.
+nqed.
+
+unification hint 1 ≔
+ AA : setoid, B,C : 𝛀^AA;
+ A ≟ carr 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))) ,
+ BB ≟ (ext_carr ? B),
+ CC ≟ (ext_carr ? C)
+(*------------------------------------------------------*) ⊢
+ ext_carr AA (R B C) ≡ substract A BB CC.
+
+(* hints for {x} *)
+nlemma single_is_morph : ∀A:setoid. (setoid1_of_setoid A) ⇒_1 Ω^A.
+#X; @; ##[ napply (λx.{(x)}); ##]
+#a b E; napply ext_set; #x; @; #H; /3/; nqed.
+
+nlemma single_is_ext: ∀A:setoid. A → 𝛀^A.
+#X a; @; ##[ napply ({(a)}); ##] #x y E; @; #H; /3/; nqed.
+
+alias symbol "hint_decl" = "hint_decl_Type1".
+unification hint 0 ≔ A : setoid, a: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;
+ MM ≟ mk_unary_morphism1 ??
+ (λa:setoid1_of_setoid A.{(a)}) (prop11 ?? (single_is_morph A))
+(*--------------------------------------------------------------------------*) ⊢
+ fun11 ?? 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;
+ R ≟ mk_unary_morphism1 ??
+ (λa: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 (R a) ≡ singleton AA a.
+
+
+
+
+
+
(*
alias symbol "hint_decl" = "hint_decl_Type2".
unification hint 0 ≔
projects / helm.git / commitdiff