How to prove (a * b)%type = (c * d)%type -> a = c /\ b = d?

Using Coq
1

Normally, for similar proofs I would use inversion, e.g.:

Definition test {a b} : S a = S b -> a = b.
Proof.
  intros.
  inversion_clear H.
  reflexivity.
Qed.

But applying inversion to (a * b) = (c * d) does nothing:

Definition prod_equal_fst {a b c d} : ((a * b)%type) = (c * d)%type -> a = c /\ b = d.
Proof.
  intros.
  split.
  - inversion H.

It gives the following subgoal:

1 subgoal
a : Type
b : Type
c : Type
d : Type
H, H1 : (a * b)%type = (c * d)%type
______________________________________(1/1)
a = c

I would expect to get a = c and b = d.

2

That’s not something you can prove.

3

That is unfortunate, I actually could use this equality as part of this proof. Is there a technical reason for not being able to prove this in Coq? In Haskell the proof is quite trivial:

{-# LANGUAGE GADTs #-}

data Equal a b where
  Refl :: Equal a a

prodEqualSpec :: Equal (a, b) (c, d) -> (Equal a c, Equal b d)
prodEqualSpec Refl = (Refl, Refl)
4

At first I thought you meant arithmetic product: there the statement is obviously false, for example we have 2 * 4 = 4 * 2 but not 4 = 2.

In types, the statement is not provable for a similar reason: it would be incompatible with various axioms that are sound/admissible, such as univalence. We could perfectly have a type theory, for example, that satisfies t * unit = t = t * unit for any type t (for the unit type with a single inhabitant), or a * b = b * a.

Functional languages with GADTs, such as Haskell and OCaml, use a much stronger “syntactic” form of equality that gives overly strong equality principles. This is actually a design problem in some instances (it can easily make NewtypeDeriving unsound if we are not careful) see the work on “roles for GADTs”.

5

Ah, I didn’t think about that. I have edited the title to make this clearer.

I don’t understand Homotopy type theory and univalence yet.

This sounds like you’re talking about a different proof system where types that are equal up to isomorphism are actually equal, but for my example isomorphisms are not necessary. The equality in the title of this post is just the injectivity of type constructors, which, just like injectivity of term level constructors, seems very trivial to me.

Maybe a simpler example would be the injectivity of the list type constructor: forall {a b}, list a = list b -> a = b. I really cannot see why this would be inconsistent with any reasonable proof system.

6

The equality in the title of this post is just the injectivity of type constructors, which, just like injectivity of term level constructors, seems very trivial to me.

That is the key assumption that needs to be substantiated. It is not actually obvious that type constructors ought to be injective, and univalence is a prime example of a reasoning principle that it contradicts.

In Haskell and OCaml, the injectivity of type constructors helps type inference, but that is a rather narrow way to look at it. More semantic interpretations of types, where types are not just labels on terms to prevent mistakes, but explicitly describe how terms “behave”, can make injectivity much harder or impossible to justify.

I really cannot see why this would be inconsistent with any reasonable proof system.

Even if it were the case that injectivity of type constructor did not contradict any worthwhile system, there may still be a cost to adding it to a particular system. In Coq, = is not a primitive of the system, it is user-defined, subject to much more fundamental rules. Slapping axioms on top arbitrarily is bound to make it more difficult to ensure the well-behavedness of the system. In that sense, injectivity of type constructors is not actually obvious.

It’s certainly feasible to live without it, although it might take some effort getting accustomed to it.

8

Hi, you can also have a look at this Coq-Club discussion from January 2010:

  • injectivity of type constructors with functor parameters is inconsistent with classical logic in a predicative type theory;
  • injectivity of type constructors with functor parameters is inconsistent with Coq, due to the impredicativity of Prop.

Another example is the contradiction between the injectivity of /\ and propositional extensionality (which is actually a particular case of univalence). By propositional extensionality, True /\ False is equal to False /\ False, but we certainly don’t want True = False.

3 Likes
9

How is /\ injective? Isn’t True /\ False = False and False /\ True = False a counterexample for the injectivity of /\? Two elements from the domain: (True, False) and (False, True), map to the same elements of the codomain False.

10

/\ is not provably injective but, as a type constructor, it would be injective if type constructors were injective. (/\ is the analog to (_ * _)%type on propositions).

11

Now I see my misunderstanding. I was under the impression that type constructors always create their own types that are completely distinct from any existing types (like in Haskell). But now I see that that does not need to be the case in Coq. But couldn’t there still be some special subset of type constructors, or perhaps another definition of syntactical equality, for which we could prove injectivity? (This was based on a typo in coqide; I typed True /\ False = False instead of (True /\ False) = False)

Edit: I have changed my mind again. (True /\ False) = (False /\ False) is not provable in Coq, so /\ is still injective.

12

@jaror , one common trick is to define your own type hierarchy T as a data type; then you can provide an interpretation function ⟦ ⟧ : T → Type by pattern matching which ought to be sound for your desired reasoning over T. Example:

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Inductive T :=
| base
| prod : T -> T -> T.

Implicit Type (t u : T).

Fixpoint I t : Type :=
  match t with
  | base => nat
  | prod t1 t2 => I t1 * I t2
  end.

Lemma prod_I t1 t2 u1 u2 : prod t1 t2 = prod u1 u2 -> t1 = u1 /\ t2 = u2.
Proof. by case. Qed.

So need to keep reasoning over the equality of T.

1 Like
13

No. The fact that you cannot prove it doesn’t mean that you could prove it using some extensions of Coq, that would be a problem them. @herbelin gave you good examples of problematic cases IMO.

14

I think the problem with this approach is that I would have to define a whole new type system inside Coq if I want tuples of richer types than just nat. That is probably not necessary for my use case, but it would be nice if I could just reuse Coq’s types.

You and @herbelin are probably right. I will need some time to read and digest the Coq-Club discussion.

15

After all it depends how much just want to stretch your trusted base; but indeed the particular injectivity condition you want is inconsistent with many other reasoning principles so you should use it with care.

16

For your use case in the other thread, it seems you just need to represent the structure of: (1) function types (2) pair types (3) then any Coq Type can be used as an “opaque” base type.