我可以在没有附加归纳类型的情况下证明引理吗

Question

我有以下类型：

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

Definition prog := list instr.

和 'execute' 程序的函数：

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.

但我不知道该怎么做。通常，instr 堆栈的大小应与数据（输入列表）的大小相同，我可以更改结构并创建一个对列表 (instr,nat)，并且运行上的归纳这个新列表。

但出于好奇，我想知道是否有办法在没有新结构的情况下证明引理。

可能吗？

谢谢！！

Answer 1

问题是您的陈述不够笼统，无法通过归纳法进行，因为归纳步骤需要处理 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.

我可以在没有附加归纳类型的情况下证明引理吗

Can I prove a lemma without an additional inductive type

coq