如何在 Coq 中用 `S d' 替换假设 `0 < d`？

Question

How to replace hypotheses 0 < d with S d' in Coq?

在 Coq 中，我有令人讨厌的假设 0 < d，我需要替换它以应用 euclid_div_succ_d_theorem 来证明 euclid_div_theorem 作为推论。

我怎样才能以某种方式将假设转换为正确的形式来应用定理？

Theorem euclid_div_theorem :
  forall d : nat,
    0 < d -> 
    forall n : nat,
    exists q r : nat,
      n = q * d + r /\ r < d.

Theorem euclid_div_succ_d_theorem :
  forall d : nat,
  forall n : nat,
  exists q r : nat,
    n = q * (S d) + r /\ r < (S d).

Answer 1

使用 Arith 模块中的标准引理，您可以将 0 < d 更改为 exists m, d = S m，这（在销毁后）会为您提供所需的结果。

Require Import Arith.

Theorem euclid_div_theorem : forall d : nat,
    0 < d -> forall n : nat, exists q r : nat, n = q * d + r /\ r < d.
Proof.
  intros d H n.
  apply Nat.lt_neq, Nat.neq_sym, Nat.neq_0_r in H.
  destruct H; rewrite H.
  apply euclid_div_succ_d_theorem.
Qed.

我是这样做的：

Search (exists _, _ = S _). 给了我们最后一个引理（恕我直言，从你的目标向后退会更容易）：

Nat.neq_0_r: forall n : nat, n <> 0 <-> (exists m : nat, n = S m)

这意味着我们需要从 0 < d 推断出 d <> 0，所以再次 Search (_ < _ -> _ <> _). 产生：

Nat.lt_neq: forall n m : nat, n < m -> n <> m

现在很容易看出我们需要交换不等式的lhs和rhs，所以我做了Search (?x <> ?y -> ?y <> ?x).:

Nat.neq_sym: forall n m : nat, n <> m -> m <> n

我还可以使用更通用的引理：

not_eq_sym: forall (A : Type) (x y : A), x <> y -> y <> x

它会给我们相同的结果。

然而，有一种不那么乏味的证明引理的方法——你总是可以使用 destruct d. 并通过案例证明它：

  intros d H n.
  destruct d.
  - inversion H.   (* H is a contradiction now: `0 < 0` *)
  - apply euclid_div_succ_d_theorem.

如何在 Coq 中用 `S d' 替换假设 `0 < d`？

How to replace hypotheses `0 < d` with `S d'` in Coq?

functional-programming

coq