Zulip Chat Archive

Stream: general

Topic: notation with unknown symbols

Patrick Massot (Apr 21 2018 at 15:16):

Is it possible to have notation using unknown symbols? Say I want a new notation for lambda abstraction (this is not my use case, I try to minimize). I try:

notation `mkfun` x `,` f := λ x, f
#check mkfun x, (x+1)

But it fails with unknown identifier 'x'

Gabriel Ebner (Apr 21 2018 at 15:18):

You might want to check out how the notation for ∃ is defined: https://github.com/leanprover/lean/blob/f59c2f0ef59fdc1833b6ead6adca721123bd7932/library/init/logic.lean#L532-L533

Patrick Massot (Apr 21 2018 at 15:19):

Thanks, it looks promising

Simon Hudon (Apr 21 2018 at 15:19):

It works with the binder / binders keywords and scoped

Patrick Massot (Apr 21 2018 at 15:20):

any chance this r:( thing is documented somewhere?

Patrick Massot (Apr 21 2018 at 15:20):

oh, binders is also a special word here?

Simon Hudon (Apr 21 2018 at 15:20):

Kevin and I had a long conversation about it on gitter. Let's see if I can find it again

Simon Hudon (Apr 21 2018 at 15:20):

yes

Simon Hudon (Apr 21 2018 at 15:24):

:point_up: January 10, 2018 5:21 PM

Simon Hudon (Apr 21 2018 at 15:27):

In short r:(...) gives a name to an expression that can be built in one of two ways:

scoped
foldl / foldr

In r:(scoped p, ...), p is a bound variable that you can use in .... It will be replaced with a lambda abstraction

Patrick Massot (Apr 21 2018 at 15:30):

It sorts of make sense, but not to the point where I could fix my mkfun example

Patrick Massot (Apr 21 2018 at 15:31):

oh wait

Patrick Massot (Apr 21 2018 at 15:31):

I can actually

Patrick Massot (Apr 21 2018 at 15:31):

notation `mkfun` binders `,` r:(scoped f, f) := r does work

Simon Hudon (Apr 21 2018 at 15:34):

So, if I may ask, why are you making fun of lambda abstractions?

Patrick Massot (Apr 21 2018 at 15:35):

I laughed. Do you also want an answer?

Simon Hudon (Apr 21 2018 at 15:35):

Both are appreciated :laughing:

Patrick Massot (Apr 21 2018 at 15:36):

I'm trying to setup some notations for sums and products

Patrick Massot (Apr 21 2018 at 15:37):

I would like to be able to write something like def f := λ n, Sum_{0 ≤ i ≤ n} i^2

Patrick Massot (Apr 21 2018 at 15:37):

I have no problem defining such a function

Patrick Massot (Apr 21 2018 at 15:38):

Using list.sum and list.range

Patrick Massot (Apr 21 2018 at 15:38):

I have trouble setting up the notation

Simon Hudon (Apr 21 2018 at 15:38):

Cool :) btw, would it be useful to you to have a notation for classical.epsilon: ε x, 1 ≤ x ≤ 3?

Kenny Lau (Apr 21 2018 at 15:38):

not sure how easy it would be to implement it

Kenny Lau (Apr 21 2018 at 15:38):

I mean, what are you going to produce when there is no such element

Kenny Lau (Apr 21 2018 at 15:39):

in classical Hilbert epsilon it is supposed to produce "whatever"

Simon Hudon (Apr 21 2018 at 15:40):

classical.epsilon already exists. It's only defined on nonempty types. When no such x exists, an arbitrary value is picked

Kenny Lau (Apr 21 2018 at 15:40):

but then it is empty

Kenny Lau (Apr 21 2018 at 15:40):

what is going to be the type of the output

Simon Hudon (Apr 21 2018 at 15:41):

@Patrick Massot Do you have a special provision for infinite sets in Sum_{ ... }?

Patrick Massot (Apr 21 2018 at 15:42):

I was thinking about finite sums here

Patrick Massot (Apr 21 2018 at 15:43):

Really I want to convert

open data.list.basic
open list
def f := λ (n : ℕ), sum (map (λ i, i*i) (range n))

to what I wrote earlier

Patrick Massot (Apr 21 2018 at 15:43):

having a nice notation

Patrick Massot (Apr 21 2018 at 15:44):

where the name of the bound variable i is not hard-wired in the notation

Simon Hudon (Apr 21 2018 at 15:45):

@Kenny Lau here is the type of epsilon:

noncomputable def epsilon {α : Sort u} [h : nonempty α] (p : α → Prop) : α :=

Kenny Lau (Apr 21 2018 at 15:46):

oh, I misinterpreted everything

Simon Hudon (Apr 21 2018 at 15:47):

@Patrick Massot
How about this as the underlying function:

sum : ℕ → (ℕ → Prop) → (ℕ → α) → α := ...

Basically, the notation should be hardwired to fix an upper bound on the range

Simon Hudon (Apr 21 2018 at 15:48):

but you still get to filter individual terms

Patrick Massot (Apr 21 2018 at 15:51):

I don't really care about the underlying function. I want my notation with only the formula in term of i, not prefaced with a lambda

Simon Hudon (Apr 21 2018 at 15:52):

One step at a time, young padawan, I'm getting there

Patrick Massot (Apr 21 2018 at 15:59):

I'm making progress

notation `Sum_{` binders `≤` n `}` r:(scoped f, f) := sum (map f $ range n)
#eval Sum_{ (i : ℕ) ≤ 4} i*i

Simon Hudon (Apr 21 2018 at 16:01):

Not bad!

Simon Hudon (Apr 21 2018 at 16:02):

I was trying:

notation `ΣΣ ` binder ` | ` f:(scoped x, x) ∧ ub:(scoped x, x) ` ≤ ` n `, ` t:(scoped x, x) :=
sum' n f t

example : (ΣΣ x | 0 ≤ x ∧ x ≤ 7, f x) ≤ 7 := _

But I think you're not allowed to use scoped so many times.

Patrick Massot (Apr 21 2018 at 16:02):

I can even replace (i : ℕ) by (i) but not by i

Simon Hudon (Apr 21 2018 at 16:03):

Not i? What error does it give you?

Patrick Massot (Apr 21 2018 at 16:04):

invalid expression

Simon Hudon (Apr 21 2018 at 16:05):

That's intriguing. You may want to try giving precedences to the tokens: ` ≤ `:0

Simon Hudon (Apr 21 2018 at 16:06):

I'll catch up with you later. There an adorable 2 year old here who needs attention :)

Patrick Massot (Apr 21 2018 at 16:06):

Too bad, I was hoping your nephew was also a Lean expert

Patrick Massot (Apr 21 2018 at 16:06):

Have fun!

Simon Hudon (Apr 21 2018 at 16:07):

He's more of an Idris kind of guy

Patrick Massot (Apr 21 2018 at 16:07):

:smile:

Simon Hudon (Apr 21 2018 at 16:07):

His name is Idris but I assume that speaks to his parents preference of Idris over Agda and Lean

Simon Hudon (Apr 21 2018 at 16:08):

And not to the sexiness of Idris Elba :stuck_out_tongue_winking_eye:

Patrick Massot (Apr 21 2018 at 20:07):

Does anyone has a decidable predicate on nat at hand?

Chris Hughes (Apr 21 2018 at 20:09):

pos

Chris Hughes (Apr 21 2018 at 20:09):

Any predicate?

Chris Hughes (Apr 21 2018 at 20:10):

(λ n : ℕ, true) :-)

Patrick Massot (Apr 21 2018 at 20:10):

Maybe somethin like even or odd exist somewhere and is decidable

Patrick Massot (Apr 21 2018 at 20:10):

I need a decidable instance in the library

Sebastian Ullrich (Apr 21 2018 at 20:10):

Fun fact: Idris has an Elab monad. Have you ever tried googling for "idris elab"?

Reid Barton (Apr 21 2018 at 20:11):

there's prime, in data.nat.prime

Chris Hughes (Apr 21 2018 at 20:11):

even is decidable, if you define it as n % 2 = 0

Chris Hughes (Apr 21 2018 at 20:13):

@Reid Barton I couldn't manage to use that instance to prove 3 is prime.

Simon Hudon (Apr 21 2018 at 20:13):

@Patrick Massot I did some more experiment and I managed to define a syntax for ΣΣ i, i ≥ 3 ∧ i < 21 ∧ even i ▻ i^2 which guarantees that i is bounded. How do you like the notation? (I made the formula a bit ugly to demonstrate that the form is pretty flexible)

Patrick Massot (Apr 21 2018 at 20:15):

#eval if nat.prime 3 then 1 else 0 does work here

Patrick Massot (Apr 21 2018 at 20:15):

thanks

Chris Hughes (Apr 21 2018 at 20:17):

example : 1 = if nat.prime 3 then (1 : ℕ) else (0 : ℕ) := rfl doesn't work though unfortunately. It does work for 2 though

Patrick Massot (Apr 21 2018 at 20:28):

My current achievements are at https://github.com/PatrickMassot/lean-scratchpad/blob/master/src/bigop.lean

Patrick Massot (Apr 21 2018 at 20:29):

I still has precedence issues

Patrick Massot (Apr 21 2018 at 20:29):

But I'm already happy

Patrick Massot (Apr 21 2018 at 20:29):

I have quite a lot of ways of computing 5!

Patrick Massot (Apr 21 2018 at 20:30):

And I seems I was able to state a lemma about big product for an associative operator and apply it to addition in nat

Patrick Massot (Apr 21 2018 at 20:31):

For those who didn't follow previous discussions, I'm going after http://hal.inria.fr/docs/00/33/11/93/PDF/main.pdf

Simon Hudon (Apr 21 2018 at 20:31):

Nice!

Simon Hudon (Apr 21 2018 at 20:31):

If you're interested, I've put my code here:

https://gist.github.com/cipher1024/604d5ec28ceb29e80219ce6e69bb1ea4

Mario Carneiro (Apr 21 2018 at 20:32):

Hopefully this will be resolved in lean 4 (@Sebastian Ullrich vm replacements please) but right now you have to make a choice between VM efficient and kernel efficient. decidable_prime_1 is kernel efficient and decidable_prime is VM efficient

Mario Carneiro (Apr 21 2018 at 20:32):

the default one you get is decidable_prime

Patrick Massot (Apr 21 2018 at 20:33):

https://github.com/PatrickMassot/lean-scratchpad/blob/master/src/bigop.lean#L67 has no trouble suming primes numbers in range 5

Patrick Massot (Apr 21 2018 at 20:33):

That's scientific computing!

Sebastian Ullrich (Apr 21 2018 at 20:35):

Lean 4 will use a simplifier on code to be compiled, which should also enable VM replacements

Patrick Massot (Apr 21 2018 at 20:42):

What is the precedence voodoo I need to get rid of parentheses in https://github.com/PatrickMassot/lean-scratchpad/blob/master/src/bigop.lean#L71 ? I mean, everything on LHS of the equality is surrounded in parenthesis, otherwise it doesn't work. How to avoid that?