如何证明所有x y, x<=y -> div2 x <= div2 y in coq?

Question

我想证明这个引理“forall x y, x<=y -> div2 x <= div2 y” in coq by induction, however I got stucked.

如何通过归纳法证明这一点？谢谢！

我尝试通过归纳法证明 x 和 y，但都卡住了。

Answer 1

我们来看看

div2

的定义：

Require Import Arith.
Import Nat.

Print div2.
(*
div2 =
fix div2 (n : nat) : nat := match n with
                            | S (S n') => S (div2 n')
                            | _ => 0
                            end
*)

递归案例使用了前驱的前驱，因此简单的归纳法不容易实现也就不足为奇了。

你如何在纸上证明这一点？

---

无论如何，为了在 Coq 中得到它，假设这不是一个练习，你可以随时寻找库引理来帮助你。这是我的过程：

Search div2 (_ <= _).

这似乎不是很有帮助，这两个对象只有两个引理，没有一个能解决问题...嗯，

div2

是除法的一个特殊情况，所以也许有除法的结果可以帮助.

Search (_ / _) (_ <= _).
(* ... among others:
Div0.div_le_mono: forall a b c : nat, a <= b -> a / c <= b / c
*)

宾果，这是我们想要的更一般的情况。现在我们只需要将

div2

翻译为

_ / 2

:

Search div2 (_ / _).
(*
div2_div: forall a : nat, div2 a = a / 2
*)

就是这样，有了这两个引理，你就得到了证明。

---

我还没有想过如何在不依赖之前的引理的情况下做到这一点，但如果你好奇，你可以随时在 Coq 源代码中找到

Div0.div_le_mono

的证明。诚然，这并不是一件小事。经过一番研究，我相信它是基于这个引理。