X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft.ma;h=ce02f95df55f5327341d25fa8fc4d4ffcac88bb3;hb=f1c4852a4359cf278ed00d73d608856ff46bafbb;hp=a4ac5d46914340de617c304a9b3d40937c53113a;hpb=590b41b39d52ae1e320bf1c01220b06fadb1ba8d;p=helm.git diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index a4ac5d469..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,54 +433,129 @@ 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". *) -#a; #p; napply cfish; -##[ (** screenshot "def-fish-rec-2". *) napply H1; - (** screenshot "def-fish-rec-3". *) napply p; -##| (** screenshot "def-fish-rec-4". *) #i; ncases (H2 a p i); - (** screenshot "def-fish-rec-5". *) #x; *; #xC; #xP; - (** screenshot "def-fish-rec-5". *) @; - ##[ (** screenshot "def-fish-rec-6". *) napply x - ##| (** screenshot "def-fish-rec-7". *) - @; ##[ napply xC; - ##| (** screenshot "def-fish-rec-8". *) - napply (fish_rec ? U P); - nassumption; - ##] + (** 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. -(*DOCBEGIN -![fish proof step][def-fish-rec-1] -![fish proof step][def-fish-rec-2] -![fish proof step][def-fish-rec-3] -![fish proof step][def-fish-rec-4] -![fish proof step][def-fish-rec-5] -![fish proof step][def-fish-rec-6] -![fish proof step][def-fish-rec-7] -![fish proof step][def-fish-rec-8] -DOCEND*) +(*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 +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. + +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) + +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`. + +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. + +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`. + +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. + +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 }. @@ -482,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). @@ -505,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 }. @@ -528,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 @@ -620,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". @@ -712,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 +*)