Search code examples
coqcoq-tactic

Stuck at a simple inequality of natural number proof in Coq

I want to prove the inversion of inequality on negation, in natural numbers:

forall i j : nat, i <= j -> forall w : nat, i <= w -> j <= w -> w - i >= w - j.

I attempt to prove by induction. I first trivially prove that w - i >= w - i by reflexity. Then I try to prove w - i >= w - S m provided that w - i >= w - m, and I get stuck. It seems that if I prove w - m >= w - S m, it's done. But I can't solve that either. Could anyone help? Thank you so much!

Why isn't there an easy list of available tactics alongside their descriptions on the web?

Solution

  • I'm no expert at this, but a way you can structure this proof in 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.

    Base Case

    If j = 0, then by the condition i ≤ j, we have i = 0. The goal is w − 0 ≥ w − 0, which is trivial.

    Inductive Step j = S m

    • We assume the hypothesis i ≤ m (i.e., w − i ≥ w − m) holds.
    • Now, we need to prove w − i ≥ w − S m.
    • We do a case analysis on whether i = S m or i < S m.
    • If i = S m, then w − i ≥ w − j is trivial since w − S m ≥ w - S m.
    • If i < S m, we use the induction hypothesis to reduce the goal and then apply basic arithmetic reasoning.

    Tactics

    • intros: Introduces the quantified variables and assumptions.
    • induction j as [| m IHm]: Performs induction on jj.
    • destruct (Nat.eq_dec i (S m)): Case analysis on whether i = S m or i < S m.
    • assert (i = 0) as Hi0 by lia: Introduces and proves a necessary equality using the lia tactic.
    • lia: A powerful tactic that solves linear arithmetic goals.
    • apply le_trans: Uses the transitivity of ≥≥ to combine results.

    Some useful Coq tactics resources on the web

    Unfortunately, there is no "easy" list of Coq tactics out there on the web, and it does require quite a digging online.

    I hope this helps!