## Stream: general

### Topic: notations to introduce proofs

#### Sebastien Gouezel (Oct 15 2018 at 08:17):

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 (Oct 15 2018 at 08:21):

Certainly calc would make sense with :=

#### Mario Carneiro (Oct 15 2018 at 08:21):

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

#### Mario Carneiro (Oct 15 2018 at 08:22):

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

#### Mario Carneiro (Oct 15 2018 at 08:22):

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

#### Sebastien Gouezel (Oct 15 2018 at 08:27):

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 (Oct 15 2018 at 08:29):

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

#### Mario Carneiro (Oct 15 2018 at 08:29):

the base Isar syntax, I mean

#### Mario Carneiro (Oct 15 2018 at 08:29):

Maybe it is Mizar influence then?

#### Sebastien Gouezel (Oct 15 2018 at 08:31):

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

#### Mario Carneiro (Oct 15 2018 at 08:32):

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 (Oct 15 2018 at 08:32):

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

#### Mario Carneiro (Oct 15 2018 at 08:33):

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

#### Sebastien Gouezel (Oct 15 2018 at 08:34):

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 (Oct 15 2018 at 08:36):

I think syntax changes like that are on the table

#### Mario Carneiro (Oct 15 2018 at 08:36):

I would be in support of using more :=

I agree.

#### Mario Carneiro (Oct 15 2018 at 08:37):

and drop the from

#### Mario Carneiro (Oct 15 2018 at 08:38):

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

#### Mario Carneiro (Oct 15 2018 at 08:38):

show A := proof

#### Mario Carneiro (Oct 15 2018 at 08:40):

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

#### Mario Carneiro (Oct 15 2018 at 08:41):

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 (Oct 15 2018 at 08:42):

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

#### Rob Lewis (Oct 15 2018 at 08:43):

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 (Oct 15 2018 at 08:43):

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

#### Mario Carneiro (Oct 15 2018 at 08:44):

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 (Oct 15 2018 at 08:44):

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

#### Mario Carneiro (Oct 15 2018 at 08:44):

short story: let and have should have the same parser

#### Sebastien Gouezel (Oct 15 2018 at 08:45):

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 (Oct 15 2018 at 08:45):

the comma would be just short form for tactic proofs.

#### Mario Carneiro (Oct 15 2018 at 08:46):

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

#### Mario Carneiro (Oct 15 2018 at 08:47):

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

#### Johannes Hölzl (Oct 15 2018 at 08:47):

hm, yes its short enough. and nicely uniform

#### Patrick Massot (Oct 15 2018 at 08:47):

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

preposterous

#### Johannes Hölzl (Oct 15 2018 at 08:48):

I guess it classes with set syntax

#### Patrick Massot (Oct 15 2018 at 08:49):

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

#### Mario Carneiro (Oct 15 2018 at 08:49):

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

#### Johannes Hölzl (Oct 15 2018 at 08:49):

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 (Oct 15 2018 at 08:51):

mutual have ... with ... ?

#### Mario Carneiro (Oct 15 2018 at 08:52):

yeah this makes a lot more sense than named match

#### Edward Ayers (Oct 15 2018 at 09:50):

Is there a general notation wishlist thread?

there is now

#### Edward Ayers (Oct 15 2018 at 19:22):

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 (Oct 17 2018 at 09:22):

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 (Dec 04 2018 at 19:38):

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 (Dec 23 2018 at 17:15):

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 (Dec 23 2018 at 22:35):

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

#### Mario Carneiro (Dec 23 2018 at 23:13):

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

#### Patrick Massot (Dec 24 2018 at 10:53):

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 (Dec 24 2018 at 10:57):

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 (Dec 24 2018 at 10:59):

You can defer proof obligations using refine

#### Mario Carneiro (Dec 24 2018 at 11:03):

Isn't this just the definition of div?

#### Mario Carneiro (Dec 24 2018 at 11:03):

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

#### Mario Carneiro (Dec 24 2018 at 11:05):

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 (Dec 24 2018 at 11:08):

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 (Dec 24 2018 at 20:20):

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 (Dec 24 2018 at 20:21):

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 (Dec 24 2018 at 20:21):

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?

Last updated: May 15 2021 at 00:39 UTC