title: Coq can't find subterm when using rewrite tactic
body: <p>I'm trying to do a modified proof of <code>compile_correct</code> from the <a href="http://adam.chlipala.net/cpdt/html/StackMachine.html" rel="noreferrer">first chapter</a> of Certified Programming with Dependent Types.  In my version, I try to make use of the fact that <code>progDenote</code> is a fold, and use a weaker inductive hypothesis in the proof of the main lemma in priving <code>compile_correct</code>.</p>
  
  <p>The code that is identical with the book is:</p>
  
  <pre><code>Require Import Bool Arith List.
  Set Implicit Arguments.
  
  Inductive binop : Set := Plus | Times.
  
  Inductive exp : Set :=
    | Const : nat -&gt; exp
    | Binop : binop -&gt; exp -&gt; exp -&gt; exp.
  
  Definition binopDenote (b : binop) : nat -&gt; nat -&gt; nat :=
    match b with
      | Plus =&gt; plus
      | Times =&gt; mult
    end.
  
  Fixpoint expDenote (e : exp) : nat :=
    match e with
      | Const n =&gt; n
      | Binop b e1 e2 =&gt; (binopDenote b) (expDenote e1) (expDenote e2)
    end.
  
  Inductive instr : Set :=
    | iConst : nat -&gt; instr
    | iBinop : binop -&gt; instr.
  
  Definition prog := list instr.
  Definition stack := list nat.
  
  Definition instrDenote (i : instr) (s : stack) : option stack :=
    match i with
      | iConst n =&gt; Some (n :: s)
      | iBinop b =&gt;
        match s with
          | arg1 :: arg2 :: s' =&gt; Some ((binopDenote b) arg1 arg2 :: s')
          | _ =&gt; None
        end
    end.
  
  Fixpoint compile (e : exp) : prog :=
    match e with
      | Const n =&gt; iConst n :: nil
      | Binop b e1 e2 =&gt; compile e2 ++ compile e1 ++ iBinop b :: nil
    end.
  </code></pre>
  
  <p>Then I define my own version of <code>prog_denote</code> which is a fold over the list of instructions in a program:</p>
  
  <pre><code>Definition bind {A B : Type} (a : option A) (f : A -&gt; option B) : option B :=
    match a with
      | Some x =&gt; f x
      | None =&gt; None
    end.
  
  Definition instrDenote' (s : option stack) (i : instr) : option stack :=
    bind s (instrDenote i).
  
  Definition progDenote (p : prog) (s : stack) : option stack :=
    fold_left instrDenote' p (Some s).
  </code></pre>
  
  <p>I then try to prove a weaker version of <code>compile_correct</code> from the book:</p>
  
  <pre><code>Lemma compile_correct' : forall e s,
    progDenote (compile e) s = Some (expDenote e :: s).
  induction e.
  intro s.
  unfold compile.
  unfold expDenote.
  unfold progDenote at 1.
  simpl.
  reflexivity.
  intro s.
  unfold compile.
  fold compile.
  unfold expDenote.
  fold expDenote.
  unfold progDenote.
  rewrite fold_left_app.
  rewrite fold_left_app.
  unfold progDenote in IHe2.
  rewrite (IHe2 s).
  unfold progDenote in IHe1.
  rewrite (IHe1 (expDenote e2 :: s)).
  </code></pre>
  
  <p>My proof breaks at the last line, with the proof state</p>
  
  <pre><code>1 subgoal
  b : binop
  e1 : exp
  e2 : exp
  IHe1 : forall s : stack,
         fold_left instrDenote' (compile e1) (Some s) =
         Some (expDenote e1 :: s)
  IHe2 : forall s : stack,
         fold_left instrDenote' (compile e2) (Some s) =
         Some (expDenote e2 :: s)
  s : stack
  ______________________________________(1/1)
  fold_left instrDenote' (iBinop b :: nil)
    (fold_left instrDenote' (compile e1) (Some (expDenote e2 :: s))) =
  Some (binopDenote b (expDenote e1) (expDenote e2) :: s)
  </code></pre>
  
  <p>And the error is</p>
  
  <pre><code>Error:
  Found no subterm matching "fold_left instrDenote' (compile e1)
                               (Some (expDenote e2 :: s))" in the current goal.
  </code></pre>
  
  <p>At this stage in the proof, I am doing induction on <code>e</code>, the expression being compiled, and dealing with the <code>Binop</code> constructor of <code>exp</code>.  I don't understand why I am getting this error, because once I apply <code>IHe1</code> to <code>expDenote e2 :: s</code> there are no bound variables.  This seems to be the usual problem with applying rewrite rules doesn't work.  I also checked that the term I'm trying to create:</p>
  
  <pre><code>fold_left instrDenote' (iBinop b :: nil)
    (Some (expDenote e1 :: expDenote e2 :: s)) =
  Some (binopDenote b (expDenote e1) (expDenote e2) :: s)
  </code></pre>
  
  <p>type checks.</p>
  
  <p>What else can go wrong with a rewrite rule, when the subexpression it's complaining about is clearly there in the goal?</p>
  
  <p>EDIT: As suggested, I changed the display settings in coqide to the equivalent of Set Printing All.  This revealed the problem to be that the definition of <code>stack</code> had been unfolded to <code>list nat</code> at one place in the goal, which prevented the subterm from being recognized.  The goal printed with the new settings was</p>
  
  <pre><code>1 subgoal
  b : binop
  e1 : exp
  e2 : exp
  IHe1 : forall s : stack,
         @eq (option stack)
           (@fold_left (option stack) instr instrDenote' (compile e1)
              (@Some stack s)) (@Some (list nat) (@cons nat (expDenote e1) s))
  IHe2 : forall s : stack,
         @eq (option stack)
           (@fold_left (option stack) instr instrDenote' (compile e2)
              (@Some stack s)) (@Some (list nat) (@cons nat (expDenote e2) s))
  s : stack
  ______________________________________(1/1)
  @eq (option stack)
    (@fold_left (option stack) instr instrDenote'
       (@cons instr (iBinop b) (@nil instr))
       (@fold_left (option stack) instr instrDenote' (compile e1)
          (@Some (list nat) (@cons nat (expDenote e2) s))))
    (@Some (list nat)
       (@cons nat (binopDenote b (expDenote e1) (expDenote e2)) s))
  </code></pre>
  
  <p>And the error was</p>
  
  <pre><code>Error:
  Found no subterm matching "@fold_left (option stack) instr instrDenote'
                               (compile e1)
                               (@Some stack (@cons nat (expDenote e2) s))" in the current goal.
  </code></pre>