Small Scale Reflection for the Working Lean user

Stream: general

[Kim Morrison]

I'd be happy to see further examples.

The main example from the paper seems to be at the top of page 16 (oof, not copy-and-pasteable). It is indeed shorter, but I don't really see any abbreviation beyond ascii art. Are there more convincing examples where something non-syntactical is happening?

[Vladimir Gladstein]

Scott Morrison said:

I'd be happy to see further examples.

The main example from the paper seems to be at the top of page 16 (oof, not copy-and-pasteable). It is indeed shorter, but I don't really see any abbreviation beyond ascii art. Are there more convincing examples where something non-syntactical is happening?

I think the main advantage of LeanSSR proofs is not the size, but that they are interactive and still as compact as handcrafted terms. Please check the explanation at section 4.2 for detailed comparison with mathlib proofs.

Other than that, LeanSSR provides a convenient machinery for forwards style reasoning (sec 2.5) and reduces the amount of required bookkeeping (sec 2.1).

You can find examples at the LeanSSR repo at Examples/ folder. Moreover, if you switch to itp24 branch, you would find some proofs ported from Mathlib Examples/Mathlib.

Another exciting (at least for me) part of LeanSSR is enhanced Computational Reflection.

[Patrick Massot]

I don’t understand the sentence “Unlike Coq, Lean assumes axioms of classical logic, such as the law of excluded middle”. I don’t think there is any difference here. Neither Coq not Lean has builtin classical logic and you can add the corresponding axioms to both.

[Jireh Loreaux]

Vladimir Gladstein said:

Scott Morrison said:

I'd be happy to see further examples.

The main example from the paper seems to be at the top of page 16 (oof, not copy-and-pasteable). It is indeed shorter, but I don't really see any abbreviation beyond ascii art. Are there more convincing examples where something non-syntactical is happening?

I think the main advantage of LeanSSR proofs is not the size, but that they are interactive and still as compact as handcrafted terms. Please check the explanation at section 4.2 for detailed comparison with mathlib proofs.

I still don't get it, and I have now read it thoroughly, including section 4.2. (By the way, the declaration from which you are taking that subgoal is docs#Finset.card_eq_of_bijective, not card_eq_of_bijective, which doesn't exist.) That is, you say "not the size", but "still as compact". Do you mean you don't care about the size of the proof script, but you do care about the size of the generated term?

Even if the answer the previous question is yes, I still don't understand. For example, the existing proof in Mathlib is interactive if you follow the "Expected Type" in the VS Code infoview. But if you really want something from the tactic state, then compare with this proof of the subgoal, which is also "interactive", but where the generated term is still small:

    have : ∀ a : α, a ∈ s ↔ ∃ (i : _) (hi : i ∈ range n), f i (mem_range.1 hi) = a := by
      /-
      running `show_term` on this shows the term is still pretty compact.
      Try this: exact fun a ↦
        {
          mp := fun ha ↦
            Exists.casesOn (hf a ha) fun i h ↦
              Exists.casesOn h fun hi eq ↦ Exists.intro i (Exists.intro (mem_range.mpr hi) eq),
          mpr := fun a_1 ↦
            Exists.casesOn a_1 fun i h ↦
              Exists.casesOn h fun hi eq ↦ Eq.mpr (id (congrArg (fun _a ↦ _a ∈ s) eq.symm)) (hf' i (mem_range.mp hi)) }
      -/
      refine fun a => ⟨fun ha => ?_, ?_⟩
      · obtain ⟨i, hi, eq⟩ := hf a ha
        exact ⟨i, mem_range.2 hi, eq⟩
      · rintro ⟨i, hi, eq⟩
        rw [← eq]
        exact hf' i (mem_range.1 hi)

Note, this is an honest question, I'm not trying to be argumentative.

[Notification Bot]

Vladimir Gladstein has marked this topic as resolved.

[Notification Bot]

Vladimir Gladstein has marked this topic as unresolved.

[Eric Wieser]

Patrick Massot said:

Neither Coq not Lean has builtin classical logic and you can add the corresponding axioms to both.

I guess you could argue that Lean has classical logic built into its standard tactics (like split), bur this is certainly a much weaker claim than one about the type theory.

[Ilya Sergey]

@Jireh Loreaux To answer your first question, no, we don't really care about the size of the generated proof term.

@Jireh Loreaux @Scott Morrison To correct the course of this discussion, let me restate our main theses:

1. SSReflect is a very powerful tactic language in the style of Forth, so proofs in it tend to be very concise. Indeed, this style might not resonate with your mental reasoning model, and this is fine. That said, the utility of Coq/SSreflect for formalising mathematics has been empirically shown by a substantial number of documented efforts. Our team felt quite handicapped not having it in Lean, so we decided to implement it ourselves.
2. Once we tried to do so, we had to dive deep into Lean metaprogramming, and we consider our experience of using it worthy of sharing in a paper.
3. We also noticed that one can make SSReflect even better with Lean's mechanisms (in terms of usability and expressivity), and so we did, which is our main pragmatic contribution. We do genuinely find LeanSSR a significant improvement over Coq/SSReflect.
4. Finally, we have shown that idiomatic proofs from mathlib, when rephrased in LeanSSR, become shorter. Whether this is an advantage one would care about, is a different question, but we believe it was important to highlight.

[Henrik Böving]

Can you give an example of what you felt limited about to the degree that you decided to go through the effort of developing this entire framework, instead of a more ad-hoc solution?

[Shreyas Srinivas]

@Ilya Sergey : I think part of the issue might be, for many lean users including me, lean is their main ITP (perhaps even the only one we use). Many of us come from non PL backgrounds. For me, the difficulty in this paper was, at least in the first half, trying to understand how LeanSSR differs from standard tactics with a sprinkling of macros to do the intros and reverts. What I think would help someone like me is to see a proof that is really hard to do with normal tactics, but super easy with LeanSSR.

That being said, teaching SSR is not the main goal of this paper, so I guess it is unfair to ask that here. SSReflect is a fairly well established tactic language in Coq.

[Ilya Sergey]

@Henrik Böving I don't think it was about a particular example, but rather about a proof style, which we were quite used to, and which is different from the idiomatic proofs in Lean, both tactic-based and explicit term constructions. A great example of SSR-style proofs is a MathComp formalisation of sequences.

At the end, it turned out to be a very fun metaprogramming exercise to add our favourite scripting front-end to Lean, and we were excited to share it with others.

[Ilya Sergey]

@Shreyas Srinivas Thank you for the feedback, this is actually quite insightful.

to see a proof that is really hard to do with normal tactics, but super easy with LeanSSR.

I feel no matter what example we pick, it might be an uphill battle, as there will always be an ad-hoc solution that adds an example-specific macro or a piece of automation in a post-hoc fashion, which trivialises its proof in "vanilla" Lean.

Perhaps, you could suggest a self-contained example from your experience with a particularly nasty Lean proof, and let us take a stab at it with unmodified LeanSSR. :)

[Kyle Miller]

I'm a fan of Forth and languages like APL and J, so I'm looking forward to trying this out sometime to see what SSR is about. I've been curious, and having a Lean version will really lower the activation energy!

[Kyle Miller]

Adding some extra context to help navigate (they haven't appeared yet in this thread):

• Zulip announcement for LeanSSR
• Github repo

[Kyle Miller]

I think it would be helpful having a "proof off" to evaluate Mathlib tactics against SSR. Have experienced users of each work together to refine the proofs as much as possible in the respective style.

In the paper, I don't feel like Fig 15(a) is a good representative example of a mathlib proof. It's a common sight, sure, but one part of mathlib style is to write a proof term directly to say "there is nothing to see here, it's obvious and you shouldn't bother reading it." These often come initially come from a tactic proof, but it gets eliminated.

[Kyle Miller]

Here's a tactic proof version, set up like an example in the paper, which works in the context set up right before docs#Finset.card_eq_of_bijective:

example (f : (i : ℕ) → i < n → α)
    (hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a)
    (hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s)
    (a : α) :
    a ∈ s ↔ ∃ i, ∃ (hi : i ∈ range n), f i (mem_range.1 hi) = a := by
  constructor
  · intro ha
    obtain ⟨i, hi, rfl⟩ := hf a ha
    use i, mem_range.2 hi
  · rintro ⟨i, hi, rfl⟩
    apply hf'

The proof can be written in three lines using semicolons

  constructor
  · intro ha; obtain ⟨i, hi, rfl⟩ := hf a ha; use i, mem_range.2 hi
  · rintro ⟨i, hi, rfl⟩; apply hf'

and the SSR for comparison (copy/pasted from the paper; any typos are my fault):

  move=> a
    ⟨/hf ![i /mem_range ? <-] // |
    ![i /mem_range /hf’ /[swap]->] //⟩

[Johan Commelin]

Another proof could be by aesop. Whether that is cheating or :golf: is left as exercise to the reader.

[Ilya Sergey]

@Kyle Miller Thanks for digging in and for the enthusiasm!

Here's the LeanSSR proof, a bit shortened compared to the version from the paper:

example (f : (i : ℕ) → i < n → α)
    (hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a)
    (hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s)
    (a : α) :
    a ∈ s ↔ ∃ i, ∃ (hi : i ∈ range n), f i (mem_range.1 hi) = a := by
  move=> ⟨/hf ![i /mem_range] | ![i hi <-]⟩ //

You can check it by inserting after line 140 of this file in the branch itp24 of the project repository.

The proof is interactive, so you can see what happens to the proof state after each symbol.

[Johan Commelin]

In the paper, you write

Finally, unlike the proof terms constructed holistically,
LeanSSR proofs are interactive: one can check the intermediate subgoals by simply pointing
to the specific location in the text buffer, resulting in a better overall proof experience

But you can also put your cursor in the middle of a term-mode proof and see the goal state at that point. So term-mode proofs are also interactive.

[Patrick Massot]

Ilya, I am afraid that some messages here failed to convey their intended tone. I’m sure nobody here thinks that your work is useless or bad. At least people coming from maths departments know that Feit-Thompson was formalized using SSReflect. So there is no need to prove that this style can be put to very good use. But it certainly looks impenetrable so people would like to understand what are the benefits. And, as Kyle wrote, having a Lean version makes it a lot more plausible that we can finally understand that by playing with it.

[Johan Commelin]

Yes, I should have been a bit more careful with how I phrased my messages above! Thanks Patrick, for your remark.

[Eric Wieser]

This paper is a great example of the flexibility of Lean's metaprogramming, and it looks like it might be effective at attracting Coq users to Lean; so even if as a Lean user I struggle to initially appreciate the unfamiliar syntax, the effort to bridge between communities is certainly appreciated!

[Patrick Massot]

I think that, beyond the cosmetic question of ascii-art abbreviations, the thing that is really unusual for us is the intro/revert dance. The standard Lean tactic try to hide this as much as possible. For instance rw tactic does need this when rewriting the local context, but it tries really really hard to pretend it does not. I can see some value in not pretending: when something goes wrong it can be pretty confusing to suddenly have two copies of your local assumptions. But this is really rare so I guess there is more motivation for explicit intro/revert.

[Eric Wieser]

Even revert is pretty rare to use in Lean; induction x generalizing y does a great job of hiding it

[Patrick Massot]

And I also wanted to say that I personally think that reports on Lean 4 meta-programming experiments are very nice. This is so true that I also wrote one for the same conference. Lean 4 is brand new and simply giving examples of things that are possible is valuable.

[Patrick Massot]

Yes, induction … generalizing … is another example of revert-hiding.

[Ilya Sergey]

@Johan Commelin Yes, this phrasing is not great. Let me clarify.

While your statement is true for a fully constructed proof term, it is not the case for a proof in progress (at least in my limited experience with the Lean term mode).

What we meant is that a partially constructed proof term does not provide the same interactive experience as the tactic mode. For example, pointing at X in the middle of the following incomplete proof in the "Expected type" mode shows the entire goal rather than the subgoal "in the focus":

example (f : (i : ℕ) → i < n → α)
    (hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a)
    (hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s)
    (a : α) :
    a ∈ s ↔ ∃ i, ∃ (hi : i ∈ range n), f i (mem_range.1 hi) = a :=
    ⟨fun ha =>
        let ⟨i, hi, eq⟩ := hf a ha
        X,
        fun ⟨i, hi, eq⟩ => eq ▸ hf' i (mem_range.1 hi)⟩

[Kyle Miller]

You're supposed to use an _ instead of an X. If you do, you can see the current goal at that point if you move your cursor before _.

[Kyle Miller]

The deal is that X is an elaboration error, but _ elaborates to a metavariable that can capture that context.

[Kyle Miller]

You can even write sorry there. Anything that doesn't give an elaboration error.

[Eric Wieser]

Why isn't the expected type shown anyway? It's shown if I add an id before the X:

import Mathlib
open Finset
variable (s : Finset α)
example (f : (i : ℕ) → i < n → α)
    (hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a)
    (hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s)
    (a : α) :
    a ∈ s ↔ ∃ i, ∃ (hi : i ∈ range n), f i (mem_range.1 hi) = a :=
    ⟨fun ha =>
        let ⟨i, hi, eq⟩ := hf a ha
        id X, -- put cursor before `id`, everything is fine
        fun ⟨i, hi, eq⟩ => eq ▸ hf' i (mem_range.1 hi)⟩

[Eric Wieser]

(my expectation would be that the X is elaborated as a sorry with an error message, and so I can get the expected type where the sorry goes)

[Ilya Sergey]

@Patrick Massot @Eric Wieser Thank you for the kind words.

But it certainly looks impenetrable so people would like to understand what are the benefits.

I can very much relate to that. So let me note that one of the key advantages of LeanSSR compared to Coq/SSReflect is that the former truly allows for the "small-step" proof debugging (this is what we consider one of the main features).

That is, if you open any of our proofs in a project that has been compiled and step between the symbols, you'll see the changes in the tactic state. This, hopefully, will provide additional intuition on what is the meaning of each operation.

[Eric Wieser]

I think the problem you are facing is that many of your readers here are not comparing to Coq/SSReflect, but to "regular" Lean tactics. As you say, there is a big advantage in your version over the Coq version; it's just not the initial comparison a Lean user will make. (I don't think this is a problem with your paper)

[Kyle Miller]

@Eric Wieser It's possible this is a bug, and we always write 100% perfect code so we've never noticed :laughing: (Rather, if there's an error we're probably focused more on that and fix it first)

[Ilya Sergey]

the thing that is really unusual for us is the intro/revert dance. The standard Lean tactic try to hide this as much as possible.

Ah, I see. This is very useful for us to realise. SSR style is certainly much more "stack-based" in spirit. So the pervasive intro/revert patterns are merely there to massage the goal (i.e., the "stack") to hit it with the hypotheses.

[Mario Carneiro]

Ilya Sergey said:

That is, if you open any of our proofs in a project that has been compiled and step between the symbols, you'll see the changes in the tactic state. This, hopefully, will provide additional intuition on what is the meaning of each operation.

I do appreciate that, but I guess as a lean user I'm used to expecting it. Unfortunately I find it's not really enough to truly grok a new proof language; I don't really know Coq but I can step though proofs in the library and observe that things change in the direction of getting solved and then poof the goal is done, and I make random modifications and then random surprising things stop working and so I just leave it as is... It's not easy to break in to the language from that angle

[Mario Carneiro]

I would really love a "Coq for the lean user" tutorial for either traditional coq or ssreflect

[Eric Wieser]

Does the Coq/SSReflect library (with an editor of your choice) provide semantic highlighting in the editor that hints at the structure of the proof? I suspect that your LeanSSR gets that for free, in the form of pale highlights over the AST nodes when you hover over them.

[Shreyas Srinivas]

@Ilya Sergey : I think another related point is that it took me until page 3 to figure out what "symbolic" meant. So one of the claims of the paper in section 2 is that lean SSR makes it more convenient to switch between the function style definition and predicate style definition with #reflect command. In lean the typical proof style is to write a definition, followed by a number of simple "API" lemmas, so that downstream theorems don't need to deal with the definition's innards. Can LeanSSR help reduce this need for API lemmas?

[Mario Carneiro]

One thing I am especially interested in is if there is a way to translate SSR to 'traditional' lean proof scripts. Given that you were able to write LeanSSR in lean I guess that all the tools are already present, but is it possible to take a SSR proof and write it entirely using regular lean tactics (even if it's much more verbose)?

[Mario Carneiro]

I think doing such a translation on some representative examples would be very helpful for the people here, including me

[Ilya Sergey]

@Eric Wieser @Shreyas Srinivas @Mario Carneiro Great questions, but please allow me or @Vladimir Gladstein handle them in a few hours: it's rather late in Singapore now.

[Kyle Miller]

(One tool tactics can use to do the revert/intro pattern is docs#Lean.MVarId.withReverted, though many tactics end up handling this themselves. That function is for fairly simple cases.)

[Eric Wieser]

(I'm curious what the effect of Elab.pushInfoLeaf is in that function, and how it manifests in the goal view)

[Sebastian Ullrich]

(It does not affect the info view, only find-references, unused-variables, and so on)

[Mario Carneiro]

fvarAliasInfo nodes are for tracking when a variable is "semantically renamed" to a different FVarId which is still morally represented by the original. This is used for example in the unused variable linter: if you have a variable h : x + 1 = 2 in context and rw or induction rewrites it to h : x = 1, then uses of the new h count as uses of the old h, and conversely if the new h is not used then we may flag the old one as unused

[Jireh Loreaux]

@Ilya Sergey thanks for this explanation, it makes sense to me now.

[Frédéric Dupuis]

Another point that I find a bit confusing is that there seems to be two completely disjoint things going on here: on the one hand, the stack-based intro/revert proof style and associated shortcuts, and on the other hand the actual small-scale reflection, #reflect and so on. Is there a particular reason why these two things are packaged together?

[Eric Wieser]

This has always been the thing that impeded me from learning what "reflection" meant in Coq, because it seemed to not be well-distinguished from the tactic framework in general

[Ilya Sergey]

Frédéric Dupuis said:

Another point that I find a bit confusing is that there seems to be two completely disjoint things going on here: on the one hand, the stack-based intro/revert proof style and associated shortcuts, and on the other hand the actual small-scale reflection, #reflect and so on. Is there a particular reason why these two things are packaged together?

Indeed, this is correct: to the large extent, the SSR language for proof context manipulation is independent from the reflection support, and, in my observation, many Coq user use just the tactic language for its concise way to express proofs without bothering to implement their own Reflect-lemmas. This is confirmed by the first 1.5 pages of the Introduction of the SSReflect tutorial.

That said, in the original SSReflect for Coq this style of proof management is chosen partially because it helps to "massage" the goal for subsequent "switching" between the logical and the symbolic representation, as we show in Fig. 14 of our paper. Somewhat curiously, this point no longer applies to LeanSSR, as the switching is done transparently (we explain it more in the paper).

@Eric Wieser The idea of proofs by reflection in Coq is much older than SSReflect, and I wouldn't even dare to say that it was Coq-specific to begin with. However, proof by symbolic computation in traditional Coq is usually hidden as a part of specialised tactics that invoke certified solvers and is not something regular users implement often. The small-scale aspect of SSR is, informally, about democratising proofs by computations with user-provided definitions, so they could be used pervasively in the proofs. LeanSSR provides precisely this experience, enhanced with Lean's capability to derive equalities about symbolic definitions (see Section 3.4 of our paper).

[Kyle Miller]

I've been trying to understand what reflection gives you, and it seems to me the main feature in the example is that if you make a boolean function that computes an inductively defined Prop, then you can automatically derive @[simp] lemmas, but I'm not sure I'm really grasping what the purpose is.

I'm sure this is more interesting for something that's not a toy example, but for what it's worth, in mathlib (lacking any automation for it) we would probably just write those simp lemmas:

inductive even : Nat -> Prop where
  | zero : even 0
  | add2 : ∀ n, even n -> even (n+2)

attribute [simp] even.zero

@[simp]
theorem even_add_two {n : Nat} : even (n + 2) ↔ even n := by
  constructor
  · generalize hm : n + 2 = m
    rintro (_|_)
    · simp at hm
    · cases hm
      assumption
  · apply even.add2

-- Written in a Lean version of SSReflect style
example n m (h : even n) : even (m + n) ↔ even m := by
  induction h generalizing m
  case' add2 => rw [← Nat.add_assoc]
  all_goals simp [*]

-- Written in a more idiomatic style
example n m (h : even n) : even (m + n) ↔ even m := by
  induction h generalizing m <;> simp [← Nat.add_assoc, *]

[Kyle Miller]

For those who are interested, here's an annotated version of the LeanSSR proof of the earlier example, using the more-or-less the corresponding Lean tactics.

example (f : (i : ℕ) → i < n → α)
    (hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a)
    (hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s)
    (a : α) :
    a ∈ s ↔ ∃ i, ∃ (hi : i ∈ range n), f i (mem_range.1 hi) = a := by
  -- The full LeanSSR proof: move=> ⟨/hf ![i /mem_range] | ![i hi <-]⟩ //
  -- move
  whnf -- this is a no-op in this case
  -- ⟨.. | ..⟩
  constructor
  case' mp =>
    -- /hf ![i /mem_range]
    -- /hf
    intro h; apply hf at h; revert h
    -- ![i ..]
    rintro ⟨i, H1, H2⟩
    revert H1 H2
    -- /mem_range
    intro H1
    rw [← Finset.mem_range] at H1
    revert H1
  case' mpr =>
    -- ![i hi <-]
    -- ![i hi ..]
    rintro ⟨i, hi, H⟩
    -- <-
    rw [← H]
    clear H
  -- //
  all_goals aesop -- not a direct translation, but same intent

[Kyle Miller]

And here's that proof but optimized a bit using Lean idioms

example (f : (i : ℕ) → i < n → α)
    (hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a)
    (hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s)
    (a : α) :
    a ∈ s ↔ ∃ i, ∃ (hi : i ∈ range n), f i (mem_range.1 hi) = a := by
  constructor
  case' mp =>
    intro h
    apply hf at h
    obtain ⟨i, H1, H2⟩ := h
    rw [← Finset.mem_range] at H1
  case' mpr =>
    rintro ⟨i, hi, rfl⟩
  all_goals aesop

(That could be compared to the one in this message that's a tactic version of the original term proof.)

[Eric Wieser]

Regarding §3.3 of the paper and the use of EnvExtensions to store tactic-local state; I suspect this is unsafe with regards to parallelism. I expect the recommended approach to be to use docs#StateT to add extra state to a TacticM, though I'm not sure how to interface that with elabTactic without duplicating all its code.

[Kyle Miller]

It seems that the "zen" of this SSR tactic language is to try to keep hypotheses in the goal as much as possible, and so there are sort of two stacks at work. First, the goal stack, which is exactly the same thing as Lean's tactic list (which already has its own stack-manipulation tactics) and second the "hypothesis stack" (my naming), of hypotheses that are still in the pi type of the goal's target. By avoiding intro-ing, you can avoid needing to name them.

It seems to me that the terseness of SSR is mostly a matter of choosing symbols for each tactic, rather than naming them, and Lean could enjoy the benefits of the SSR philosophy by having additional "normal" tactics that have their features.

That loses the APL philosophy where you want to cram as much as possible into a short amount of space, but SSR doesn't seem like it's intended to be a "tool of thought" like APL is — you don't really reason about tactic proofs like you do an expression.

[Eric Wieser]

Eric Wieser said:

I suspect that your LeanSSR gets that for free, in the form of pale highlights over the AST nodes when you hover over them.

I had a closer look: to make this work, you need to add docstrings to each of your syntaxes:

/-- simplification by evaluation -/
syntax "/=" : ssrTriv

etc

[Kyle Miller]

Some examples of SSR-like tactics that we could have in mathlib:

• Versions of apply that effectively does intro enough times, applies those to the lemma, then revert.
• Version of cases that effectively does intro, does cases on that, and then reverts everything. (Note: you don't actually need to implement it this way.)
• An extension to rintro that in addition to being able to use a rfl pattern for substitution, lets you do <- and -> patterns to rewrite.
• A recursive version of cases that keeps doing cases on the last constructor argument, as an inverse to anonymous constructor notation.
• Versions of constructor that let you do case => or case' => on each goal in a structured way. (Maybe we just need a version of next => that is like case' => but pushes the goal to the end of the goal list at the end?)

[Eric Wieser]

Version of cases that effectively does intro, does cases on that, and then reverts everything. (Note: you don't actually need to implement it this way.)

I think this is currently captured in docs#Prod.forall etc, though perhaps our current approach is worse than the one you suggest

[Kyle Miller]

Yeah, that's how we usually handle this. It's fine, but the cost is we have to write a forall lemma for every single type we want to do this for.

[Jireh Loreaux]

Kyle, I'm not necessarily saying we shouldn't have those, but I do worry it could lead to over-golfing.

[Eric Wieser]

I think it would be reasonable for them to be autogenerated with every structure; but the nice thing about your suggestion is that it makes it easier to choose which binders to apply the unpacking to

[Jireh Loreaux]

That (over-golfed) was my impression of the SS reflect tactic language (the utility of reflection aside), but I was holding my tongue because I know that it could just be my lack of familiarity with the syntax.

[Kyle Miller]

Jireh Loreaux said:

Kyle, I'm not necessarily saying we shouldn't have those, but I do worry it could lead to over-golfing.

There are lots of little manipulations where it's just logic, and you just want to restructure some exists/foralls/sigmas/what-have-you and it's obvious from there.

But in any case, I think the broader point is that the really terse symbolic language that SS reflect presents you is obscuring the fact that there are some useful tactics in here that I think we're missing, that would look perfectly fine as Lean tactics. As far as I understand it, there's nothing about SS reflect that requires each tactic to be a couple symbols long.

[Kyle Miller]

Consider going from

hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
a : α
⊢ a ∈ s → ∃ i, ∃ (hi : i ∈ range n), f i ⋯ = a

to

a : α
⊢ (∃ i, ∃ (h : i < n), f i h = a) → ∃ i, ∃ (hi : i ∈ range n), f i ⋯ = a

by "applying" hf to the front of the goal's target. Then you could do an rintro to deconstruct that existential, or simp using docs#forall_exists_index (This tactic state appears in the examples above.)

The only way I know how to do that is intro h; apply hf at h; revert h, and that's using @Adam Topaz's relatively new apply ... at ... tactic. This one acting on the goal could potentially be apply hf at ⊢ (Not to be confused with apply hf, which also acts on the goal!)

[Kyle Miller]

Of course, every new tactic is a new tactic to learn, and this is just combining a few basic tactics.

[Shreyas Srinivas]

Kyle Miller said:

I've been trying to understand what reflection gives you, and it seems to me the main feature in the example is that if you make a boolean function that computes an inductively defined Prop, then you can automatically derive @[simp] lemmas, but I'm not sure I'm really grasping what the purpose is.

Whence my question about reducing the manual work of writing these lemmas as API lemmas.

Another question that might be of interest: what is the anticipated effect of using this proof style on the compilation time of mathlib.

[Vladimir Gladstein]

Good morning (Singapore time) every one, finally I am woke up and can handle your questions.
First of all, let me thank all of you for a really detailed and thoughtful discussion on LeanSSR. Reading all your comments, I have learnt a lot, and would be happy to integrate your comments to make LeanSSR even better.

Let me first address concerns raised by @Kyle Miller and @Shreyas Srinivas about computational reflection.
As @Ilya Sergey has already mentioned, the main feature of Coq/SSReflect is that it allows you to bind the boolean and propositional representations of the same predicate.
The main idea here is that you only have to prove Reflect instance for two predicates, and you will get three things for free:

1. First, you get partial evaluations principles. In Coq/SSreflect, whenever you want to use them, you have to “switch” from propositional representation to a boolean one. Please refer to the Coq proof in Section 4.1. Correspondent switches are done via /subseqP.
2. Second, you can still enjoy the inductive nature of your predicate. Like induction on even n in section 2.6, and case analysis on line 7 of Fig 8.b
3. Finally, you actually prove that your predicate is decidable for free as well! You can case analysis on true/false values of your predicate, use it inside if-the-else and so on…

The beauty of this approach is that all 3 advantages come from one principle: reflection.
For sure, using “API” lemmas + proving the Deciable instance manually would give same benefits. But the advantage of reflection is that it allows to unify “API” lemmas and Deciablein one concept, and minimise the manual effort to achieve the same thing.
For example, we invite you to prove “API” lemmas for subseq predicate (seq. 2.7) and also prove that it is Decidable. During the proof of Decidability via reflection with subseqbyou will essentially have to prove that subseq behaves in the same way as subseqb does. And this is pretty much the same as proving “API” lemmas (where we once again establish that subseq can be reduced in the same way as subseqb)

If you have a look at the MathComp libraries about lists seq.v and path.v you will see that they contain 70 other reflect lemmas for such predicates on lists as all , has (= any), uniq (uniqness of list elements), constant (all elements of the sequence are equal) and so forth.
Hence, boolean/propositional reflection can be well-integrated in the process of developing mechanised libraries for various data structures. Here, automated generation of “API” lemmas and Decidable instances can help to minimise the effort for such developments.

[Vladimir Gladstein]

From the technical side, LeanSSR reflection is easy to control. Autogenerated lemmas are added as unfolding theorems for a propositional predicate. So writing simp only [even] and simp [-even] is available.

[Shreyas Srinivas]

Thanks for this answer. I think I see a clear way forward to understand the benefits of SSR with the subseqb example and this reflection could very well be the MVP of this paper for me personally. I am curious to see how this can help with reducing the size of Std which has a lot of the computational stuff. Not sure about Mathlib since most of the stuff I know in there is built around typeclasses.

[Shreyas Srinivas]

Also, another small point is that, based on the proofs written by Johann and Kyle, it seems a shortcut for Aesop would be handy

[Vladimir Gladstein]

Let me also address concerns about LeanSSR as a tactic language. First, I have to admit, SSReflect proof style 90% is a matter of taste. From my own experience, all Coq users I know are either absolutely hate it, or absolutely love it.
Let me try to list my objective reasons which make me use SSReflect anytime I can. If those reasons resonate with you, you might also consider trying SSReflect in your project.

1. First of all, I hate coming up with names for hypothesis. Thinking of a name for a fact that I might end up using only once (or not using at all) slows me down. SSReflect allows me to either (a) use facts on top of the stack without explicitly naming them via ->, <-, []… or (b) reorder the elements of the goal stack (via /[swap] and /[dup]) and do (a).
2. Informally, I always prove lemmas using forwards style of reasoning. That is, I always make facts from my local context strong enough, such that automation can handle the rest. And it is hard for me to think of a proof in terms of backwards style reasoning, where you simplify the goal instead. That is why it is inconvenient for me to prove lemmas by manually handcrafting the term: it enforces the backwards style of reasoning (we explain it in sec. 4.2). In vanilla Lean, I would have to use obtain/apply at to incorporate forwards style. But it forces me to name everything I might need in future. Views, from sec. 2.5, neither require explicit naming of the argument, which I apply my lemma to, nor require me to name the result.
3. Another concern about obtain, is not as smart as apply .. in .. and apply .. at ... So it will not figure out dependent arguments in application automatically. In the same time, views will figure out all dependent arguments. Here it is important that, unlike apply .. at .., views will not create any subgoals for unknown arguments. It will just keep them as preconditions for the lemma after application (explained below). This is essential because you can use the result in SSReflect style of proof further.

For example, (A -> B -> C) -> B -> A -> C can be simply solved as move=> H /H //, or even better using a shortcut for H /H as move=> /[apply] //. Here, after we apply A -> B -> C to B we get A -> C at the goal stack. For more elaborated examples, try out this line. Here /(_ X) pattern is the reverse of /X: it applies the top element of the stack to X

[Vladimir Gladstein]

Shreyas Srinivas said:

Also, another small point is that, based on the proofs written by Johann and Kyle, it seems a shortcut for Aesop would be handy

Yeah, this is a good idea indeed. The only problem is that we don't want SSReflect to depend on anything, rather than std4. You might also consider augmenting // with aesop or extending ssrTriv/ssrIntro with it locally. It can easily be done following suggestions from sec 3.2

[Vladimir Gladstein]

Eric Wieser said:

Eric Wieser said:

I suspect that your LeanSSR gets that for free, in the form of pale highlights over the AST nodes when you hover over them.

I had a closer look: to make this work, you need to add docstrings to each of your syntaxes:

/-- simplification by evaluation -/
syntax "/=" : ssrTriv

etc

That is super cool, thanks! We will add docs for each LeanSSR tactic.

[Vladimir Gladstein]

Kyle Miller said:

Some examples of SSR-like tactics that we could have in mathlib:

• Versions of apply that effectively does intro enough times, applies those to the lemma, then revert.
• Version of cases that effectively does intro, does cases on that, and then reverts everything. (Note: you don't actually need to implement it this way.)
• An extension to rintro that in addition to being able to use a rfl pattern for substitution, lets you do <- and -> patterns to rewrite.
• A recursive version of cases that keeps doing cases on the last constructor argument, as an inverse to anonymous constructor notation.
• Versions of constructor that let you do case => or case' => on each goal in a structured way. (Maybe we just need a version of next => that is like case' => but pushes the goal to the end of the goal list at the end?)

One more thing that we have in LeanSSR (and that we didn't have space to cover in the paper) are suggestions for case analysis. For example, in LeanSSR if you write ?[] LeanSSR will suggest you to replace it with [ | | ... | ] with a correspondent number of alternations. As LeanSSR doesn't require mentioning constructors of the term being destructed (and doesn't require naming arguments of those constructors) ?[] is super easy to implement.

[Mario Carneiro]

that's close to what rcases? does (or did, it hasn't yet been ported to lean 4)

[Vladimir Gladstein]

Eric Wieser said:

Regarding §3.3 of the paper and the use of EnvExtensions to store tactic-local state; I suspect this is unsafe with regards to parallelism. I expect the recommended approach to be to use docs#StateT to add extra state to a TacticM, though I'm not sure how to interface that with elabTactic without duplicating all its code.

Thanks for pointing this out! I will try to ask it during Lean office hours to receive more comments.

[Vladimir Gladstein]

Mario Carneiro said:

that's close to what rcases? does (or did, it hasn't yet been ported to lean 4)

I think you meant that [ | | .. | ] is close to rcases, right? It is true indeed.
The difference of [ | | .. | ]and rcases/rintro is that [ | | .. | ] allows you to use all other intro patterns inside each branch (like views /hyp, automation //, applying ext lemmas ! and so on)

However, in my message, I was mostly talking about providing Try this: suggestions for a number of alternations.

[Mario Carneiro]

I was speaking specifically about the ?[] behavior, which is similar to rcases?

[Mario Carneiro]

that is, a code action and try this which suggests a pattern match (it's more than just number of alternations because it can be nested)

[Vladimir Gladstein]

Mario Carneiro said:

I was speaking specifically about the ?[] behavior, which is similar to rcases?

Oh sorry, I missed ? in rcases?. I am not familiar with this tactic, but I suppose that yes, it is similar

[Mario Carneiro]

rcases syntax is inspired by intro patterns in Coq

[Vladimir Gladstein]

As far as I can tell intro patterns are inspired by SSReflect :)

[Mario Carneiro]

although it doesn't have the view pattern stuff (this is a deliberate design decision though, it's a bit hard to motivate applying a lemma as a "pattern" in the traditional sense)

[Mario Carneiro]

I think the fanciest rcases patterns get is the - pattern which clears the hypothesis

[Vladimir Gladstein]

Mario Carneiro said:

One thing I am especially interested in is if there is a way to translate SSR to 'traditional' lean proof scripts. Given that you were able to write LeanSSR in lean I guess that all the tools are already present, but is it possible to take a SSR proof and write it entirely using regular lean tactics (even if it's much more verbose)?

Thanks for asking! We were thinking of doing that as well. The only problem is apply in tactic for views, which doesn't correspond to anything in Lean. Modulo this tactic, I suppose we can make such translation.

[Vladimir Gladstein]

Mario Carneiro said:

I think the fanciest rcases patterns get is the - pattern which clears the hypothesis

You can look up all LeanSSR intro patterns at our wiki

[Mario Carneiro]

I can definitely see that using the pattern grammar for more things is a powerful mechanism for increasing the expressivity of the language, but lean's tactic language is to some extent deliberately simplified such that it's not too unfamiliar to those with some general programming background. SSReflect to me looks like the "vim" of tactic languages: optimized for the expert and impenetrable to the newcomer

[Mario Carneiro]

and also so core to your interaction that you want to take it with you wherever you go once you learn it :)

[Vladimir Gladstein]

Mario Carneiro said:

I can definitely see that using the pattern grammar for more things is a powerful mechanism for increasing the expressivity of the language, but lean's tactic language is to some extent deliberately simplified such that it's not too unfamiliar to those with some general programming background. SSReflect to me looks like the "vim" of tactic languages: optimized for the expert and impenetrable to the newcomer

That is true. To somehow tackle this, we do two things:

1. We (as well as initial SSR developers) try to keep it minimalistic. LeanSSR has around 20 different intro pattens, where only 15 of them, you will use in your "every day life". It is slightly more than CoqSSR, I think we have added 3 new intro patterns. Those patterns should be enough (at least from my experience) for almost any reasonable goal manipulation.
2. Unlike CoqSSR, we have LeanSSR interactive: such that you can step through each symbol ad see what happens there.

[Vladimir Gladstein]

But I acknowledge that it is might be impenetrable to the newcomer

[Mario Carneiro]

Do you find the goals of SSR to be incompatible with having a newcomer friendly language? That is, if you were to take all the tactics and make a mechanical translation into "traditional style" tactics which is still idiomatic and effective, would it no longer serve the goals of SSR proof style? (This is a question along the lines of Kyle's reference to "APL as a tool of thought", where making the core commands less terse would actually defeat the purpose, or so the proponents say.) This would clearly fail in the goal of being syntactically compatible with Coq's ssreflect, so it probably wouldn't be appropriate for LeanSSR (which from what I can tell is primarily aimed at giving people with prior ssreflect experience an analogue in Lean), but it seems like this is the most promising avenue for feeding the new tactics back into lean core and mathlib.

[Vladimir Gladstein]

Mario Carneiro said:

Do you find the goals of SSR to be incompatible with having a newcomer friendly language? That is, if you were to take all the tactics and make a mechanical translation into "traditional style" tactics which is still idiomatic and effective, would it no longer serve the goals of SSR proof style? This would clearly fail in the goal of being syntactically compatible with Coq's ssreflect, so it probably wouldn't be appropriate for LeanSSR (which from what I can tell is primarily aimed at giving people with prior ssreflect experience an analogue in Lean), but it seems like this is the most promising avenue for feeding the new tactics back into lean core and mathlib.

That is certainly a good question which requires a thoughtful investigation. At the first glance, it seems to me that we indeed can provide LeanSSR with a friendlier syntax by implementing @Kyle Miller suggestions. On the other side, I don't see any obstacles in having two different dialects of the same proof language. With LeanSSR->Lean translation, we can easily transform LeanSSR proofs, if we want to merge them in Mathlib. But do you see any problems in having a second proof dialect for new end-to-end projects? As for me, it can only turn more people to Lean side.

[Vladimir Gladstein]

Think the main goal of our development was not to make all Lean users switch to LeanSSR, but to provide a new proof style alternative to attract even more people.

[Vladimir Gladstein]

I mean, CoqSSR community is quite big and exceptionally prolific, and they have their own reasons to use SSReflect proof style. Let's try to turn them to Lean as well.

[Vladimir Gladstein]

Kyle Miller said:

I've been trying to understand what reflection gives you, and it seems to me the main feature in the example is that if you make a boolean function that computes an inductively defined Prop, then you can automatically derive @[simp] lemmas, but I'm not sure I'm really grasping what the purpose is.

I'm sure this is more interesting for something that's not a toy example, but for what it's worth, in mathlib (lacking any automation for it) we would probably just write those simp lemmas:

inductive even : Nat -> Prop where
  | zero : even 0
  | add2 : ∀ n, even n -> even (n+2)

attribute [simp] even.zero

@[simp]
theorem even_add_two {n : Nat} : even (n + 2) ↔ even n := by
  constructor
  · generalize hm : n + 2 = m
    rintro (_|_)
    · simp at hm
    · cases hm
      assumption
  · apply even.add2

-- Written in a Lean version of SSReflect style
example n m (h : even n) : even (m + n) ↔ even m := by
  induction h generalizing m
  case' add2 => rw [← Nat.add_assoc]
  all_goals simp [*]

-- Written in a more idiomatic style
example n m (h : even n) : even (m + n) ↔ even m := by
  induction h generalizing m <;> simp [← Nat.add_assoc, *]

Actually, Lean SSR reflect proof can be simplified to

inductive even : Nat -> Prop where
  | zero : even 0
  | add2 : ∀ n, even n -> even (n+2)

@[reflect]
instance evP n : Reflect (even n) (evenb n):=
  match n with
  | 0 => by sdone
  | 1 => by apply Reflect.F=> // []
  | n + 2 => by scase: (evP n)=> /== ?->
                { sby apply Reflect.T }
                sby apply Reflect.F=> // []

#reflect even evenb

example : even n -> even (m + n) = even m := by
  sby elim; srw -?Nat.add_assoc

Not that in the LeanSSR proof, we also get the Decidable instance for even

[Mario Carneiro]

I'm totally on board with having LeanSSR exactly as is or even better, as a way of implementing SSReflect itself in Lean for people who prefer that style and bringing more people over from Coq which are hampered by the mismatch. But I don't see it ever making it into mathlib because of the style differences, and that's why pursuing some kind of "disguised SSR" which is more mathlib-compatible would also be a useful line of investigation.

[Mario Carneiro]

Certainly lean/std/mathlib have struggled a lot (mostly successfully) with trying to put up a united front with respect to having a similar proof style so that code in one project can be transplanted to another project or moved upstream. I think that one reasonable concern about LeanSSR (or more accurately, the projects using it) is that it promotes a fracturing of the ecosystem in proof style. I'm not too worried about this because the projects that use SSR style would probably not be written at all without it, but I think we should also give thought to how to breach the new barrier of translating between LeanSSR and traditional lean, through tooling and documentation.

[Vladimir Gladstein]

@Mario Carneiro thanks for your comments, I totally agree. Let us aim then for LeanSSR->Lean translation first. After that, if we will get a bit more (than 0) LeanSSR users from the Lean side, we can start thinking together what would be a better syntax for SSR proofs.

[Marc Huisinga]

Vladimir Gladstein said:

Let me also address concerns about LeanSSR as a tactic language. First, I have to admit, SSReflect proof style 90% is a matter of taste. From my own experience, all Coq users I know are either absolutely hate it, or absolutely love it.
Let me try to list my objective reasons which make me use SSReflect anytime I can. If those reasons resonate with you, you might also consider trying SSReflect in your project.

1. First of all, I hate coming up with names for hypothesis. Thinking of a name for a fact that I might end up using only once (or not using at all) slows me down. SSReflect allows me to either (a) use facts on top of the stack without explicitly naming them via ->, <-, []… or (b) reorder the elements of the goal stack (via /[swap] and /[dup]) and do (a).
2. Informally, I always prove lemmas using forwards style of reasoning. That is, I always make facts from my local context strong enough, such that automation can handle the rest. And it is hard for me to think of a proof in terms of backwards style reasoning, where you simplify the goal instead. That is why it is inconvenient for me to prove lemmas by manually handcrafting the term: it enforces the backwards style of reasoning (we explain it in sec. 4.2). In vanilla Lean, I would have to use obtain/apply at to incorporate forwards style. But it forces me to name everything I might need in future. Views, from sec. 2.5, neither require explicit naming of the argument, which I apply my lemma to, nor require me to name the result.
3. Another concern about obtain, is not as smart as apply .. in .. and apply .. at ... So it will not figure out dependent arguments in application automatically. In the same time, views will figure out all dependent arguments. Here it is important that, unlike apply .. at .., views will not create any subgoals for unknown arguments. It will just keep them as preconditions for the lemma after application (explained below). This is essential because you can use the result in SSReflect style of proof further.

For example, (A -> B -> C) -> B -> A -> C can be simply solved as move=> H /H //, or even better using a shortcut for H /H as move=> /[apply] //. Here, after we apply A -> B -> C to B we get A -> C at the goal stack. For more elaborated examples, try out this line. Here /(_ X) pattern is the reverse of /X: it applies the top element of the stack to X

Idly wondering: how does SSReflect fare in terms of proof brittleness / how easy it is to fix proofs when definitions change?

[Ilya Sergey]

@Marc Huisinga This is a brilliant question, which would require quite a bit of empirical studies, and we are wondering if someone has done any evaluation of Lean capacities with regard to Proof Repair.

For Coq, this has been done, to some extent, in the scope of Talia Ringer's earlier works on refactoring proofs about functional programs, and our own work on proof repair for imperative code. It would be very interesting to apply these techniques for evolving mathlib-style proofs, but it would require to have some motivating examples first.

[Eric Wieser]

Vladimir Gladstein said:

Thanks for pointing this out! I will try to ask it during Lean office hours to receive more comments.

Please report back with your findings after you've done this :). I'm curious to know what the "correct" approach is.

[Frédéric Dupuis]

Vladimir Gladstein said:

Mario Carneiro thanks for your comments, I totally agree. Let us aim then for LeanSSR->Lean translation first. After that, if we will get a bit more (than 0) LeanSSR users from the Lean side, we can start thinking together what would be a better syntax for SSR proofs.

I think it would also be worth it to try to "decouple" the reflection part from the proof style part of LeanSSR: I don't see any reason why we wouldn't want the former in mathlib!

[Joachim Breitner]

Hello Ilya, nice to see you here!

Unlike CoqSSR, we have LeanSSR interactive: such that you can step through each symbol ad see what happens there.

I’m baffled that Coq users manage these kind of proofs at all without this feature. (Back in my Coq days I stepped around SSReflect, maybe partially because of that, or maybe because the APL-like syntax scared me.)

[Ilya Sergey]

Hi @Joachim Breitner

I’m baffled that Coq users manage these kind of proofs at all without this feature.

They are a tough bunch indeed. But not nearly as tough as Dafny users that manage their proofs without any access to the proof context whatsoever. :nerd:

[Kyle Miller]

Something I'm still not understanding is what the Reflect typeclass is for, and what it gives that Decidable can't.

I can see that Reflect could be used to lift boolean expressions to Prop expressions, which is neat, since then you can, for example, do cases on && or || like they were And or Or.

But for deriving equations, it seems to me that you can get this from Decidable.

Here's an experiment creating a reflect_unfold tactic that unfolds an inductive predicate by looking for a Decidable instance:

code

import Mathlib

namespace DecTest

set_option autoImplicit true

instance (p : Prop) : CoeOut (Decidable p) Bool := ⟨@decide p⟩

@[inline] def dtrue {p : Prop} (h : p := by aesop) : Decidable p := isTrue h
@[inline] def dfalse {p : Prop} (h : ¬ p := by aesop) : Decidable p := isFalse h
@[inline] def decide_by {p : Prop} (q : Prop) [Decidable q] (h : q ↔ p := by aesop) : Decidable p :=
  decidable_of_iff q h

inductive Even : Nat -> Prop where
  | zero : Even 0
  | add2 : ∀ n, Even n -> Even (n+2)

attribute [simp] Even.zero Even.add2
attribute [aesop safe cases] Even

instance evend : DecidablePred Even
  | 0 => dtrue
  | 1 => dfalse
  | n+2 => decide_by (evend n)

theorem decide_prop (p : Prop) [Decidable p] : p = decide p := by simp only [decide_eq_true_eq]

theorem decide_decide_by (p q : Prop) {dq : Decidable q} (h : q ↔ p) :
    @decide p (decide_by q h) ↔ q := by simp [h]

section
open Lean Meta Elab

private def getSimpUnfoldContext : MetaM Simp.Context :=
   return {
      congrTheorems := (← getSimpCongrTheorems)
      config        := Simp.neutralConfig
   }

def reflect_unfold (e : Expr) (declName : Name) : MetaM Simp.Result := do
  (·.1) <$> Simp.main e (← getSimpUnfoldContext) (methods := { pre := pre })
where
  pre (e : Expr) : SimpM Simp.Step := do
    if e.isAppOf ``Decidable.decide then return .done {expr := e}
    unless e.isAppOf declName do return .continue
    let inst ← try synthInstance (← mkAppM ``Decidable #[e]) catch _ => return .continue
    let some inst ← withDefault <| unfoldDefinition? inst | return .continue
    let eq ← mkAppOptM ``decide_prop #[e, inst]
    let eqTy := (← inferType eq).eq?.get!
    return .done {expr := eqTy.2.2, proof? := eq}

elab "reflect_unfold' " declNameId:ident : tactic => do
  let declName ← resolveGlobalConstNoOverloadWithInfo declNameId
  Tactic.liftMetaTactic1 fun mvarId => do
    let target ← instantiateMVars (← mvarId.getType)
    let r ← reflect_unfold target declName
    if r.expr == target then throwError "\
      tactic 'reflect_unfold' failed to unfold '{declName}' at{indentExpr target}"
    applySimpResultToTarget mvarId target r

macro "reflect_unfold " declNameId:ident : tactic =>
  `(tactic| (reflect_unfold' $declNameId ; (try simp only [decide_decide_by]); try simp))

end

example (h : Even n) : Even (m + n) ↔ Even m := by
  induction h
  · rfl
  · rw [← Nat.add_assoc]
    /-
    a_ih✝ : Even (m + n✝) ↔ Even m
    ⊢ Even (m + n✝ + 2) ↔ Even m
    -/
    reflect_unfold Even
    /-
    a_ih✝ : Even (m + n✝) ↔ Even m
    ⊢ Even (m + n✝) ↔ Even m
    -/
    assumption

Two things to focus on:

1. With some helper functions for Decidable, you can write the Decidable instance like it was a boolean function. This works here because the inductive predicate is simple enough, and aesop can do cases on it to prove the side goals.

instance evend : DecidablePred Even
  | 0 => dtrue
  | 1 => dfalse
  | n+2 => decide_by (evend n)

2. An example of the tactic, which "unfolds" Even by synthesizing a Decidable instance, unfolding it, and converting it back to the land of propositions by applying some simp lemmas.

example (h : Even n) : Even (m + n) ↔ Even m := by
  induction h
  · rfl
  · rw [← Nat.add_assoc]
    /-
    a_ih✝ : Even (m + n✝) ↔ Even m
    ⊢ Even (m + n✝ + 2) ↔ Even m
    -/
    reflect_unfold Even
    /-
    a_ih✝ : Even (m + n✝) ↔ Even m
    ⊢ Even (m + n✝) ↔ Even m
    -/
    assumption

[Kyle Miller]

Btw, your paper, and, in particular, your repository has been very helpful to understand the SSR tactic framework. The metaprogramming code has been a "Rosetta stone" for me :smile:

I'm just trying to understand "what's really going on" to see what Lean is missing -- this unfolding-via-decidable-instances is certainly not something I've seen before, and it would be good to know if Reflect contributes more than this idea, and/or if the typeclass isn't necessary and the rest can be done with simp lemmas, sort of like how the norm_cast tactics work.

[Joachim Breitner]

I wonder how this reflect_unfold relates to the simp lemmas that you get for an inductive predicate in Isabelle. I think there you will get, from the inductive Even, the (very useful!) simp lemma Even (n + 2) \iff Even n without further ado.

[Shreyas Srinivas]

My understanding of Vladimir's response is that we get a bunch of simp lemmas for free

[Kyle Miller]

This reflect_unfold tactic could be turned into a simp lemma generator, but for a prototype it was easy to do it this way as a tactic.

[Shreyas Srinivas]

Ah I see Joachim's message precedes mine.

Anyway, I haven't had access to my machine to test this yet and won't have one for a few days. I am trying to understand precisely what this entails.

[Kyle Miller]

Two quick tests, just to see what it would do with the first mathlib predicates I could think of:

-- The global `Even`, not the `Even` from the previous code blocks.
example (n : Nat) : Even n := by
  reflect_unfold Even
  -- ⊢ n % 2 = 0
  sorry

-- Unfolds to `List.isPerm`, which makes sense, but it can be unfolded more.
example (x : Nat) (xs ys : List Nat) : List.Perm (x :: xs) ys := by
  reflect_unfold List.Perm
  /-
  ⊢ List.isPerm (x :: xs) ys = true
  -/
  unfold List.isPerm
  /-
  ⊢ (List.contains ys x && List.isPerm xs (List.erase ys x)) = true
  -/

[Joachim Breitner]

Maybe it's fair to say that the decidable instance deriver does more or less what Isabelle's simp lemma generator does: both have to construct equations describing when the predicate holds; the decidable instance then additionally turns these equations into a function.

[Kyle Miller]

It would be neat if there were a Decidable deriver in Lean for this example

inductive Even : Nat -> Prop where
  | zero : Even 0
  | add2 : ∀ n, Even n -> Even (n+2)
  deriving Decidable

(but alas I had to write that instance myself)

[Shreyas Srinivas]

Were you able to run the experiment Vladimir suggested with subseqb?

[Joachim Breitner]

Oh, I somehow assumed there was, no reason why I did. So more to play catch up with Isabelle…

[Vladimir Gladstein]

Thanks @Kyle Miller for your comment! Actually, initially, I was also thinking about generating simp lemmas by extracting them from the proof of Decidable instance. I think I gave up on it because of two reasons. First one is that I am not that familiar with Lean metaprogramming and this way appears to me a bit harder than via Refelct. So now I am happy to see this implementation from experts. There is a second, more subtle, reason. Let me try to explain it below.
Correct me if I am wrong, but what you essentially do is that you try to fetch the boolean representation from the proof of Decidable instance, right? Then the benefit of Reflect type class is that you can hint how to “reflect” each particular boolean sub routine used in the boolean representation.

For example, have a look at has (equivalent to List.any) predicate. Our goal is to make has a (x :: xs) be unfolded to a x \/ has a xs.
Let's see how we can prove Decidbale instance for has. One way would be to do something like:

namespace HasTest

variable (a : α -> Prop) [DecidableEq α] [DecidablePred a]

def has (s : List α) : Prop := ∃ (x : α), x ∈ s ∧ a x

instance hasd :  DecidablePred (has a)
  | [] => decide_by False (by simp [has])
  | x :: s =>
    if a x then
      decide_by True (by sorry)
    else decide_by (hasd s) (by sorry)

example x (xs : List α) : has a (x :: xs) = a x ∨ has a xs := by
  reflect_unfold has
  /- (decide (has a (x :: xs)) = true) = a x ∨ decide (has a xs) = true -/
  sorry

In this case, reflect_unfold will get stuck because it doesn't know how to deal with if-then-else statement in the second branch of hasd definition. To fix it, we will have to prove a lemma similar to decide_decide_by which will say how to propagate decide over if-then-else statement, and add it to reflect_unfold definition:

theorem decide_ite {t e : Decidable p} [Decidable b] :
    @decide p (ite b t e) = ite b (decide t) (decide e)  := by sorry

macro "reflect_unfold " declNameId:ident : tactic =>
  `(tactic| (reflect_unfold' $declNameId ; try simp only [decide_decide_by, decide_ite]; try simp))

However, it will still only reduce has to if-then-else statement, not a x \/ has a xs.
So another way would be to specify exactly what has a (x :: xs) should be simplified to by:

instance hasd :  DecidablePred (has a)
  | [] => decide_by False (by simp [has])
  | x :: s =>
    @decide_by _ (a x ∨ has a s) (@Or.decidable _ _ (decide_by (a x)) (decide_by (hasd s))) (by sorry)

Now you can check that refelct_unfold will unfold has a (x :: xs) to a x \/ has a xs.
The problem with this approach is that you will have to provide the unfolded form of the predicate to decide_by in each non-trivial branch.
The benefit of Reflect is that if you provide an instance for each standard boolean function (in the same way as we do at Fig 13), then type class resolution will figure out what this unfolded form should look like automatically.

More specifically, in our approach, we take the unfolded form of the boolean predicate and via type class resolution infer the propositional representation for it. In the case, when this unfolded form is a composite expression, type class resolution will replace each subcomponent, making use of corresponded Reflect instances.
Here, as we know that hasb a (x :: xs) is unfolded to a x || hasb a xs, and we have a Reflect instance for ||, type class resolution will replace it with a x \/ has a xs.

Moreover, using instance priorities, you can control what propositional representations should we peak in each particular case.

[Vladimir Gladstein]

To sum up, assume we have proven Refelct P b. Then types of simp lemmas generated for P are determined by the definition of b. Type class resolution will take care of replacing each sub-expression of b in the way we want. Note that, that is what we want: we want P to reduce in exactly the same way as b does.
In addition, do you don't have to care, how do you actually prove Refelct P b. And this proof can be quite complicated.

If you want to extract simp lemmas from the proof of Decidableyou will either

1. have to take care of the construction you use in the proof, such that we know to fold them into a boolean function. This might not be so pleasant with complicated Decidable instances
2. or you will have to explicitly say how your proof should be extracted (via the first arg of decide_by). This is exactly what type classes are meant to automate.

[Kyle Miller]

One thing to keep in mind is that for Decidable instances, you ought to take care in their construction anyway. They're not just proofs, and they actually get run in a few places (either in proof by reflection using the decide tactic, or in executable code, where Decidable gets extracted as a plain boolean in C). If this is too complicated, you can use docs#decidable_of_iff (which is what my decide_by is a frontend to) to specify which boolean function to use instead, and then you are able to reduce the problem to providing a mere proof rather than interleaving proof and algorithm.

Regarding needing simp lemmas to push propagate decide, yeah, that would be what is required for reflect_unfold. In Lean you can create "simp sets" of lemmas, which can be added to by the user, and there could be a simp set for pushing decide into an expression. This can be a much more powerful approach than relying on typeclass resolution. In fact, there are now simprocs, so users could add arbitrary transformations to this simp set. (When I referred to norm_cast, that's part of a pair of tactics that pushes or pulls coercions into or out of an expression. It's driven by simp sets. Pushing decide into expressions seems similar.)

[Kyle Miller]

Vladimir Gladstein said:

And this proof can be quite complicated.

I spent a little time looking at doing this using mathlib style for comparison (though was pulled away to grade final exams for calculus...) and something that I was struggling with was that it seemed like this Reflect theorem would be easier to prove if I were to prove all the small "API lemmas" first, and these would include the equation lemmas that #reflect would later generate. Then, if I did that, there felt like there would be no point to the experiment.

In mathlib we're generally wary of seeing a giant proof, since a giant proof is usually not irreducibly complex, and everyone would be better off if it were refactored to be a small proof applying numerous factored-out helper lemmas.

[Kyle Miller]

This seems like a possible framework:

1. propify and boolify to translate a statement to and from Prop and Bool, driven by simp sets (and perhaps the Reflect class). These could be aware of decide. The simp sets could be full of rw-style theorems like p <-> b = true to drive the translation. (It would need two simp sets, one for the p <-> b = true direction, and another for the b = decide p direction. There could be a @[boolify] attribute that validates a lemma and adds both versions to the simp sets.)
2. reflect_unfold that uses the propify/boolify machinery. It (1) locates the definition to unfold, (2) uses a @[boolify] lemma on it if one exists, and otherwise generates one from a Decidable instance, (3) unfolds what it sees, then (4) applies propify.

Maybe the reflect_unfold tactic could also be provided an explicit @[boolify] theorem for performing the unfolding.

[Kyle Miller]

#reflect could work by taking the equation lemmas for a particular boolean definition or decidable instance and then propify them.

This all seems to be similar to what your library is doing, but having dedicated propify and boolify tactics would be very useful. Especially now that there are many library functions that take Bool-valued functions rather than decidable predicates (for example, docs#List.all), and now that there is a BEq class in addition to the DecidableEq class.

[Vladimir Gladstein]

Thanks for your clarifications! I generally feel inclined towards your suggestions, and I suspect that this framework can indeed be designed in terms of Decidabe using more advanced tricks with simp. However, I still have a couple of concerns.

[Vladimir Gladstein]

Kyle Miller said:

Regarding needing simp lemmas to push propagate decide, yeah, that would be what is required for reflect_unfold. In Lean you can create "simp sets" of lemmas, which can be added to by the user, and there could be a simp set for pushing decide into an expression. This can be a much more powerful approach than relying on typeclass resolution. In fact, there are now simprocs, so users could add arbitrary transformations to this simp set. (When I referred to norm_cast, that's part of a pair of tactics that pushes or pulls coercions into or out of an expression. It's driven by simp sets. Pushing decide into expressions seems similar.)

At this point, it would be interesting to see an example when somprocs can give more than type classes do in the scope of boolean/propositional reflection

[Vladimir Gladstein]

Kyle Miller said:

This seems like a possible framework:

1. propify and boolify to translate a statement to and from Prop and Bool, driven by simp sets (and perhaps the Reflect class). These could be aware of decide. The simp sets could be full of rw-style theorems like p <-> b = true to drive the translation. (It would need two simp sets, one for the p <-> b = true direction, and another for the b = decide p direction. There could be a @[boolify] attribute that validates a lemma and adds both versions to the simp sets.)
2. reflect_unfold that uses the propify/boolify machinery. It (1) locates the definition to unfold, (2) uses a @[boolify] lemma on it if one exists, and otherwise generates one from a Decidable instance, (3) unfolds what it sees, then (4) applies propify.

Maybe the reflect_unfold tactic could also be provided an explicit @[boolify] theorem for performing the unfolding.

I wonder what would be situations where we need to use @[boolify] and @[propify] except translating boolean reduction principles to prop? I mean, assume we have already proven reflect statements for all our predicates. Then why would even use boolean representations again? Can't we just formulate everything in terms of those propositional representations?
And if we formulate everything, in terms of propositional predicates, do we need to “boolify” or “porpify” anything at all?

[Vladimir Gladstein]

One more thing.

Kyle Miller said:

This seems like a possible framework:

1. propify and boolify to translate a statement to and from Prop and Bool, driven by simp sets (and perhaps the Reflect class). These could be aware of decide. The simp sets could be full of rw-style theorems like p <-> b = true to drive the translation. (It would need two simp sets, one for the p <-> b = true direction, and another for the b = decide p direction. There could be a @[boolify] attribute that validates a lemma and adds both versions to the simp sets.)
2. reflect_unfold that uses the propify/boolify machinery. It (1) locates the definition to unfold, (2) uses a @[boolify] lemma on it if one exists, and otherwise generates one from a Decidable instance, (3) unfolds what it sees, then (4) applies propify.

Maybe the reflect_unfold tactic could also be provided an explicit @[boolify] theorem for performing the unfolding.

This is really similar to the approach people are using in general proofs by reflection in Coq. The idea is exactly the same:

1. we find an expression that we want to solve/simplify (for example p)
2. we change its representation to the more convenient one (p → decide p = true)
3. then we use some ad-hoc machinery to reason about the convenient representation (simplify decide p using simp sets)
   There are a bunch of Coq Reflection papers and books: chapter 15 at CPDT, ITP14 paper, Rtac framework for Coq.

I strongly believe that the approach you are suggesting would be a nice alternative to the line of work on reflective proofs done in Coq. I am happy to take this discussion offline and see if we can do better in Lean with these regards.

[Vladimir Gladstein]

You can have a look at 15.3 chapter of CPDT to see a good non prop/bool example of reflective proof.

[Vladimir Gladstein]

Actually, general reflective proofs in Lean are something I was planning to look at in the nearest future. In particular, I am interested in program verification via reflection.

[Assia Mahboubi]

I am jumping in this discussion quite late and I apologize in advance for the long post. Indeed, LeanSSR is really cool! Like @Ilya Sergey , I also find it cooler than the original ssreflect on the fragment it implements. And this is yet another example of how neat metaprogramming in Lean is.

[Assia Mahboubi]

Now I will also react to some points raised earlier in the thread.

[Assia Mahboubi]

As already emphasized, ssreflect should not be confused with its characteristic choices of syntax, as characteristic and debatable as they can be. These choices could have been different, provided they satisfy the constraints of "compositionality" and the collection of features it provides.

[Assia Mahboubi]

The distinguishing features of ssreflect are what make people adopt the language, as whole or only for a specific selection of these features. I am pretty sure a vast majority of the users would be perfectly fine with a different syntax, provided the features remain. And, as for any tactic language, the design of these features proceeds from the combination of several objectives.

[Assia Mahboubi]

Some are specific to certain formalization methodologies, e.g., small scale reflection in the case of ssreflect. Defining (small-scale) reflection, illustrating its benefits and evaluating whether or not lean/mathlib would benefit from additional support for this a question I am leaving aside for now, despite the title of the topic.

[Assia Mahboubi]

Other objectives are quite universal I guess, typically striving to provide appropriate tools for producing robust scripts, easy to maintain over time. At least, this point is also obviously taken very seriously by the mathlib community. And this was another of the main concerns guiding the design of ssreflect. Robustness here refers both to changes in the proofs / dependencies but also in the behavior of the proof assistant itself. The formal proof of the four color theorem is more than 20 year old, the one of the Odd Order theorem (including a large chunk of what is called today Mathematical Components) is more than 10 years old. Meanwhile, Coq has changed a lot , and the libraries have also of course evolved significantly. Yet the maintenance effort is really very minimal in terms of manpower.

[Notification Bot]

37 messages were moved from this topic to #general > ssreflect idioms in Lean by Kyle Miller.

[Shreyas Srinivas]

Notification Bot said:

37 messages were moved from this topic to #general > ssreflect idioms in Lean by Kyle Miller.

This link seems inaccessible. I was able to click on it and read the discussion about various conv patterns by Eric and Mario once, but the entire conversation seems to have disappeared.

[Michael Stoll]

I think it is here .

[Shreyas Srinivas]

Thanks :)