From fded205dcf11e18d06429e645243395d79dd16af Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 17 Oct 2009 07:03:03 +0000 Subject: [PATCH] some more work --- .../matita/nlibrary/topology/cantor.ma | 124 +---- .../nlibrary/topology/igft-minimality-CIC.svg | 507 ++++++++++++++---- .../software/matita/nlibrary/topology/igft.ma | 84 ++- .../matita/nlibrary/topology/preamble.xml | 5 +- 4 files changed, 511 insertions(+), 209 deletions(-) diff --git a/helm/software/matita/nlibrary/topology/cantor.ma b/helm/software/matita/nlibrary/topology/cantor.ma index 822c88fc0..b8f8a5543 100644 --- a/helm/software/matita/nlibrary/topology/cantor.ma +++ b/helm/software/matita/nlibrary/topology/cantor.ma @@ -127,109 +127,31 @@ unification hint 0 ≔ ; 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 ◃ ∅); ##[ - 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 *) -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; - ##] -##] +alias symbol "eq" = "leibnitz's equality". +alias symbol "eq" = "setoid1 eq". +alias symbol "covers" = "covers". +naxiom Ph : ∀x.h x = O \liff x ◃ ∅. + +nlemma replace_char: + ∀A:Ax.∀U,V.U ⊆ V → V ⊆ U → ∀a:A.a ◃ U → a ◃ V. +#A; #U; #V; #a; #H1; #H2; #E; nelim E; +##[ #b; #Hb; @; nauto; +##| #b; #i; #H3; #H4; @2 i; #c; #Hc; 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). - -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); -##] +ntheorem th_ch3: ¬∃a:caxs.∀x.ϕ a x = h x. +*; #a; #H; +ncut (a ◃ { x | x ◃ ∅}); ##[ + napply (replace_char … { x | h x = O }); ##[ ##1,2: #x; ncases (Ph x); + (* nauto; *) #H1; #H2; #H3; nauto; (* ??? *) ##] + napply (replace_char … { x | ϕ a x = O }); ##[##1,2: #x; nrewrite > (H x); + (* nauto; *) #E; napply E; ##] + napply (axiom_cond … a one); ##] #H1; +ncut (a ◃ ∅); ##[ napply (transitivity … H1); #x; nauto; ##] #H2; +nlapply (col2_4 …H2); #H3; +ncut (a ∈ 𝐂 a one); ##[ + nnormalize; ncases (Ph a); nrewrite > (H a); nauto; ##] #H4; +nauto; 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-minimality-CIC.svg b/helm/software/matita/nlibrary/topology/igft-minimality-CIC.svg index 3cf9b46fb..06c2b36ee 100644 --- a/helm/software/matita/nlibrary/topology/igft-minimality-CIC.svg +++ b/helm/software/matita/nlibrary/topology/igft-minimality-CIC.svg @@ -8,8 +8,8 @@ xmlns="http://www.w3.org/2000/svg" xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd" xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape" - width="371.16943" - height="210.00404" + width="496.06299" + height="318.89764" id="svg2" sodipodi:version="0.32" inkscape:version="0.46" @@ -18,6 +18,52 @@ version="1.0"> + + + + + + + + + + + + + inkscape:window-y="26" + inkscape:showpageshadow="true" + units="cm" /> @@ -87,121 +135,394 @@ inkscape:label="Layer 1" inkscape:groupmode="layer" id="layer1" - transform="translate(-100.2483,-683.58839)"> + transform="translate(-52.527322,-573.92589)"> Matita's CICCProp impredicative + CProp,Type predicativeCProp = Type + + + No elim CProp toward Type Matita's CICCProp,Type predicativeNo elim CProp toward Type + + + + + Coq's CIC (work in Prop)Prop impredicativeNo elim Prop toward Type + + + + + + + Coq's CIC (work in CProp)CProp=Type predicativeMartin Löf Axiom of Choice + + + + CIC + EMProp impredicative with EMNo elim Prop toward Type + + + + + + + - + x="440.85757" + y="668.56934" + id="tspan6207">Excluded Middle + + + + + + + + + + EM for CPropAxiom of ChoiceCProp impredicative + x="236.74605" + y="713.91022" + id="tspan8393" /> CProp[i] = Type[i]Where's the content?Exists = Sigma - + x="206.57732" + y="618.78223" + id="tspan8399" /> Reuse theorems inCProp Impredicativea classical setting - + x="221.84404" + y="786.26294" + id="tspan8405" /> Martin LöfGirard's paradoxAxiom of Choice - + x="228.09178" + y="751.88953" + id="tspan8415" /> + style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;marker-start:none;marker-end:url(#Arrow2Lend);stroke-opacity:1" + d="M 359.90647,612.92159 C 359.90647,612.92159 212.45038,602.47727 189.20314,691.03816" + id="path8417" + sodipodi:nodetypes="cc" /> + + + + + Axiom of Choice + ?????????????? diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index 075828b60..d595882bc 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -1,7 +1,7 @@ (*D -Matita Tutorial: inductively generated formal topologies -======================================================== +Inductively generated formal topologies in Matita +================================================= This is a not so short introduction to [Matita][2], based on the formalization of the paper @@ -14,18 +14,21 @@ by Stefano Berardi and Silvio Valentini. The tutorial is by Enrico Tassi. -The tutorial spends a considerable amount of effort in defining +The reader should be familiar with inductively generated +formal topologies and have some basic knowledge of type theory and λ-calculus. + +A considerable part of this tutorial is devoted to explain how to define notations that resemble the ones used in the original paper. We believe -this is a important part of every formalization, not only from the aesthetic +this is an important part of every formalization, not only from the aesthetic point of view, but also from the practical point of view. Being consistent allows to follow the paper in a pedantic way, and hopefully to make the formalization (at least the definitions and proved statements) readable to the author of the paper. -The formalization uses the ng (new generation) version of Matita +The formalization uses the "new generation" version of Matita (that will be named 1.x when finally released). Last stable release of the "old" system is named 0.5.7; the ng system -is coexisting with the old one in every development release +is coexisting with the old one in all development release (named "nightly builds" in the download page of Matita) with a version strictly greater than 0.5.7. @@ -144,29 +147,83 @@ A predicative proposition cannot be eliminated toward with 0 or 1 constructors with propositional arguments, like `Id` and `And` but not like `Or`). -The distintion between predicative propositions and predicative data types +The distinction between predicative propositions and predicative data types is a peculirity of Matita (for example in CIC as implemented by Coq they are the same). The additional restriction of not allowing the elimination of a CProp toward a Type makes the theory of Matita minimal in the following sense: -Theorems proved in this setting can be reused in a classical framwork (forcing -Matita to collapse the hierarchy of constructive propositions). Alternatively, -one can decide to collapse predicative propositions and datatypes recovering the -Axiom of Choice (i.e. ∃ really holds a content and can thus be eliminated to -provide a witness for a Σ). +Theorems proved in CIC as implemented in Matita can be reused in a classical +and impredicative framework (i.e. forcing Matita to collapse the hierarchy of +constructive propositions and assuming the excluded middle on them). +Alternatively, one can decide to collapse predicative propositions and +datatypes recovering the Axiom of Choice in the sense of Martin Löf +(i.e. ∃ really holds a witness and can be eliminated to inhabit a type). + +This implementation of CIC is the result of the collaboration with Maietti M., +Sambin G. and Valentini S. of the University of Padua. Formalization choices --------------------- +There are many different ways of formalizing the same piece of mathematics +in CIC, depending on what our interests are. There is usually a tradeoff +between the possibility of reuse the formalization we did and its complexity. + +In this work, our decisions mainly regarded the following two areas + +- Equality: Id or not +- Axiom of Choice: controlled use or not + +### Equality + +TODO We will avoid using `Id` (Leibniz equality), thus we will explicitly equip a set with an equivalence relation when needed. We will call this structure a _setoid_. Note that we will attach the infix `=` symbol only to the equality of a setoid, not to Id. - +### Axiom of Choice + +In this paper it is clear that the author is interested in using the Axiom +of Choice, thus choosing to identify ∃ and Σ (i.e. working in the +leftmost box of the graph "Coq's CIC (work in CProp)") would be a safe decision +(that is, the author of the paper would not complain we formalized something +diffrent from what he had in mind). + +Anyway, we may benefit from the minimality of CIC as implemented in Matita, +"asking" the type system to ensure we do no use the Axiom of Choice elswhere +in the proof (by mistake or as a shortcut). If we identify ∃ and Σ from the +very beginnig, the system will not complain if we use the Axiom of Choice at all. +Moreover, the elimination of an inductive type (like ∃) is a so common operation +that the syntax chosen for the elimination command is very compact and non +informative, hard to spot for a human being +(in fact it is just two characters long!). + +We decided to formalize the whole paper without identifying +CProp and Type and assuming the Axiom of Choice as a real axiom +(i.e. a black hole with no computational content, a function with no body). + +It is clear that this approach give us full control on when/where we really use +the Axiom of Choice. But, what are we loosing? What happens to the computational +content of the proofs if the Axiom of Choice gives no content back? + +It really +depends on when we actually look at the computational content of the proof and +we "run" that program. We can extract the content and run it before or after +informing the system that our propositions are actually code (i.e. identifying +∃ and Σ). If we run the program before, as soon as the computation reaches the +Axiom of Choice it stops, giving no output. If we tell the system that CProp and +Type are the same, we can exhibit a body for the Axiom of Choice (i.e. a projection) +and the extracted code would compute an output. + +Note that the computational +content is there even if the Axiom of Choice is an axiom, the difference is +just that we cannot use it (the typing rules inhibit the elimination of the +existential). This is possible only thanks to the minimality of CIC as implemented +in Matita. The standard library and the `include` command ---------------------------------------------- @@ -1034,6 +1091,7 @@ alias symbol "covers" = "new covers". alias symbol "covers" = "new covers set". alias symbol "covers" = "new covers". alias symbol "covers" = "new covers set". +alias symbol "covers" = "new covers". ntheorem new_coverage_infinity: ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U. #A; #U; #a; (** screenshot "n-cov-inf-1". *) diff --git a/helm/software/matita/nlibrary/topology/preamble.xml b/helm/software/matita/nlibrary/topology/preamble.xml index 45bc7da38..018c0b445 100644 --- a/helm/software/matita/nlibrary/topology/preamble.xml +++ b/helm/software/matita/nlibrary/topology/preamble.xml @@ -39,10 +39,11 @@ date { } body { - margin-right: 3em; - margin-left: 4em; + margin-right: 3cm; + margin-left: 3cm; } + p { text-align: justify; } -- 2.39.2