如何在coq中编写一个函数，该函数将2个列表所代表的整数和代表保留的布尔值相加?

Question

我想设置递归函数badd_r: list bool ->List bool ->bool→列表bool值表示两个列表所表示的整数的和，Boolean值表示保留值。我需要使用这两个函数b1add_r(两个列表的和)，bsucc(由布尔值列表表示的二进制数的后继数)。下面是两个函数:

Fixpoint bsucc (l: list bool):  list bool :=
match l with
| []  =>[true]
| true::r => false:: (bsucc r)
| false::r => true::r
end.
Definition b1add_r b1 b2 r :=
match b1,b2 with
true, true => (r,true)
| true,false => (negb r, r)
| false, true => (negb r,r)
| false,false => (r, false)
end.

我不知道如何在coq中编码这个函数以及如何证明它…

Lemma badd_rOK: forall l1 l2 r,
value (badd_r l1 l2 r) = value l1 + value l2 + (if r then 1 else 0).
Fixpoint value (l: list bool) :=
match l with
| [] => 0
| true :: r => 1 + 2 * value r
| false :: r => 2 * value r
end.

任何帮助将不胜感激!

Answer 1

你的函数可能有以下形式:

Fixpoint badd_r (l1 l2:list bool) (r : bool) : list bool :=
match l1, l2 with
nil, nil => (* base case 1 *)
| a::r1, nil => (* base case 2 *)
| nil, b::r2 => (* base case 3 *)
| a::r1, b:: r2 => let (c, r') := b1add_r a b r
in (* recursive case *)
end.

为了填补漏洞/注释，并计划证明正确性，您可以将算术属性与可能的情况联系起来。例如，等式(1+2*x)+(0+2*y)+1= 0+2(x+y+1)对应于情况add_r (true::r) (false::s) true = false :: (add_r r s true)