Zulip Chat Archive

Stream: general

Topic: notations to introduce proofs


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:21):

Certainly calc would make sense with :=

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:21):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:22):

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

view this post on Zulip 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".

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:29):

the base Isar syntax, I mean

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:29):

Maybe it is Mizar influence then?

view this post on Zulip Sebastien Gouezel (Oct 15 2018 at 08:31):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:32):

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

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:33):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:36):

I think syntax changes like that are on the table

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:36):

I would be in support of using more :=

view this post on Zulip Sebastien Gouezel (Oct 15 2018 at 08:37):

I agree.

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:37):

and drop the from

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:38):

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

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:38):

show A := proof

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:40):

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

view this post on Zulip 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

view this post on Zulip 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, ...

view this post on Zulip 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.

view this post on Zulip Johannes Hölzl (Oct 15 2018 at 08:43):

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

view this post on Zulip 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

view this post on Zulip 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 := ..., ...

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:44):

short story: let and have should have the same parser

view this post on Zulip 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).

view this post on Zulip Johannes Hölzl (Oct 15 2018 at 08:45):

the comma would be just short form for tactic proofs.

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:46):

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

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:47):

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

view this post on Zulip Johannes Hölzl (Oct 15 2018 at 08:47):

hm, yes its short enough. and nicely uniform

view this post on Zulip Patrick Massot (Oct 15 2018 at 08:47):

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

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:47):

preposterous

view this post on Zulip Johannes Hölzl (Oct 15 2018 at 08:48):

I guess it classes with set syntax

view this post on Zulip Patrick Massot (Oct 15 2018 at 08:49):

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

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:49):

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

view this post on Zulip 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 := ...,
...

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:51):

mutual have ... with ... ?

view this post on Zulip Mario Carneiro (Oct 15 2018 at 08:52):

yeah this makes a lot more sense than named match

view this post on Zulip Edward Ayers (Oct 15 2018 at 09:50):

Is there a general notation wishlist thread?

view this post on Zulip Mario Carneiro (Oct 15 2018 at 19:17):

there is now

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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].

view this post on Zulip 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))

view this post on Zulip Mario Carneiro (Dec 23 2018 at 22:35):

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

view this post on Zulip Mario Carneiro (Dec 23 2018 at 23:13):

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

view this post on Zulip 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).

view this post on Zulip 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:

view this post on Zulip Mario Carneiro (Dec 24 2018 at 10:59):

You can defer proof obligations using refine

view this post on Zulip Mario Carneiro (Dec 24 2018 at 11:03):

Isn't this just the definition of div?

view this post on Zulip Mario Carneiro (Dec 24 2018 at 11:03):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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