Drop lemma for algorithm termination proof - q=1 edge case i

Stream: new members

[Harikrishnan R]

Title: Drop lemma for algorithm termination proof - q=1 edge case issue

I'm working on proving termination for Vedic algorithms and encountering an issue with a drop lemma where one case leads to a mathematical contradiction. Here's my MWE:

import Mathlib

-- MWE: Drop lemma for algorithm termination proof - q=1 edge case issue
-- Context: Proving WellFounded (fun a b => Algorithm b a) requires drop lemma

-- CORE ISSUE: How to handle mathematical contradiction in drop lemma?
lemma problematic_drop (p q : ℕ) (hp_pos : 0 < p) (hq_pos : 0 < q)
    (h_factor : ∃ k > 1, p = k * q) :
    p > p / q := by
  obtain ⟨k, hk_eq, hk_gt⟩ := h_factor
  rw [hk_eq]
  have h_div_eq : k * q / q = k := Nat.mul_div_cancel k hq_pos
  rw [h_div_eq]
  -- Goal: prove k * q > k where k > 1 and q > 0
  have h_k_pos : k > 0 := Nat.lt_trans Nat.zero_lt_one hk_gt

  by_cases h_q_eq_one : q = 1
  · -- PROBLEM: When q = 1, goal becomes k * 1 > k, i.e., k > k (impossible!)
    -- Question: How should we handle this mathematical contradiction?
    exfalso
    -- ATTEMPT 1: Try to derive k > k and show contradiction
    have h_impossible : k > k := by
      convert (by assumption : k * q > k)  -- ERROR: tactic 'assumption' failed
      rw [h_q_eq_one, Nat.mul_one]
    exact Nat.lt_irrefl k h_impossible
  · -- Case q > 1: this works fine
    have h_q_gt_one : q > 1 := Nat.succ_le_of_lt hq_pos (Ne.symm h_q_eq_one)
    -- k * q > k * 1 = k when q > 1
    rw [← Nat.mul_one k]
    exact Nat.mul_lt_mul_left h_k_pos h_q_gt_one

-- Demonstration that q=1 case is indeed impossible:
example (k : ℕ) (hk_gt : k > 1) : k * 1 > k → False := by
  intro h
  rw [Nat.mul_one] at h
  exact Nat.lt_irrefl k h

-- Working alternative with q > 1 precondition:
lemma alternative_drop (p q : ℕ) (hp_pos : 0 < p) (hq_gt : q > 1)
    (h_factor : ∃ k > 1, p = k * q) :
    p > p / q := by
  obtain ⟨k, hk_eq, hk_gt⟩ := h_factor
  rw [hk_eq]
  have h_div_eq : k * q / q = k := Nat.mul_div_cancel k (Nat.zero_lt_of_lt hq_gt)
  rw [h_div_eq, ← Nat.mul_one k]
  exact Nat.mul_lt_mul_left (Nat.zero_lt_of_lt hk_gt) hq_gt

My specific questions:

1. How should we handle the q=1 mathematical contradiction? When q=1, the goal k * q > k becomes k > k, which is impossible. What's the correct approach: (a) Add precondition q > 1 to exclude this case? (b) Use exfalso to show the case leads to contradiction? (c) Different proof strategy entirely?

2. Why does assumption tactic fail in the exfalso approach? The goal is k * q > k, but assumption can't find it. How to properly derive a contradiction when we know the goal is mathematically impossible?

3. For algorithm termination, should drop lemmas handle ALL cases or exclude mathematically impossible cases via preconditions? Context: This is for WellFounded (fun a b => Algorithm b a)

4. Which approach is mathematically and computationally sound for proving termination of algorithms that may have edge cases?

The alternative_drop lemma with q > 1 precondition works fine, but I'm unsure if excluding the q=1 case is the right approach for algorithm termination proofs.

[Harikrishnan R]

Title: Drop lemma for algorithm termination proof - q=1 edge case issue

I'm working on proving termination for Vedic algorithms and encountering an issue with a drop lemma where one case leads to a mathematical contradiction. Here's my MWE:

import Mathlib

-- MWE: Drop lemma for algorithm termination proof - q=1 edge case issue
-- Context: Proving WellFounded (fun a b => Algorithm b a) requires drop lemma

-- CORE ISSUE: How to handle mathematical contradiction in drop lemma?
lemma problematic_drop (p q : ℕ) (hp_pos : 0 < p) (hq_pos : 0 < q)
    (h_factor : ∃ k > 1, p = k * q) :
    p > p / q := by
  obtain ⟨k, hk_eq, hk_gt⟩ := h_factor
  rw [hk_eq]
  have h_div_eq : k * q / q = k := Nat.mul_div_cancel k hq_pos
  rw [h_div_eq]
  -- Goal: prove k * q > k where k > 1 and q > 0
  have h_k_pos : k > 0 := Nat.lt_trans Nat.zero_lt_one hk_gt

  by_cases h_q_eq_one : q = 1
  · -- PROBLEM: When q = 1, goal becomes k * 1 > k, i.e., k > k (impossible!)
    -- Question: How should we handle this mathematical contradiction?
    exfalso
    -- ATTEMPT 1: Try to derive k > k and show contradiction
    have h_impossible : k > k := by
      convert (by assumption : k * q > k)  -- ERROR: tactic 'assumption' failed
      rw [h_q_eq_one, Nat.mul_one]
    exact Nat.lt_irrefl k h_impossible
  · -- Case q > 1: this works fine
    have h_q_gt_one : q > 1 := Nat.succ_le_of_lt hq_pos (Ne.symm h_q_eq_one)
    -- k * q > k * 1 = k when q > 1
    rw [← Nat.mul_one k]
    exact Nat.mul_lt_mul_left h_k_pos h_q_gt_one

-- Demonstration that q=1 case is indeed impossible:
example (k : ℕ) (hk_gt : k > 1) : k * 1 > k → False := by
  intro h
  rw [Nat.mul_one] at h
  exact Nat.lt_irrefl k h

-- Working alternative with q > 1 precondition:
lemma alternative_drop (p q : ℕ) (hp_pos : 0 < p) (hq_gt : q > 1)
    (h_factor : ∃ k > 1, p = k * q) :
    p > p / q := by
  obtain ⟨k, hk_eq, hk_gt⟩ := h_factor
  rw [hk_eq]
  have h_div_eq : k * q / q = k := Nat.mul_div_cancel k (Nat.zero_lt_of_lt hq_gt)
  rw [h_div_eq, ← Nat.mul_one k]
  exact Nat.mul_lt_mul_left (Nat.zero_lt_of_lt hk_gt) hq_gt

My specific questions:

1. How should we handle the q=1 mathematical contradiction? When q=1, the goal k * q > k becomes k > k, which is impossible. What's the correct approach: (a) Add precondition q > 1 to exclude this case? (b) Use exfalso to show the case leads to contradiction? (c) Different proof strategy entirely?

2. Why does assumption tactic fail in the exfalso approach? The goal is k * q > k, but assumption can't find it. How to properly derive a contradiction when we know the goal is mathematically impossible?

3. For algorithm termination, should drop lemmas handle ALL cases or exclude mathematically impossible cases via preconditions? Context: This is for WellFounded (fun a b => Algorithm b a)

4. Which approach is mathematically and computationally sound for proving termination of algorithms that may have edge cases?

The alternative_drop lemma with q > 1 precondition works fine, but I'm unsure if excluding the q=1 case is the right approach for algorithm termination proofs.

[Weiyi Wang]

You code weirdly doesn't compile on the latest lean at

obtain ⟨k, hk_eq, hk_gt⟩ := h_factor
rw [hk_eq]

It is as if hk_eq and hk_gt were swapped

---

If your goal becomes False or any obviously false statement at any point without you doing any "proof-by-contradiction-like" tactic (by_contra/contraposeetc) before hand (Edit: or, you didn't introduce a false hypothesis by cases/split/etc.), it means the theorem you want to prove is actually false, and you should review the statement and correct it

[Weiyi Wang]

So to your question 1, (a) is the correct approach, as it corrects the statement

[Weiyi Wang]

I think we will need more context to provide concrete advise to question 3 and 4, but in general: you will need to handle all cases, but for impossible cases, you can explicitly show how the case is impossible, which becomes a valid proof for that case.

[Notification Bot]

A message was moved here from #lean4 > `omega` works for `Int.natAbs` but not for `abs` by Kim Morrison.