notations to introduce proofs

Stream: general

[Sebastien Gouezel]

In the following snippet,

lemma foo : (0 : ℕ) = 0 :=
begin
  have : (0 : ℕ) = 0        := by simp,
  have B:= calc (0 : ℕ) = 0 : by simp,
  show (0 : ℕ) = 0          , by simp
end

you can see that a proof after have is introduced by :=, after calc by : and after show by ,. And they can essentially not be used one for the other (the only allowed change is to use , instead of := on the first line). I am plainly used to it, but I would like to understand the rationale behind it. Is it to ease parsing? Or just for historical reasons? Would it make sense to use, say, := everywhere, to avoid confusing newcomers for no reason?

[Mario Carneiro]

Certainly calc would make sense with :=

[Mario Carneiro]

the commas in show and have are likely due to influence from Isar

[Mario Carneiro]

Of course you should be looking at term proofs not tactic proofs, which are at best an approximation of the term equivalents

[Mario Carneiro]

I'm not sure what notation Isar uses for let. Do you?

[Sebastien Gouezel]

There are no commas in Isar. The formula to be proved is enclosed in quotes, and then you give the proof. Either it is a direct proof, and then you just write something like using foo by auto. Or it is a complex proof, and it is enclosed in proof ... qed. The let equivalent is called define, and used like define foo where "foo = 0".

[Mario Carneiro]

interesting. That's more different than I expected. Has it changed significantly in the past 10 years?

[Mario Carneiro]

the base Isar syntax, I mean

[Mario Carneiro]

Maybe it is Mizar influence then?

[Sebastien Gouezel]

The definesyntax is a recent change, it used to be def "foo = 0".

[Mario Carneiro]

I was under the impression that the original term mode syntax of lean was basically lifted directly from the syntax of another language, probably Isar

[Mario Carneiro]

and it has since been simplified a bit but is otherwise unchanged

[Mario Carneiro]

like I think and have and hence used to exist and don't anymore

[Sebastien Gouezel]

Since formulas to be proved are enclosed in quotes in Isar, you don't a separator as in Lean. The comma makes sense, as would :=, but having two or three different separators depending on the context might be misleading to newcomers. Will it be uniformized in Lean 4, or is the syntax expected not to change?

[Mario Carneiro]

I think syntax changes like that are on the table

[Mario Carneiro]

I would be in support of using more :=

[Sebastien Gouezel]

I agree.

[Mario Carneiro]

and drop the from

[Mario Carneiro]

i.e. have A := proof in B or have A := by tac in B

[Mario Carneiro]

show A := proof

[Mario Carneiro]

calc A = B := proof ... = C := proof

[Mario Carneiro]

although I guess have in has the problem that it won't look like the tactic version which is have A := proof, tac

[Johannes Hölzl]

I would prefer to get rid of the in in let and just write let a := x, ...

[Rob Lewis]

I don't mind the from so much, it makes things read slightly more naturally. Although I'm sure I wouldn't miss it for long if it disappeared. I get more annoyed with the difference between term and tactic have.

[Johannes Hölzl]

and have h : A, by tac, ... or have h : A := ..., ...

[Mario Carneiro]

I think that have h : A := by tac, ... is more uniform. Putting a comma in there doesn't seem to win much

[Johannes Hölzl]

it would also be nice to have parameters for have and show:
have h (a : A) (b : B) : T := ..., ...

[Mario Carneiro]

short story: let and have should have the same parser

[Sebastien Gouezel]

and have h : A, by tac, ... or have h : A := ..., ...

So you would still use , to introduce a proof, and to separate a statement from the next. I think I would favor := to introduce proofs, and , to go to the next statement (removing in, as you say).

[Johannes Hölzl]

the comma would be just short form for tactic proofs.

[Mario Carneiro]

right, but I don't think that needs to be a thing

[Mario Carneiro]

like have h : A := by tac, ... and have h : A := begin end, ... are plenty short

[Johannes Hölzl]

hm, yes its short enough. and nicely uniform

[Patrick Massot]

what about have h : A := { ... },?

[Mario Carneiro]

preposterous

[Johannes Hölzl]

I guess it classes with set syntax

[Patrick Massot]

Then we would still have inconsistency with the goal focussing {...}

[Mario Carneiro]

just think of begin end as goal focussing brackets that work outside tactic mode

[Johannes Hölzl]

another dream: not only unify let and have but unify it also with def, i.e. allow to use the equation compiler in proofs, ala

have h : a \/ b -> c
| or.inl a := ...
| or.inr b := ...,
...

[Mario Carneiro]

mutual have ... with ... ?

[Mario Carneiro]

yeah this makes a lot more sense than named match

[Edward Ayers]

Is there a general notation wishlist thread?

[Mario Carneiro]

there is now

[Edward Ayers]

I would really like all of the bells and whistles you get with {!...!} to work with _ when it fails to fill in the proof. But I guess that's more of an editor feature.

[Sebastian Ullrich]

Lean 4 will most likely replace the hole syntax with _. Input to hole commands should be handled by the editor (which would've been basically impossible in Lean 3's infrastructure).

[Sebastien Gouezel]

Is there a general notation wishlist thread?

Another notation wish: as for rw I would like simp [←foo] to add reversed foo to the simpset. And possibly to remove foo if it is in the simpset. Currently, if foo has say two variables, I achieve this with simp[-foo, (foo _ _).symm].

[Patrick Massot]

New notation wishlist item: be able to replace, say in a parameter list, (n : { n : ℕ // 0 < n }) by (n : ℕ // 0 < n) (or, even better, (n : ℕ | 0 < n))

[Mario Carneiro]

is there a reason you aren't uskng two arguments?

[Mario Carneiro]

Also (n > 0) already does almost exactly what you are saying

[Patrick Massot]

It's not exactly the same. I can indeed modify my example to:

def euclid : Π (m : ℕ) (n > 0), {p : ℕ × ℕ // m = n*p.1 + p.2 ∧ p.2 < n}
| m n := λ n_pos,
         if h : m < n then
           ⟨(0, m), by simp *⟩
         else
           have m - n < m, by apply nat.sub_lt ; linarith,
           let ⟨⟨q, r⟩, ⟨H, H'⟩⟩ := euclid (m-n) n n_pos in
             ⟨(q+1, r),
              ⟨begin
                rw nat.sub_eq_iff_eq_add (le_of_not_lt h) at H,
                simp [H], ring,
               end, H'⟩⟩

but I still think the notation (n : nat | n > 0) in a parameter list would be good to have (and they have it in Coq).

[Patrick Massot]

By the way, the context is given by https://www.college-de-france.fr/site/xavier-leroy/seminar-2018-12-12-11h30.htm which shows programming with recursion and dependent pattern matching in Coq. They have all sorts of cool tricks in this area, including deferring proof obligations after writing the program, you can have a look at minute 51 to see their version of the above function. And of course they also have (q, r) : ℕ × ℕ instead of our p : ℕ × ℕ, and a linear arithmetic tactic doing everything :sad:

[Mario Carneiro]

You can defer proof obligations using refine

[Mario Carneiro]

Isn't this just the definition of div?

[Mario Carneiro]

you can have a look at how it's defined in core

[Mario Carneiro]

You can also write something with explicit binding for q,r but we try not to use it because it doesn't unfold as much

[Mario Carneiro]

you can do something like this (the notation isn't there, but you get the idea)

def euclid (m : ℕ) (n > 0) : @subtype (ℕ × ℕ) (λ ⟨q, r⟩, m = n*q + r ∧ r < n) := sorry

Unfortunately I think lean has a bug with generating names for the auxiliary match and it clashes with the let statement in the body

[Patrick Massot]

You can defer proof obligations using refine

It only defers a tiny bit. You need to close the goal before leaving the tactic block. DId you look at what Program does in this video? (you only have to look at the time I mentioned).

[Patrick Massot]

you can have a look at how it's defined in core

In core the output type does not assert correction. I'm not saying it should, I was doing an exercise.

[Patrick Massot]

you can do something like this (the notation isn't there, but you get the idea)

def euclid (m : ℕ) (n > 0) : @subtype (ℕ × ℕ) (λ ⟨q, r⟩, m = n*q + r ∧ r < n) := sorry

Unfortunately I think lean has a bug with generating names for the auxiliary match and it clashes with the let statement in the body

Can you use well founded recursion if m and n are left of colon?