Zulip Chat Archive

Stream: new members

Topic: desugaring have


view this post on Zulip Olli (Sep 02 2018 at 19:49):

https://gist.github.com/luxbock/f0c19afd8d88fef9c13814ba072b9eb5

Can anyone explain what I'm doing wrong? I tried adding parentheses in different places but couldn't make it work

view this post on Zulip Etienne Laurin (Sep 02 2018 at 19:59):

I think you need to add parenthesis around (and.right h) and (and.left h)

view this post on Zulip Reid Barton (Sep 02 2018 at 20:00):

In this case around and.left h

view this post on Zulip Reid Barton (Sep 02 2018 at 20:00):

You need parentheses around the argument of a function. f x y means (f x) y

view this post on Zulip Olli (Sep 02 2018 at 20:01):

thanks, yeah that did it

view this post on Zulip Olli (Sep 04 2018 at 20:11):

https://gist.github.com/luxbock/0e19b04aaca49ccf18e5df060d2d3e8e

same as last time, except now I feel fairly confident that I should have got this right, but I don't understand why it's not able to infer the right types for the disjunction. I realize this is probably not how you'd ever write things, but nevertheless am I doing something wrong here?

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 20:55):

I get a gazillion errors when I copy paste

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 21:03):

but apart from that, as I'm sure you know, the problem is that or.inl hq doesn't have enough information to know it's a proof of q or r.

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 21:03):

Here are two ways to fix it: for the first error, replace the offending line with and.intro hp (@or.inl q r hq)) i.e. use the @ trick and tell Lean the implicit variables yourself

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 21:04):

For the second line, you could write and.intro hp (or.inr hr : q ∨ r)) , i.e. tell Lean the type you want it to be.

view this post on Zulip Olli (Sep 05 2018 at 06:59):

thanks, that does indeed work.

The reason I find this confusing is because based on reading the tutorial, I thought that have would desugar as I wrote it. It should have all the same information compared writing it with have.

view this post on Zulip Kevin Buzzard (Sep 05 2018 at 07:31):

My non-expert guess as to what is going on is this. Lean sometimes doesn't have enough information to work out what the type of something is (e.g. when you type or.inr hr). When this happens it inserts a metavariable instead (e.g. ?m_1[hpr, _, _]). You talk about desugaring, but I think the process which is behaving differently in the two cases is the elaboration process, when these metavariables get solved. Elaboration is a complicated thing and depends on a lot of stuff going on in the background, for example whether various terms are tagged elab_simple or elab_as_eliminator or whatever -- even changing the way you apply a function f {a} b from f b to @f _ b can (and often does) change the elaboration strategy. In short, I don't think this is about desugaring, it's about the complex elaboration process which goes on behind the scenes after that.

view this post on Zulip Olli (Sep 05 2018 at 09:54):

yeah it was a good exercise to do, because I learned something from it


Last updated: May 16 2021 at 05:21 UTC