Inequality between Types

Using Coq
1

Say that I want to relate “types” generated by Ott to Coq types:

Inductive typ : Set := typ_nat | typ_bool.

Definition type_of_typ (t : typ) : Type :=
  match t with
  | typ_nat  => nat
  | typ_bool => bool
  end.

Goal forall (t : typ),
     type_of_typ t = nat ->
     t = typ_nat.
  intros t H; destruct t; auto; simpl in H.
  Fail discriminate H.

The command has indeed failed with message:
Error: Ltac call to “discriminate (destruction_arg)” failed.
Not a discriminable equality.

My questions are:

  1. Is this goal provable?
  2. What kinds of equalities are discriminable?
2

Proof (for bool <> unit, but you get the idea) https://gist.github.com/Lysxia/ae6cd8e64e9e7c9b03a8088b26e3f270

The two types do not have the same cardinality, whereas the equality assumption provides a bijection between them.

1 Like
3

Here is the documentation for the discriminate tactic: user manual.

The values bool and nat do not belong to the same inductive type, thus this tactic cannot show that there are different. As Li-yao suggested, a common method to prove this kind of dis-equality is to resort to a cardinality argument: on one hand you can show that there are only two boolean values; on the other hand, you can exhibit at least three different natural numbers.

4

My intuition is that Coq is compatible with univalence, which means to prove an inequality between types you must disprove the existence of an isomorphism between the types. Since Coq is also compatible with types-as-sets, the only way to disprove the isomorphism is to show that the types have different cardinality. So in fact cardinality is the only way to do this sort of thing.

On the other hand, I generally never have to do this in a serious development - if you find yourself doing so, maybe ask where that goal came from!

4 Likes
5

@Lys One point of defining typ is that you can pattern match (and discriminate, etc.) on typ, but not on Type: typ and type_of_typ are called a universe construction (tho it’s a pretty small one), and elements of typ are called codes for types. The point of using universe constructions is the following. If at some point you have as hypothesis something like type_of_typ t = nat, then you should change your definitions/proof steps so that you have t = typ_nat instead.

In this case your lemma holds, but if you add enough constructors to typ, it could fail. For instance, you could add a unit type and sum types — so that in typ you’d have a “code” for the type unit + unit. Then,
you’d lose the property that forall (t : typ), type_of_typ t = bool -> t = typ_bool.
Don’t want sum types? Add a type of strings instead! Since there are countably many strings, the lemma you gave on typ_nat would fail instead.

3 Likes
6

It is true that Coq is compatible with univalence (modulo bugs), and thus that the only types you can prove to be distinct are types which are provably not isomorphic. However, you don’t have to go through cardinalities to do this (though in fact any provably non-isomorphic types in Coq will have distinct cardinalities, I think). Consider nat and nat -> bool. Standard diagonalization will prove that there is no isomorphism, without introducing any notion of cardinality.

7

I’m trying to evaluate typed expressions:

Inductive exp : Set := …
Inductive typing : exp -> typ -> Prop := …

Inductive typed_exp : Set -> Set :=
  Typed : forall (t : typ) (e : exp),
    typing e t ->
    typed_exp (coq_type_of_typ t).

Inductive evalE : Type -> Type :=
  Eval : typed_exp bool -> evalE bool.

From the discussions, maybe I should change it to:

Inductive typed_exp : typ -> Set :=
  Typed : forall (t : typ) (e : exp),
    typing e t ->
    typed_exp t.

Inductive evalE : Type -> Type :=
  Eval : typed_exp typ_bool -> evalE bool.
1 Like
8

Yes, this is what I meant.

9

Without knowing much about the rest of your development, that seems to me like a reasonable change to make.

1 Like