证明二进制添加功能
我对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 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱,如果其他用户或者作者回复了您的评论,将不能在第一时间通知您!
发布评论
评论(1)
您可以通过
l1
的归纳来证明您的目标,并具有与先前的bsucc
正确性证明相同的工具。请注意,对于奇数数字(第一个数字为
true
),您可以将此引理使用重写BSUCC_OK
。You can prove your goal by induction on
l1
, with the same tools as your previous proof of correctness ofbsucc
.Note that in the case of an odd number (first digit is
true
), you may use this lemma withrewrite bsucc_ok
.