Zulip Chat Archive

Stream: lean4

Topic: Hints for foundations for lemmas on Rat


Arien Malec (Oct 30 2022 at 22:30):

I'm a bit over my skis working on basic lemmas for Rat. In Lean 3 mathlib, https://github.com/leanprover-community/mathlib/blob/master/src/data/rat/defs.lean most of the really basic lemmas are defined in terms of num_denom_cases_on', e.g.:

protected theorem add_zero : a + 0 = a :=
num_denom_cases_on' a $ λ n d h,
by rw [ zero_mk d]; simp [h, -zero_mk]

and num_denom_cases_on' is defined in terms of num_denom, which relies on some definitional and implementation behavior that's different in Lean 4 (e.g., there's no pnat) and in terms of operators I don't understand (e.g. what's '/.'?)

In general rat and Rat are heavily pre-optimized, and add is inherently pretty complicated.

Some hints on the best Lean 4 equivalent for num_denom_cases_on' for the Lean 4 version of Rat would be greatly welcome.

Kevin Buzzard (Oct 30 2022 at 22:33):

docs4#Rat does this work?

Kevin Buzzard (Oct 30 2022 at 22:34):

So it looks like all the data has been defined (addition, subtraction etc) but none of the proofs?

Kevin Buzzard (Oct 30 2022 at 22:39):

Why not just sorry the proofs and make the ring instance?

Arien Malec (Oct 30 2022 at 22:56):

That would advance my project for sure but create a poor PR. If I had pointers to the hard bits I’d be happy to do the grunt work for a PR.

Scott Morrison (Oct 30 2022 at 23:02):

I think we have transitioned to the point in mathlib4 where PRs should either be

  1. ports of entire files from mathlib3, faithfully preserving all their content and organisation
  2. ad-hoc ports of material only if it is supporting tactic implementation.

Scott Morrison (Oct 30 2022 at 23:04):

So the ideal way to work on data/rat/defs.lean is first to run

cd src
leanproject import-graph --to data.rat.defs --exclude-tactics --port-status --reduce data.rat.defs.pdf

inside the mathlib repository.

Scott Morrison (Oct 30 2022 at 23:05):

This produces data.rat.defs.pdf

Arien Malec (Oct 30 2022 at 23:09):

What’s confusing is that this has moved to Std4 & the implementation details are just different enough that it’s not a mechanical port….

Scott Morrison (Oct 30 2022 at 23:14):

Oh dear, I hadn't realised Rat was in Std already!

Scott Morrison (Oct 30 2022 at 23:15):

Maybe the right choice is actually to backport this definition to mathlib3, so we can resume the "mechanical port".

Arien Malec (Oct 31 2022 at 01:03):

Arien Malec said:

in terms of operators I don't understand (e.g. what's '/.'?)

Realized that this is localized "infix (name := rat.mk) /. :70 := rat.mk" in rat so I can just use Rat.mk.

Arien Malec (Oct 31 2022 at 03:43):

I'm sorta making progress here, but I'm confused.

Given that /. means rat.mk and rat.mk is sorta 'mkRat' in Lean 4 Std4 (sorta because mathlib rat is defined in terms of int and pnat, where as Rat is Int and Nat & rat.mk is int -> int -> rat whereas mkRat is Int -> Nat -> Rat, I decided to try to rewrite

@[simp] theorem num_denom :  {a : }, a.num /. a.denom = a
| n, d, h, (c:_=1)⟩ := show mk_nat n d = _,
  by simp [mk_nat, ne_of_gt h, mk_pnat, c]

as

@[simp] theorem num_den :  {a : Rat}, mkRat a.num a.den = a
| n, d, h, (c:_=1)⟩ => show mkRat n d = _ by
  simp [mkRat, Nat.ne_of_gt h, mkRat, c]

but the net_of_gt simplification isn't working, and it's confusing to me why it should work in mathlib

It's spelled

lemma ne_of_gt {a b : α} (h : b < a) : a  b :=
λ he, absurd h (he  lt_irrefl a)

in mathlib

and

theorem ne_of_gt {a b : Nat} (h : b < a) : a  b := (ne_of_lt h).symm
theorem ne_of_lt {a b : Nat} (h : a < b) : a  b :=
  fun he => absurd (he  h) (Nat.lt_irrefl a)

In Lean 4

Since the type of h is … OH(!) the types in mathlib and Lean 4 differ.

In mathlib the corresponding type is 0 < denom and in Lean 4 it's den ≠ 0 so back to the mines.

Arien Malec (Oct 31 2022 at 03:49):

So

@[simp] theorem num_den :  {a : Rat}, mkRat a.num a.den = a
| n, d, h, (c:_=1)⟩ => show mkRat n d = _ by
  simp [mkRat,h,normalize, maybeNormalize,c]

closes the goal

Progress.

Arien Malec (Oct 31 2022 at 03:57):

I also now think I understand what that simp step is doing -- it's leading Lean down the path of understanding that mkRat is already pre-normalized by hypothesis.

Kevin Buzzard (Oct 31 2022 at 05:03):

docs#rat

Kevin Buzzard (Oct 31 2022 at 05:04):

You've made the assertion more than once that in loan 3 rat is defined using pnat but I don't think it's true.

Mario Carneiro (Oct 31 2022 at 05:13):

rat itself doesn't use pnat, but rat.mk uses rat.mk_pnat

Kevin Buzzard (Oct 31 2022 at 05:14):

Right -- the builtin constructor for rat is not rat.mk, it's rat.mk'

Mario Carneiro (Oct 31 2022 at 05:15):

ah yeah, maybe we should do that too, so we can use Rat.mk for the smart constructor

Mario Carneiro (Oct 31 2022 at 05:17):

The current lean 4 file is based not on the original data.rat.basic but on lean 4's Lean.Rat, which has slightly more efficient operations. We should try to make it align with mathlib better where it's reasonable to do so

Mario Carneiro (Oct 31 2022 at 05:19):

We also have another tool for replacements, @[csimp] lemmas, which allow us to use a naive and simple-to-reason-about definition as the official definition and sequester the messy and efficient definition to an auxiliary. I don't usually bother though unless we care about the defeqs

Arien Malec (Oct 31 2022 at 15:14):

Kevin Buzzard said:

You've made the assertion more than once that in loan 3 rat is defined using pnat but I don't think it's true.

Sorry, you are correct - as @Mario Carneiro notes, the path to construction goes through pnat but the rat itself is in terms of nat plus the assertion pos : 0 < denom

Arien Malec (Oct 31 2022 at 16:05):

Should the Lean 4 equivalent of /. for Rat be an HDiv?

Arien Malec (Oct 31 2022 at 16:12):

And…, how does one spell @[elab_as_eliminator] in Lean 4?

David Renshaw (Oct 31 2022 at 16:23):

@[elabAsElim]

Jannis Limperg (Oct 31 2022 at 16:46):

@[elab_as_elim] for recent nightlies -- the naming convention for attributes has reverted to snake_case.

Arien Malec (Oct 31 2022 at 23:22):

The update in this adventure is that things are going mostly well:

theorem ext_iff {p q : Rat} : p = q  p.num = q.num  p.den = q.den := by
  cases p; cases q; simp

@[ext] theorem ext {p q : Rat} (hn : p.num = q.num) (hd : p.den = q.den) : p = q := Rat.ext_iff.mpr hn, hd

@[simp] theorem num_den :  {a : Rat}, mkRat a.num a.den = a
| n, d, h, (c:_=1)⟩ => show mkRat n d = _ by
  simp [mkRat,h,normalize, maybeNormalize,c]

theorem num_den' : (⟨n, d, h, c : Rat) = mkRat n d := num_den.symm

/-- Define a (dependent) function or prove `∀ r : Rat, p r` by dealing with rational
numbers of the form `mkRat n d` with `d ≠ 0` and coprime `n`, `d`. -/
@[elab_as_elim] def num_denom_cases_on {C : Rat  Sort u} :
  (a : Rat) (H :  n d, d  0  (n.natAbs).coprime d  C (mkRat n  d)), C a
 | n, d, h, c⟩, H => by rw [num_den']; exact H n d h c

 /-- Define a (dependent) function or prove `∀ r : Rat, p r` by dealing with rational
numbers of the form `n /. d` with `d ≠ 0`. -/
@[elab_as_elim] def num_denom_cases_on' {C : Rat  Sort u}
   (a : Rat) (H :  (n: Int) (d: Nat), d  0  C (mkRat n d)) : C a :=
num_denom_cases_on a <| fun n d h _ => H n d h

But things that should be easy like the analogue of

@[simp] theorem zero_mk (n) : 0 /. n = 0 :=
by cases n; simp [mk]

end up being terrifying.

Arien Malec (Nov 01 2022 at 04:47):

I'm close, I think.

After

@[simp] theorem mk_zero: (mkRat 0 n) = 0 := by
  cases n with
  | zero => simp [mkRat]
  | succ n => simp [mkRat, normalize, maybeNormalize, Int.natAbs, Nat.gcd_zero_left, Int.zero_div]

I'm down to:

case succ
n: Nat
 (if h : n = 0 then mk 0 (Nat.succ n) else mk 0 (Nat.succ n / Nat.succ n)) = 0

which, since I already handled the zero case in the first cases branch, and since Nat.succ n is always > 0, should resolve down to mk 0 1=0 which should close by rfl but I'm stuck in how to tell Lean that.

Kevin Buzzard (Nov 01 2022 at 06:56):

Assuming there's not yet a splitIfs tactic in lean 4, you want to do cases on n=0 and use if_pos and if_neg or whatever they're called in lean 4

Damiano Testa (Nov 01 2022 at 07:00):

There might be split_ifs

Scott Morrison (Nov 01 2022 at 07:22):

Yes, split_ifs landed in mathlib4#508.

Sebastian Ullrich (Nov 01 2022 at 11:44):

Is split_ifs mostly intended for porting and otherwise should be covered by core split (which also handles match) in most cases? It would be great if such overlaps would be discussed in the doc strings.

Scott Morrison (Nov 01 2022 at 13:21):

It is briefly mentioned in the doc-string at https://github.com/leanprover-community/mathlib4/pull/508/files#diff-42751ffdb8743d3ea4b619276a2600ccc8dd8476d972087dfcddb3bbfe52dc58R77.

Perhaps it would be worthwhile to go through the test file, and annotate the use cases for which the core split suffices.

Arien Malec (Nov 01 2022 at 14:42):

Now I see that I should have taken care of this case earlier.

That branch descends from
Nat.gcd (Int.natAbs 0) (Nat.succ n)=1 so it suffices to prove ∀ n, Nat.gcd (Int.natAbs 0) (Nat.succ n) ≠ 1

Arien Malec (Nov 01 2022 at 15:02):

Oh, but that's not true.

Arien Malec (Nov 01 2022 at 15:03):

It is, however, only true in the exact case where the theorem is true.

Mario Carneiro (Nov 01 2022 at 17:01):

You generally don't want to unfold multiple definitions in a single theorem, so this should be broken into multiple theorems. I came up with this:

import Std.Data.Rat

namespace Rat

attribute [simp] Int.ofNat_zero Int.ofNat_one

@[simp] theorem maybeNormalize_eq {num den g} (den_nz reduced) :
    maybeNormalize num den g den_nz reduced =
    { num := num / g, den := den / g, den_nz, reduced } := by
  unfold maybeNormalize <;> split
  · subst g; simp
  · rfl

@[simp] theorem normalize_zero (nz) : normalize 0 d nz = 0 := by
  simp [normalize, Int.zero_div, Int.natAbs_zero, Nat.div_self (Nat.pos_of_ne_zero nz)]; rfl

@[simp] theorem mk_zero : mkRat 0 n = 0 := by unfold mkRat; split <;> simp

Arien Malec (Nov 01 2022 at 17:21):

I love this!

Arien Malec (Nov 02 2022 at 18:58):

So update:

1) I hope my adventures here are useful -- aspirationally, I'd like to post a PR, but this may be beyond my capabilities at current levels of learning; less aspirationally, I'm hopeful that my struggles here in the differences between Lean 4 Std4 and mathlib are helpful for the eventual refactor and reconciliation -- if this is all distracting, I'm happy to self-mute
2) I realize now most of the heavy lifting in the core lemmas in mathlib is done in theorems like add_def that prove the behavior and invariants of the core operations and those go through lift_binop_eqwhich has a particularly hairy signature...
3) The signature of rat is in terms of int/nat with appropriate constraints on nonzero denominator, but the constructor goes mk_pnat and most of the /. heavy lifting is through rat.mk that is int -> int -> rat, and addressing that variation to Lean 4 makes signature modification for lift_binop_eq particularly hairy (that theorem assumes everything is int)

I think the pathway here is to recreate the mathlib equivalent for an Int -> Int -> Rat constructor, & try to port lift_binop_eq but happy to take any feedback....

Arien Malec (Nov 02 2022 at 19:11):

(FWIW, I think that core Std4.Rat should have the helper APIs and invariant lemmata on the core operations, and with that in place, proving the various algebraic lemmata in, say Std4.Rat.Basic would be pretty trivial.)


Last updated: Dec 20 2023 at 11:08 UTC