how to explicitly rfl for ℚ?

Stream: new members

[Yongyi Chen]

Let's say you want to prove

example : (1 / 3 : ℚ) + 2 / 3 = 1

without any tactics. Now, the tactic by rfl works and expands using by? to Eq.refl (1 / 3 + 2 / 3) but unfortunately this does not type check in Lean.
Of course, 1/3 + 2/3 as output by the pretty printer is not the right expression, because those literals being interpreted in the world of naturals, so I tried Eq.refl ((1 / 3 : ℚ) + 2 / 3) instead. Still nope.

by linarith and by norm_num expand to horrible messes which, unfortunately, suffer from the same Eq.refl issues as above.

[Yongyi Chen]

Interestingly, by decide does not work here. Must be a recent breakage, or am I dreaming?

[Eric Wieser]

I assume your question is this:

import Mathlib.Data.Rat.Basic

example : (1 / 3 : ℚ) + 2 / 3 = 1 := by show_term rfl -- works
example : (1 / 3 : ℚ) + 2 / 3 = 1 := Eq.refl ((1 / 3 : ℚ) + 2 / 3) -- fails: why?
example : (1 / 3 : ℚ) + 2 / 3 = 1 := rfl -- fails: why?

[Eric Wieser]

That is, why by rfl succeeds but seems to generate a term that fails on its own

[Yongyi Chen]

Well, kind of. As in, I'm familiar with the terms generated by show_term often failing, and that might be a whole (already known) question on its own, but my specific question here is how to actually prove the equality with a term.

[Eric Wieser]

example : (1 / 3 : ℚ) + 2 / 3 = 1 := by with_unfolding_all exact rfl works

[Yongyi Chen]

Apparently that just show_terms to rfl which does not work, sadly.

[Eric Wieser]

Right, the point is that the term is valid from the kernel's point of view, but the elaborator has to be tricked via with_unfolding_all

[Yongyi Chen]

Oh, I see. So rfl technically is valid but doesn't compile because something was marked as irreducible? So I guess there is no reasonable (without going into tactic mode) term that can prove that 1/3 + 2/3 = 1?

[Eric Wieser]

It seems like you have to go into tactic mode, turn off irreducibility checking, then go back into term mode; the rfl in my proof is the term-mode rfl

[Eric Wieser]

Though something very strange does seem to be happening here; I can't work out where Lean is recording the decision to ignore reducibility

[Eric Wieser]

I couldn't get this to work:

elab "with_unfolding_all% " y:term : term <= expectedType =>
  withTransparency TransparencyMode.all <| (Lean.Elab.Term.elabTerm y expectedType)

example : (1 / 3 : ℚ) + 2 / 3 = 1 := with_unfolding_all% rfl -- fails

[Kyle Miller]

If your goal has no free variables, the eq_refl tactic uses the kernel checker rather than the elaborator's:

example : (1 / 3 : ℚ) + 2 / 3 = 1 := by eq_refl

[Yongyi Chen]

That's basically what rfl calls, right?

macro "rfl" : tactic => `(tactic| eq_refl)

[Kyle Miller]

@Eric Wieser I'm guessing with your example that the example command is itself ensuring that the term has the right type. You can insert a type hint:

example : (1 / 3 : ℚ) + 2 / 3 = 1 := with_unfolding_all% id rfl

(You can also get your elaborator to insert a type hint, via an id, with mkExpectedTypeHint)

[Kyle Miller]

@Yongyi Chen I forgot that rfl was different from exact rfl. I think I learned about eq_refl from a thread where I learned and immediately forgot that.

[Yongyi Chen]

So after thinking about this, I think that Rat.add and siblings should not be marked as irreducible, so that simp and decide and rfl can work properly. (Currently simp won't even simplify rational expressions.)

[Eric Wieser]

Note that norm_num works fine here, though that isn't necessarily an argument for keeping the irreducibility

[Eric Wieser]

(simp can't reasonably be expected to work here, it's not possible to write a lemma that matches arbitrary pairs of digits)

[Yongyi Chen]

Eric Wieser said:

(simp can't reasonably be expected to work here, it's not possible to write a lemma that matches arbitrary pairs of digits)

I guess so, since simp doesn't simplify (1 : ℤ) + (2 : ℤ) either.

[Eric Rodriguez]

decide should work regardless of irreducibility I thought

[Yongyi Chen]

Doesn't! But if I make a local copy of the Rat file and remove the irreducible modifiers on mul and inv, then it does.

[Yongyi Chen]

By the way, I solved the original task!

theorem ddd : (1 / 3 : ℚ) + 2 / 3 = 1 := Rat.div_def 1 _ ▸ Rat.div_def 2 _ ▸ Rat.inv_def _ ▸ Rat.mul_def _ _ ▸ Rat.mul_def 2 _ ▸ Rat.add_def' _ _ ▸ rfl

[Eric Wieser]

Eric Rodriguez said:

decide should work regardless of irreducibility I thought

decide relies on the decidability instance being sufficiently reducible in some way

[Kevin Buzzard]

I don't see the logic in changing reducibility settings just so rfl can do a job which norm_num was designed to do...

[Eric Wieser]

But nor do I think that "norm_num doesn't care" is a good answer to "why are Rat operations irreducible?"

[Yongyi Chen]

I see linarith and norm_num as sledgehammers for the purpose of deciding equality of easily decidable things like integers and rationals, mainly because they produce very long (and slow) code under the hood.

[Ruben Van de Velde]

norm_num is the minimal supported approach to proving things about concrete numbers

[Ruben Van de Velde]

If there's ways in which it's suboptimal, it's better to improve it rather than trying to work around it

[Yongyi Chen]

I don't think this is an argument for why decide should fail to decide that two rational numbers are equal.

[Kyle Miller]

norm_num isn't a sledgehammer tactic though -- it just evaluates numeric expressions, and its aim is to generate efficient proofs of the correctness of the evaluation.

[Kyle Miller]

There are cases where norm_num is faster than rfl because it knows a better way to compute a function than by appealing to its definition.

[Kyle Miller]

(I know that it used to be that because GCD is defined using well-founded recursion that you couldn't really prove anything about it by rfl, but it seems that examples like example : Nat.gcd 15 25 = 5 := rfl work now. I'm not sure what the status is for whether that being provable by rfl is meant to be supported.)

[Kyle Miller]

I agree that using linarith to prove equalities about concrete rationals is overkill.

[Kyle Miller]

Eric Rodriguez said:

decide should work regardless of irreducibility I thought

The DecidableEq instance for Rat is basically that to prove p = q then see if (rfl : p.num = q.num) and (rfl : q.den = q.den) typecheck. That means whatever is going on in p and q have to be reducible enough.

[Kyle Miller]

I'm pretty sure that for equalities of naturals, integers, and rationals that decide has no special powers that rfl doesn't already have...

[Yongyi Chen]

So Rat derives from DecidableEqbut yet...

example {x : ℚ} : (4 / 2 : ℚ) = 2 := by
  /-
  failed to reduce to 'true'
    Decidable.rec (fun h => (fun x => false) h) (fun h => (fun x => true) h) (instDecidableEqRat (4 / 2) 2)
  -/
  decide

[Yongyi Chen]

This contradicts what the docs say on Decidable:

If a proposition p is Decidable, then (by decide : p) will prove it by evaluating the decidability instance to isTrue h and returning h.

[Kyle Miller]

Right, like I said it depends on checking that rfl can prove that the numerators and denominators are equal.

[Kyle Miller]

This fails:

example {x : ℚ} : (4 / 2 : ℚ).num = (2 : ℚ).num := rfl

so decide fails.

[Kyle Miller]

There's generally no point in using decide to prove equalities of naturals, integers, and rationals since it's a more roundabout rfl. I'm pretty sure there are no exceptions here.

[Kyle Miller]

Yongyi Chen said:

This contradicts what the docs say on Decidable: [...]

There's no contradiction. It failed to evaluate the decidable instance to isTrue. The word "evaluate" might not be good here though, since "reduce" is would be more precise.

[Kyle Miller]

When I hear "evaluate" I think about #eval. Decidable instances can always be evaluated that way, but they don't generate proofs in that case.

#eval decide ((4 / 2 : ℚ) = 2)
-- true

[Yongyi Chen]

So to summarize, for equalities of rational numbers involving literals,
by rfl, by norm_num work, while
rfl ( = by exact rfl), by decide, and by aesop don't work,
and everyone but me agrees this is how it should be?

[Kyle Miller]

I'd say by rfl accidentally works, since it's circumventing transparency settings by using the kernel defeq checker.

[Kyle Miller]

And this is how it should be in the sense that the designers of Rat made the actual definitions of the arithmetic operations be behind the API.

[Yaël Dillies]

Not sure why you would expect aesop to work here

[Yongyi Chen]

Kyle Miller said:

There's no contradiction. It failed to evaluate the decidable instance to isTrue. The word "evaluate" might not be good here though, since "reduce" is would be more precise.

OK, I think I thought too naively what Decidable means. So for example there is a term of type Decidable (BB(9001) = 0) as well (I think?)

[Yongyi Chen]

Yaël Dillies said:

Not sure why you would expect aesop to work here

To me it seems more surprising a tool like aesopcouldn't do this.

[Yaël Dillies]

aesop does logic puzzles. Computing is not a logic puzzle

[Kyle Miller]

If reducing Nat.gcd in the kernel is now reliable (which by my recollection it wasn't before) maybe the arithmetic operations' definitions could be made semireducible rather than irreducible. However, I do not know if rfl proofs for rationals are actually efficient. I wouldn't be surprised if the norm_num ones typecheck faster.

[Kyle Miller]

@Yaël Dillies Doesn't aesop use simp? Couldn't it use norm_num?

[Kyle Miller]

(I actually don't know if aesop uses simp or not)

[Yongyi Chen]

About norm_num:

theorem thirds_inefficient : (1 / 3 : ℚ) + 2 / 3 = 1 := by norm_num

expands to

theorem thirds_inefficient : (1 / 3 : ℚ) + 2 / 3 = 1 := of_eq_true
  (eq_true
    (Mathlib.Meta.NormNum.isNat_eq_true
      (Mathlib.Meta.NormNum.IsInt.to_isNat
        (Mathlib.Meta.NormNum.IsRat.to_isInt
          (Mathlib.Meta.NormNum.isRat_add (Eq.refl HAdd.hAdd)
            (Mathlib.Meta.NormNum.isRat_div
              (Mathlib.Meta.NormNum.isRat_mul (Eq.refl HMul.hMul)
                (Mathlib.Meta.NormNum.IsNat.to_isRat
                  (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1)))
                (Mathlib.Meta.NormNum.isRat_inv_pos
                  (Mathlib.Meta.NormNum.IsNat.to_isRat
                    (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 3))))
                (Eq.refl (Int.mul (Int.ofNat 1) (Int.ofNat 1))) (Eq.refl 3)))
            (Mathlib.Meta.NormNum.isRat_div
              (Mathlib.Meta.NormNum.isRat_mul (Eq.refl HMul.hMul)
                (Mathlib.Meta.NormNum.IsNat.to_isRat
                  (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 2)))
                (Mathlib.Meta.NormNum.isRat_inv_pos
                  (Mathlib.Meta.NormNum.IsNat.to_isRat
                    (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 3))))
                (Eq.refl (Int.mul (Int.ofNat 2) (Int.ofNat 1))) (Eq.refl 3)))
            (Eq.refl (Int.ofNat 9)) (Eq.refl 9))))
      (Mathlib.Meta.NormNum.isNat_ofNat ℚ (Eq.refl 1))))

with typecheck errors on two of the (Eq.refl 3) terms complaining of an application type mismatch.

[Yaël Dillies]

aesop does use simp as a preprocessing step (every time a rule is applied!). I guess norm_num could be plugged in there too.

[Kyle Miller]

1. Pretty printing unfortunately fails to round-trip too often. That's the only thing you can infer from Eq.refl 3 causing typechecking failures.
2. The proof looks big, but that doesn't mean it's slow to typecheck. These norm_num proofs are set up so that defeq checks are trivial, except for places where it's doing Nat computations.

[Yaël Dillies]

Yongyi, that doesn't mean much, really. It just means that "pretty-printing doesn't round-trip", namely you can't trust the printing of an expression to elaborate back to that expression.

[Yaël Dillies]

It's also pretty big just because every lemma is prefixed with Mathlib.Meta.NormNum, so :shrug:

[Yongyi Chen]

I think, as in the examples at the start of this conversation, there isn't an actual term similar to this that type-checks. Because I think the Eq.refl errors are the same seeing-through-irreducibility issues as earlier.

[Kyle Miller]

Yongyi Chen said:

I think the Eq.refl errors are the same seeing-through-irreducibility issues as earlier.

This is false. These are Nat refls.

[Yongyi Chen]

Oh, OK. So for the error

argument
  Eq.refl 3
has type
  3 = 3 : Prop
but is expected to have type
  Nat.mul 1 (Nat.succ 2) = Nat.mul 1 ?m.7106 : Prop

what should go instead of Eq.refl 3?

[Kyle Miller]

The problem is that the elaborator isn't able to elaborate the pretty printed term, and it could be because of any number of things, most likely missing implicit arguments.

[Kyle Miller]

The pretty printing "sledgehammer" is setting set_option pp.all true. That one typechecks, I've verified it just now.

[Kyle Miller]

But to "what should go instead of Eq.refl 3", I'd say "nothing, delete that whole proof term and use norm_num"

[Yongyi Chen]

Kyle Miller said:

The pretty printing "sledgehammer" is setting set_option pp.all true. That one typechecks, I've verified it just now.

Oh! That's useful. Also verified it on my end.

[Yongyi Chen]

Yaël Dillies said:

It's also pretty big just because every lemma is prefixed with Mathlib.Meta.NormNum, so :shrug:

With open Mathlib.Meta.NormNum I guess it's not so bad anymore

theorem thirds_inefficient : (1 / 3 : ℚ) + 2 / 3 = 1 := of_eq_true
  (eq_true
    (isNat_eq_true
      (IsInt.to_isNat
        (IsRat.to_isInt
          (isRat_add (Eq.refl HAdd.hAdd)
            (isRat_div
              (isRat_mul (Eq.refl HMul.hMul) (IsNat.to_isRat (isNat_ofNat ℚ (Eq.refl 1)))
                (isRat_inv_pos (IsNat.to_isRat (isNat_ofNat ℚ (Eq.refl 3))))
                (Eq.refl (Int.mul (Int.ofNat 1) (Int.ofNat 1))) (Eq.refl 3)))
            (isRat_div
              (isRat_mul (Eq.refl HMul.hMul) (IsNat.to_isRat (isNat_ofNat ℚ (Eq.refl 2)))
                (isRat_inv_pos (IsNat.to_isRat (isNat_ofNat ℚ (Eq.refl 3))))
                (Eq.refl (Int.mul (Int.ofNat 2) (Int.ofNat 1))) (Eq.refl 3)))
            (Eq.refl (Int.ofNat 9)) (Eq.refl 9))))
      (isNat_ofNat ℚ (Eq.refl 1))))

which I guess has similar structure to my hand-crafted

theorem thirds : (1 / 3 : ℚ) + 2 / 3 = 1 := div_def 1 _ ▸ div_def 2 _ ▸ inv_def _ ▸ mul_def _ _ ▸ mul_def 2 _ ▸ add_def' _ _ ▸ rfl

[Kyle Miller]

And it might elaborate faster than yours, since ▸ is hiding some automation.

[Yongyi Chen]

So it does. 35 ms for mine and 20 ms for norm_num. Wow!

[Kyle Miller]

So make sure to profile things before assuming they're inefficient :smile:

[Kyle Miller]

(That's still really slow for just adding two rational numbers of course, but adding rationals usually isn't in the hot path for theorem proving)

[Yongyi Chen]

True, by rfl or by eq_refl is a 5 ms typecheck

[Kyle Miller]

For larger examples, the difference between by rfl and by norm_num goes down.

-- 0.0138 s
example : (1/10001 + 1/10002 + 1/10003 + 1/10004 + 1/10005 : ℚ) = 2781112528027793/5563893612361263340 := by rfl
-- 0.0185 s
example : (1/10001 + 1/10002 + 1/10003 + 1/10004 + 1/10005 : ℚ) = 2781112528027793/5563893612361263340 := by norm_num

[Yongyi Chen]

How long does a sorry take there?

[Kyle Miller]

Too little time for set_option trace.profiler true to report it

[Yongyi Chen]

Oh very interesting! sorrythere takes over 100 ms to elaborate on my Windows machine. Let me dual-boot and see if it's a Windows issue.

[Kyle Miller]

There's a lot of noise in these measurements, so my method is to set up the three examples and then insert some whitespace before the first example to get them to all re-elaborate

[Kyle Miller]

When I first created the sorry example it was measureable on its own (at 300ms or so), but then after that it stopped being measurable.

[Kyle Miller]

Maybe it's something with the process of typing out sorry putting a lot of pressure on the elaborator due to repeated re-elaboration on each keystroke?

[Yongyi Chen]

Haha it was something stupid on my part. The section I was working in had variables for modules and other high-complexity objects. Going into a fresh file and using #time shows a timing of around 13ms for sorrys

[Kyle Miller]

Oh, yeah, variable bindings get re-elaborated for every declaration from scratch

[Yongyi Chen]

Results: 13 ms for sorry, 20 ms for rfl, and 29 ms for norm_num