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
(*D
+The cover relation
+------------------
+
We can now define the cover relation using the `◃` notation for
the premise of infinity.
D*)
(*D
+
+The fish relation
+-----------------
+
The definition of fish works exactly the same way as for cover, except
that it is defined as a coinductive proposition.
D*)
(*D
+Introction rule for fish
+------------------------
+
Matita is able to generate elimination rules for inductive types,
but not introduction rules for the coinductive case.
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 }.
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).
##]
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
##]
nqed.
+
+(*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