Applying a Program Definition fails with "unable to unify Prop with [goal]"

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

Display all goals and responses

Question

In Coq, I showed the associativity of append on vectors using:

Require Import Coq.Vectors.VectorDef Coq.micromega.Lia.

Program Definition t_app_assoc v p q r (a : t v p) (b : t v q) (c : t v r) :=
  append (append a b) c = append a (append b c).
Next Obligation.v: Type
p, q, r: nat
a: t v p
b: t v q
c: t v r
p + (q + r) = p + q + r lia. Qed.

I now want to apply this equality in a proof. Below is the easiest goal that I would expect to be provable with t_app_assoc. Of course it can be proven by simpl - this is just an example.

This apply fails:

Goal (append (append (nil nat) (nil _)) (nil _)
      = append (nil _) (append (nil _) (nil _))).append (append (nil nat) (nil nat)) (nil nat) =
append (nil nat) (append (nil nat) (nil nat))
  apply t_app_assoc.Unable to unify "Prop" with
 "append (append (nil nat) (nil nat)) (nil nat) =
  append (nil nat) (append (nil nat) (nil nat))".

How can I apply t_app_assoc? Or is there a better way to define it? I thought I needed a Program Definition, because simply using a Lemma leads to a type error because t v (p + (q + r)) and t v (p + q + r) are not the same to Coq.

Answer

Prologue

I guess what you want to to is to prove that the vector concatenation is associative and then use that fact as a lemma.

But t_app_assoc as you define it has the following type:

t_app_assoc
     : forall (v : Type) (p q r : nat),
       t v p -> t v q -> t v r -> Prop

You basically want to use : instead of := as follows.

From Coq Require Import Vector Arith.
Import VectorNotations.
Import EqNotations.                  (* rew notation, see below *)
Require Import Coq.Program.Equality. (* heterogeneous equality *)

Section Append.

  Variable A : Type.
  Variable p q r : nat.
  Variables (a : t A p) (b : t A q) (c : t A r).

  Fail Lemma t_app_assoc :
    append (append a b) c = append a (append b c).The command has indeed failed with message:
In environment
A : Type
p, q, r : nat
a : t A p
b : t A q
c : t A r
The term "a ++ b ++ c" has type "t A (p + (q + r))"
while it is expected to have type "t A (p + q + r)".

Unfortunately, we cannot even state a lemma like this using the usual homogeneous equality.

The left-hand side has the following type:

  Check append (append a b) c : t A (p + q + r).(a ++ b) ++ c : t A (p + q + r)
     : t A (p + q + r)

whereas the right-hand side is of type

  Check append a (append b c) : t A (p + (q + r)).a ++ b ++ c : t A (p + (q + r))
     : t A (p + (q + r))

Since t A (p + q + r) is not the same as t A (p + (q + r)) we cannot use = to state the above lemma.

Let me describe some ways of working around this issue:

rew notation

  Lemma t_app_assoc_rew :
    append (append a b) c = rew (plus_assoc _ _ _) in
      append a (append b c).A: Type
p, q, r: nat
a: t A p
b: t A q
c: t A r
(a ++ b) ++ c =
rew [t A] Nat.add_assoc p q r in (a ++ b ++ c)
  Admitted.

Here we just use the law of associativity of addition for natural numbers to cast the type of RHS to t A (p + q + r).

To make it work one needs to Import EqNotations. before.

cast function

This is a common problem, so the authors of the Vector library decided to provide a cast function with the following type:

cast
     : VectorDef.t ?A ?m ->
       forall n : nat, ?m = n -> VectorDef.t ?A n
where
?A : [A : Type
      p : nat
      q : nat
      r : nat
      a : t A p
      b : t A q
      c : t A r |- Type]
?m : [A : Type
      p : nat
      q : nat
      r : nat
      a : t A p
      b : t A q
      c : t A r |- nat]

Let me show how one can use it to prove the law of associativity for vectors. But let's prove the following auxiliary lemma first:

  Lemma uncast {X n} {v : Vector.t X n} e :
    cast v e = v.A: Type
p, q, r: nat
a: t A p
b: t A q
c: t A r
X: Type
n: nat
v: t X n
e: n = n
cast v e = v
  Proof.A: Type
p, q, r: nat
a: t A p
b: t A q
c: t A r
X: Type
n: nat
v: t X n
e: n = n
cast v e = v induction v as [|??? IH]; simpl; rewrite ?IH; reflexivity. Qed.

Now we are all set:

  Lemma t_app_assoc_cast :
    append (append a b) c = cast (append a (append b c)) (plus_assoc _ _ _).A: Type
p, q, r: nat
a: t A p
b: t A q
c: t A r
(a ++ b) ++ c =
cast (a ++ b ++ c) (Nat.add_assoc p q r)
  Proof.A: Type
p, q, r: nat
a: t A p
b: t A q
c: t A r
(a ++ b) ++ c =
cast (a ++ b ++ c) (Nat.add_assoc p q r)
    generalize (Nat.add_assoc p q r).A: Type
p, q, r: nat
a: t A p
b: t A q
c: t A r
forall e : p + (q + r) = p + q + r,
(a ++ b) ++ c = cast (a ++ b ++ c) e
    induction a as [|h p' a' IH]; intros e.A: Type
q, r: nat
a: t A 0
b: t A q
c: t A r
e: 0 + (q + r) = 0 + q + r
([] ++ b) ++ c = cast ([] ++ b ++ c) e
A: Type
q, r, p': nat
a: t A (S p')
b: t A q
c: t A r
h: A
a': t A p'
IH: t A p' ->
forall e : p' + (q + r) = p' + q + r,
(a' ++ b) ++ c = cast (a' ++ b ++ c) e
e: S p' + (q + r) = S p' + q + r
((h :: a') ++ b) ++ c = cast ((h :: a') ++ b ++ c) e
    -A: Type
q, r: nat
a: t A 0
b: t A q
c: t A r
e: 0 + (q + r) = 0 + q + r
([] ++ b) ++ c = cast ([] ++ b ++ c) e now rewrite uncast.
    -A: Type
q, r, p': nat
a: t A (S p')
b: t A q
c: t A r
h: A
a': t A p'
IH: t A p' ->
forall e : p' + (q + r) = p' + q + r,
(a' ++ b) ++ c = cast (a' ++ b ++ c) e
e: S p' + (q + r) = S p' + q + r
((h :: a') ++ b) ++ c = cast ((h :: a') ++ b ++ c) e simpl.A: Type
q, r, p': nat
a: t A (S p')
b: t A q
c: t A r
h: A
a': t A p'
IH: t A p' ->
forall e : p' + (q + r) = p' + q + r,
(a' ++ b) ++ c = cast (a' ++ b ++ c) e
e: S p' + (q + r) = S p' + q + r
h :: (a' ++ b) ++ c =
h :: cast (a' ++ b ++ c) (f_equal Init.Nat.pred e) f_equal.A: Type
q, r, p': nat
a: t A (S p')
b: t A q
c: t A r
h: A
a': t A p'
IH: t A p' ->
forall e : p' + (q + r) = p' + q + r,
(a' ++ b) ++ c = cast (a' ++ b ++ c) e
e: S p' + (q + r) = S p' + q + r
(a' ++ b) ++ c =
cast (a' ++ b ++ c) (f_equal Init.Nat.pred e) now apply IH.
  Qed.

Heterogeneous equality (a.k.a. John Major equality)

  Lemma t_app_assoc_jmeq :
    append (append a b) c ~= append a (append b c).A: Type
p, q, r: nat
a: t A p
b: t A q
c: t A r
(a ++ b) ++ c ~= a ++ b ++ c
  Admitted.

End Append.

If you compare the definition of the homogeneous equality

Inductive eq (A : Type) (x : A) : A -> Prop :=
    eq_refl : x = x

Arguments eq {A}%type_scope _ _
Arguments eq_refl {A}%type_scope {x}, [_] _

and the definition of heterogeneous equality

Inductive
JMeq (A : Type) (x : A)
  : forall B : Type, B -> Prop :=  JMeq_refl : x ~= x

Arguments JMeq [A]%type_scope _ [B]%type_scope _
Arguments JMeq_refl {A}%type_scope {x}, [_] _

you will see that with JMeq the LHS and RHS don't have to be of the same type and this is why the statement of t_app_assoc_jmeq looks a bit simpler than the previous ones.

Other approaches to vectors

See e.g. this question and this one; I also find this answer very useful too.