desugaring have

Stream: new members

[Olli]

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

[Etienne Laurin]

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

[Reid Barton]

In this case around and.left h

[Reid Barton]

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

[Olli]

thanks, yeah that did it

[Olli]

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?

[Kevin Buzzard]

I get a gazillion errors when I copy paste

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Olli]

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.

[Kevin Buzzard]

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.

[Olli]

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