From 3cb42e0873c101c6c5a8b9967d765b5135882685 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Sep 2009 15:28:24 +0000 Subject: [PATCH] ... --- helm/software/matita/matitaScript.ml | 6 +- .../matita/nlibrary/topology/convert.awk | 85 ++++++- .../matita/nlibrary/topology/grafite.lang | 2 +- .../software/matita/nlibrary/topology/igft.ma | 227 ++++++++++-------- .../matita/nlibrary/topology/preamble.xml | 3 + .../matita/nlibrary/topology/sh_grafite.js | 2 +- 6 files changed, 217 insertions(+), 108 deletions(-) diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index d4ef4c6e0..aaa703348 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -372,7 +372,11 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us let status = script#grafite_status in let _,_,menv,subst,_ = status#obj in let name = Filename.dirname (script#filename) ^ "/" ^ name in - guistuff.mathviewer#screenshot status menv menv subst name; + let sequents = + let selected = Continuationals.Stack.head_goals status#stack in + List.filter (fun x,_ -> List.mem x selected) menv + in + guistuff.mathviewer#screenshot status sequents menv subst name; [status, parsed_text], "", parsed_text_length | TA.NCheck (_,t) -> let status = script#grafite_status in diff --git a/helm/software/matita/nlibrary/topology/convert.awk b/helm/software/matita/nlibrary/topology/convert.awk index 757872324..5f72889f7 100644 --- a/helm/software/matita/nlibrary/topology/convert.awk +++ b/helm/software/matita/nlibrary/topology/convert.awk @@ -1,7 +1,58 @@ +function process(s) { + if(match(s,/^__docfor:(.*)/,data)){ + s=docfor[data[1]]; + } + return s; +} + +function emit(s) { + lines[length(lines)] = s; +} + +function emit_line() { + if (! line_done) emit(indent $0); + line_done = 0; +} + +function emit_docfor(k) { + emit(); + emit("__docfor:" k); + emit(); +} + +function emit_img(key) { + emit(); + emit("![" key "][" key "]"); + emit(); +} + +function done() { line_done = 1; } + +function check_begin_docfor(s){ + if (match(s,/^\(\*D\[([^\]]*)\]/,data)) { + curdocblock = data[1]; + } else if (match(s,/^D\[([^\]]*)\]/,data)) { + curdocblock = data[1]; + } else { + curdocblock = ""; + } +} + +function store_docfor_if_docforblock(s) { + if (!line_done && curdocblock != "") { + docfor[curdocblock] = docfor[curdocblock] "\n" s; + done(); + } +} + BEGIN { do_print = 1; indent = ""; refs["matita"] = "http://matita.cs.unibo.it"; + docfor[0]="" + curdocblock=""; + lines[0]=""; + line_done =0; } # markdown mangling @@ -10,22 +61,46 @@ BEGIN { key = data[1]; refs[key] = key ".png"; $0 = gensub(/\(\*\* *screenshot[^*]*\*\)/,"",$0); + emit_line(); + emit_img(key); + emit_docfor(key); + done(); } # literate programming -/DOCBEGIN/ { - indent = ""; NF = 0; } -/DOCEND/ { - indent = " "; NF = 0; } +/^\(\*D/ { + check_begin_docfor($0); + indent = ""; + done(); + } +/^D\[.*\]/ { + check_begin_docfor($0); + indent = ""; + done(); + } +/^D\*\)/ { + indent = " "; + curdocblock = ""; + emit(); + done(); + } /HIDE/ { do_print = 0; } { - if (do_print == 1) print indent $0; } + if (do_print == 1) { + store_docfor_if_docforblock($0); + emit_line(); + } + } /UNHIDE/ { do_print = 1; } # closing END { + print length(lines) > "/dev/stderr"; + for (i =0; i< length(lines); i++){ + print process(lines[i]); + } for (i in refs) { print "[" i "]: " refs[i]; } diff --git a/helm/software/matita/nlibrary/topology/grafite.lang b/helm/software/matita/nlibrary/topology/grafite.lang index 93fabcc0c..7770cbf57 100644 --- a/helm/software/matita/nlibrary/topology/grafite.lang +++ b/helm/software/matita/nlibrary/topology/grafite.lang @@ -6,7 +6,7 @@ number = string delim "\"" "\"" escape "\\" -keyword = "match|with|naxiom|nlemma|ntheorem|nrecord|for|ninductive|ncoinductive|ndefinition|nlet|rec|corec|notation|interpretation|nqed|include" +keyword = "match|with|in|naxiom|nlemma|ntheorem|nrecord|for|ninductive|ncoinductive|ndefinition|nlet|rec|corec|notation|interpretation|nqed|include" comment delim "(*" "*)" multiline nested diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index 66c7dd3a1..6b2b73f88 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 ======================================================== @@ -22,6 +22,13 @@ statements) readable to the author of the paper. Orientering ----------- + ? : A +apply (f : A -> B): -------------------- + (f ? ) : B + + f: A1 -> ... -> An -> B ?1: A1 ... ?n: An +apply (f : A -> B): ------------------------------------------------ + apply f == f \ldots == f ? ... ? : B TODO @@ -55,7 +62,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 +81,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 +93,7 @@ Defining Axiom set records, projections, types of projections.. -DOCEND*) +D*) nrecord Ax : Type[1] ≝ { S :> setoid; @@ -94,7 +101,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 +137,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 +152,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 +179,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 +204,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 +220,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 +248,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 +272,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 +288,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 +313,19 @@ 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 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 +334,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 +352,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 +366,52 @@ 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*) -(*DOCBEGIN +(*D 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 +431,46 @@ nqed. interpretation "fish set" 'fish A U = (fish_set fish ? U A). interpretation "fish" 'fish a U = (fish ? U a). -(*DOCBEGIN +(*D 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 +478,67 @@ 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*) ndefinition coverage : ∀A:Ax.∀U:Ω^A.Ω^A ≝ λA,U.{ a | a ◃ U }. @@ -657,12 +684,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 +776,8 @@ nelim o; ##] nqed. -(*DOCBEGIN +(*D [1]: http://upsilon.cc/~zack/research/publications/notation.pdf -*) \ No newline at end of file +*) diff --git a/helm/software/matita/nlibrary/topology/preamble.xml b/helm/software/matita/nlibrary/topology/preamble.xml index 3864f2e19..3a1892cd4 100644 --- a/helm/software/matita/nlibrary/topology/preamble.xml +++ b/helm/software/matita/nlibrary/topology/preamble.xml @@ -13,6 +13,9 @@ margin-right: auto; display: block; } + body { + margin-right: 1em; + } diff --git a/helm/software/matita/nlibrary/topology/sh_grafite.js b/helm/software/matita/nlibrary/topology/sh_grafite.js index f327caada..2e6bcdff4 100644 --- a/helm/software/matita/nlibrary/topology/sh_grafite.js +++ b/helm/software/matita/nlibrary/topology/sh_grafite.js @@ -19,7 +19,7 @@ sh_languages['grafite'] = [ 1 ], [ - /\b(?:match|with|naxiom|nlemma|ntheorem|nrecord|for|ninductive|ncoinductive|ndefinition|nlet|rec|corec|notation|interpretation|nqed|include)\b/g, + /\b(?:match|with|in|naxiom|nlemma|ntheorem|nrecord|for|ninductive|ncoinductive|ndefinition|nlet|rec|corec|notation|interpretation|nqed|include)\b/g, 'sh_keyword', -1 ], -- 2.39.2