如何将Coq中的“0<d”替换为“in”？

Question

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

在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 _).给出了最后一个引理(更容易从您的目标倒退，imho)：

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.