Pattern-match on type in order to implement equality for existentially typed constructor in Coq

Link:: https://stackoverflow.com/q/42140009

Display all goals and responses

Question

Let's say I have again a small problem with my datatype with an existential quantified component. This time I want to define when two values of type ext are equal.

Inductive ext (A : Set) :=
| ext_ : forall (X : Set), option X -> ext A.

Fail Definition ext_eq (A : Set) (x y : ext A) : Prop :=
  match x with
  | ext_ _ ox => match y with
                 | ext_ _ oy => (* only when they have the same types *)
                     ox = oy
                 end
  end.The command has indeed failed with message:
The constructor ext_ (in type ext) expects 3 arguments.

What I'd like to do is somehow distinguish between the cases where the existential type is actually same and where it's not. Is this a case for JMeq or is there some other way to accomplish such a case distinction?

I googled a lot, but unfortunately I mostly stumbled upon posts about dependent pattern matching.

I also tried to generate a (boolean) scheme with Scheme Equality for ext, but this wasn't successful because of the type argument.

Answer

What I'd like to do is somehow distinguish between the cases where the existential type is actually same and where it's not.

This is not possible as Coq's logic is compatible with the univalence axiom which says that isomorphic types are equal. So even though (unit * unit) and unit are syntactically distinct, they cannot be distinguished by Coq's logic.

A possible work-around is to have a datatype of codes for the types you are interested in and store that as an existential. Something like this:

Inductive Code : Type :=
| Nat : Code
| List : Code -> Code.

Fixpoint meaning (c : Code) :=
  match c with
  | Nat     => nat
  | List c' => list (meaning c')
  end.

Inductive ext (A : Set) :=
| ext_ : forall (c : Code), option (meaning c) -> ext A.

Lemma Code_eq_dec : forall (c d : Code), {c = d} + {c <> d}.forall c d : Code, {c = d} + {c <> d}
Proof.forall c d : Code, {c = d} + {c <> d}
  intros c.c: Code
forall d : Code, {c = d} + {c <> d} induction c; intros d; destruct d.{Nat = Nat} + {Nat <> Nat}
d: Code
{Nat = List d} + {Nat <> List d}
c: Code
IHc: forall d : Code, {c = d} + {c <> d}
{List c = Nat} + {List c <> Nat}
c: Code
IHc: forall d : Code, {c = d} + {c <> d}
d: Code
{List c = List d} + {List c <> List d}
  -{Nat = Nat} + {Nat <> Nat} left.Nat = Nat reflexivity.
  -d: Code
{Nat = List d} + {Nat <> List d} right.d: Code
Nat <> List d inversion 1.
  -c: Code
IHc: forall d : Code, {c = d} + {c <> d}
{List c = Nat} + {List c <> Nat} right.c: Code
IHc: forall d : Code, {c = d} + {c <> d}
List c <> Nat inversion 1.
  -c: Code
IHc: forall d : Code, {c = d} + {c <> d}
d: Code
{List c = List d} + {List c <> List d} destruct (IHc d).c: Code
IHc: forall d : Code, {c = d} + {c <> d}
d: Code
e: c = d
{List c = List d} + {List c <> List d}
c: Code
IHc: forall d : Code, {c = d} + {c <> d}
d: Code
n: c <> d
{List c = List d} + {List c <> List d}
    +c: Code
IHc: forall d : Code, {c = d} + {c <> d}
d: Code
e: c = d
{List c = List d} + {List c <> List d} left.c: Code
IHc: forall d : Code, {c = d} + {c <> d}
d: Code
e: c = d
List c = List d congruence.
    +c: Code
IHc: forall d : Code, {c = d} + {c <> d}
d: Code
n: c <> d
{List c = List d} + {List c <> List d} right.c: Code
IHc: forall d : Code, {c = d} + {c <> d}
d: Code
n: c <> d
List c <> List d inversion 1.c: Code
IHc: forall d : Code, {c = d} + {c <> d}
d: Code
n: c <> d
H: List c = List d
H1: c = d
False contradiction.
Defined.

Definition ext_eq (A : Set) (x y : ext A) : Prop.A: Set
x, y: ext A
Prop
  refine (match x with
          | @ext_ _ c ox =>
              match y with
              | @ext_ _ d oy =>
                  match Code_eq_dec c d with
                  | left eq   => _
                  | right neq => False
                  end end end).A: Set
x, y: ext A
c: Code
ox: option (meaning c)
d: Code
oy: option (meaning d)
eq: c = d
Prop
  subst.A: Set
x, y: ext A
d: Code
ox, oy: option (meaning d)
Prop exact (ox = oy).
Defined.

However this obviously limits quite a lot the sort of types you can pack in an ext. Other, more powerful, languages (e.g. equipped with Induction-recursion) would give you more expressive power.

A: Nice workaround! Let me add a couple comments: (1) Code_eq_dec can be literally defined using the decide equality tactic, which will really shine when we start adding more data constructors into Code; (2) ext_ can be destructed using the let expression (since it has only one constructor), which makes the code a bit more concise: let (c,ox) := x in ...