Zulip Chat Archive

I am within a branch of a by_cases statement. I have as a hypothesis A, as a goal B, and have a theorem A ∧ B → False. Ideally, I would like to tell Lean to assume B and change my goal to False, then apply my theorem to show a contradiction. Is there a tactic for the first part of this?

theorem Nat.exists_div_mod (n:Nat) {q: Nat} (hq: q.IsPos) :
    ∃ m r: Nat, 0 ≤ r ∧ r < q ∧ n = m * q + r := by -- exercise
  revert n; apply induction
  . use 0, 0                      -- base case: (n = 0), (m = 0), (r = 0) ⊢ 0 ≤ r < q ∧ n = m * q + r
    refine ⟨?_, ?_, ?_⟩
    . exact le_refl 0               -- ⊢ 0 ≤ 0
    . refine ⟨?_, ?_⟩               -- ⊢ 0 < q
      . use q; rw [zero_add]          --         ⊢ 0 ≤ q
      . symm; exact hq                -- q.isPos ⊢ q ≠ 0
    . rw [zero_mul, add_zero]       -- ⊢ 0 = 0 * q + 0
  . intro n ih                    -- ind. case: ∃mr st. 0 ≤ r < q ∧ n = m * q + r
    obtain ⟨m, r, _, hrq, hnm⟩ := ih   -- prove: ⊢ ∃ab, 0 ≤ b < q ∧ n++ = a * q + b
    rw [succ_eq_succ, ← add_succ] at hnm
    by_cases h : q = (r++)
    . use m++, 0
      rw [h] at hnm
      rw [add_zero]
      refine ⟨?_, ?_, ?_⟩
      . exact zero_le 0
      . rw [h]
        refine ⟨?_, ?_⟩
        . exact zero_le (r++)
        . symm; exact succ_ne r
      . rw [succ_mul, h]; exact hnm
    . use m, (r++)
      refine ⟨?_, ?_, ?_⟩
      . exact zero_le (r++)
      . have tri := trichotomous q (r++)
        rcases tri with lt | eq | gt
        . rw [← gt_iff_lt]
          -- lt : q < r++
          -- goal : q > r++
          -- i have a theorem not_lt_of_gt : a < b ∧ a > b → False
          sorry
        . contradiction
        . rw [← gt_iff_lt]; exact gt
      . exact hnm

This is within a proof of Euclid's division lemma. The place I'd like to be able to do this is marked by the sorry above. I may have done something wrong to get to this state, but I think the reasoning as described above is sound? Thanks for any advice.

Matt Diamond (Aug 04 2025 at 05:38):

I can't run your example in the playground, but if you have a hypothesis q < r++ then proving q > r++ is impossible, since if it were true that would be a contradiction

JJ (Aug 04 2025 at 05:39):

Yeah. That it is a contradiction is exactly what I want to show. I am in a branch of by_cases and one of my other cases is true, this one and another should lead to contradictions.

Matt Diamond (Aug 04 2025 at 05:41):

I mean, that's not how proof by contradiction works... if I have an assumption A, and I want to prove ¬A, I can't say "well if ¬A were true then it would be a contradiction, therefore I can close the goal"

JJ (Aug 04 2025 at 05:41):

Why not?

Matt Diamond (Aug 04 2025 at 05:42):

well, let's say the assumption is 1 < 2... I think we can both agree that that's true

Matt Diamond (Aug 04 2025 at 05:42):

now let's say my goal is ¬(1 < 2)... I don't think I can prove that using contradiction

Matt Diamond (Aug 04 2025 at 05:43):

otherwise we would have just proved that 1 was not less than 2

Matt Diamond (Aug 04 2025 at 05:44):

contradiction lets you prove a goal when you have an impossible set of assumptions, not when (or rather, not just because) the goal itself is impossible

Matt Diamond (Aug 04 2025 at 05:45):

it would be kind of silly to say "the conclusion I want to prove is contradicted by what I know is true, therefore it's a contradiction and I can now close the goal and prove the conclusion is true"

Niels Voss (Aug 04 2025 at 05:49):

To answer your question directly, you are probably looking for the by_contra h tactic (defined in Batteries, so if you have no imports you'll probably need to import something) but like Matt Diamond said, it won't work in this case