如何在COQ一个函数中进行编码，该函数汇总了由2个列表代表的整数和代表holdback的布尔值？

Question

我想设置递归函数badd_r：list bool - ＆gt;列表bool-＆gt;布尔 - ＆gt;列表布尔，总和由2个列表代表的整数和布尔值代表保留。 我需要使用这两个函数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 rs true）