X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft.ma;h=d6043fba2c1d413fc22626fd567e18dbc34c5779;hb=8b33918a53a2c752e2256b328bc0e45f4827beac;hp=d595882bcd1f746c40a40c43e2a5cdb342028fa4;hpb=fded205dcf11e18d06429e645243395d79dd16af;p=helm.git diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index d595882bc..d6043fba2 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -12,7 +12,7 @@ the formalization of the paper by Stefano Berardi and Silvio Valentini. -The tutorial is by Enrico Tassi. +The tutorial and the formalization are by Enrico Tassi. The reader should be familiar with inductively generated formal topologies and have some basic knowledge of type theory and λ-calculus. @@ -115,9 +115,7 @@ of output). The CIC λ-calculus is equipped with a pattern matching construct (match) on inductive types defined in the environment. This construct, together with the possibility to definable total recursive functions, allows to define eliminators (or constructors) -for (co)inductive types. The λ-calculus is also equipped with explicitly typed -local definitions (let in) that in the degenerate case work as casts (i.e. -the type annotation `(t : T)` is implemented as `let x : T ≝ t in x`). +for (co)inductive types. Types are compare up to conversion. Since types may depend on terms, conversion involves β-reduction, δ-reduction (definition unfolding), ζ-reduction (local @@ -137,28 +135,31 @@ universes are declared by the user. The standard library defines > Type[0] < Type[1] < Type[2] +Matita implements a variant of CIC in which constructive and predicative proposition +are distinguished from predicative data types. + For every `Type[i]` there is a corresponding level of predicative propositions `CProp[i]` (the C initial is due to historical reasons, and -stands for constructive, `PProp` would be more appropriate). +stands for constructive). A predicative proposition cannot be eliminated toward `Type[j]` unless it holds no computational content (i.e. it is an inductive proposition with 0 or 1 constructors with propositional arguments, like `Id` and `And` but not like `Or`). 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 +is a peculiarity 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 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 +predicative data types 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., @@ -168,22 +169,13 @@ 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 +in CIC, depending on what our interests are. There is usually a trade-off 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. +- Equality: Id or not ### Axiom of Choice @@ -191,12 +183,12 @@ 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). +different 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 +"asking" the type system to ensure we do no use the Axiom of Choice elsewhere 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. +very beginning, 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 @@ -225,6 +217,31 @@ 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. +### Equality + +What we have to decide here is which models we admit. The paper does not +mention quotiented sets, thus using an intensional equality is enough +to capture the intended content of the paper. Nevertheless, the formalization +cannot be reused in a concrete example where the (families of) sets +that will build the axiom set are quotiented. + +Matita gives support for setoid rewriting under a context built with +non dependent morphisms. As we will detail later, if we assume a generic +equality over the carrier of our axiom set, a non trivial inductive +construction over the ordinals has to be proved to respect extensionality +(i.e. if the input is an extensional set, also the output is). +The proof requires to rewrite under the context formed by the family of sets +`I` and `D`, that have a dependent type. Declaring them as dependently typed +morphisms is possible, but Matita does not provide an adequate support for them, +and would thus need more effort than formalizing the whole paper. + +Anyway, in a preliminary attempt of formalization, we tried the setoid approach, +reaching the end of the formalization, but we had to assume the proof +of the extensionality of the `U_x` construction (while there is no +need to assume the same property for `F_x`!). + +The current version of the formalization uses `Id`. + The standard library and the `include` command ---------------------------------------------- @@ -256,7 +273,7 @@ Some basic results that we will use are also part of the sets library: Defining Axiom set ------------------ -A set of axioms is made of a set(oid) `S`, a family of sets `I` and a +A set of axioms is made of a set `S`, a family of sets `I` and a family `C` of subsets of `S` indexed by elements `a` of `S` and elements of `I(a)`. @@ -284,13 +301,6 @@ the record definition. It is made of a list of pairs: a name, followed by `:` and the its type. It is a dependently typed tuple, thus already defined names (fields) can be used in the types that follow. -Note that `S` is declared to be a `setoid` and not a Type. The original -paper probably also considers I to generate setoids, and both I and C -to be (dependent) morphisms. For the sake of simplicity, we will "cheat" and use -setoids only when strictly needed (i.e. where we want to talk about -equality). Setoids will play a role only when we will define -the alternative version of the axiom set. - Note that the field `S` was declared with `:>` instead of a simple `:`. This declares the `S` projection to be a coercion. A coercion is a "cast" function the system automatically inserts when it is needed. @@ -429,6 +439,10 @@ has to notice that the infinity rule uses, in its hypotheses, the cover relation between two subsets, while the inductive predicate we are going to define relates an element and a subset. + a ∈ U i ∈ I(a) C(a,i) ◃ U + (reflexivity) ⎼⎼⎼⎼⎼⎼⎼⎼⎼ (infinity) ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼ + a ◃ U a ◃ U + An option would be to unfold the definition of cover between subsets, but we prefer to define the abstract notion of cover between subsets (so that we can attach a (ambiguous) notation to it). @@ -461,6 +475,12 @@ but under the assumption that (for every y) `y ◃ U`. In that rule, the left had side of the predicate changes, thus it has to be abstracted (in the arity of the inductive predicate) on the right of `:`. +The intuition Valentini suggests is that we are defining the unary predicate +"being covered by U" (i.e. `_ ◃ U`) and not "being covered" (i.e. `_ ◃ _`). +Unluckily, the syntax of Matita forces us to abstract `U` first, and +we will make it the second argument of the predicate using +the notational support Matita offers. + D*) (** ncheck xcreflexivity. *) (* shows: ∀A:Ax.∀U:Ω^A.∀a:A.a∈U → xcover A U a *) @@ -636,15 +656,19 @@ interpretation "fish" 'fish a U = (fish ? U a). Introduction rule for fish --------------------------- -Matita is able to generate elimination rules for inductive types, -but not introduction rules for the coinductive case. - +Matita is able to generate elimination rules for inductive types D*) (** ncheck cover_rect_CProp0. *) (*D +but not introduction rules for the coinductive case. + + P ⊆ U (∀x,j.x ∈ P → C(x,j) ≬ P) a ∈ P + (fish intro) ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼ + a ⋉ U + We thus have to define the introduction rule for fish by co-recursion. Here we again use the proof mode of Matita to exhibit the body of the corecursive function. @@ -717,7 +741,7 @@ In CIC it is a defined notion, that is an inductive type with just one constructor (one introduction rule) holding the witness and the proof that the witness satisfies a proposition. -> ncheck Ex. +> ncheck Ex. Instead of trying to remember the name of the constructor, that should be used as the argument of `napply`, we can ask the system to find by @@ -887,8 +911,9 @@ form a subset, i.e. to place a single variable `{ here | … }` of type `S`. > Im[d(a,i)] = { y | ∃j:D(a,i). y = d(a,i,j) } -This poses no theoretical problems, since `S` is a setoid and thus equipped -with an equality. +This poses no theoretical problems, since `S` is a Type and thus +equipped with the `Id` equality. If `S` was a setoid, here the equality +would have been the one of the setoid. Unless we define two different images, one for stating that the image is ⊆ of something and another one to define `𝐂`, we end up using always the latter. @@ -896,10 +921,19 @@ Thus the statement `Im[d(a,i)] ⊆ V` unfolds to > ∀x:S. ( ∃j.x = d(a,i,j) ) → x ∈ V -That, up to rewriting with the equation defining `x`, is what we mean. -The technical problem arises later, when `V` will be a complex -construction that has to be proved extensional -(i.e. ∀x,y. x = y → x ∈ V → y ∈ V). +That, up to rewriting with the equation defining `x`, is what we mean. +Since we decided to use `Id` the rewriting always work (the elimination +principle for `Id` is Leibnitz's equality, that is quantified over +the context. + +The problem that arises if we decide to make `S` a setoid is that +`V` has to be extensional w.r.t. the equality of `S` (i.e. the characteristic +functional proposition has to quotient its input with a relation bigger +than the one of `S`. + +> ∀x,y:S. x = y → x ∈ V → y ∈ V + +If `V` is a complex construction, the proof may not be trivial. D*) @@ -933,19 +967,65 @@ ndefinition nAx_of_Ax : Ax → nAx. ##] nqed. +(*D + +We now prove that the two function above form a retraction pair for +the `C` component of the axiom set. To prove that we face a little +problem since CIC is not equipped with η-conversion. This means that +the followin does not hold (where `A` is an axiom set). + +> A = (S A, I A, C A) + +This can be proved only under a pattern mach over `A`, that means +that the resulting computation content of the proof is a program +that computes something only if `A` is a concrete axiom set. + +To state the lemma we have to drop notation, and explicitly +give the axiom set in input to the `C` projection. + +D*) + 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; +#A; #a; #i; @; #b; #H; (** screenshot "retr-1". *) +##[ ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H;(** screenshot "retr-2". *) + nchange in a with S; nwhd in H; (** screenshot "retr-3". *) + ncases H; #x; #E; nrewrite > E; nwhd in x; (** screenshot "retr-4". *) + ncases x; #b; #Hb; nnormalize; nassumption; ##| ncases A in a i b H; #S; #I; #C; #a; #i; #b; #H; @; ##[ @ b; nassumption; ##| nnormalize; @; ##] ##] nqed. +(*D +D[retr-1] +Look for example the type of `a`. The command `nchange in a with A` +would fail because of the missing η-conversion rule. We have thus +to pattern match over `A` and introduce its pieces. + +D[retr-2] +Now the system accepts that the type of `a` is the fist component +of the axiom set, now called `S`. Unfolding definitions in `H` we discover +there is still some work to do. + +D[retr-3] +To use the equation defining `b` we have to eliminate `H`. Unfolding +definitions in `x` tell us there is still something to do. The `nrewrite` +tactic is a shortcut for the elimination principle of the equality. +It accepts an additional argument `<` or `>` to rewrite left-to-right +or right-to-left. + +D[retr-4] +We defined `𝐝` to be the first projection of `x`, thus we have to +eliminate `x` to actually compute `𝐝`. + +The remaining part of the proof it not interesting and poses no +new problems. + +D*) + (*D We then define the inductive type of ordinals, parametrized over an axiom @@ -1039,30 +1119,34 @@ to provide the witness for the second. D*) -nlemma AC_fake : ∀A,a,i,U. +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 + +Note that, if we will decide later to identify ∃ and Σ, `AC` is +trivially provable + +D*) + +nlemma AC_exists_is_sigma : ∀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 -In the proof of infinity, we have to rewrite under the ∈ predicate. -It is clearly possible to show that `U⎽x` is an extensional set: +In case we made `S` a setoid, the following property has to be proved -> a = b → a ∈ U⎽x → b ∈ U⎽x +> nlemma U_x_is_ext: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ U⎽x. Anyway this proof is a non trivial induction over x, that requires `𝐈` and `𝐃` to be -declared as morphisms. This poses no problem, but goes out of the scope of the -tutorial, since dependent morphisms are hard to manipulate, and we thus assume it. +declared as morphisms. D*) -naxiom U_x_is_ext: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ U⎽x. (*D @@ -1084,20 +1168,13 @@ 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". -alias symbol "covers" = "new covers". +alias symbol "covers" (instance 3) = "new covers set". 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". *) *; #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; @; ##] #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". *) @@ -1308,9 +1385,6 @@ The proof that `⋉(F)` is maximal is exactly the dual one of the minimality of `◃(U)`. Thus the main problem is to obtain `G ⊆ F⎽o` before doing the induction over `o`. -Note that `G` is assumed to be of type `𝛀^A`, that means an extensional -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. @@ -1328,37 +1402,15 @@ nelim o; ##] nqed. -(*D -D[n-f-max-1] -Here the situation looks really similar to the one of the dual proof where -we had to apply the assumption `U_x_is_ext`, but here the set is just `G` -not `F_x`. Since we assumed `G` to be extensional we can -exploit the facilities -Matita provides to perform rewriting in the general setting of setoids. - -The `.` notation simply triggers the mechanism, while the given argument has to -mimic the context under which the rewriting has to happen. In that case -we want to rewrite the left hand side of the binary morphism `∈`. -The infix notation -to represent the context of a binary morphism is `‡`. The right hand side -has to be left untouched, and the identity rewriting step is represented with -`#` (actually a reflexivity proof for the subterm identified by the context). - -We want to rewrite the left hand side using `Ed` right-to-left (the default -is left-to-right). We thus write `Ed^-1`, that is a proof that `𝐝 x i d = c`. -The complete command is `napply (. Ed^-1‡#)` that has to be read like: - -> perform some rewritings under a binary morphism, -> on the right do nothing, -> on the left rewrite with Ed right-to-left. - -After the rewriting step the goal is exactly the `cG` assumption. - -D*) +(*D +D[n-f-max-1] +Note that here the right hand side of `∈` is `G` and not `F⎽p` as +in the dual proof. If `S` was declare to be a setoid, to finish this proof +would be enough to assume `G` extensional, and no proof of the +extensionality of `F⎽p` is required. -(*D
Appendix: tactics explanation -----------------------------