functional-programming - 如何在 Coq 中用 `0 < d` ` 替换假设 `S 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)

这意味着我们需要推断 d <> 0来自 0 < d ，所以再次 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.