Застрял на простом неравенстве доказательства натуральных чисел в Coq

Я не эксперт в этом, но вы можете структурировать это доказательство 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: Мощная тактика, решающая задачи линейной арифметики.
• apply le_trans: использует транзитивность ≥≥ для объединения результатов.

Несколько полезных Coq ресурсов по тактике в Интернете

• https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html
• https://coq.inria.fr/doc/V8.19.2/refman/proof-engine/tactics.html
• https://www.inf.ed.ac.uk/teaching/courses/tspl/cheatsheet.pdf
• https://julesjacobs.com/notes/coq-cheatsheet/coq-cheatsheet.pdf

К сожалению, в сети нет «простого» списка Coq тактик, и для этого нужно немало покопаться в Интернете.

Надеюсь, это поможет!

Благодаря @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.