-(*DOCBEGIN
+(*D
Matita Tutorial: inductively generated formal topologies
========================================================
Orientering
-----------
+
+
TODO
buttons, PG-interaction-model, sequent window, script window, ncheck
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".
nqed.
(*UNHIDE*)
-(*DOCBEGIN
+(*D
Some basic results that we will use are also part of the sets library:
records, projections, types of projections..
-DOCEND*)
+D*)
nrecord Ax : Type[1] ≝ {
S :> setoid;
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
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
`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
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
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
`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
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
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.
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.
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
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
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.
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.
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 }.
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).
##]
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 }.
#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
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".
##]
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
+*)
projects / helm.git / blobdiff