From e008452eb6b63f53b4eafc13853f7521d411dd00 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 16 Oct 2009 12:36:12 +0000 Subject: [PATCH] ... --- .../matita/nlibrary/logic/destruct_bb.ma | 4 +- .../matita/nlibrary/logic/equality.ma | 2 +- .../matita/nlibrary/sets/partitions.ma | 1 + .../matita/nlibrary/topology/cantor.ma | 233 ++++++++++++++++-- .../software/matita/nlibrary/topology/igft.ma | 67 +++-- .../matita/nlibrary/topology/preamble.xml | 5 +- 6 files changed, 265 insertions(+), 47 deletions(-) diff --git a/helm/software/matita/nlibrary/logic/destruct_bb.ma b/helm/software/matita/nlibrary/logic/destruct_bb.ma index d3d2aadc3..f167be393 100644 --- a/helm/software/matita/nlibrary/logic/destruct_bb.ma +++ b/helm/software/matita/nlibrary/logic/destruct_bb.ma @@ -67,13 +67,13 @@ ndefinition R3 : ∀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); diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma index ac8a2a20c..715423143 100644 --- a/helm/software/matita/nlibrary/logic/equality.ma +++ b/helm/software/matita/nlibrary/logic/equality.ma @@ -25,7 +25,7 @@ nqed. 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). diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index 95145b11b..1bb482f6e 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -21,6 +21,7 @@ include "datatypes/pairs.ma". 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; diff --git a/helm/software/matita/nlibrary/topology/cantor.ma b/helm/software/matita/nlibrary/topology/cantor.ma index 95cf6b3aa..822c88fc0 100644 --- a/helm/software/matita/nlibrary/topology/cantor.ma +++ b/helm/software/matita/nlibrary/topology/cantor.ma @@ -2,45 +2,234 @@ 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 diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index 21194951b..39497ac7b 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -192,9 +192,9 @@ with `C A`. 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 @@ -440,8 +440,8 @@ the premise of infinity. 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. @@ -575,11 +575,11 @@ nlet corec fish_rec (A:Ax) (U: Ω^A) (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 @@ -756,8 +756,8 @@ in the new definition of the axiom set with `n`. 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 @@ -823,6 +823,8 @@ construction that has to be proved extensional 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 }. @@ -851,6 +853,19 @@ ndefinition nAx_of_Ax : Ax → nAx. ##] 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 @@ -912,7 +927,8 @@ of the tutorial works only for the old axiom set. 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. @@ -943,6 +959,13 @@ to provide the witness for the second. 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)). @@ -982,6 +1005,9 @@ We now proceed with the proof of the infinity rule. 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". @@ -990,14 +1016,14 @@ ntheorem new_coverage_infinity: #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 @@ -1015,8 +1041,7 @@ We thus assert (`ncut`) the nicer form of `H` and prove it. 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 @@ -1071,7 +1096,7 @@ nlemma new_coverage_min : *; #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; ##] @@ -1133,7 +1158,8 @@ We assume the dual of the axiom of choice, as in the paper proof. 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 @@ -1206,7 +1232,7 @@ subset of `S`, while `Ω^A` means just a subset (note that the former is bold). 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); @@ -1214,9 +1240,8 @@ nelim 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; ##] @@ -1262,9 +1287,9 @@ in terms of sequent calculus rules annotated with proofs. 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; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼ diff --git a/helm/software/matita/nlibrary/topology/preamble.xml b/helm/software/matita/nlibrary/topology/preamble.xml index 65351001c..3e76da66b 100644 --- a/helm/software/matita/nlibrary/topology/preamble.xml +++ b/helm/software/matita/nlibrary/topology/preamble.xml @@ -39,8 +39,11 @@ date { } body { - margin-right: 1em; + margin-right: 3em; + margin-left: 4em; } + +p { text-align: justify; } -- 2.39.2