Zulip Chat Archive

Stream: lean4

Topic: Possible bug from Elim0 on Fin


zbatt (Aug 02 2022 at 15:27):

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 (Aug 02 2022 at 15:33):

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 (Aug 02 2022 at 15:35):

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 (Aug 02 2022 at 15:38):

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 (Aug 02 2022 at 15:45):

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 (Aug 02 2022 at 15:45):

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

zbatt (Aug 02 2022 at 15:52):

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 (Aug 03 2022 at 00:03):

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.


Last updated: Dec 20 2023 at 11:08 UTC