如何进行归纳证明

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].

这里是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 或 simpl、case、rewrite 和 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.

如何进行归纳证明

How to do an inductive proof

proof

coq

induction