Possible bug from Elim0 on Fin

Stream: lean4

[zbatt]

I came across what i think might be a bug so I thought I should report it. There's a good amount of depenencies so I'm not sure how to share it other than a screenshot for now Screenshot_2022-08-02_11-20-44.png

Clearly the issue is I have z : 1 = 0 but it's not letting me exact it for a goal 1 = 0. What's interesting though is something like

def foo (x : Fin 0) : 1 = 0 :=
  by
    exact @FinElim0 (λ _ => 1 = 0) x

has no issues, so I'm not sure what's causing the issue. Just thought I should share :D (and sorry if it's not actually a bug)

[Henrik Böving]

Are you sure that the 1 and the 0 in both types are the same? I.e. not one Nat and one Fin? You can check this by set_option pp.explicit true above your theorem

[zbatt]

Henrik Böving said:

Are you sure that the 1 and the 0 in both types are the same? I.e. not one Nat and one Fin? You can check this by set_option pp.explicit true above your theorem

Ah yes that was it. It wanted @Eq Float 1 0 but I was providing @Eq Nat 1 0. Apologies for misreporting!

[Henrik Böving]

No it is still a bug, although a usability one.

My suggestion for this would be: If we report a type mismatch and notice that the two Exprs pretty print to the same string do also re-pretty-print them with pp.explicit set so the users can instantly see the difference.

CC: @Sebastian Ullrich

[Sebastian Ullrich]

I cannot reproduce that

example (h : (1 : Float) = 0) : (1 : Nat) = 0 := h

type mismatch
  h
has type
  @OfNat.ofNat Float 1 instOfNatFloat = 0 : Prop
but is expected to have type
  @OfNat.ofNat Nat 1 (instOfNatNat 1) = 0 : Prop

[Sebastian Ullrich]

IOW, we should already do that, but you should file an #mwe as an issue

[zbatt]

I'm not sure this is minimal, but this is sufficient to cause it

def foo (h : (1 : Float) = 0) : (1 : Nat) = 0 :=
  by
    have z := h
    exact z

I'd be more than happy to submit an issue on the the lean4 github, but admittedly I'm not entirely sure if there's some sort of procedure for that other than just submitting it haha

[Mac]

zbatt said:

I'm not entirely sure if there's some sort of procedure for that other than just submitting it haha

Nope, just submit away! When a create a new issue, it will start you with a template to follow and you should try to fill it in, but other than that there is no special process.