defining power

Stream: new members

[Matt Chen]

Hi! I am new to lean. I have defined rings, ordered rings, and well ordered rings on my own.

import Mathlib.Data.Set.Lattice

structure myRing (α : Type) where

  add : α → α → α

  mul : α → α → α

  zero : α

  one : α

  neg : α → α

  add_comm : ∀ x y : α, add x y = add y x

  mul_comm : ∀ x y : α, mul x y = mul y x

  add_assoc : ∀ x y z : α, add (add x y) z = add x (add y z)

  mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z)

  distrib : ∀ x y z : α, mul x (add y z) = add (mul x y) (mul x z)

  add_zero : ∀ x : α, add x zero = x

  add_inv : ∀ x : α, add x (neg x) = zero

  mul_ident : ∀ x : α, mul x one = x

structure myOrderedRing (α : Type) extends myRing α where

  P : Set α -- α → Prop

  P_nonempty : P.Nonempty -- ∃ x : α , P α

  P_add : ∀ a b : α, a ∈ P → b ∈ P → add a b ∈ P

  P_mul : ∀ a b : α, a ∈ P → b ∈ P → mul a b ∈ P

  trichotomy1 : zero ∉ P

  trichotomy2 : ∀ a , a ∈ P → neg a ∉ P

  trichotomy3 : ∀ a , a ∉ P → a ≠ zero → neg a ∈ P

def myRing.sub {α : Type} (R : myRing α) (x y : α) : α :=

  R.add x (R.neg y)

def myOrderedRing.lt {α : Type} (R : myOrderedRing α) (a b : α) : Prop :=

  R.add a (R.neg b) ∈ R.P

def myOrderedRing.le {α : Type} (R : myOrderedRing α) (a b : α) : Prop :=

  R.add a (R.neg b) ∈ R.P ∨ a = b

def myOrderedRing.gt {α : Type} (R : myOrderedRing α) (a b : α) : Prop := -- b > a

  R.add b (R.neg a) ∈ R.P

def myOrderedRing.ge {α : Type} (R : myOrderedRing α) (a b : α) : Prop := -- b > a

  R.add b (R.neg a) ∈ R.P ∨ a = b

structure WellOrderedRing (α : Type) extends myOrderedRing α where

  well_ordered : ∀ (S : Set α), S.Nonempty → S ⊆ tomyOrderedRing.P →

  ∃ m ∈ S, ∀ s ∈ S, myOrderedRing.le tomyOrderedRing s m

now I am struggling with defining power.

def pow {α : Type} (R : WellOrderedRing α) (base : α) : α → α

  | R.zero => R.one -- error : invalid pattern variable, must be atomic

  | R.add R.one n => pow base n

I don't quite understand what is atomic. Thanks for your help!

[Edward van de Meent]

the issue is that you cannot pattern match on just anything. Typically, you'd pattern match on constructors of an inductive type, which are atomic in the sense that as far as the type system is concerned, those are the indivisible value-producing functions for such a type.

[Matt Chen]

how can I define a constructor of inductive type for pattern matching?

[Edward van de Meent]

i don't think it's very much applicable in this case? you don't know what type you're endowing with ring structure, and you don't even know if this definition always terminates. (for example, what happens when the exponent is -1:Int? what happens for 0.5:Real?)

[Edward van de Meent]

in this case, once you decide what algorithm you want to use (that always terminates), you will likely want to use some kind of if exponent = 0 then 1 else something

[Matt Chen]

https://github.com/cymcymcymcym/Unique_Factorization_Lean4

The thing is i am trying to prove number theory results from scratch in lean. defining a well-ordered ring allows me to construct integers from scratch. this pow function that I want to define can just be limited to positive power of positive elements.

I tried using "if else"

def power {α : Type} (R : WellOrderedRing α) (base : α) : α → α
  | exp =>
    if exp = R.zero then R.one  -- error : failed to synthesize Decidable (exp = R.zero)
    else R.mul base (power R base (R.sub exp R.one))

The error suggests equality here is not decidable

[Edward van de Meent]

that's something you can consider to be an assumption

[Edward van de Meent]

without that, you really won't be able to get anywhere

[Matt Chen]

how can I make

exp = R.zero

decidable?

[Edward van de Meent]

add [decidableEq:DecidableEq α] as a field to myring and follow the structure with a line attribute [instance] myRing.decidableEq

[Jireh Loreaux]

Can't you just prove that every WellOrderedRing is isomorphic (as an ordered ring) to ℤ?

[Johan Commelin]

Matt Chen said:

how can I make

exp = R.zero

decidable?

You can also open Classical at the top of your file.

[Kevin Buzzard]

Are you trying to define x^y for x and y elements of an arbitrary ordered ring, by "x^0=1 and for all other y, x^y is defined to be x*x^(y-1)"? Isn't this nonsense? It won't terminate for e.g. (-1)^(-1) or 1^(0.5) etc etc.

[Edward van de Meent]

an arbitrary Well-Ordered ring (being isomorphic to $\mathbb{Z}$) would allow a similar definition, although proving termination would still be hell without lifting through $\mathbb{Z}$

[Kevin Buzzard]

Z is not well-ordered.

[Edward van de Meent]

the well-ordering is on the positive subset

[Edward van de Meent]

(in this case)

[Kevin Buzzard]

It still wouldn't be good enough if there are elements which are not of the form 1+1+1+1+...+1.

[Edward van de Meent]

that's true; you will still need to do the 3 cases of postive, negative, and zero.