∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type[0].
∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ??? a1 ? p0 = x1.
- ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 x0 p0 ? p1 a2 = x2 → Type[0].
+ ∀x2:T2 x0 p0 x1 p1.R2 ???? ? ? p0 ? p1 a2 = x2 → Type[0].
∀b0:T0.
∀e0:a0 = b0.
∀b1: T1 b0 e0.
∀e1:R1 ??? a1 ? e0 = b1.
∀b2: T2 b0 e0 b1 e1.
- ∀e2:R2 ???? T2 b0 e0 ? e1 a2 = b2.
+ ∀e2:R2 ???? ? ? e0 ? e1 a2 = b2.
∀so:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).T3 b0 e0 b1 e1 b2 e2.
#T0;#a0;#T1;#a1;#T2;#a2;#T3;#b0;#e0;#b1;#e1;#b2;#e2;#H;
napply (eq_rect_Type0 ????? e2);
nlemma eq_rect_CProp0_r:
∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A; #a; #x; #p; #x0; #p0; napply eq_rect_CProp0_r'; nassumption.
+ #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
nqed.
interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
alias symbol "eq" = "setoid eq".
alias symbol "eq" = "setoid1 eq".
alias symbol "eq" = "setoid eq".
+alias symbol "eq" = "setoid1 eq".
nrecord partition (A: setoid) : Type[1] ≝
{ support: setoid;
indexes: ext_powerclass support;
include "topology/igft.ma".
+ntheorem axiom_cond: ∀A:Ax.∀a:A.∀i:𝐈 a.a ◃ 𝐂 a i.
+#A; #a; #i; @2 i; #x; #H; @; napply H;
+nqed.
+
+nlemma hint_auto1 : ∀A,U,V. (∀x.x ∈ U → x ◃ V) → cover_set cover A U V.
+nnormalize; nauto.
+nqed.
+
+alias symbol "covers" (instance 1) = "covers".
+alias symbol "covers" (instance 2) = "covers set".
+alias symbol "covers" (instance 3) = "covers".
+ntheorem transitivity: ∀A:Ax.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
+#A; #a; #U; #V; #aU; #UV;
+nelim aU;
+##[ #c; #H; nauto;
+##| #c; #i; #HCU; #H; @2 i; nauto;
+##]
+nqed.
+
+ndefinition emptyset: ∀A.Ω^A ≝ λA.{x | False}.
+
+notation "∅" non associative with precedence 90 for @{ 'empty }.
+interpretation "empty" 'empty = (emptyset ?).
+
+naxiom EM : ∀A:Ax.∀a:A.∀i_star.(a ∈ 𝐂 a i_star) ∨ ¬( a ∈ 𝐂 a i_star).
+
+ntheorem th2_3 :
+ ∀A:Ax.∀a:A. a ◃ ∅ → ∃i. ¬ a ∈ 𝐂 a i.
+#A; #a; #H; nelim H;
+##[ #n; *;
+##| #b; #i_star; #IH1; #IH2;
+ ncases (EM … b i_star);
+ ##[##2: (* nauto; *) #W; @i_star; napply W;
+ ##| nauto;
+ ##]
+##]
+nqed.
+
+ninductive eq1 (A : Type[0]) : Type[0] → CProp[0] ≝
+| refl1 : eq1 A A.
+
+notation "hvbox( a break ∼ b)" non associative with precedence 40
+for @{ 'eqT $a $b }.
+
+interpretation "eq between types" 'eqT a b = (eq1 a b).
+
ninductive unit : Type[0] ≝ one : unit.
-naxiom E: setoid.
-naxiom R: E → Ω^E.
+nrecord uAx : Type[1] ≝ {
+ uax_ : Ax;
+ with_ : ∀a:uax_.𝐈 a ∼ unit
+}.
-ndefinition axs: Ax.
-@ E (λ_.unit) (λa,x.R a);
+ndefinition uax : uAx → Ax.
+#A; @ (uax_ A) (λx.unit); #a; #_; napply (𝐂 a ?); nlapply one; ncases (with_ A a); nauto;
nqed.
+ncoercion uax : ∀u:uAx. Ax ≝ uax on _u : uAx to Ax.
+
+naxiom A: Type[0].
+naxiom S: A → Ω^A.
+
+ndefinition axs: uAx.
+@; ##[ @ A (λ_.unit) (λa,x.S a); ##| #_; @; ##]
+nqed.
+
+alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)".
unification hint 0 ≔ ;
x ≟ axs
(* -------------- *) ⊢
- S x ≡ E.
-
-ndefinition emptyset: Ω^axs ≝ {x | False}.
+ S x ≡ A.
-ndefinition Z: Ω^axs ≝ {x | x ◃ emptyset}.
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers set".
-ntheorem cover_trans: ∀A:Ax.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
-#A; #a; #U; #V; #aU; #UV;
-nelim aU;
-##[ #c; #H; napply (UV … H);
-##| #c; #i; #HCU; #H; napply (cinfinity … i); napply H;
-##]
+ntheorem col2_4 :
+ ∀A:uAx.∀a:A. a ◃ ∅ → ¬ a ∈ 𝐂 a ?. ##[ (* bug *) ##2: nnormalize; napply one; ##]
+#A; #a; #H; nelim H;
+##[ #n; *;
+##| #b; #i_star; #IH1; #IH2; #H3; nlapply (IH2 … H3); #H4; nauto;
+##]
+nqed.
+
+ndefinition Z : Ω^axs ≝ { x | x ◃ ∅ }.
+
+ntheorem cover_monotone: ∀A:Ax.∀a:A.∀U,V.U ⊆ V → a ◃ U → a ◃ V.
+#A; #a; #U; #V; #HUV; #H; nelim H;
+##[ nauto;
+##| #b; #i; #HCU; #W; @2 i; #x; nauto; ##]
+nqed.
+
+ntheorem th3_1: ¬∃a:axs.Z ⊆ S a ∧ S a ⊆ Z.
+*; #a; *; #ZSa; #SaZ;
+ncut (a ◃ Z); ##[
+ nlapply (axiom_cond … a one); #AxCon; nchange in AxCon with (a ◃ S a);
+ (* nauto; *) napply (cover_monotone … AxCon); nassumption; ##] #H;
+ncut (a ◃ ∅); ##[ napply (transitivity … H); #x; #E; napply E; ##] #H1;
+ncut (¬ a ∈ S a); ##[ napply (col2_4 … H1); ##] #H2;
+ncut (a ∈ S a); ##[ napply ZSa; napply H1; ##] #H3;
+nauto;
nqed.
+include "nat/nat.ma".
+
+naxiom phi : nat → nat → nat.
+
+notation > "ϕ" non associative with precedence 90 for @{ 'phi }.
+interpretation "phi" 'phi = phi.
+
+notation < "ϕ a i" non associative with precedence 90 for @{ 'phi2 $a $i}.
+interpretation "phi2" 'phi2 a i = (phi a i).
+notation < "ϕ a" non associative with precedence 90 for @{ 'phi1 $a }.
+interpretation "phi2" 'phi1 a = (phi a).
+
+ndefinition caxs : uAx.
+@; ##[ @ nat (λ_.unit); #a; #_; napply { x | ϕ a x = O } ##| #_; @; ##]
+nqed.
+
+
+alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)".
+unification hint 0 ≔ ;
+ x ≟ caxs
+ (* -------------- *) ⊢
+ S x ≡ nat.
+
+naxiom h : nat → nat.
+
+naxiom Ph : ∀x.h x = O → x ◃ ∅.
+
+ninductive eq2 (A : Type[1]) (a : A) : A → CProp[0] ≝
+| refl2 : eq2 A a a.
+
+interpretation "eq2" 'eq T a b = (eq2 T a b).
+
+ntheorem th_ch3: ¬∃a:caxs.∀x.ϕ a x = h x.
+*; #a; #H;
+ncut ((𝐂 a one) ⊆ { x | x ◃ ∅ }); (* bug *)
+nchange in xx with { x | h x
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
ntheorem cantor: ∀a:axs. ¬ (Z ⊆ R a ∧ R a ⊆ Z).
#a; *; #ZRa; #RaZ;
-ncut (a ◃ R a); ##[ @2; ##[ napply one; ##] #x; #H; @; napply H; ##] #H1;
-ncut (a ◃ emptyset); ##[
+ncut (a ◃ R a); ##[ @2; ##[ napply one; ##] #x; #H; @; napply H; ##] #H1;
+ncut (a ◃ ∅); ##[
napply (cover_trans … H1);
#x; #H; nlapply (RaZ … H); #ABS; napply ABS; ##] #H2;
ncut (a ∈ R a); ##[ napply ZRa; napply H2; ##] #H3;
nelim H2 in H3;
-##[ nauto.
-##| nnormalize; nauto. ##] (* se lo lancio su entrambi fallisce di width *)
+##[ nauto.
+##| nnormalize; nauto. ##] (* se lo lancio su entrambi fallisce di width *)
+nqed.
+
+ninductive deduct (A : nAx) (U : Ω^A) : A → CProp[0] ≝
+| drefl : ∀a.a ∈ U → deduct A U a
+| dcut : ∀a.∀i:𝐈 a. (∀y:𝐃 a i.deduct A U (𝐝 a i y)) → deduct A U a.
+
+notation " a ⊢ b " non associative with precedence 45 for @{ 'deduct $a $b }.
+interpretation "deduct" 'deduct a b = (deduct ? b a).
+
+ntheorem th2_3_1 : ∀A:nAx.∀a:A.∀i:𝐈 a. a ⊢ 𝐈𝐦[𝐝 a i].
+#A; #a; #i;
+ncut (∀y:𝐃 a i.𝐝 a i y ⊢ 𝐈𝐦[𝐝 a i]); ##[ #y; @; @y; @; ##] #H1;
+napply (dcut … i); nassumption;
+nqed.
+
+ntheorem th2_3_2 :
+ ∀A:nAx.∀a:A.∀i:𝐈 a.∀U,V. a ⊢ U → (∀u.u ∈ U → u ⊢ V) → a ⊢ V.
+#A; #a; #i; #U; #V; #aU; #xUxV;
+nelim aU;
+##[ nassumption;
+##| #b; #i; #dU; #dV; @2 i; nassumption;
+##]
nqed.
+ntheorem th2_3 :
+ ∀A:nAx.
+ (∀a:A.∀i_star.(∃y:𝐃 a i_star.𝐝 a i_star y = a) ∨ ¬(∃y:𝐃 a i_star.𝐝 a i_star y = a)) →
+ ∀a:A. a ◃ ∅ → ∃i:𝐈 a. ¬ a \in Z
+#A; #EM; #a; #H; nelim H;
+##[ #n; *;
+##| #b; #i_star; #IH1; #IH2;
+ ncases (EM b i_star);
+ ##[##2: #W; @i_star; napply W;
+ ##| *; #y_star; #E; nlapply (IH2 y_star); nrewrite > E; #OK; napply OK;
+ ##]
+##]
+nqed.
+
+ninductive eq1 (A : Type[0]) : Type[0] → CProp[0] ≝
+| refl1 : eq1 A A.
+
+notation "hvbox( a break ∼ b)" non associative with precedence 40
+for @{ 'eqT $a $b }.
+
+interpretation "eq between types" 'eqT a b = (eq1 a b).
+
+nrecord uAx : Type[1] ≝ {
+ uax_ : Ax;
+ with_ : ∀a:uax_.𝐈 a ∼ unit
+}.
+
+ndefinition uax : uAx → Ax.
+*; #A; #E; @ A (λx.unit); #a; ncases (E a);
+##[ #i; napply (𝐃 a i);
+##| #i; nnormalize; #j; napply (𝐝 a i j);
+##]
+nqed.
+
+ncoercion uax : ∀u:unAx. nAx ≝ uax on _u : unAx to nAx.
+
+
+nlemma cor_2_5 : ∀A:unAx.∀a:A.∀i.a ⊢ ∅ → ¬(a ∈ 𝐈𝐦[𝐝 a i]).
+#A; #a; #i; #H; nelim H in i;
+##[ #w; *;
+##| #a; #i; #IH1; #IH2;
+
+
+
+
\ No newline at end of file
D*)
nrecord Ax : Type[1] ≝ {
- S :> setoid;
+ S :> Type[0];
I : S → Type[0];
- C : ∀a:S. I a → Ω ^ S
+ C : ∀a:S. I a → Ω^S
}.
(*D
D*)
ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝
-| creflexivity : ∀a. a ∈ U → cover ? U a
-| cinfinity : ∀a. ∀i. 𝐂 a i ◃ U → cover ? U a.
+| creflexivity : ∀a. a ∈ U → cover A U a
+| cinfinity : ∀a. ∀i. 𝐂 a i ◃ U → cover A U a.
(** screenshot "cover". *)
napply cover;
nqed.
(P: Ω^A) (H1: P ⊆ U)
(H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P): ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
(** screenshot "def-fish-rec-1". *)
-#a; #p; napply cfish; (** screenshot "def-fish-rec-2". *)
+#a; #a_in_P; napply cfish; (** screenshot "def-fish-rec-2". *)
##[ nchange in H1 with (∀b.b∈P → b∈U); (** screenshot "def-fish-rec-2-1". *)
napply H1; (** screenshot "def-fish-rec-3". *)
nassumption;
-##| #i; ncases (H2 a p i); (** screenshot "def-fish-rec-5". *)
+##| #i; ncases (H2 a a_in_P i); (** screenshot "def-fish-rec-5". *)
#x; *; #xC; #xP; (** screenshot "def-fish-rec-5-1". *)
@; (** screenshot "def-fish-rec-6". *)
##[ napply x
D*)
-nrecord nAx : Type[2] ≝ {
- nS:> setoid;
+nrecord nAx : Type[1] ≝ {
+ nS:> Type[0];
nI: nS → Type[0];
nD: ∀a:nS. nI a → Type[0];
nd: ∀a:nS. ∀i:nI a. nD a i → nS
D*)
+include "logic/equality.ma".
+
ndefinition image ≝ λA:nAx.λa:A.λi. { x | ∃j:𝐃 a i. x = 𝐝 a i j }.
notation > "𝐈𝐦 [𝐝 term 90 a term 90 i]" non associative with precedence 70 for @{ 'Im $a $i }.
##]
nqed.
+nlemma Ax_nAx_equiv :
+ ∀A:Ax. ∀a,i. C (Ax_of_nAx (nAx_of_Ax A)) a i ⊆ C A a i ∧
+ C A a i ⊆ C (Ax_of_nAx (nAx_of_Ax A)) a i.
+#A; #a; #i; @; #b; #H;
+##[ ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H;
+ nwhd in H; ncases H; #x; #E; nrewrite > E;
+ ncases x in E; #b; #Hb; #_; nnormalize; nassumption;
+##| ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H; @;
+ ##[ @ b; nassumption;
+ ##| nnormalize; @; ##]
+##]
+nqed.
+
(*D
We then define the inductive type of ordinals, parametrized over an axiom
D*)
-ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
+ndefinition ord_coverage : ∀A:nAx.∀U:Ω^A.Ω^A ≝
+ λA,U.{ y | ∃x:Ord A. y ∈ famU ? U x }.
ndefinition ord_cover_set ≝ λc:∀A:nAx.Ω^A → Ω^A.λA,C,U.
∀y.y ∈ C → y ∈ c A U.
D*)
+nlemma AC_fake : ∀A,a,i,U.
+ (∀j:𝐃 a i.Σx:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
+#A; #a; #i; #U; #H; @;
+##[ #j; ncases (H j); #x; #_; napply x;
+##| #j; ncases (H j); #x; #Hx; napply Hx; ##]
+nqed.
+
naxiom AC : ∀A,a,i,U.
(∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf.∀j:𝐃 a i.𝐝 a i j ∈ U⎽(f j)).
D*)
+alias symbol "exists" (instance 1) = "exists".
+alias symbol "covers" = "new covers set".
+alias symbol "covers" = "new covers".
alias symbol "covers" = "new covers set".
alias symbol "covers" = "new covers".
alias symbol "covers" = "new covers set".
#A; #U; #a; (** screenshot "n-cov-inf-1". *)
*; #i; #H; nnormalize in H; (** screenshot "n-cov-inf-2". *)
ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[ (** screenshot "n-cov-inf-3". *)
- #z; napply H; @ z; napply #; ##] #H'; (** screenshot "n-cov-inf-4". *)
+ #z; napply H; @ z; @; ##] #H'; (** screenshot "n-cov-inf-4". *)
ncases (AC … H'); #f; #Hf; (** screenshot "n-cov-inf-5". *)
ncut (∀j.𝐝 a i j ∈ U⎽(Λ f));
##[ #j; napply (ord_subset … f … (Hf j));##] #Hf';(** screenshot "n-cov-inf-6". *)
@ (Λ f+1); (** screenshot "n-cov-inf-7". *)
@2; (** screenshot "n-cov-inf-8". *)
@i; #x; *; #d; #Hd; (** screenshot "n-cov-inf-9". *)
-napply (U_x_is_ext … Hd); napply Hf';
+nrewrite > Hd; napply Hf';
nqed.
(*D
D[n-cov-inf-3]
After introducing `z`, `H` can be applied (choosing `𝐝 a i z` as `y`).
What is the left to prove is that `∃j: 𝐃 a j. 𝐝 a i z = 𝐝 a i j`, that
-becomes trivial if `j` is chosen to be `z`. In the command `napply #`,
-the `#` is a standard notation for the reflexivity property of the equality.
+becomes trivial if `j` is chosen to be `z`.
D[n-cov-inf-4]
Under `H'` the axiom of choice `AC` can be eliminated, obtaining the `f` and
*; #o; (** screenshot "n-cov-min-3". *)
ngeneralize in match b; nchange with (U⎽o ⊆ V); (** screenshot "n-cov-min-4". *)
nelim o; (** screenshot "n-cov-min-5". *)
-##[ #b; #bU0; napply HUV; napply bU0;
+##[ napply HUV;
##| #p; #IH; napply subseteq_union_l; ##[ nassumption; ##]
#x; *; #i; #H; napply (Im ? i); napply (subseteq_trans … IH); napply H;
##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
D*)
naxiom AC_dual: ∀A:nAx.∀a:A.∀i,F.
- (∀f:𝐃 a i → Ord A.∃x:𝐃 a i.𝐝 a i x ∈ F⎽(f x)) → ∃j:𝐃 a i.∀x:Ord A.𝐝 a i j ∈ F⎽x.
+ (∀f:𝐃 a i → Ord A.∃x:𝐃 a i.𝐝 a i x ∈ F⎽(f x))
+ → ∃j:𝐃 a i.∀x:Ord A.𝐝 a i j ∈ F⎽x.
(*D
D*)
ntheorem max_new_fished:
- ∀A:nAx.∀G:𝛀^A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
+ ∀A:nAx.∀G:Ω^A.∀F:Ω^A.G ⊆ F → (∀a.a ∈ G → ∀i.𝐈𝐦[𝐝 a i] ≬ G) → G ⊆ ⋉F.
#A; #G; #F; #GF; #H; #b; #HbG; #o;
ngeneralize in match HbG; ngeneralize in match b;
nchange with (G ⊆ F⎽o);
##[ napply GF;
##| #p; #IH; napply (subseteq_intersection_r … IH);
#x; #Hx; #i; ncases (H … Hx i); #c; *; *; #d; #Ed; #cG;
- @d; napply IH; (** screenshot "n-f-max-1". *)
- alias symbol "prop2" = "prop21".
- napply (. Ed^-1‡#); napply cG;
+ @d; napply IH; (** screenshot "n-f-max-1". *)
+ nrewrite < Ed; napply cG;
##| #a; #i; #f; #Hf; nchange with (G ⊆ { y | ∀x. y ∈ F⎽(f x) });
#b; #Hb; #d; napply (Hf d); napply Hb;
##]
The `:` separator has to be read as _is a proof of_, in the spirit
of the Curry-Howard isomorphism.
- Γ ⊢ f : A1 → … → An → B Γ ⊢ ?1 : A1 … ?n : An
+ Γ ⊢ f : A_1 → … → A_n → B Γ ⊢ ?_i : A_i
napply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
- Γ ⊢ (f ?1 … ?n ) : B
+ Γ ⊢ (f ?_1 … ?_n ) : B
Γ ⊢ ? : F → B Γ ⊢ f : F
nlapply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
}
body {
- margin-right: 1em;
+ margin-right: 3em;
+ margin-left: 4em;
}
+
+p { text-align: justify; }
</style>
<script type="text/javascript" src="sh_main.js"></script>
<script type="text/javascript" src="sh_grafite.js"></script>
projects / helm.git / commitdiff