Proving findLeast: an experience report

Stream: lean4

[Mario Carneiro]

This originated in a question by Jeremy Avigad about how to prove that this function:

def findLeast (a : Array Nat) : Nat := do
  let mut smallest := a[0]
  for i in [1:a.size] do
    if a[i] ≤ smallest then
      smallest := a[i]
  return smallest

#eval findLeast #[8, 3, 10, 4, 6]

actually computes the least element of the array. The complete proof is here: https://gist.github.com/digama0/404b4a49ccf378847b7ad2c12374bae2

My experience report: There are still huge missing pieces and a lot of things are significantly more painful compared to lean 3. (Warning: this will come off a bit harsh, but I've tried to turn the unfocused frustration into as actionable items as I could.)

• The trustme tactic is a hack to work around the lack of equation lemmas. It acts like exact except it doesn't check that the given term has the correct type; it's safe because the kernel will catch you if you do something wrong, but it lets us implement delta in this case, to prove loop_eq, which would be by delta loop in lean 3.
  • This relates to https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Smart.20unfolding.20produces.20ununfoldable.20terms . As far as I know, there is no way in lean 4 currently to prove the theorem without this "cheating" tactic.
• Stating the type of loop_eq is a challenge. Taking the result of #print loop directly doesn't work for a number of type inference reasons. It seems that the delaborator still needs some more work.
• I originally tried to prove findLeast_min with a single large theorem, but local let was not as powerful as I first thought, so I eventually abandoned it and this version uses a definition findLeastRec for the inner let instead.
  • More specifically, I found that using local definitions with theorem foo := ... where bar := ..., the definition of bar is not available in foo, it only appears as a local hypothesis, like have bar := ... which is no good for a definition like findLeastRec.
• cases and the match tactic seem to do approximately the same thing, but they are each limited in different ways. The match tactic inherits from the match term the undesirable behavior that it does not generalize other variables in the context dependent on the one being pattern matched, unlike cases - for example if h : x < y is in the context, match x with | 0 => ..., you lose the fact that 0 < y. On the other hand, cases apparently does not support nested pattern matches or the ability to use other expressions in the branches, for example matching a Nat as 0 and n+1 instead of zero and succ n (and putting those terms in the goal).

• Keeping the tactic proof well formed is a challenge, and sometimes the whitespace sensitivity causes surprises. I particularly miss being able to use { } to create blocks; lean 4 {} blocks don't work well with the indentation rules.

  • More specifically:

    have foo : type
    { tac
      tac }

    doesn't work like it would in lean 3, the indentation level of the two tactics is different and this messes things up.

  • have : type doesn't work as a tactic without from or by afterward.

  • have := term doesn't work. I use this all the time in lean 3 and have _ from term is not a great substitute. This is nothing that a mathlib prelude can't solve, though. (Can we just eliminate from here in the syntax? I'd rather it just always use :=.)
  • Implicit lambdas caused a number of issues because they get eagerly applied everywhere and it's difficult to control this behavior. I ended up having to avoid them entirely in things like the induction hypothesis. We need semi-implicits, I think.
  • I should find a more specific example here, but implicit lambda introduction was something I had to force-disable more often than use.
  • There are lots and lots of inaccessible names, which makes quick and dirty proving much more onerous. I generally write proofs in quick and dirty mode first and then clean them up once the proof is complete, because iteration on a dirty proof is a lot faster. Lean 4 makes you be a lot more explicit in each step which makes this harder.
  • Writing tactics and finding things is very difficult. In lean 3, even without anything imported the entire tactic framework is available in init and everything is in namespace tactic. In lean 4 there are a ton of different files and all the prominent constants like CoreM, ElabTermM, elabTerm are in different namespaces and require different files to be imported, and I had to go spelunking through the lean 4 source to find where anything is.
  • There are no tactic writing docs in the lean 4 reference, almost no tactic writing examples in tests, and looking through the lean 4 source for examples is of limited utility when many of the tools used inside lean 4 are of the builtin variety and you the user are supposed to be using something else.

[Yury G. Kudryashov]

About have _ := _ vs have _, from _ in lean3 (sorry for semi-offtopic). When I write have a = 5, from h _, it is guaranteed to fail unless Lean can find _. With have a = 5 := h _ it creates extra goals.

[Mario Carneiro]

Actually, that brings me to another point of note: refine in lean 4 acts basically like lean 3 exact, in that any _ get red squiggles on them and the tactic does not proceed. In order to recover lean 3 refine you have to use ?_ instead. At the same time exact also does that, except it has a much worse error reporting - any error and the whole exact line gets highlighted. As a result, it seems like it might be better to just ditch exact and make it a synonym for refine, since it supports both modes explicitly.

[Daniel Selsam]

More specifically, I found that using local definitions with theorem foo := ... where bar := ..., the definition of bar is not available in foo, it only appears as a local hypothesis, like have bar := ... which is no good for a definition like findLeastRec.

FYI

theorem lookAtLetDef (n : Nat) : foo n = n + 1 :=
  let bar (n : Nat) : Nat := n + 1
  have foo n = bar n := rfl -- ok
  sorry

theorem lookAtWhereDef (n : Nat) : foo n = n + 1 :=
  have foo n = bar n := rfl -- type error
  sorry
  where bar (n : Nat) : Nat := n+1

theorem lookAtLetRecDef (n : Nat) : foo n = n + 1 :=
  let rec bar (n : Nat) : Nat := n + 1
  have foo n = bar n := rfl -- type error
  sorry

[Daniel Selsam]

def foo (n : Nat) : Nat :=
  let lbar (n : Nat) : Nat := n + 1
  let rec lrbar (n : Nat) : Nat := n + 1
  lbar n + lrbar n + wbar n where wbar n := n + 1

#print foo
/-
def foo : Nat → Nat :=
fun (n : Nat) =>
  (fun (wbar : Nat → Nat) =>
      let lbar : Nat → Nat := fun (n : Nat) => n + 1;
      (fun (lrbar : Nat → Nat) => lbar n + lrbar n + wbar n) foo.lrbar)
    foo.wbar
-/

So both let rec and where use auxiliary definitions, and my guess is that there is good reason to treat them as opaque while elaborating foo. But maybe where could notice when it is not recursive and be elaborated as a regular let.

[Mario Carneiro]

In my case, I wanted the let rec to turn into an auxiliary definition, not a local constant

[Daniel Selsam]

It seems that the delaborator still needs some more work.

The delaborator definitely needs more work (https://github.com/leanprover/lean4/issues/368) but it should be rare to need to elaborate brecOns once equation lemmas are being generated.

[Mario Carneiro]

specifically, I would like the delaborator to always produce a term that typechecks. For anything with a higher order matching problem it should make the motive := ... explicit

[Daniel Selsam]

That is indeed the stated goal in the issue I linked to above. "round trip" means it re-elaborates to the original term.

[Daniel Selsam]

Mario Carneiro said:

In my case, I wanted the let rec to turn into an auxiliary definition, not a local constant

In your case, the function wasn't recursive.

theorem foo : False :=
  let findLeastRec (f : Nat → Nat) (lo hi z j b : Nat) : Nat :=
    Std.Range.forIn.loop (m := Id) [lo:hi]
      (fun i r => if f i ≤ r then yield (f i) else yield r) z j b
  sorry

[Mario Carneiro]

Oh I guess that's true. I think it was in another version of the proof

[Daniel Selsam]

In my case, I wanted the let rec to turn into an auxiliary definition, not a local constant

I think the issue is that it could be mutually recursive with the top-level definition. So similar to my suggestion that where detect when it is not recursive, perhaps letrec and where could also detect when it is "self-contained recursive", i.e. safe to turn into an auxiliary definition that does not refer to the current one.

[Mario Carneiro]

Oh, that's interesting. How commonly is that used? Maybe there should be a special indicator for that, like where mutual or something

[Mario Carneiro]

detecting self-contained recursive is tough because you have to first run the tactics to find out what the term is, and the data given to the tactics depends on the result of the analysis (since they would be able to see whether an auxiliary definition was created)

[Daniel Selsam]

Currently, both of these work:

mutual
 partial def mfoo (n : Nat) : Nat := if n = 0 then 0 else mbar (n-1)
 partial def mbar (n : Nat) : Nat := if n = 0 then 1 else mfoo (n-1)
end

partial def foo (n : Nat) : Nat := if n = 0 then 0 else wbar (n-1) where
  wbar (n : Nat) : Nat := if n = 0 then 1 else foo (n-1)

[Daniel Selsam]

I think where mutual is tricky because you might batch many different functions in a where clause. But what about function-specific prefix?

partial def foo (n : Nat) : Nat := if n = 0 then base else wbar (n-1) where
  mutual wbar (n : Nat) : Nat := if n = 0 then 1 else foo (n-1)
  base : Nat := 0

[Mario Carneiro]

I was thinking you would either make all of them mutual or none

[Mario Carneiro]

but your version reads well

[Mario Carneiro]

if you could put def or let or have on definitions in where clauses that would also let you control whether they show up as local constants, auxiliary definitions, or let bindings

[Daniel Selsam]

for example if h : x < y is in the context, match x with | 0 => ..., you lose the fact that 0 < y.

And presumably you think it is too annoying to match on h explicitly as in:

theorem foo (n : Nat) (h : n < n + 1) : n < n + 1 :=
  match n, h with
  | 0,   h2 => h2
  | n+1, h2 => h2

I think it is good practice to match on the h explicitly, but agree it is annoying to need to put it in every branch. What about a macro:

theorem foo (n : Nat) (h : n < n + 1) : n < n + 1 :=
  match n generalizing h with
  | 0 => ...
  | n+1 => ...

-- could turn into:
theorem foo (n : Nat) (h : n < n + 1) : n < n + 1 :=
  match n,  h with
  | 0, h => ...
  | n+1, h => ...

[Mario Carneiro]

In cases , you just use cases n and it generalizes everything in the context that depends on n. I've never seen a situation where this was undesirable

[Mario Carneiro]

induction is another matter, but match doesn't support induction anyway

[Mario Carneiro]

Note that induction will automatically add generalizing h whenever h depends on the induction variable

[Mario Carneiro]

so you actually have to use clear if you don't want that

[Daniel Selsam]

Mario Carneiro said:

if you could put def or let or have on definitions in where clauses that would also let you control whether they show up as local constants, auxiliary definitions, or let bindings

I tentatively like this proposal

[Daniel Selsam]

Mario Carneiro said:

so you actually have to use clear if you don't want that

Seems like apples-to-oranges since match is term mode, not tactic mode.

On the other hand, cases apparently does not support nested pattern matches or the ability to use other expressions in the branches, for example matching a Nat as 0 and n+1 instead of zero and succ n (and putting those terms in the goal).

Can you write the syntax you would want for cases and induction?

[Daniel Selsam]

Writing tactics and finding things is very difficult.

FYI here is the API for builtin tactics designed for interactive mode: https://github.com/leanprover/lean4/blob/master/src/Init/Notation.lean#L189-L325

[Daniel Selsam]

Writing tactics and finding things is very difficult.

I agree, though one doesn't need to find nearly as much when there are working, illustrative examples to copy-paste-tweak. How about we start collecting a set of informative examples in mathlib-prelude?

[Yakov Pechersky]

Here's an example of a macro that took me very long to figure out. I'm sure it's still buggy. How does one use lemma instead of theorem?

macro "lemma" n:declId sig:declSig ":=" s:term : command =>
  `(theorem $n:declId $sig:declSig := $s:term)

[Daniel Selsam]

Also, there are a few tricks we can put in a doc, e.g. to find how a command (e.g. namespace) is elaborated,

$ grep -rni "commandElab.*namespace" ../../lean4/src/Lean
../../lean4/src/Lean/Elab/Command.lean:376:@[builtinCommandElab «namespace»] def elabNamespace : CommandElab := fun stx =>

or parsed:

$ grep -rni "commandParser.*namespace" ../../lean4/src/Lean/
../../lean4/src/Lean/Parser/Command.lean:67:@[builtinCommandParser] def «namespace»    := leading_parser "namespace " >> ident

[Mario Carneiro]

Daniel Selsam said:

Mario Carneiro said:

so you actually have to use clear if you don't want that

Seems like apples-to-oranges since match is term mode, not tactic mode.

My original comment was about the match tactic as compared to the cases tactic

[Mario Carneiro]

Daniel Selsam said:

On the other hand, cases apparently does not support nested pattern matches or the ability to use other expressions in the branches, for example matching a Nat as 0 and n+1 instead of zero and succ n (and putting those terms in the goal).

Can you write the syntax you would want for cases and induction?

here's a start:

cases n
| 0 => ...
| n+1 => ...

induction is harder since it has the extra ih argument hanging off.

induction n
| 0 => ...
| n+1, ih => ...

[Daniel Selsam]

Yakov Pechersky said:

Here's an example of a macro that took me very long to figure out. I'm sure it's still buggy. How does one use lemma instead of theorem?

macro "lemma" n:declId sig:declSig ":=" s:term : command =>
  `(theorem $n:declId $sig:declSig := $s:term)

The only issue I see with yours is that theorem is actually a bit more powerful than that: https://github.com/leanprover/lean4/blob/master/src/Lean/Parser/Command.lean#L40 After adding a line to that file to export the declVal shorthand, you can write:

macro "lemma" n:declId sig:declSig val:declVal : command => `(theorem $n $sig $val)

I believe this will make lemma and theorem equivalent.

[Mario Carneiro]

Yakov Pechersky said:

Here's an example of a macro that took me very long to figure out. I'm sure it's still buggy. How does one use lemma instead of theorem?

macro "lemma" n:declId sig:declSig ":=" s:term : command =>
  `(theorem $n:declId $sig:declSig := $s:term)

Based on the theorem parser, I think you want the last bit to be declVal:

macro "lemma" n:declId sig:declSig val:declVal : command =>
  `(theorem $n:declId $sig:declSig $val:declVal)

However, this causes the same quotation panic that I've triggered in two other threads

[Yakov Pechersky]

Right, so the working one I have is weaker, but functional. I didn't file a bug report on the panic, rather tried to find a stopgap partial replacement.

[Mario Carneiro]

After adding a line to that file to export the declVal shorthand,

Oh, that sounds problematic

[Daniel Selsam]

Mario Carneiro said:

After adding a line to that file to export the declVal shorthand, you can write:

Oh, that sounds problematic

I will PR it.

[Mario Carneiro]

This actually relates to another issue I've hit on: there are a lot of private functions in lean 4. I had to kill these with fire in lean 3 because they really hamper reuse

[Daniel Selsam]

Mario Carneiro said:

This actually relates to another issue I've hit on: there are a lot of private functions in lean 4. I had to kill these with fire in lean 3 because they really hamper reuse

Can you please explain the issue?

[Mario Carneiro]

I recently tried to get the parsed PreDeclaration for a theorem. In order to do so, I had to bring in 15 or so (large) private definitions, before eventually getting stuck on a private macro, which I have no idea how to duplicate

[Mario Carneiro]

You can't call private functions

[Mario Carneiro]

so that means if you want to adapt a function that calls a private function, you have to copy and paste it, as well as any private functions it calls and so on transitively

[Mario Carneiro]

it's a huge pain

[Mario Carneiro]

I think private should never be used. You never know when someone is going to want to use your function

[Daniel Selsam]

Is this just for debugging?

[Mario Carneiro]

Yes and no

[Daniel Selsam]

Mario Carneiro said:

I think private should never be used. You never know when someone is going to want to use your function

This seems pretty extreme. Encapsulation is generally considered good design.

[Mario Carneiro]

In that particular example it was for debugging, but it's totally legitimate to want to work with PreDefinition or any other implementation item

[Mario Carneiro]

Not in a theorem prover that is meant to be hacked on by users

[Daniel Selsam]

Mario Carneiro said:

so that means if you want to adapt a function that calls a private function, you have to copy and paste it, as well as any private functions it calls and so on transitively

Personally, I tweak lean4 and rebuild all the time for things like this. The slow recompilation speed is annoying but my own fault for not having a threadripper.

[Mario Carneiro]

Yeah, I'm worried I'm going to need to fork lean 4

[Mario Carneiro]

Ultimately I thought the idea was that we don't need to

[Mario Carneiro]

Daniel Selsam said:

Mario Carneiro said:

I think private should never be used. You never know when someone is going to want to use your function

This seems pretty extreme. Encapsulation is generally considered good design.

If there was a way to open a namespace and get at the private functions this would be fine. But lean is intentionally designed to be modified and I don't think there is a single component of the system that isn't "incomplete" in the sense that users may want to add functionality to what is already there, and work with the data structures of that file

[Mario Carneiro]

Certainly in mathlib every single time someone thought it would be a good idea to put private it turned out to be a mistake. At minimum, it is difficult to prove theorems about a private function, so in the far future when someone decides to prove e.g. the parser correct, they will get stuck on any "encapsulation"

[Daniel Selsam]

Mario Carneiro said:

Yeah, I'm worried I'm going to need to fork lean 4

FWIW I don't think it would be so bad for there to be a lean-community:lean4 as long as the patches were small enough that it could be frequently rebased.

[Mario Carneiro]

I can live with that if others can

[Mario Carneiro]

At least then I can get the mountain of PRs I'm holding off on off my back

[Daniel Selsam]

Even if the goal is to keep the lean-community version exactly equal to the main one, it may still make sense to fork now and experiment with your suggested changes. Leo will be much more likely to consider a PR down the road if it has been stress-tested and if there is community consensus on its value.

[Mario Carneiro]

(okay, not a mountain, a few pebbles. But I don't know how to build the mountain when I can't place the first pebble.)

[Mario Carneiro]

Can someone who knows how to do so set up a community lean 4 nightly?

[Daniel Selsam]

Mario Carneiro said:

• Keeping the tactic proof well formed is a challenge, and sometimes the whitespace sensitivity causes surprises.

Note that you can also use braces and semicolons:

theorem foo (n : Nat) : True := by {
   match n with
 | 0   => _
    | n+1 => _; exact sorry;
     exact sorry
}

[Mario Carneiro]

not quite:

theorem foo (n : Nat) : True := by {
   match n with
      | 0   => _
    | n+1 => _; exact sorry;
     exact sorry
}

[Daniel Selsam]

Ah, it looks like all subsequent bars after the first need to have at least as much offset, even in tactic-mode-with-bars

[Mario Carneiro]

I haven't found a whitespace insensitive version of the syntax either

[Mario Carneiro]

Oh, also it seems like _ is a tactic now? I have a macro in my test file for that

[Mario Carneiro]

I used refine _ as the expansion because that gives a red squiggle and tells you the type, but also eats a goal and allows the rest to proceed, like sorry

[Sebastian Ullrich]

This is also the reason why

have foo : type
{ tac
  tac }

didn't work: inside braces, you must use semicolons. I've written a fair chunk of tactic proofs in Lean 4, but I never noticed that one because I tend to use Lean 4's new structuring techniques (all the stuff with =>) instead of braces.

[Daniel Selsam]

Mario Carneiro said:

I used refine _ as the expansion because that gives a red squiggle and tells you the type, but also eats a goal and allows the rest to proceed, like sorry

The match tactic calls refine automatically (https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/Match.lean#L66) and has for 6 months according to GitHub's blame

[Mario Carneiro]

I'm fine with using the new structuring techniques, but it's awkward around have because of the by

[Mario Carneiro]

I mean the _ tactic, as in by _

[Mario Carneiro]

that did not work a few weeks ago

[Sebastian Ullrich]

But indentation should work for that, right?

have t by
  t'1
  t'2
t

[Mario Carneiro]

It does

[Mario Carneiro]

I just want to drop the by

[Mario Carneiro]

lean 3 doesn't need it

[Daniel Selsam]

Mario Carneiro said:

I mean the _ tactic, as in by _

theorem foo : True := by _ gives me:

error: expected '{' or tactic
error: unexpected command

[Mario Carneiro]

Also, a common lean 3 proof style is

have := lemma,
rw [lemma2] at this,
exact this

This doesn't work in lean 4 because the have doesn't proceed until all the metavariables in lemma are filled (while the proof technique might be using lemma2 and the exact to figure out the metavariables)

[Mario Carneiro]

@Daniel Selsam That's odd, since your badly formatted code example uses the _ tactic twice

[Daniel Selsam]

No, because the match tactic is transforming the syntax to call refine

[Mario Carneiro]

you what now?

[Mario Carneiro]

how does that work?

[Daniel Selsam]

This is the link I posted a few comments above: https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/Match.lean#L66-L68

[Daniel Selsam]

Sebastian Ullrich said:

But indentation should work for that, right?

have t by
  t'1
  t'2
t

FWIW I like the by here.

[Mario Carneiro]

Does the by create a new tactic scope like in lean 3?

[Mario Carneiro]

if so that might explain the reason why the rwa proof style fails

[Mario Carneiro]

Thoughts on => as alternative / in addition to by?

[Mario Carneiro]

and := as alternative to from as I mentioned before

[Mario Carneiro]

I'm not a fan of the many syntaxes for introducing subgoals, by to start, => after cases, match, induction, ; after refine (actually I haven't figured out how to select refine subgoals using multiple blocks yet)

[Mario Carneiro]

refine foo ?_ ?_ ?_
  tac1a
  tac1b
  done
  tac2a
  tac2b
  done
  tac3a
  tac3b
  done

[Mario Carneiro]

With lean 3 style blocks this would be

refine foo ?_ ?_ ?_
{ tac1a
  tac1b }
{ tac2a
  tac2b }
{ tac3a
  tac3b }

all the lean 4 options seem to be a lot more verbose

[Mario Carneiro]

Sebastian Ullrich said:

This is also the reason why

have foo : type
{ tac
  tac }

didn't work: inside braces, you must use semicolons.

Can we make that work with whitespace sensitivity? The rule I want is that the column starts at the first token after the {

[Sebastian Ullrich]

They look both pretty bad to me. How about naming them and using case?

[Mario Carneiro]

because they don't have names

[Daniel Selsam]

@Mario Carneiro This works for me:

structure A : Prop where
structure B : Prop where
structure C : Prop where

axiom AB : A → B
axiom BC : B → C

theorem foo (a : A) : C ∧ C := by
  refine And.intro ?x ?y
  { apply BC; apply AB; assumption }
  { apply BC; apply AB; assumption }

[Mario Carneiro]

Yes that works, but it means I have to give up whitespace sensitive lines

[Mario Carneiro]

which screws up the overall formatting if I'm using it elsewhere

[Mario Carneiro]

if some tactic lines end in ; and others don't that will read weirdly

[Daniel Selsam]

This also works:

theorem foo (a : A) : C ∧ C := by
  refine And.intro ?x ?y
  focus
    apply BC
    apply AB
    assumption
  focus
    apply BC
    apply AB
    assumption

[Mario Carneiro]

oh that's not bad

[Daniel Selsam]

And there can probably be a variant where you name the focus branches

[Mario Carneiro]

that's the version sebastian was suggesting

[Daniel Selsam]

like case ?x instead of focus

[Mario Carneiro]

but I don't want to give names to goals where the best name is an ordinal

[Mario Carneiro]

Also, can ? work instead of ?_? It's an extra character compared to lean 3

[Sebastian Ullrich]

You can use refine' foo _ _ _ :)

[Daniel Selsam]

I am pro-names in general

[Mario Carneiro]

I want to be able to keep the structure of lean 3 proofs for the most part

[Mario Carneiro]

names should be an option

[Daniel Selsam]

meaning the same lack of structure?

[Mario Carneiro]

They are structured

[Mario Carneiro]

they are block structured proofs

[Mario Carneiro]

We are pretty strict about that

[Mario Carneiro]

I'm not about to rewrite all lean 3 proofs for style in the middle of a giant port

[Mario Carneiro]

You can write unstructured proofs in lean 3 but I'm not talking about those

[Daniel Selsam]

Got it

[Mario Carneiro]

in fact it seems like lean 4's support for unstructured proofs is pretty much the same

[Daniel Selsam]

It does seem so. I thought at some point the plan was to require names and case ?x but I guess that was ditched.

[Mario Carneiro]

I like the current setup: you can write names and case if you want but you don't have to

[Mario Carneiro]

lean 3 also cultivated (at least) two distinct styles: mathlib's block structured proofs and NNG's unstructured proofs (plus term mode proofs, which have several different styles)

[Mario Carneiro]

I can imagine having a style linter to ensure adherence to one style or another

[Mario Carneiro]

but the core syntax should be multi-paradigm

[Sebastian Ullrich]

Mario Carneiro said:

I'm not about to rewrite all lean 3 proofs for style in the middle of a giant port

Then that should be discussed in a different topic. I don't mind if mathport implements its own tactic compatibility layer. But this topic started as an experience report on Lean 4, not porting, so it should discuss the best solutions for Lean 4 irrespective of Lean 3 solutions. Which always was our modus operandi for Lean 4.

[Mario Carneiro]

Fair enough. I guess I'm saying that even for green field lean 4 projects I'm not sold on the | => stuff

[Mario Carneiro]

in coq I think the equivalent is -

[Mario Carneiro]

I really want a way to not waste a line saying "here's a goal"

[Daniel Selsam]

@Sebastian Ullrich

I've written a fair chunk of tactic proofs in Lean 4

Are these on GitHub somewhere?

[Sebastian Ullrich]

Not publicly, unfortunately, since they are the solutions to our course project :frowning:

[Sebastian Ullrich]

Mario Carneiro said:

in coq I think the equivalent is -

I kind of like that, I think it would be a better fit for the whitespace-sensitive syntax than braces

[Yury G. Kudryashov]

Coq syntax

[Daniel Selsam]

Mario Carneiro said:

• Implicit lambdas caused a number of issues because they get eagerly applied everywhere and it's difficult to control this behavior. I ended up having to avoid them entirely in things like the induction hypothesis. We need semi-implicits, I think.
  • I should find a more specific example here, but implicit lambda introduction was something I had to force-disable more often than use.

I am curious about this one. I don't see any @funs in the file you posted so I am guessing it was earlier in development.

[Mario Carneiro]

I was curious about when coq uses - vs *; It is discussed in the "bullets" section, and it seems like you can use any of -, + and * to select subgoals, where I guess the idea is that you can use different delimiters at different levels. (I assume all delimiters at a given subgoal splitting have to agree.) Personally I think it would be better to just use one of them, since users might come up with some other meaning for the other sigils

[Mario Carneiro]

I can't replicate the @fun issues. I think I was forgetting fun {i} =>

[Mario Carneiro]

Oh there was a bug in a tactic involving implicit lambdas, let me see if I can replicate

[Mario Carneiro]

example : ∀ {i : Nat}, i < 0 := by
  -- ⊢ ∀ {i : Nat}, i < 0
  have _ from 1
  -- i✝ this : Nat ⊢ i✝ < 0
  skip

The same thing happens with let and match

[Zygimantas Straznickas]

Mario Carneiro said:

I was curious about when coq uses - vs *; It is discussed in the "bullets" section, and it seems like you can use any of -, + and * to select subgoals, where I guess the idea is that you can use different delimiters at different levels. (I assume all delimiters at a given subgoal splitting have to agree.) Personally I think it would be better to just use one of them, since users might come up with some other meaning for the other sigils

Yup, any bullet can be used in any nesting level as long as the same bullet is used for the same level. Also, indentation doesn't matter when using bullets -- these are all legal (though obviously only the first one is a good idea):

Theorem ex : (True /\ True /\ (True /\ True) /\ True).
Proof.
  split; [|split]; [| |split]. (* split into multiple goals for demonstration*)

  * constructor.
  * constructor.
  * split.
    - constructor.
    - constructor.
  * constructor.
Qed.

Theorem ex2 : (True /\ True /\ (True /\ True) /\ True).
Proof.
  split; [|split]; [| |split]. (* split into multiple goals for demonstration*)

  * constructor.
    * constructor.
* split.
  - constructor. - constructor.
  * constructor.
Qed.

Theorem ex3 : (True /\ True /\ (True /\ True) /\ True).
Proof.
  split; [|split]; [| |split]. (* split into multiple goals for demonstration*)

  * constructor. * constructor. * split. - constructor. - constructor. * constructor.
Qed.

One limitation of this notation is that you can do at most three levels of nesting. But one might argue that if you need more, your proof is too complicated and you need to refactor :)

[Mario Carneiro]

Oh I see, it's not whitespace sensitive so the different sigils are required

[Daniel Selsam]

Mario Carneiro said:

example : ∀ {i : Nat}, i < 0 := by
  -- ⊢ ∀ {i : Nat}, i < 0
  have _ from 1
  -- i✝ this : Nat ⊢ i✝ < 0
  skip

The same thing happens with let and match

This is really weird. Here are some more examples:

example (P : Prop) : ∀ {p : P}, P := by
  exact id -- error: type mismatch, expected type P

example (P : Prop) : ∀ {p : P}, P := by
  exact @id _ -- works

example (P : Prop) : ∀ {p : P}, P := by
  apply id -- works

example (P : Prop) : ∀ {p : P}, P := by
  have _ from 1
  apply id -- error: unsolved goals |- P

[Mario Carneiro]

yeah, I think that first example was the issue I hit that caused me to abandon the approach

[Daniel Selsam]

I don't even understand what is happening there.

[Mario Carneiro]

the type just felt very unstable, as if looking at it wrong causes it to get instantiated

[Daniel Selsam]

@Yakov Pechersky FYI declVal is exposed now on master so

macro "lemma" n:declId sig:declSig val:declVal : command => `(theorem $n $sig $val)

should work.

[Daniel Selsam]

I just read over the implicit-lambda code. It is surprisingly aggressive but based on relatively simple rules. Basically, any variant of the above examples will have a lambda inserted, unless it (a) doesn't involve elaborating a term with the expected type or (b) explicitly disables it. The reason the apply id example works is that apply (unlike exact) detects that id is an identifier and doesn't actually elaborate it using the expected type.

[Jeremy Avigad]

Sorry to be late to this party, but regarding the "private" keyword, would it help to keep their names but prefix the namespace with "private"? They could then be filtered by documentation and search, but determined users could still access them. The main problem would be name clashes -- users would have to use private foo and private foo1 and private foo2 in the namespace where they could just use private foo repeatedly before.

[Sebastian Ullrich]

The names are preserved, including namespaces: https://github.com/leanprover/lean4/blob/bf4b9b0ccd7688d3d4024bc06a0c7a3b207124bd/src/Lean/Modifiers.lean#L24-L27
A dedicated meta hacker could write a tear_open_private command that walks through the declarations of a specified module and creates accessible aliases of such names. But there would be no guarantee that this will keep working indefinitely, of course. For example, it is incompatible with any kind of module system where private declarations are not part of the "signature" .olean file to begin with (though the full .olean file should still be around to load instead). At that point private declarations would also become much more useful: you could add new ones without having to recompile (some) downstream modules.

[Daniel Selsam]

FWIW I am skeptical that private is a real issue right now. For random experiments and traces, locally rebuilding Lean is fine.

[Gabriel Ebner]

tear_open_private is called import_private right now. :smile:

[Daniel Selsam]

(and if there are some private defs that are deemed important to expose, these can be changed on case-by-case basis)

[Gabriel Ebner]

For example, it is incompatible with any kind of module system where private declarations are not part of the "signature" .olean file to begin with

I don't think that is realistic. Private definitions are part of the public interface because they are exposed during unification. In particular, changing private definitions is a breaking change because it affects definitional equality.
On the other hand, leaving out "definitions" of constants would be fair game.

[Sebastian Ullrich]

Ah, but the module system that only exists in my head would also seal (make opaque) public definitions by default... it might be mostly useful for programming and not proving, so it would most likely be opt-in and the standard import would keep its current lax semantics.

[Sebastian Ullrich]

Using private declarations from a reducible or otherwise exposed declaration should ideally be a compiler error

[Gabriel Ebner]

Would type-checking also be restricted to reducible transparency?

[Sebastian Ullrich]

For imported definitions? If you imported them via say import signature and they don't have some other attribute that says "transparent in signature imports but not reducible", then yes.

[Sebastian Ullrich]

So it's not really a change in the transparency predicate, but import signature importing definitions as value-less constants by default.

[Sebastian Ullrich]

And then you'd just need some content-addressed build system to actually make use of that... it's as thought-out as it sounds, yes

[Gabriel Ebner]

Ah, so things like def Options := KVMap would still reduce because they're not imported as signature. It's an interesting dialect, but probably not that useful if you want to keep theorems close to your definitions.