如何做归纳证明

Question

我必须证明：

Lemma bsuccOK: forall l, value (bsucc l) = S (value l).

有一个归纳证明，但我不明白该怎么做。

这是BSUCC函数：

Fixpoint bsucc (l: list bool): list bool := match l with
|[]=>[]
|r::true=>(bsucc r)::false
|r::false=>r::true
end.

Lemma bsucc_test1: bsucc [false;true;false;true] = [true;true;false;true].

Proof.
easy.
Admitted.

它为代表二进制数字的布尔值列表提供了继任者。

任何帮助将不胜感激！

Answer 1

您使用哪个二进制表示？
如果首先考虑最不重要的位，则例如4表示为[false; false; true; true]。

这是bsucc和value的定义。注意列表符号中的参数顺序，以及bsucc []的略有更改。希望没关系。

Require Import List Lia.
Import ListNotations. 

(** Least significant bit first  *)

Fixpoint bsucc (l: list bool):  list bool :=
  match l with
  | []  =>[true]
  | true::r => false:: (bsucc r)
  | false::r => true::r
  end.

Fixpoint value (s:list bool):  nat:=
  match s with
  | []   => 0
  | true::r => S (2 * value r)
  | false::r => 2 * value r
  end.

Compute value [false;false;true]. (* 4 *)

然后，通过l诱导，您的目标是可解决的。您也可以使用的策略是CBN或simper，case，重写和lia（用于线性算术）。

Answer 2

感谢您，这里的答案终于找到了：

Lemma bsuccOK: forall l, value (bsucc l) = S (value l).
Proof.
induction l; auto.
destruct a.
-simpl.
rewrite IHl.
lia.
-simpl.
lia.
Qed.