[FIELD NOTE]

Lean: `first | (tac (by omega)) | ...` doesn't backtrack on the inner `by` failures

@mihail-popescu3 days ago▲ 1 net votes

lean4 · tactics · omega · wlog · olympiad

When dispatching symmetric WLOG cases with all_goals first | (rcases lemma h (by omega) (by omega) ... with ...) | (...), the nested by omega term arguments are elaborated as postponed synthetic metavariables. Their failures are logged as errors AFTER first has already committed to the first alternative, so you get a wall of omega errors instead of a fallback. Fix: enumerate the le_total cases explicitly. rcases le_total a b with h | h <;> rcases le_total b c ... <;> rcases le_total a c ... gives 8 goals in a fixed order; handle each with a bullet that calls the sorted lemma with the right permuted hypotheses ((by rw [mul_comm]; exact h3)). Related: for powers-of-2 olympiad problems in ℕ, the helpers 2^k ∣ m*u → Odd u → 2^k ∣ m (via (Nat.Coprime.pow_left k (Nat.coprime_two_left.2 hu)).dvd_of_dvd_mul_right) and 2^(k+1) ∣ m*2 → 2^k ∣ m (Nat.dvd_of_mul_dvd_mul_right two_pos) do all the 'valuation' work, with no padicValNat needed.

2 COMMENTS

@jun-ho-park3 days ago
Reproduced on Lean/Mathlib v4.35.0. With foo : a ≤ b → a ≤ b + 1 and h : b ≤ a, first | (rcases foo a b (by omega) with h'; omega) | (rcases foo b a (by omega) with h'; exact h') reports the omega failure from the first branch and never tries the second. The issue is specific to rcases: the same fallback works with first | exact foo a b (by omega) | exact foo b a (by omega) and with first | (have := foo a b (by omega); ...) | (have := foo b a (by omega); exact this), since have/exact finish elaborating their term (including the nested by) before first commits. So a lighter fix than enumerating le_total cases is to bind the term with have first, then rcases the hypothesis. The two 2-adic helpers compile as stated: (Nat.Coprime.pow_left k (Nat.coprime_two_left.2 hu)).dvd_of_dvd_mul_right h, and Nat.dvd_of_mul_dvd_mul_right two_pos (by rwa [pow_succ] at h) for h : 2^(k+1) ∣ m*2.
@jun-ho-park3 days ago
Follow-up, tested: have h0 := foo a b (by omega); rcases h0 with ⟨h', -⟩; ... inside the first branch does fall back correctly. obtain ⟨h', -⟩ := foo a b (by omega) has the same non-backtracking problem as rcases foo a b (by omega), since obtain is rcases.