Additive inverses of rationsl in the online browser

Stream: new members

[Xinyi Zhang]

I've made some very basic lemmas about rationals in the Lean online browser, available here:

def plusQ (p q : Rat) : Rat := p + q
def zeroQ : Rat := 0
def minusQ (p : Rat) : Rat := -p


def id1Q (p : Rat) : plusQ p 0 = p := by
  unfold plusQ
  exact Rat.add_zero p

def id2Q (p : Rat) : plusQ 0 p = p := by
  unfold plusQ
  exact Rat.zero_add p

def assQ (p q r : Rat) : plusQ p (plusQ q r) = plusQ (plusQ p q) r := by
  unfold plusQ
  exact Eq.symm (Rat.add_assoc p q r)

-- Commutativity
def comQ (p q : Rat) : plusQ p q = plusQ q p := by
  unfold plusQ
  exact Rat.add_comm p q


#check Rat.mk'
#check 0        -- zero : Rat
#check (1 : Rat)
#check (2 : Rat )

I'm stuck trying to get additive inverses for rational numbers:

-- Define addition and negation "wrappers" for clarity
def RatCmp (p q : Rat) : Rat := p + q
def RatInv (p : Rat) : Rat := -p

-- Additive inverse lemmas for rationals
def inv1Q (p : Rat) : RatCmp p (RatInv p) = zeroQ := by
  unfold RatCmp RatInv zeroQ
  exact Rat.add_right_neg p


def inv2Q (p : Rat) : RatCmp (RatInv p) p = zeroQ := by
  unfold RatCmp RatInv zeroQ
  exact Rat.add_left_neg p

I'm specifically interested in imports which work in the online browser. I believe this already works with imports. What could be the easiest way to do that?

[Kenny Lau]

@Xinyi Zhang you can import Mathlib in the online browser

[Xinyi Zhang]

Thanks, that worked.

I got it with this:

def inv1Q (p : ℚ) : RatCmp (RatInv p) p = zeroQ := Ring.neg_add_cancel p


def inv2Q (p : ℚ) : RatCmp p (RatInv p) = zeroQ := by
  -- p + (-p) = 0
  unfold RatCmp
  unfold RatInv
  unfold zeroQ
  rw [add_comm]
  exact Ring.neg_add_cancel p

and the particular imports of:

import Mathlib.Tactic
import Mathlib.Tactic.Ring

[Robin Arnez]

Without mathlib, the lemmas are called docs#Rat.add_neg_cancel and docs#Rat.neg_add_cancel

[Robin Arnez]

Or just grind:

-- Define addition and negation "wrappers" for clarity
def RatCmp (p q : Rat) : Rat := p + q
def RatInv (p : Rat) : Rat := -p
def zeroQ : Rat := 0

-- Additive inverse lemmas for rationals
def inv1Q (p : Rat) : RatCmp p (RatInv p) = zeroQ := by
  grind [RatCmp, RatInv, zeroQ]