Stuck on Coq proof with list induction

Question

I'm finding myself stuck on a Coq proof.

Preliminary definitions:

Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Coq.omega.Omega.
Require Import Coq.Lists.List.
Require Export Coq.Strings.String.
Import ListNotations.


Definition total_map (A:Type) := string -> A.
Definition state := total_map nat.

Inductive sinstr : Type :=
| SPush : nat -> sinstr
| SLoad : string -> sinstr
| SPlus : sinstr
| SMinus : sinstr
| SMult : sinstr.



Definition s_execute_instr (st : state) (stack : list nat)
         (instr : sinstr)
  : option (list nat) :=
  match instr with
  | SPush n => Some (n :: stack)
  | SLoad x => Some (st x :: stack)
  | SPlus => match stack with
            | x :: y :: stack' => Some (x+y :: stack')
            | _ => None
            end
  | SMinus => match stack with
             | x :: y :: stack' => Some (y-x :: stack')
             | _ => None
             end
  | SMult => match stack with
            | x :: y :: stack' => Some (x*y::stack')
            | _ => None
            end
  end.

Fixpoint s_execute (st : state) (stack : list nat)
                   (prog : list sinstr)
  : option (list nat) :=
  match prog with
  | [] => Some (stack)
  | instr::prog' => match (s_execute_instr st stack instr) with
                  | Some stack' => s_execute st stack' prog'
                  | None => None
                  end
  end.

And my attempt at a theorem proof:

Theorem s_execute_relational : forall (l1 l2: list sinstr) (sk sk': list nat) (st : state),
  s_execute st sk l1 = Some sk' ->
  s_execute st sk (l1 ++ l2) = s_execute st sk' l2.
Proof.
  intros l1 l2 sk sk' st H.
  induction l1 as [|l1' l1].
  - inversion H. reflexivity.
  -

The current status is:

  l1' : sinstr
  l1, l2 : list sinstr
  sk, sk' : list nat
  st : state
  H : s_execute st sk (l1' :: l1) = Some sk'
  IHl1 : s_execute st sk l1 = Some sk' -> s_execute st sk (l1 ++ l2) = s_execute st sk' l2
  ============================
  s_execute st sk ((l1' :: l1) ++ l2) = s_execute st sk' l2

I've gone this path because I think I need to use induction somehow, but at this point, I'm not sure how to proceed.

I tried induction on l2 as well, but that doesn't seem to get me anywhere, either;

Theorem s_execute_relational : forall (l1 l2: list sinstr) (sk sk': list nat) (st : state),
  s_execute st sk l1 = Some sk' ->
  s_execute st sk (l1 ++ l2) = s_execute st sk' l2.
Proof.
  intros l1 l2 sk sk' st H.
  induction l2 as [|l2' l2].
  - simpl. rewrite <- H. replace (l1 ++ []) with l1.
    + reflexivity.
    + symmetry. apply app_nil_r.
  - 

  l1 : list sinstr
  l2' : sinstr
  l2 : list sinstr
  sk, sk' : list nat
  st : state
  H : s_execute st sk l1 = Some sk'
  IHl2 : s_execute st sk (l1 ++ l2) = s_execute st sk' l2
  ============================
  s_execute st sk (l1 ++ l2' :: l2) =
  s_execute st sk' (l2' :: l2)

It's strange asking this type of question on SO because it's not...really a reusable question/title is bad, but unsure how to improve on that front, either.

Answer 1

you should not introduce all variables as you do in the first line. You should first look at your recursive functions and has yourself two questions:

1. What are the recursive functions and their "structurally recursive arguments" here. You may have noticed that when Coq accepts a recursive definition, it tells you with respect to which argument it is structurally recursive.

2. What happens to the arguments that are not structurally recursives in the function: do they change between the recursive call or not?

Answer to question 1:

In your case, we have two main recursive functions List.app and s_execute. The recursive argument to s_execute is l1 on the left hand side of the implication. The recursive argument to s_execute is l1 ++ l2 in the left-hand side of the final equality, and the recursive argument to s_execute is only l2 in the right hand side. Because l1 ++ l2 is in position of a recursive argument, we can now look at the recursive argument of app by looking at its code, and we see that the argument that decreases structurally at the recursive call is again l1. This gives a strong feeling that induction should be performed on l1.

Answer to question 2: s_execute takes three arguments. The state does not change during execution, but the stack does. So you can fix st for the whole proof, but the stack argument should not be fixed. A similar observation appears for app: the second argument does not change during recursive calls.

Practically, you can start your proof with

intros l1 l2.
induction l1 ....

Don't go any further in the intros, because the stack should be left flexible, you will need this flexibility when using the induction hypothesis.

Just for the fun, you can try introducing more arguments, but you have to free the flexible ones by using the revert tactic. Just like so:

intros l1 l2 sk sk' st; revert sk.
induction l1 as ....

Here only sk has to be freed (or unfixed, or reverted).

This is actually a very good question, and the need to avoid fixing arguments that will need to change in uses of the induction hypothesis pops up regularly in formal proofs.

Later edit

Here is how I started your proof:

Theorem s_execute_relational : forall (l1 l2: list sinstr) (sk sk': list nat) (st : state),
  s_execute st sk l1 = Some sk' ->
  s_execute st sk (l1 ++ l2) = s_execute st sk' l2.
Proof.
intros l1 l2 sk sk' st; revert sk.
induction l1 as [ | n l1 Ih].  
  simpl; intros sk [= skk']; rewrite skk'; easy.

Now we are in the induction step case. The stack is still universally quantified in the goal's conclusion. So the induction hypothesis and the goal are actually talking about two potentially different stacks. The next step is to fix an arbitrary stack to reason on the conclusion.

intros sk.

Then we compute,

simpl.

We are reasoning about a symbolic execution of the code, and we don't know how (s_execute_instr st sk n) will result, so we need to cover both cases, this is what the destruct step does.

destruct (s_execute_instr st sk n) as [sk1 | ].

In the first case (for the execution of (s_execute_instr st sk n)), a new state sk1 appears, on which execution will proceed, and we know that execution of l1 from that state leads exactly to Some sk'. Let's give the name complete_l1 to that new state. Now it happens that the proof can be finished by instantiating the induction hypothesis on this new state.

  intros complete_l1.
  now rewrite (Ih sk1).

There remain the other case produced by the destruct step, but this case contains a self-inconsistent assumption of the form None = Some sk'. The easy tactic knows how to get rid of this (actually easy relies on discriminate, which implements what I like to call the non-confusion property of data-types).

easy.
Qed.

Please tell me what was missing in your attempt? Was it the destruct step?

Answer 2

Eventually, I figured it out.

Theorem s_execute_relational : forall (l1 l2: list sinstr) (sk sk': list nat) (st : state),
  s_execute st sk l1 = Some sk' ->
  s_execute st sk (l1 ++ l2) = s_execute st sk' l2.
Proof.
  intros l1.
  induction l1 as [| l1' l1].
  - intros l2 sk sk' st H. simpl.
    inversion H. reflexivity.
  - intros l2 sk sk' st H.
    assert (forall (x:sinstr) (xs ys: list sinstr), (x::xs) ++ys = x::(xs++ys)) as app_comm_cons.
    {
      auto.
    }
    rewrite app_comm_cons.
    unfold s_execute in *. destruct (s_execute_instr st sk l1').
    + eapply IHl1. apply H.
    + inversion H.
Qed.