title: Weird proof obligations resulting from a push/pop evaluator in Coq
body: <p>I'm trying to define a simple stack-based language in Coq. For now, the instruction set contains <code>push</code> which pushes a <code>nat</code>, and an instruction <code>pop</code> which pops one. The idea is that programs are dependently typed; <code>Prog 2</code> is a program which leaves two elements on the stack after execution.</p>
  
  <p>This is implemented by this simple program:</p>
  
  <pre class="lang-coq prettyprint-override"><code>Require Import Coq.Vectors.VectorDef.
  
  Inductive Prog : nat -&gt; Type :=
    | push : forall n : nat, nat -&gt; Prog n -&gt; Prog (S n)
    | pop  : forall n : nat, Prog (S n) -&gt; Prog n.
  
  Fixpoint eval (n : nat) (p : Prog n) : t nat n :=
    match p with
    | push _ n p =&gt; cons _ n _ (eval _ p)
    | pop _ p =&gt; match eval _ p with
      | cons _ _ _ stack =&gt; stack
      end
    end.
  </code></pre>
  
  <p>I now want to add an instruction <code>pop'</code> which pops an element of the stack but can only be applied when there are at least two elements on the stack.</p>
  
  <pre class="lang-coq prettyprint-override"><code>Inductive Prog : nat -&gt; Type :=
    | push : forall n : nat, nat -&gt; Prog n -&gt; Prog (S n)
    | pop' : forall n : nat, Prog (S (S n)) -&gt; Prog (S n).
  </code></pre>
  
  <p>When using the same <code>Fixpoint</code> as above (changing <code>pop</code> to <code>pop'</code>) I get the error</p>
  
  <blockquote>
    <p>The term "stack" has type "t nat n0" while it is expected to have type "t nat (S k)".</p>
  </blockquote>
  
  <p>So I thought I could do this with <code>Program</code>. So I use:</p>
  
  <pre class="lang-coq prettyprint-override"><code>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 =&gt; cons _ n _ (eval _ p)
    | pop' k p =&gt; match eval _ p with
      | cons _ l _ stack =&gt; stack
      | nil _ =&gt; _
      end
    end.
  </code></pre>
  
  <p>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:</p>
  
  <pre><code>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
  </code></pre>
  
  <p>I don't see a way to link the <code>k</code>, which is the type argument for <code>Prog</code>, and the <code>n0</code>, which is the type argument for the vector type <code>t</code>.</p>
  
  <p>Why does this <code>Program</code> yield this weird obligation, and how can I write the evaluation function circumventing this issue?</p>