help with lean proofs for new number system

Stream: new members

[prodgang]

Hello, I've recently finished writing up some results about a new number system I've been working on. The results are legit (including some nice heyting algebras) and to dispel crackpot allegations, I had hoped to also formalize the proofs in lean but struggled with the nested inductions they kept producing. Would anyone be willing to help me with this?

The main results are summarized here and my failed lean proofs are here.

I apologize if this is not the appropriate place to be posting this, let me know if there is a better option. Many thanks!

[Notification Bot]

This topic was moved here from #maths > help with lean proofs for new number system by Johan Commelin.

[Jz Pan]

I think you shouldn't use axiom prod_pad (ps : List prod_num) : prod_num.pli (ps ++ [prod_num.p0]) = prod_num.pli ps. You should call your pre_prod_num, define an equivalence relation on it, and define prod_num as a quotient type of it. Ideally you should also provide DecidableEq pre_prod_num instances, etc.

[prodgang]

Thanks will try this out. What makes you think it would be easier?

[Matt Diamond]

In general it's a good idea to avoid axioms if you can, and the "Type is quotient of preType" pattern is common in Mathlib

[Eric Wieser]

I think this result might already exist in mathlib as docs#Nat.factorization

(your "prods" type is trivially isomorphic to mathlib's ℕ →₀ ℕ)

[Eric Wieser]

prodgang said:

my failed lean proofs are here.

It's very important when sharing Lean proofs to also commit the lakefile.* and lake-manifest.json files that should have been generated with lake new. Can you add these?

[Kevin Buzzard]

Eric Wieser said:

I think this result might already exist in mathlib as docs#Nat.factorization

(your "prods" type is trivially isomorphic to mathlib's ℕ →₀ ℕ)

Is this true? That type is Additive (PNat). The type in question has terms like [p0,p0,p0] and [p0] which both eval to 1, and terms like [[p0],p0] and [[[p0]]] and [[p0,p0],p0] that all eval to 2 etc.

[Eric Wieser]

The bit I crossed out or the other bit?

[Eric Wieser]

On reflection I think you're right though, they're not isomorphic after all!

[Eric Wieser]

Jz Pan said:

You should call your pre_prod_num, define an equivalence relation on it, and define prod_num as a quotient type of it.

Or define an inductive predicate:

inductive PreProdNum : Type
| p0 : PreProdNum
| pli (l : List PreProdNum) : PreProdNum

inductive PreProdNum.IsProper : PreProdNum → Prop
/-- p0 is proper. -/
| p0 : IsProper .p0
/-- A concatenation is proper if all elements are, and the last element is not `p0`. -/
| concat (ps ps' : List PreProdNum) (hps : ∀ p ∈ ps, p.IsProper) (hps' : ∀ p ∈ ps', p.IsProper):
  IsProper (.pli <| ps ++ [.pli ps'])

abbrev ProdNum := {p : PreProdNum // p.IsProper }

[Jz Pan]

Eric Wieser said:

Or define an inductive predicate

Good idea! At first I want to define PreProdNum.pli by requiring the tail of the list is not equal to p0, but seems that it's not possible:

inductive Test : Type
| zero : Test
| test (a b : Test) (hb : b ≠ Test.zero) : Test -- not possible

[Jz Pan]

Do you think this is better?

inductive PreProdNum : Type
| p0 : PreProdNum
| pli (l : List PreProdNum) : PreProdNum

def PreProdNum.IsProper : PreProdNum → Prop
| p0 => True
| pli (l : List PreProdNum) => l.getLast? ≠ some p0

-- TODO: `DecidableEq PreProdNum` and `DecidablePred PreProdNum.IsProper`

@[simp]
theorem PreProdNum.isProper_p0 : p0.IsProper := trivial

@[simp]
theorem PreProdNum.isProper_pli_iff (l : List PreProdNum) :
    (pli l).IsProper ↔ l.getLast? ≠ some p0 := Iff.rfl

example : (PreProdNum.pli []).IsProper := by simp

abbrev ProdNum := { p : PreProdNum // p.IsProper }

[Jz Pan]

I don't know how to write this sorry, as I need to use DecidableEq PreProdNum recursively...

instance : DecidableEq PreProdNum
| .p0, .p0 => .isTrue rfl
| .p0, .pli _ => .isFalse nofun
| .pli _, .p0 => .isFalse nofun
| .pli l1, .pli l2 => sorry

instance : DecidablePred PreProdNum.IsProper
| .p0 => .isTrue trivial
| .pli l =>
  if h : l.getLast? = some .p0 then
    .isFalse (by simp [PreProdNum.IsProper, h])
  else
    .isTrue h

[prodgang]

Eric Wieser said:

It's very important when sharing Lean proofs to also commit the lakefile.* and lake-manifest.json files that should have been generated with lake new. Can you add these?

Apologies - fixed.

[prodgang]

Eric Wieser said:

On reflection I think you're right though, they're not isomorphic after all!

Prods do end up being isomorphic to nats - thats the first big theorem im trying to prove (its not trivial).

[Aaron Liu]

Since they're isomorphic to Nat, you could "cheat" and just implement them as Nat:

import Mathlib

def ProdNum := Nat

@[inline]
def ProdNum.toNat : ProdNum ≃ Nat := Equiv.refl _

instance : Zero ProdNum := ⟨ProdNum.toNat.symm 0⟩

def ProdNum.ofList (xs : List ProdNum) : ProdNum :=
  go xs 1 1
where
  go (xs : List ProdNum) (n : Nat) (acc : Nat) : ProdNum :=
    match xs with
    | [] => acc
    | x :: xs =>
      let n := n + 1
      let n := n + Nat.find
        (show (∃ m, Nat.Prime (n + m)) by
          obtain ⟨m, hnm, hm⟩ := Nat.exists_infinite_primes n
          use m - n
          rwa [add_tsub_cancel_of_le hnm])
      go xs n (acc * n ^ toNat x)
-- etc

[Eric Wieser]

Jz Pan said:

Do you think this is better?

def PreProdNum.IsProper : PreProdNum → Prop
| p0 => True
| pli (l : List PreProdNum) => l.getLast? ≠ some p0

this doesn't work, you're missing the fact that everything in l is also proper

[Eric Wieser]

The nice thing about my spelling is you get a possibly-useful induction principle

[prodgang]

Yeah there definitely needs to be an easy to use induction. I need to be able to implement proofs like this one

[prodgang]

Eric Wieser said:

abbrev ProdNum := {p : PreProdNum // p.IsProper }

It seems like this would ban prods from ending with zeros. But its very important I can pad with zeros because there are binary relations which require both arguments to be the same length. It should just be that padding with zeros preserves equality

[Jz Pan]

So it's best to use quotient type approach.

[Eric Wieser]

I suspect that padding with zeros is not useful after all

[Eric Wieser]

If the padding is irrelevant, then by definition you should not need to add it

[Kyle Miller]

Jz Pan said:

So it's best to use quotient type approach.

If it's possible to normalize terms, often it's better to define a type using normalized terms, and then define a normalization function — this is the quotient map. You don't need to use Quot/Quotient to have quotient types. A quotient is any type that satisfies the universal property.

[Eric Wieser]

Here's an example of defining the graft operation without introducing trailing zeros:

@[simp]
def PreProdNum.sup : PreProdNum → PreProdNum → PreProdNum
  | .p0, x => x
  | x, .p0 => x
  | .pli xs, .pli ys => .pli (supList xs ys)
where
  supList : List PreProdNum → List PreProdNum → List PreProdNum
  | [], ys => ys
  | xs, [] => xs
  | (x :: xs), (y :: ys) => x.sup y :: supList xs ys

[Eric Wieser]

Proving

theorem PreProdNum.IsProper.sup {x y : PreProdNum} (hx : x.IsProper) (hy : y.IsProper) :
    (x.sup y).IsProper := by

looks to be quite fiddly though, so perhaps this definition (or the definition of IsProper isn't the most convenient

[Jz Pan]

Eric Wieser said:

this doesn't work, you're missing the fact that everything in l is also proper

I try to fix it with this:

inductive PreProdNum : Type
| p0 : PreProdNum
| pli (l : List PreProdNum) : PreProdNum

def PreProdNum.IsProper : PreProdNum → Prop
| p0 => True
| pli (l : List PreProdNum) => l.getLast? ≠ some p0 ∧ ∀ n, (l.getD n p0).IsProper

but it complains for termination proof in PreProdNum.IsProper...

[Jz Pan]

OK this works, but a little bit stupid:

inductive PreProdNum : Type
| p0 : PreProdNum
| pli (l : List PreProdNum) : PreProdNum

def PreProdNum.IsProper : PreProdNum → Prop
| p0 => True
| pli [] => True
| pli (x :: xs) => x.IsProper ∧ (pli xs).IsProper ∧ (x :: xs).getLast? ≠ some p0

[Jz Pan]

prodgang said:

Eric Wieser said:

abbrev ProdNum := {p : PreProdNum // p.IsProper }

It seems like this would ban prods from ending with zeros. But its very important I can pad with zeros because there are binary relations which require both arguments to be the same length. It should just be that padding with zeros preserves equality

You can define the "pad zero" function by l.getD n .p0.