我可以证明没有其他电感类型的引理

Question

我有以下类型：

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

Definition prog := list instr.

以及“执行”程序的功能：

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.

我可以在各种输入上尝试：

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

现在我想证明以下引理：

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.

但是我看不到该怎么做。 通常，乐器堆栈的大小应与数据的大小相同（输入列表），我可以更改结构并创建对（仪器，NAT）的列表，并在此新列表上运行归纳。

但是出于好奇，我想知道是否有一种方法可以证明没有新结构的引理。

是否可以 ？

谢谢 ！！

Answer 1

问题是您的语句不够笼统，无法通过归纳进行，因为归纳步骤需要处理head [] 以外的head。修复很容易：

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.