Weird proof obligations resulting from a push/pop evaluator in Coq

Question

I'm trying to define a simple stack-based language in Coq. For now, the instruction set contains push which pushes a nat, and an instruction pop which pops one. The idea is that programs are dependently typed; Prog 2 is a program which leaves two elements on the stack after execution.

This is implemented by this simple program:

Require Import Coq.Vectors.VectorDef.

Inductive Prog : nat -> Type :=
  | push : forall n : nat, nat -> Prog n -> Prog (S n)
  | pop  : forall n : nat, Prog (S n) -> Prog n.

Fixpoint eval (n : nat) (p : Prog n) : t nat n :=
  match p with
  | push _ n p => cons _ n _ (eval _ p)
  | pop _ p => match eval _ p with
    | cons _ _ _ stack => stack
    end
  end.

I now want to add an instruction pop' which pops an element of the stack but can only be applied when there are at least two elements on the stack.

Inductive Prog : nat -> Type :=
  | push : forall n : nat, nat -> Prog n -> Prog (S n)
  | pop' : forall n : nat, Prog (S (S n)) -> Prog (S n).

When using the same Fixpoint as above (changing pop to pop') I get the error

The term "stack" has type "t nat n0" while it is expected to have type "t nat (S k)".

So I thought I could do this with Program. So I use:

Require Import Coq.Program.Tactics Coq.Logic.JMeq.

Program Fixpoint eval (n : nat) (p : Prog n) : t nat n :=
  match p with
  | push _ n p => cons _ n _ (eval _ p)
  | pop' k p => match eval _ p with
    | cons _ l _ stack => stack
    | nil _ => _
    end
  end.

However, for some reason this generates weird obligations, which I don't think can be solved. The first (of two) obligations left after automatic attempts is:

k : nat
p0 : Prog (S k)
p : Prog (S (S k))
Heq_p : JMeq (pop' k p) p0
l, n0 : nat
stack : t nat n0
h : nat
t : t nat n0
Heq_anonymous0 : JMeq (cons nat l n0 stack) (cons nat h n0 t)
______________________________________(1/1)
n0 = S k

I don't see a way to link the k, which is the type argument for Prog, and the n0, which is the type argument for the vector type t.

Why does this Program yield this weird obligation, and how can I write the evaluation function circumventing this issue?

Answer 1

I couldn't get Program Fixpoint to remember the appropriate equality, but here's a definition using tactics, where we can use remember to create a convoy pattern around an equality proof. The two subproofs in the proof term were generated by abstract; they're both really simple proofs about constructors.

Fixpoint eval (n : nat) (p : Prog n) : t nat n.
  refine (match p with
          | push n' v p' => cons _ v _ (eval _ p')
          | pop' n' p' => _
          end).
  set (x := eval _ p').
  remember (S (S n')).
  destruct x.
  abstract congruence. (* nil case *)
  assert (n0 = S n') by (abstract congruence).
  rewrite H in x.
  exact x.
Defined.

Print eval.
(*
eval =
fix eval (n : nat) (p : Prog n) {struct p} :
t nat n :=
  match p in (Prog n0) return (t nat n0) with
  | push n' v p' => cons nat v n' (eval n' p')
  | pop' n' p' =>
      let x := eval (S (S n')) p' in
      let n0 := S (S n') in
      let Heqn0 : n0 = S (S n') := eq_refl in
      match
        x in (t _ n1)
        return (n1 = S (S n') -> Prog n1 -> t nat (S n'))
      with
      | nil _ =>
          fun (Heqn1 : 0 = S (S n')) (_ : Prog 0) =>
          eval_subproof n' Heqn1
      | cons _ _ n1 x0 =>
          fun (Heqn1 : S n1 = S (S n')) (_ : Prog (S n1)) =>
          let H : n1 = S n' := eval_subproof0 n' n1 Heqn1 in
          let x1 :=
            eq_rec n1 (fun n2 : nat => t nat n2) x0 (S n') H in
          x1
      end Heqn0 p'
  end
     : forall n : nat, Prog n -> t nat n
*)