主页 / coding / 问题 / 78942664
Accepted
Kaiwen
Asked: 2024-09-03 12:27:06 +0800 CST

在 Coq 中，自然数证明的一个简单不等式被卡住了

  • 772

我想证明自然数中不等式的否定逆：

对于所有 ij：nat，i <= j -> 对于所有 w：nat，i <= w -> j <= w -> w - i >= w - j。

我尝试通过归纳法来证明。我首先w - i >= w - i通过反身性简单地证明。然后我尝试证明w - i >= w - S m只要有w - i >= w - m，我就会卡住。似乎如果我证明w - m >= w - S m，就完成了。但我也无法解决这个问题。有人能帮忙吗？非常感谢！

为什么网络上没有可用策略的简单列表及其描述？

coq

2 个回答

  1. Best Answer

    我不是这方面的专家，但你可以用以下方式构建这个证明Coq：

    Require Import Arith.

Lemma le_minus : forall i j : nat, i <= j -> forall w : nat, i <= w -> j <= w -> w - i >= w - j.
Proof.
  intros i j H1 w H2 H3.
  (* Induction on j *)
  induction j as [| m IHm].
  - (* Base Case: j = 0 *)
    assert (i = 0) as Hi0 by lia.
    rewrite Hi0. simpl. auto.
  - (* Inductive Step: j = S m *)
    destruct (Nat.eq_dec i (S m)).
    + (* Case: i = S m *)
      subst. lia.
    + (* Case: i < S m *)
      assert (i <= m) as H4 by lia.
      specialize (IHm H4 w H2).
      apply le_trans with (w - m). 
      * apply IHm. lia.
      * simpl. lia.
Qed.

    基本情况

    如果j = 0，那么根据条件i ≤ j，我们有i = 0。目标是w − 0 ≥ w − 0，这很简单。

    归纳步骤j = S m

    • 我们假定假设i ≤ m（即w − i ≥ w − m）成立。
    • 现在，我们需要证明w − i ≥ w − S m。
    • i = S m我们就是否进行案例分析i < S m。
    • 如果i = S m，那么w − i ≥ w − j是平凡的，因为w − S m ≥ w - S m。
    • 如果i < S m，我们使用归纳假设来减少目标，然后应用基本的算术推理。

    策略

    • intros：介绍量化的变量和假设。
    • induction j as [| m IHm]：对jj进行归纳推理。
    • destruct (Nat.eq_dec i (S m))i = S m: 是否的案例 分析i < S m.
    • assert (i = 0) as Hi0 by lia：使用 lia 策略引入并证明必要等式。
    • lia：一种解决线性算术目标的强大策略。
    • apply le_trans：利用≥≥的传递性来合并结果。

    Coq网络上一些有用的策略资源

    Coq不幸的是，网络上没有“简单”的策略列表，而且它确实需要在网上进行大量挖掘。

    我希望这有帮助！

    • 0

  2. 感谢@Alizain，经过反复试验后，我根据他/她的回答找到了一个可运行的脚本，其中有一些拼写错误：

    Require Import Arith.
Require Import Lia.

Lemma le_minus : forall i j : nat, i <= j -> forall w : nat, i <= w -> j <= w -> w - i >= w - j.
Proof.
  intros i j H1 w H2 H3.
  (* Induction on j *)
  induction j as [| m IHm].
  - (* Base Case: j = 0 *)
    assert (i = 0) as Hi0 by lia.
    rewrite Hi0. auto.
  - (* Inductive Step: j = S m *)
    destruct (Nat.eq_dec i (S m)).
    + (* Case: i = S m *)
      subst. lia.
    + (* Case: i < S m *)
      assert (i <= m) as H4 by lia.
      assert (m <= w) as H5 by lia.
      specialize (IHm H4 H5).
      apply le_trans with (w - m); lia.
Qed.

    编辑：

    事实上，使用起来会更简单lia：

    Lemma le_minus : forall i j : nat, i <= j -> forall w : nat, i <= w -> j <= w -> w - i >= w - j.
Proof. lia. Qed.
    • 0

相关问题