X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft.ma;h=ce02f95df55f5327341d25fa8fc4d4ffcac88bb3;hb=e91e815449698c6f2595958f94cd06c10ba10398;hp=66c7dd3a14e9dd9811d43847bb3aef37d7c0d829;hpb=8d321a03cf328b85fe7c084bb22685673633d2ee;p=helm.git diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index 66c7dd3a1..ce02f95df 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -1,4 +1,4 @@ -(*DOCBEGIN +(*D Matita Tutorial: inductively generated formal topologies ======================================================== @@ -23,6 +23,8 @@ statements) readable to the author of the paper. Orientering ----------- + + TODO buttons, PG-interaction-model, sequent window, script window, ncheck @@ -55,7 +57,7 @@ some notation attached to them: The `include` command tells Matita to load a part of the library, in particular the part that we will use can be loaded as follows: -DOCEND*) +D*) include "sets/sets.ma". @@ -74,7 +76,7 @@ nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ nqed. (*UNHIDE*) -(*DOCBEGIN +(*D Some basic results that we will use are also part of the sets library: @@ -86,7 +88,7 @@ Defining Axiom set records, projections, types of projections.. -DOCEND*) +D*) nrecord Ax : Type[1] ≝ { S :> setoid; @@ -94,7 +96,7 @@ nrecord Ax : Type[1] ≝ { C : ∀a:S. I a → Ω ^ S }. -(*DOCBEGIN +(*D Note that the field `S` was declared with `:>` instead of a simple `:`. This declares the `S` projection to be a coercion. A coercion is @@ -130,12 +132,12 @@ Something that is not still satisfactory, in that the dependent type of `I` and `C` are abstracted over the Axiom set. To obtain the precise type of a term, you can use the `ncheck` command as follows. -DOCEND*) +D*) (* ncheck I. *) (* ncheck C. *) -(*DOCBEGIN +(*D One would like to write `I a` and not `I A a` under a context where `A` is an axiom set and `a` has type `S A` (or thanks to the coercion @@ -145,11 +147,11 @@ infer. Matita performs some sort of type inference, thus writing `I ? a` is enough: since the second argument of `I` is typed by the first one, the first one can be inferred just computing the type of `a`. -DOCEND*) +D*) (* ncheck (∀A:Ax.∀a:A.I ? a). *) -(*DOCBEGIN +(*D This is still not completely satisfactory, since you have always type `?`; to fix this minor issue we have to introduce the notational @@ -172,12 +174,12 @@ keyboard and what is displayed in the sequent window) and the content level is defined with the `notation` command. When followed by `>`, it defines an input (only) notation. -DOCEND*) +D*) notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }. notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }. -(*DOCBEGIN +(*D The forst notation defines the writing `𝐈 a` where `a` is a generic term of precedence 90, the maximum one. This high precedence forces @@ -197,12 +199,12 @@ new content element to which a term `$a` is passed. Content elements have to be interpreted, and possibly multiple, incompatible, interpretations can be defined. -DOCEND*) +D*) interpretation "I" 'I a = (I ? a). interpretation "C" 'C a i = (C ? a i). -(*DOCBEGIN +(*D The `interpretation` command allows to define the mapping between the content level and the terms level. Here we associate the `I` and @@ -213,12 +215,12 @@ Interpretation are bi-directional, thus when displaying a term like `C _ a i`, the system looks for a presentation for the content element `'C a i`. -DOCEND*) +D*) notation < "𝐈 \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }. notation < "𝐂 \sub( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'C $a $i }. -(*DOCBEGIN +(*D For output purposes we can define more complex notations, for example we can put bold parenteses around the arguments of `𝐈` and `𝐂`, decreasing @@ -241,13 +243,13 @@ Anyway, to ease the understaing of the definition of the cover relation between subsets, we first define the inductive predicate unfolding the definition, and we later refine it with. -DOCEND*) +D*) ninductive xcover (A : Ax) (U : Ω^A) : A → CProp[0] ≝ | xcreflexivity : ∀a:A. a ∈ U → xcover A U a | xcinfinity : ∀a:A.∀i:𝐈 a. (∀y.y ∈ 𝐂 a i → xcover A U y) → xcover A U a. -(*DOCBEGIN +(*D We defined the xcover (x will be removed in the final version of the definition) as an inductive predicate. The arity of the inductive @@ -265,11 +267,11 @@ 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 abstrated (in the arity of the inductive predicate) on the right of `:`. -DOCEND*) +D*) (* ncheck xcreflexivity. *) -(*DOCBEGIN +(*D We want now to abstract out `(∀y.y ∈ 𝐂 a i → xcover A U y)` and define a notion `cover_set` to which a notation `𝐂 a i ◃ U` can be attached. @@ -281,14 +283,14 @@ Then it has to be abstracted over the arguments of that cover relation, i.e. the axiom set and the set U, and the subset (in that case `𝐂 a i`) sitting on the left hand side of `◃`. -DOCEND*) +D*) ndefinition cover_set : ∀cover: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0] ≝ λcover. λA, C,U. ∀y.y ∈ C → cover A U y. -(*DOCBEGIN +(*D The `ndefinition` command takes a name, a type and body (of that type). The type can be omitted, and in that case it is inferred by the system. @@ -306,19 +308,22 @@ interpretation `covers set temp`: we will later define another interpretation in which the cover relation is the one we are going to define. -DOCEND*) +D*) notation "hvbox(a break ◃ b)" non associative with precedence 45 for @{ 'covers $a $b }. interpretation "covers set temp" 'covers C U = (cover_set ?? C U). -(*DOCBEGIN +(*D + +The cover relation +------------------ We can now define the cover relation using the `◃` notation for the premise of infinity. -DOCEND*) +D*) ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝ | creflexivity : ∀a. a ∈ U → cover ? U a @@ -327,13 +332,13 @@ ninductive cover (A : Ax) (U : Ω^A) : A → CProp[0] ≝ napply cover; nqed. -(*DOCBEGIN +(*D Note that the system accepts the definition but prompts the user for the relation the `cover_set` notion is abstracted on. -![The system asks for a cover relation][cover] + The orizontal line separates the hypotheses from the conclusion. The `napply cover` command tells the system that the relation @@ -345,12 +350,12 @@ We can now define the interpretation for the cover relation between an element and a subset fist, then between two subsets (but this time we fixed the relation `cover_set` is abstracted on). -DOCEND*) +D*) interpretation "covers" 'covers a U = (cover ? U a). interpretation "covers set" 'covers a U = (cover_set cover ? a U). -(*DOCBEGIN +(*D We will proceed similarly for the fish relation, but before going on it is better to give a short introduction to the proof mode of Matita. @@ -359,55 +364,56 @@ its body interactively. In λ-calculus Matita is based on, CIC, proofs and terms share the same syntax, and it thus possible to use the commands devoted to build proof term to build regular definitions. -DOCEND*) - +D*) ndefinition xcover_set : ∀c: ∀A:Ax.Ω^A → A → CProp[0]. ∀A:Ax.∀C,U:Ω^A. CProp[0]. -(** screenshot "xcover-set-1". *) -(*DOCBEGIN + (** screenshot "xcover-set-1". *) +#cover; #A; #C; #U; (** screenshot "xcover-set-2". *) +napply (∀y:A.y ∈ C → ?); (** screenshot "xcover-set-3". *) +napply cover; (** screenshot "xcover-set-4". *) +##[ napply A; +##| napply U; +##| napply y; +##] +nqed. + +(*D[xcover-set-1] The system asks for a proof of the full statement, in an empty context. -![xcover_set proof step ][xcover-set-1] -The `#` command in the ∀-introduction rule, it gives a name to an + +The `#` command is the ∀-introduction rule, it gives a name to an assumption putting it in the context, and generates a λ-abstraction in the proof term. -DOCEND*) -#cover; #A; #C; #U; (** screenshot "xcover-set-2". *) -(*DOCBEGIN -![xcover_set proof step ][xcover-set-2] + +D[xcover-set-2] We have now to provide a proposition, and we exhibit it. We left a part of it implicit; since the system cannot infer it it will ask it later. Note that the type of `∀y:A.y ∈ C → ?` is a proposition whenever `?` is. -DOCEND*) -napply (∀y:A.y ∈ C → ?); (** screenshot "xcover-set-3". *) -(*DOCBEGIN -![xcover_set proof step ][xcover-set-3] + +D[xcover-set-3] The proposition we want to provide is an application of the cover relation we have abstracted in the context. The command `napply`, if the given term has not the expected type (in that case it is a product versus a proposition) it applies it to as many implicit arguments as necessary (in that case `? ? ?`). -DOCEND*) -napply cover; (** screenshot "xcover-set-4". *) -(*DOCBEGIN -![xcover_set proof step ][xcover-set-4] + +D[xcover-set-4] The system will now ask in turn the three implicit arguments passed to cover. The syntax `##[` allows to start a branching to tackle every sub proof individually, otherwise every command is applied to every subrpoof. The command `##|` switches to the next subproof and `##]` ends the branching. -DOCEND*) -##[ napply A; -##| napply U; -##| napply y; -##] -nqed. +D*) + +(*D + +The fish relation +----------------- -(*DOCBEGIN The definition of fish works exactly the same way as for cover, except that it is defined as a coinductive proposition. -DOCEND*) +D*) ndefinition fish_set ≝ λf:∀A:Ax.Ω^A → A → CProp[0]. λA,U,V. @@ -427,29 +433,49 @@ nqed. interpretation "fish set" 'fish A U = (fish_set fish ? U A). interpretation "fish" 'fish a U = (fish ? U a). -(*DOCBEGIN +(*D + +Introction rule for fish +------------------------ Matita is able to generate elimination rules for inductive types, but not introduction rules for the coinductive case. -DOCEND*) +D*) (* ncheck cover_rect_CProp0. *) -(*DOCBEGIN +(*D We thus have to define the introduction rule for fish by corecursion. Here we again use the proof mode of Matita to exhibit the body of the corecursive function. -DOCEND*) +D*) 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". *) -(*DOCBEGIN -![fish proof step][def-fish-rec-1] + (** screenshot "def-fish-rec-1". *) +#a; #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". *) + #x; *; #xC; #xP; (** screenshot "def-fish-rec-5-1". *) + @; (** screenshot "def-fish-rec-6". *) + ##[ napply x + ##| @; (** screenshot "def-fish-rec-7". *) + ##[ napply xC; + ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *) + nassumption; + ##] + ##] +##] +nqed. + +(*D +D[def-fish-rec-1] Note the first item of the context, it is the corecursive function we are defining. This item allows to perform the recursive call, but we will be allowed to do such call only after having generated a constructor of @@ -457,61 +483,79 @@ the fish coinductive type. We introduce `a` and `p`, and then return the fish constructor `cfish`. Since the constructor accepts two arguments, the system asks for them. -DOCEND*) -#a; #p; napply cfish; (** screenshot "def-fish-rec-2". *) -(*DOCBEGIN -![fish proof step][def-fish-rec-2] + +D[def-fish-rec-2] The first one is a proof that `a ∈ U`. This can be proved using `H1` and `p`. With the `nchange` tactic we change `H1` into an equivalent form (this step can be skipped, since the systeem would be able to unfold the definition of inclusion by itself) -DOCEND*) -##[ nchange in H1 with (∀b.b∈P → b∈U); - (** screenshot "def-fish-rec-2-1". *) napply H1; - (** screenshot "def-fish-rec-3". *) nassumption; -(*DOCBEGIN -![fish proof step][def-fish-rec-2-1] +D[def-fish-rec-2-1] It is now clear that `H1` can be applied. Again `napply` adds two implicit arguments to `H1 ? ?`, obtaining a proof of `? ∈ U` given a proof that `? ∈ P`. Thanks to unification, the system understands that `?` is actually `a`, and it asks a proof that `a ∈ P`. -![fish proof step][def-fish-rec-3] + +D[def-fish-rec-3] The `nassumption` tactic looks for the required proof in the context, and in that cases finds it in the last context position. We move now to the second branch of the proof, corresponding to the second argument of the `cfish` constructor. -![fish proof step][def-fish-rec-4] -DOCEND*) -##| (** screenshot "def-fish-rec-4". *) #i; ncases (H2 a p i); - (** screenshot "def-fish-rec-5". *) #x; *; #xC; #xP; - (** screenshot "def-fish-rec-5-1". *) @; - ##[ (** screenshot "def-fish-rec-6". *) napply x - ##| (** screenshot "def-fish-rec-7". *) - @; ##[ napply xC; - ##| (** screenshot "def-fish-rec-8". *) - napply (fish_rec ? U P); - (** screenshot "def-fish-rec-9". *) - nassumption; - ##] - ##] -##] -nqed. -(*DOCBEGIN + We introduce `i` and then we destruct `H2 a p i`, that being a proof of an overlap predicate, give as an element and a proof that it is both in `𝐂 a i` and `P`. -![fish proof step][def-fish-rec-5] + +D[def-fish-rec-5] We then introduce `x`, break the conjunction (the `*;` command is the equivalent of `ncases` but operates on the first hypothesis that can be introduced. We then introduce the two sides of the conjuction. -![fish proof step][def-fish-rec-5-1] -![fish proof step][def-fish-rec-6] -![fish proof step][def-fish-rec-7] -![fish proof step][def-fish-rec-8] -![fish proof step][def-fish-rec-9] -DOCEND*) + +D[def-fish-rec-5-1] +The goal is now the existence of an a point in `𝐂 a i` fished by `U`. +We thus need to use the introduction rulle for the existential quantifier. +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. + +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 +itself the constructor name and apply it with the `@` tactic. +Note that some inductive predicates, like the disjunction, have multiple +introduction rules, and thus `@` can be followed by a number identifying +the constructor. + +D[def-fish-rec-6] +After choosing `x` as the witness, we have to prove a conjunction, +and we again apply the introduction rule for the inductively defined +predicate `∧`. + +D[def-fish-rec-7] +The left hand side of the conjunction is trivial to prove, since it +is already in the context. The right hand side needs to perform +the co-recursive call. + +D[def-fish-rec-9] +The co-recursive call needs some arguments, but all of them live +in the context. Instead of explicitly mention them, we use the +`nassumption` tactic, that simply tries to apply every context item. + +D*) + +(*D + +Subset of covered/fished points +------------------------------- + +We now have to define the subset of `S` of points covered by `U`. +We also define a prefix notation for it. Remember that the precedence +of the prefix form of a symbol has to be lower than the precedence +of its infix form. + +D*) ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }. @@ -519,6 +563,15 @@ notation "◃U" non associative with precedence 55 for @{ 'coverage $U }. interpretation "coverage cover" 'coverage U = (coverage ? U). +(*D + +Here we define the equation characterizing the cover relation. +In the igft.ma file we proved that `◃U` is the minimum solution for +such equation, the interested reader should be able to reply the proof +with Matita. + +D*) + ndefinition cover_equation : ∀A:Ax.∀U,X:Ω^A.CProp[0] ≝ λA,U,X. ∀a.a ∈ X ↔ (a ∈ U ∨ ∃i:𝐈 a.∀y.y ∈ 𝐂 a i → y ∈ X). @@ -542,6 +595,14 @@ ntheorem coverage_min_cover_equation : ##] nqed. +(*D + +We similarly define the subset of point fished by `F`, the +equation characterizing `⋉F` and prove that fish is +the biggest solution for such equation. + +D*) + notation "⋉F" non associative with precedence 55 for @{ 'fished $F }. @@ -565,8 +626,15 @@ ntheorem fised_max_fish_equation : ∀A,F,G. fish_equation A F G → G ⊆ ⋉F. #b; ncases (H b); #H1; #_; #bG; ncases (H1 bG); #E1; #E2; nassumption; nqed. +(*D + +Part 2, the new set of axioms +----------------------------- + +D*) + nrecord nAx : Type[2] ≝ { - nS:> setoid; (*Type[0];*) + nS:> setoid; nI: nS → Type[0]; nD: ∀a:nS. nI a → Type[0]; nd: ∀a:nS. ∀i:nI a. nD a i → nS @@ -657,12 +725,12 @@ naxiom AC : ∀A,a,i,U.(∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf. naxiom setoidification : ∀A:nAx.∀a,b:A.∀U.a=b → b ∈ U → a ∈ U. -(*DOCBEGIN +(*D Bla Bla, -DOCEND*) +D*) alias symbol "covers" = "new covers". alias symbol "covers" = "new covers set". @@ -749,8 +817,60 @@ nelim o; ##] nqed. -(*DOCBEGIN + +(*D +Appendix: natural deduction like tactics explanation +----------------------------------------------------- + +In this appendix we try to give a description of tactics +in terms of natural deduction 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 + napply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼ + (f ?1 … ?n ) : B + +foo + + [x : T] + ⋮ + ? : P(x) + #x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼ + λx:T.? : ∀x:T.P(x) + +baz + + (?1 args1) : P(k1 args1) … (?n argsn) : P(kn argsn) + ncases x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼ + match x with k1 args1 ⇒ ?1 | … | kn argsn ⇒ ?n : P(x) + +bar + + [ IH : P(t) ] + ⋮ + x : T ?1 : P(k1) … ?n : P(kn t) + nelim x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼ + (T_rect_CProp0 ?1 … ?n) : P(x) + +Where `T_rect_CProp0` is the induction principle for the +inductive type `T`. + + ? : Q Q ≡ P + nchange with Q; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼ + ? : P + +Where the equivalence relation between types `≡` keeps into account +β-reduction, δ-reduction (definition unfolding), ζ-reduction (local +definition unfolding), ι-reduction (pattern matching simplification), +μ-reduction (recursive function computation) and ν-reduction (co-fixpoint +computation). + +D*) + + +(*D [1]: http://upsilon.cc/~zack/research/publications/notation.pdf -*) \ No newline at end of file +*)