show_term bug?

Stream: batteries

[Heather Macbeth]

Is the following known: show_term producing a term which doesn't seem to work?

import Std.Data.Rat.Lemmas

example : (1:Rat) + 1 = 2 := show_term by rfl
-- Try this: Eq.refl (1 + 1)

example : (1:Rat) + 1 = 2 := Eq.refl (1 + 1)
/-
type mismatch
  Eq.refl (1 + 1)
has type
  1 + 1 = 1 + 1 : Prop
but is expected to have type
  1 + 1 = 2 : Prop
-/

[Heather Macbeth]

Update: It seems that this is not so much a show_term issue, as an issue that the tactic rfl can check defeq of irreducible things even though the term proof rfl would fail:

structure Int2 where
  val : Int

instance : OfNat Int2 n := ⟨{ val := n }⟩

@[irreducible]
def Int2.add (a b : Int2) : Int2 := { val := a.val  + b.val  }

example : Int2.add (1:Int2) 1 = 2 := rfl -- fails
/-
type mismatch
  rfl
has type
  Int2.add 1 1 = Int2.add 1 1 : Prop
but is expected to have type
  Int2.add 1 1 = 2 : Prop
-/

def foo : Int2.add (1:Int2) 1 = 2 := by eq_refl -- works

#print foo
/-
def foo : Int2.add 1 1 = 2 :=
Eq.refl (Int2.add 1 1)
-/

[Heather Macbeth]

This behaviour is rather surprising to me, but maybe one of the devs can explain whether it is intended behaviour.

[Heather Macbeth]

Further update: it looks like this is the raison d'être of the Mathlib irreducible_def command, which I had never appreciated before. Should that command perhaps be upstreamed so that Rat.add can be defined with irreducible_def?

[Heather Macbeth]

import Mathlib.Tactic.IrreducibleDef

example : (1:Rat) + 1 = 2 := rfl -- fails
example : (1:Rat) + 1 = 2 := by rfl -- works

irreducible_def Rat.add' := Rat.add
instance : Add Rat := ⟨Rat.add'⟩

example : (1:Rat) + 1 = 2 := rfl -- fails
example : (1:Rat) + 1 = 2 := by rfl -- fails

[Heather Macbeth]

Also: should show_term include a test that the term produced indeed elaborates (and print a warning message if it doesn't)?

[Mario Carneiro]

This is expected behavior. Although it is rare, in general terms produced by tactics don't necessarily re-check in the elaborator, they are supposed to be valid for the kernel and that ignores @[irreducible] annotations

[Mario Carneiro]

You can address this by using by with_unfolding_all exact before the proof