证明二进制添加功能

发布于 2025-01-22 12:49:48 字数 713 浏览 0 评论 0原文

我对COQ语言的新手是新手,我想证明一个功能,该函数从表示为列表的数字(最不重要的前期)。

我创建了一个可以做到这一点的糟糕功能,现在我想证明这一点:


Fixpoint badd (l1 l2: list bool): list bool := 
  match l1 with
  | [] => l2
  | true :: l1 =>  bsucc (badd l1 (badd l1 l2))
  | false :: l1 => badd l1 (badd l1 l2)
end.

Lemma baddOK: forall l1 l2, value (badd l1 l2) = value l1 + value l2.

这里有BSUCC和值:

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

Fixpoint value (l: list bool) :=
  match l with
  | [] => 0
  | true :: r => 1 + 2 * value r
  | false :: r => 2 * value r
end.

事先感谢您的帮助!

I'm fairly new to the Coq language and I want to prove a function that does an binary add from numbers represented as a list (least significant bit upfront).

I have created this badd function that does that and now I want to prove it:


Fixpoint badd (l1 l2: list bool): list bool := 
  match l1 with
  | [] => l2
  | true :: l1 =>  bsucc (badd l1 (badd l1 l2))
  | false :: l1 => badd l1 (badd l1 l2)
end.

Lemma baddOK: forall l1 l2, value (badd l1 l2) = value l1 + value l2.

Here are bsucc and value:

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

Fixpoint value (l: list bool) :=
  match l with
  | [] => 0
  | true :: r => 1 + 2 * value r
  | false :: r => 2 * value r
end.

Thank you in advance for your help!

如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。

评论(1

你的他你的她 2025-01-29 12:49:48

您可以通过l1的归纳来证明您的目标,并具有与先前的bsucc正确性证明相同的工具。

Lemma bsucc_ok l : value (bsucc l) = S (value l).

请注意,对于奇数数字(第一个数字为true),您可以将此引理使用重写BSUCC_OK

You can prove your goal by induction on l1, with the same tools as your previous proof of correctness of bsucc.

Lemma bsucc_ok l : value (bsucc l) = S (value l).

Note that in the case of an odd number (first digit is true), you may use this lemma with rewrite bsucc_ok.

~没有更多了~
我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
原文