Coq can't find subterm when using rewrite tactic

Question

I'm trying to do a modified proof of compile_correct from the first chapter of Certified Programming with Dependent Types. In my version, I try to make use of the fact that progDenote is a fold, and use a weaker inductive hypothesis in the proof of the main lemma in priving compile_correct.

The code that is identical with the book is:

Require Import Bool Arith List.
Set Implicit Arguments.

Inductive binop : Set := Plus | Times.

Inductive exp : Set :=
  | Const : nat -> exp
  | Binop : binop -> exp -> exp -> exp.

Definition binopDenote (b : binop) : nat -> nat -> nat :=
  match b with
    | Plus => plus
    | Times => mult
  end.

Fixpoint expDenote (e : exp) : nat :=
  match e with
    | Const n => n
    | Binop b e1 e2 => (binopDenote b) (expDenote e1) (expDenote e2)
  end.

Inductive instr : Set :=
  | iConst : nat -> instr
  | iBinop : binop -> instr.

Definition prog := list instr.
Definition stack := list nat.

Definition instrDenote (i : instr) (s : stack) : option stack :=
  match i with
    | iConst n => Some (n :: s)
    | iBinop b =>
      match s with
        | arg1 :: arg2 :: s' => Some ((binopDenote b) arg1 arg2 :: s')
        | _ => None
      end
  end.

Fixpoint compile (e : exp) : prog :=
  match e with
    | Const n => iConst n :: nil
    | Binop b e1 e2 => compile e2 ++ compile e1 ++ iBinop b :: nil
  end.

Then I define my own version of prog_denote which is a fold over the list of instructions in a program:

Definition bind {A B : Type} (a : option A) (f : A -> option B) : option B :=
  match a with
    | Some x => f x
    | None => 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).

I then try to prove a weaker version of compile_correct from the book:

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)).

My proof breaks at the last line, with the proof state

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)

And the error is

Error:
Found no subterm matching "fold_left instrDenote' (compile e1)
                             (Some (expDenote e2 :: s))" in the current goal.

At this stage in the proof, I am doing induction on e, the expression being compiled, and dealing with the Binop constructor of exp. I don't understand why I am getting this error, because once I apply IHe1 to expDenote e2 :: s 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:

fold_left instrDenote' (iBinop b :: nil)
  (Some (expDenote e1 :: expDenote e2 :: s)) =
Some (binopDenote b (expDenote e1) (expDenote e2) :: s)

type checks.

What else can go wrong with a rewrite rule, when the subexpression it's complaining about is clearly there in the goal?

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 stack had been unfolded to list nat at one place in the goal, which prevented the subterm from being recognized. The goal printed with the new settings was

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))

And the error was

Error:
Found no subterm matching "@fold_left (option stack) instr instrDenote'
                             (compile e1)
                             (@Some stack (@cons nat (expDenote e2) s))" in the current goal.

Could you add what gets printed if you enable Set Printing All.? (Just add this line before your proof). — Arthur Azevedo De Amorim
Done, thanks for the suggestion. Now I see that the expressions are different, as stack appears as list nat in the goal. I don't know enough about Coq to understand why the definition of stack has been expanded like this in the goal (and why it's still displayed as stack with default Printing settings). — Kester Tong
Now that I see what happened, fold stack fixes the issue. From what I've read, the unfold tactic is not completely obvious for a beginner in how deep it unfolds an expression, so that combined with the default display settings seems to be the cause of the problem. — Kester Tong

Kester Tong Kester Tong · Accepted Answer · 2015-06-06T01:49:33

Even though with default display settings, the subterm seems to appear in the goal, with Set Printing All enabled, it becomes clear that the subterm does not match the goal because in the goal, stack has been unfolded to list nat. So fold stack is needed to turn list nat back into stack in the goal.

It seems like as a beginner I was tripped up by the combination of the following:

The unfold tactic unfolds more definitions than a beginner would expect.
The default display settings (in CoqIDE in my case) can hide this because they fold some terms.

Thanks to Arthur Azevedo De Amorim for suggesting enabling Set Printing All.

Coq can't find subterm when using rewrite tactic

1 Answers