CODEWITHSUNDEEP
coq
Sven Williamson
Sven Williamson

Reputation: 1124

Proving equality between instances of dependent types

When attempting to formalize the class which corresponds to an algebraic structure (for example the class of all monoids), a natural design is to create a type monoid (a:Type) as a product type which models all the required fields (an element e:a, an operator app : a -> a -> a, proofs that the monoid laws are satisfied etc.). In doing so, we are creating a map monoid: Type -> Type. A possible drawback of this approach is that given a monoid m:monoid a (a monoid with support type a) and m':monoid b (a monoid wih support type b), we cannot even write the equality m = m' (let alone prove it) because it is ill-typed. An alternative design would be to create a type monoid where the support type is just another field a:Type, so that given m m':monoid, it is always meaningful to ask whether m = m'. Somehow, one would like to argue that if m and m' have the same supports (a m = a m) and the operators are equals (app m = app m', which may be achieved thanks to some extensional equality axiom), and that the proof fields do not matter (because we have some proof irrelevance axiom) etc. , then m = m'. Unfortunately, we can't event express the equality app m = app m' because it is ill-typed...

To simplify the problem, suppose we have:

Inductive myType : Type :=
| make : forall (a:Type), a -> myType.
.

I would like to have results of the form:

forall (a b:Type) (x:a) (y:b), a = b -> x = y -> make a x = make b y.

This statement is ill-typed so we can't have it.

I may have axioms allowing me to prove that two types a and b are same, and I may be able to show that x and y are indeed the same too, but I want to have a tool allowing me to conclude that make a x = make b y. Any suggestion is welcome.

Upvotes: 2

Views: 578

Answers (1)

Vilhelm Sjöberg
Vilhelm Sjöberg

Reputation: 503

A low-tech way to prove this is to insert a manual type-cast, using the provided equality. That is, instead of having an assumption x = y, you have an assumption (CAST q x) = y. Below I explicitly write the cast as a match, but you could also make it look nicer by defining a function to do it.

Inductive myType : Type :=
| make : forall (a:Type), a -> myType.

Lemma ex : forall (a b:Type) (x:a) (y:b) (q: a = b), (match q in _ = T return T with eq_refl => x end) = y -> make a x = make b y.
Proof.
  destruct q.
  intros q.
  congruence.
Qed.

There is a nicer way to hide most of this machinery by using "heterogenous equality", also known as JMeq. I recommend the Equality chapter of CPDT for a detailed introduction. Your example becomes

Require Import  Coq.Logic.JMeq.

Infix "==" := JMeq (at level 70, no associativity).

Inductive myType : Type :=
| make : forall (a:Type), a -> myType.

Lemma ex : forall (a b:Type) (x:a) (y:b), a = b -> x == y -> make a x = make b y.
Proof.
  intros.
  rewrite H0.
  reflexivity.
Qed.

In general, although this particular theorem can be proved without axioms, if you do the formalization in this style you are likely to encounter goals that can not be proven in Coq without axioms about equality. In particular, injectivity for this kind of dependent records is not provable. The JMEq library will automatically use an axiom JMeq_eq about heterogeneous equality, which makes it quite convenient.

Upvotes: 4

Related Questions