Defining different types of equality as inductive types in Coq
I am trying to define different types of equality in Coq. During my university course, my professor gave us four different types of rules, as shown below (I only provide links to the rules):
- Gentzen: https://ibb.co/imQOCF
- Leibniz: https://ibb.co/n0uBzv
- Martin-Lof: https://ibb.co/fALZKv
- Path induction: https://ibb.co/esZuKv
The difference between these four types depends on the type C.
I am trying to prove isomorphism among them. Unfortunately, I have some problems when declaring the inductive types of the first and the second, because I cannot find a way to specify the type of C. I have a definition for the third and the fourth, and I have already proved the isomorphism between them.
Thanks in advance.
source to share
You cannot use inductive types to get something that exactly the first two principles without getting the other two. The reason for this is that inductive Coq datatypes automatically support heavy dependent exception, which means that it is allowed for the result type to reference the excluded member. This is what you see in the last two sets of rules you specified: a type is C
allowed to refer to proof p
that two dots a
and b
are equal. Any reasonable inductively defined type of equality automatically supports rules 3 and 4, and therefore rules 1 and 2, which are weaker. For example, here's how you get 1 and 2 with Coq standard equality.
Section Gentzen.
Variables (A : Type) (C : A -> A -> Type).
Definition e_id_g {a b : A} (p : a = b) (c : C a a) : C a b :=
match p with eq_refl => fun c => c end c.
Definition c_id_g (a : A) (c : C a a) : e_id_g (eq_refl a) c = c :=
eq_refl.
End Gentzen.
Section Leibniz.
Variables (A : Type) (C : A -> A -> Type).
Definition e_id_l {a b : A} (p : a = b) (c : forall x, C x x) : C a b :=
match p with eq_refl => c a end.
Definition c_id_l (a : A) (c : forall x, C x x) :
e_id_l (eq_refl a) c = c a :=
eq_refl.
End Leibniz.
Another definition can be given, which only supports rules 1 and 2, but not 3 and 4, using the church equality coding:
Definition eq {A} (a b : A) : Prop :=
forall P : A -> Prop, P a -> P b.
Definition refl {A} (a : A) : eq a a :=
fun P x => x.
The idea here - as with similar encodings for data types in the lambda calculus - is to define a type as the type of its (independent) rectifier or collapse. This definition is sometimes referred to as Leibniz's equality and does provide essentially the same proof rules as in 1 and 2, as shown in the following script.
Section Gentzen.
Variables (A : Type) (C : A -> A -> Prop).
Definition e_id_g {a b : A} (p : eq a b) (c : C a a) : C a b :=
p (C a) c.
Definition c_id_g (a : A) (c : C a a) : e_id_g (refl a) c = c :=
eq_refl.
End Gentzen.
Section Leibniz.
Variables (A : Type) (C : A -> A -> Prop).
Definition e_id_l {a b : A} (p : eq a b) (c : forall x, C x x) : C a b :=
p (C a) (c a).
Definition c_id_l (a : A) (c : forall x, C x x) :
e_id_l (refl a) c = c a :=
eq_refl.
End Leibniz.
(These principles are actually slightly different: they are limited Prop
, due to limitations in the basic theory of Coq related to something called impredicativity. But this is an orthogonal problem.)
Without the assertion of additional axioms, it is impossible to obtain principles 3 and 4 for this new equality coding. Proving this would require analyzing the case on type elements forall P, P a -> P b
and asserting that all these elements have a form refl
applied to something. However, this is a type of function, and there is no possibility for case analysis in the main theory of Cock. Note that this argument lies outside of Cock's theory: do not contradict the assertion as an additional axiom that 3 and 4 are valid for this new type; it simply cannot be proved without these axioms.
source to share