The tutorial spends a considerable amount of effort in defining
notations that resemble the ones used in the original paper. We believe
-this a important part of every formalization, not only for the aesthetic
+this is a important part of every formalization, not only from the aesthetic
point of view, but also from the practical point of view. Being
consistent allows to follow the paper in a pedantic way, and hopefully
to make the formalization (at least the definitions and proved
CIC (as implemented in Matita) in a nutshell
--------------------------------------------
-...
+CIC is a full and functional Pure Type System (all products do exist,
+and their sort is is determined by the target) with an impedicative sort
+Prop and a predicative sort Type. The environment can be populated with
+well typed definitions or theorems, (co)inductive types validating positivity
+conditions and recursive functions provably total by simple syntactical
+analysis (recursive call on structurally smaller subterms). Co-recursive
+functions can be defined as well, and must satisfy a dual condition, that is
+performing the recursive call only after having generated a constructor (a piece
+of output).
+
+The λ-calculus is equipped with a pattern matching construct (match) on inductive
+types defined in the environment that combined with the definable total
+structural recursive functions allows to define eliminators (or constructors)
+for (co)inductive types. The λ-calculus is also equipped with explicitly types
+local definitions (let in) that in the degenerate case work as casts (i.e.
+the type annotation `(t : T)` is implemented as `let x : T ≝ t in x`).
+
+Types are compare up to conversion. Since types may depend on terms, conversion
+involves β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
+definition unfolding), ι-reduction (pattern matching simplification),
+μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
+computation).
-Type is a set equipped with the Id equality (i.e. an intensional,
+Since we are going to formalize constructive and predicative mathematics
+in an intensional type theory like CIC, we try to establish some terminology.
+Type is the sort of sets equipped with the Id equality (i.e. an intensional,
not quotiented set). We will avoid using Leibnitz equality Id,
thus we will explicitly equip a set with an equality when needed.
We will call this structure `setoid`. Note that we will
-attach the infix = symbols only to the equality of a setoid,
+attach the infix = symbol only to the equality of a setoid,
not to Id.
-...
-
We write Type[i] to mention a Type in the predicative hierarchy
of types. To ease the comprehension we will use Type[0] for sets,
and Type[1] for classes.
For every Type[i] there is a corresponding level of predicative
propositions CProp[i].
-CIC is also equipped with an impredicative sort Prop that we will not
-use in this tutorial.
The standard library and the `include` command
----------------------------------------------
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". *)
+ (** 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". *)
+ napply H1; (** screenshot "def-fish-rec-3". *)
nassumption;
-##| #i; ncases (H2 a p i); (** screenshot "def-fish-rec-5". *)
+##| #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". *)
+ @; (** screenshot "def-fish-rec-6". *)
##[ napply x
- ##| @; (** screenshot "def-fish-rec-7". *)
+ ##| @; (** screenshot "def-fish-rec-7". *)
##[ napply xC;
- ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *)
+ ##| napply (fish_rec ? U P); (** screenshot "def-fish-rec-9". *)
nassumption;
##]
##]
ntheorem coverage_cover_equation : ∀A,U. cover_equation A U (◃U).
#A; #U; #a; @; #H;
-##[ nelim H; #b; (* manca clear *)
+##[ nelim H; #b;
##[ #bU; @1; nassumption;
##| #i; #CaiU; #IH; @2; @ i; #c; #cCbi; ncases (IH ? cCbi);
##[ #E; @; napply E;
> Im[d(a,i)] = { d(a,i,j) | j : D(a,i) }
-but this cannot be ..... MAIL
+but this not so formal notation poses some problems. The image is
+often used as the left hand side of the ⊆ predicate
> Im[d(a,i)] ⊆ V
-Allora ha una comoda interpretazione (che voi usate liberamente)
+Of course this writing is interpreted by the authors as follows
> ∀j:D(a,i). d(a,i,j) ∈ V
-Ma se voglio usare Im per definire C, che è un subset di S, devo per
-forza (almeno credo) definire un subset, ovvero dire che
+If we need to use the image to define 𝐂 (a subset of S) we are obliged to
+form a subset, i.e. to place a single variable `{ here | … }`.
+
+> Im[d(a,i)] = { y | ∃j:D(a,i). y = d(a,i,j) }
-> Im[d(a,i)] = { y : S | ∃j:D(a,i). y = d(a,i,j) }
+This poses no theoretical problems, since `S` is a setoid and thus equipped
+with an equality.
-Non ci sono problemi di sostanza, per voi S è un set, quindi ha la sua
-uguaglianza..., ma quando mi chiedo se l'immagine è contenuta si
-scatenano i setoidi. Ovvero Im[d(a,i)] ⊆ V diventa il seguente
+Unless we difene two different images, one for stating the image is ⊆ of
+something and another one to define 𝐂, we end up using always the latter.
+Thus the statement `Im[d(a,i)] ⊆ V` unfolds to
> ∀x:S. ( ∃j.x = d(a,i,j) ) → x ∈ V
+That up to rewriting with the equation defining `x` is what we mean. The
+technical problem arises when `V` is a complex construction that has to
+be proved extensional (i.e. ∀x,y. x = y → x ∈ V → y ∈ V).
D*)
(*D
-
+Thanks to our definition of image, we ca trivially a function mapping a
+new axiom set to an old one and viceversa. Note that in the second
+definition, when defining 𝐝, the projection of the Σ type is inlined
+(constructed on the fly by `*;`) while in the paper it was named `fst`.
D*)
(*D
+The dfinition of `U_x` is by recursion over the ordinal `x`.
+We thus define a recursive function. The `on x` directive tells
+the system on which argument the function is (structurally) recursive.
+
+In the `oS` case we use a local definition to name the recursive call
+since it is used twice.
+
Note that Matita does not support notation in the left hand side
of a pattern match, and thus the names of the constructors have to
be spelled out verbatim.
-BLA let rec. Bla let_in.
-
D*)
nlet rec famU (A : nAx) (U : Ω^A) (x : Ord A) on x : Ω^A ≝
match x with
[ oO ⇒ U
- | oS y ⇒ let Un ≝ famU A U y in Un ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ Un}
+ | oS y ⇒ let U_n ≝ famU A U y in U_n ∪ { x | ∃i.𝐈𝐦[𝐝 x i] ⊆ U_n}
| oL a i f ⇒ { x | ∃j.x ∈ famU A U (f j) } ].
notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
D*)
-nlemma ord_subset:
- ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i.U⎽(f j) ⊆ U⎽(Λ f).
+nlemma ord_subset: ∀A:nAx.∀a:A.∀i,f,U.∀j:𝐃 a i. U⎽(f j) ⊆ U⎽(Λ f).
#A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
nqed.
In the proof of infinity, we have to rewrite under the ∈ predicate.
It is clearly possible to show that U_x is an extensional set:
-> a=b → a ∈ U_x → b ∈ U_x
+> a = b → a ∈ U_x → b ∈ U_x
Anyway this proof in non trivial induction over x, that requires 𝐈 and 𝐃 to be
declared as morphisms. This poses to problem, but goes out of the scope of the
D*)
-naxiom setoidification :
- ∀A:nAx.∀a,b:A.∀x.∀U.a=b → b ∈ U⎽x → a ∈ U⎽x.
+naxiom setoidification: ∀A:nAx.∀a,b:A.∀x.∀U. a = b → b ∈ U⎽x → a ∈ U⎽x.
(*D
as a witness, then ◃(U) reduces to U by definition, hence the conclusion.
D*)
-ntheorem new_coverage_reflexive:
- ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
+ntheorem new_coverage_reflexive: ∀A:nAx.∀U:Ω^A.∀a. a ∈ U → a ◃ U.
#A; #U; #a; #H; @ (0); napply H;
nqed.
alias symbol "covers" = "new covers".
alias symbol "covers" = "new covers set".
alias symbol "covers" = "new covers".
+alias symbol "covers" = "new covers set".
ntheorem new_coverage_infinity:
∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U.
#A; #U; #a; (** screenshot "n-cov-inf-1". *)
(*D
The next proof is that ◃(U) is mininal. The hardest part of the proof
-it to prepare the goal for the induction. The desiderata is to prove
+is to prepare the goal for the induction. The desiderata is to prove
`U⎽o ⊆ V` by induction on `o`, but the conclusion of the lemma is,
unfolding all definitions:
(*D
-bla bla
+The notion `F_x` is again defined by recursion over the ordinal `x`.
D*)
nlet rec famF (A: nAx) (F : Ω^A) (x : Ord A) on x : Ω^A ≝
match x with
[ oO ⇒ F
- | oS o ⇒ let Fo ≝ famF A F o in Fo ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ Fo }
+ | oS o ⇒ let F_o ≝ famF A F o in F_o ∩ { x | ∀i:𝐈 x.∃j:𝐃 x i.𝐝 x i j ∈ F_o }
| oL a i f ⇒ { x | ∀j:𝐃 a i.x ∈ famF A F (f j) }
].
(*D
The proof of compatibility uses this little result, that we
-factored out.
+proved outside the mail proof.
D*)
-nlemma co_ord_subset:
- ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
+nlemma co_ord_subset: ∀A:nAx.∀F:Ω^A.∀a,i.∀f:𝐃 a i → Ord A.∀j. F⎽(Λ f) ⊆ F⎽(f j).
#A; #F; #a; #i; #f; #j; #x; #H; napply H;
nqed.
We assume the dual of the axiom of choice, as in the paper proof.
D*)
-naxiom AC_dual :
- ∀A:nAx.∀a:A.∀i,F. (∀f:𝐃 a i → Ord A.∃x:𝐃 a i.𝐝 a i x ∈ F⎽(f x)) → ∃j:𝐃 a i.∀x:Ord A.𝐝 a i j ∈ F⎽x.
+naxiom AC_dual: ∀A:nAx.∀a:A.∀i,F.
+ (∀f:𝐃 a i → Ord A.∃x:𝐃 a i.𝐝 a i x ∈ F⎽(f x)) → ∃j:𝐃 a i.∀x:Ord A.𝐝 a i j ∈ F⎽x.
(*D
-Proving the anti-reflexivity property is simce, since the
+Proving the anti-reflexivity property is simple, since the
assumption `a ⋉ F` states that for every ordinal `x` (and thus also 0)
`a ∈ F⎽x`. If `x` is choosen to be `0`, we obtain the thesis.
D*)
-ntheorem new_fish_antirefl:
- ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
+ntheorem new_fish_antirefl: ∀A:nAx.∀F:Ω^A.∀a. a ⋉ F → a ∈ F.
#A; #F; #a; #H; nlapply (H 0); #aFo; napply aFo;
nqed.
projects / helm.git / blobdiff