Axiom list - simp tag - simp line

Stream: new members

[Michael Bucko]

I wrote three lemmas, but they all have sorry. Then I turned them into axioms and added the simp tag.

Is true that I can now use them while using simp? (I am also assuming that axioms are noncomputable by default)

import Mathlib
import Lean

def is_k_almost_prime (k n : Nat) : Bool :=
  n > 1 && n.factorization.sum (fun _ multiplicity => multiplicity) == k

def is_k_almost_prime_prop (k n : Nat) : Prop :=
  is_k_almost_prime k n = true

noncomputable def nth_k_almost_prime (k i : Nat) : Nat :=
  Classical.epsilon (fun n =>
    is_k_almost_prime_prop k n ∧
    (((List.range (n+1)).filter (is_k_almost_prime k)).length = i+1)
  )

noncomputable def almost_prime_table (k i : Nat) : Nat :=
  nth_k_almost_prime (k+1) i

def col_has_power (k power : Nat) : Prop :=
  ∃ i, almost_prime_table k i = power

noncomputable instance (k power : Nat) : Decidable (col_has_power k power) :=
  Classical.propDecidable _

noncomputable def find_power_index (k power : Nat) : Option Nat :=
  if h : col_has_power k power then
    some (Nat.find h)
  else
    none

noncomputable def red_diamond_sequence_column (k : Nat) : Set Nat :=
  let currentPower := 3^(k+1)
  let nextPower := 3^(k+2)
  match find_power_index (k+1) nextPower with
  | some r => { n | n ≥ currentPower ∧ ∃ i, i < r ∧ almost_prime_table k i = n }
  | none   => { n | n ≥ currentPower ∧ ∃ i, almost_prime_table k i = n }

-- Red Diamond Conjecture
@[simp]
axiom red_diamond_conjecture_infinite : ∀ k,
  (∀ r, find_power_index (k+1) (3^(k+2)) = some r →
    almost_prime_table (k+1) r = 3^(k+2) ∧
    (∀ i, i < r → almost_prime_table k i ∈ red_diamond_sequence_column k))

-- Beal's Conjecture (correction suggested by Yael Dillies)
@[simp]
axiom BealConjecture :
  ∀ x y z : ℕ, x > 2 → y > 2 → z > 2 →
  ∀ A B C : ℕ, A > 0 → B > 0 → C > 0 →
  A ^ x + B ^ y = C ^ z →
  Finset.gcd {A, B, C} id > 1

-- ABC Conjecture
@[simp]
axiom abc_conjecture :
  ∀ (ε : ℝ) (_ : 0 < ε), ∃ (K : ℝ),
    ∀ (a b c : ℕ), a > 0 → b > 0 → c > 0 →
    a + b = c →
    gcd a b = 1 →
    (↑c : ℝ) < K * Real.rpow (↑(Nat.primeFactorsList (a * b * c)).prod) (1 + ε)

[Violeta Hernández]

simp shouldn't care about axiom lists. That being said, none of these seem like they would do much as simp lemmas.

[Violeta Hernández]

Your prototypical simp lemma looks like p x = q x or p x iff q x, where q x is some expression that is "simpler" than p x. For instance, x ^ 2 = 0 iff x = 0 would make a good simp lemma. None of these axioms are doing anything like that.

[Michael Bucko]

That's very useful. Thank you :thank_you:

Is there any way in which I assume that my ten statements are true (that's what I tried to do when using the keyword axiom), and then use them to perform some sort of (higher-order, or whatever is possible using intelligent tactics) simplification of a certain goal?