Can I prove a lemma without an additional inductive type

Question

I have the following types :

Inductive instr : Set :=
 | Select    : nat -> instr
 | Backspace : instr.

Definition prog := list instr.

and a function to 'execute' the program :

Fixpoint execProg (p:prog) (head: list nat) (input: list nat)
 : option (list nat) :=
 match p with
  | nil => match input with 
            | nil => Some head
            | _::_ => None
           end
  | m::rest =>
    match m with
    | Select n =>
      match input with 
      | nil => None
      | x::r => if (beq_nat n x ) then
                  match (execProg rest (head++[x]) r) with
                  | None => None
                  | Some l => Some l
                  end
                else None
      end
    | Backspace =>
      match input with
      | nil => None
      | x::r => match (execProg rest (removelast head) r) with
                | None => None
                | Some l => Some l
                end
      end
    end
 end.

I can try it on various inputs :

Eval compute in
  execProg (Backspace::Select 1::Select 4::Backspace::nil)
    nil (1::1::4::5::nil).

Now I'd like to prove the following lemma:

Lemma app_denoteSB :
  forall (a b:nat) (p:prog) (input output:list nat) ,
    execProg p [] input = Some output ->
    execProg (p++[Select a; Backspace]) [] (input ++ [a;b])
      = Some output.

But I don't see how to do that. As normally, the size of the instr stack should be the same as the size of the data (input list), I can change the structures and create a list of pairs (instr,nat), and run the induction on this new list.

But out of curiosity, I was wondering if there was a way to prove the lemma without the new structure.

Is it possible ?

Thanks !!

Answer 1

The issue is that your statement is not general enough to go through by induction, because the inductive step needs to handle values of head other than []. The fix is easy:

Require Import Arith.
Require Import List.
Import ListNotations.

Inductive instr : Set :=
 | Select    : nat -> instr
 | Backspace : instr.

Definition prog := list instr.


Fixpoint execProg (p:prog) (head input: list nat) : option (list nat) :=
  match p, input with
  | [], [] => Some head
  | [], _ :: _ => None
  | Select n :: rest, [] => None
  | Select n :: rest, x :: r =>
      if beq_nat n x then execProg rest (head++[x]) r
      else None
  | Backspace :: rest, [] => None
  | Backspace :: rest, x :: r => execProg rest (removelast head) r
  end.

Lemma app_denoteSB :
  forall (a b:nat) (p:prog) (head: list nat) (input output:list nat) ,
    execProg p head input = Some output ->
    execProg (p++[Select a; Backspace]) head (input ++ [a;b]) = Some output.
Proof.
intros a b p.
induction p as [|[n|] p IH].
- intros head [|??]; simpl; try easy.
  intros output H; injection H as <-.
  now rewrite Nat.eqb_refl, removelast_last.
- intros head [|x input] output; simpl; try easy.
  destruct (Nat.eqb_spec n x) as [<-|ne]; try easy.
  apply IH.
- intros head [|x input] output; simpl; try easy.
  apply IH.
Qed.