Abbreviations in tactic mode

[robertylewis]

I'm close to finishing the construction of the reals- currently I've shown through commutative ring, with a few holes. The missing theorems have some annoying notation that would be nice to abbreviate.

Currently you can use 'let' to define new terms in tactic proofs, but this is only useful for props, as the data seems to be lost:

example (a b : ℕ) : a = a :=
  begin
    let z := a,
    --have H : z = a, from rfl,  -- this line doesn't work
    apply refl
  end

Is there a way to introduce an abbreviation using let (or something similar), and rewrite the context/goal using the new abbreviation?

[leodemoura]

Unfortunately, this is not supported. Given the goal,

   a b : nat |- a = a

The tactic let z := a is reducing it to the new goal:

  a b : nat, z : nat |- a = a

Suppose we resolve the new goal, and obtain a proof term pr : forall (a b : nat) (z : nat), a = a. Then, the proof term for the original goal is fun (a b : nat), pr a b a.

To do what you want, we would need to add a new kind of hypothesis: z : nat := a. This is a big change since it affects all tactics.

That being said, we can break big theorems in smaller pieces in a section, and define local notation. It would be something like

section big_theorem
   parameters {A : Type} (a b : A) (f : A -> A -> A)
   hypothesis (h : a = b)
   hypothesis ...
   local notation `*` := f
   private lemma aux_lemma_1 (c : A) : a * c = c := ...
   private lemma aux_lemma_2 ...

   theorem my_big_theorem : ... := ...
end big_theorem

[robertylewis]

I see. Thanks for the explanation! I'll find a way to work around it like you suggest.

[leodemoura]

@avigad @fpvandoorn This is an important issue. We should decide whether we support let-expressions in the kernel or not. It is tricky to postpone the decision because it will get harder and harder to implement as the code base increases in size.

Right now, we don't, the let-expressions are "simulated" in the frontend. Jeremy: I don't know if you remember but we discussed this issue in the past. To add let-expressions, we have to:

• add let-expression expr.h and a new kind of local constant (aka free variable) x : type := value.
• all procedures that manipulate expressions have to be updated since there are two new kinds of expressions.
• the normalizer have to implement the reduction x : type := value => value.
• the unifier and matcher have to take into account the new kind of expression
• the goal has a new kind of hypothesis x : type := value. So, anything (e.g., tactics) that manipulate goals have to be adjusted.

This is a big change... I'm not excited about doing it, but this is not the first time we had problems because we do not have let-expressions in the kernel.

[avigad]

I remember the discussions. How is "let" handled now? My understanding is that the terms that the kernel sees are fully expanded (though perhaps stored in compressed form, with pointers), but there are annotations in the term that tell the pretty-printer to use a "let" abbreviation. Is that right?

I don't have a strong opinion here. Until this point, I would not have noticed any difference. But I have not used tactics so much yet for long proofs (like Rob is doing). I remember that when working in SSReflect, being able to write "pose" in a tactic proof, ("pose a := foo bar") was helpful.

Can one simulate it somewhat by going into proof-term mode, and using the "let" there?

What are some other problems we have had without "let" in the kernel?

[leodemoura]

I remember the discussions. How is "let" handled now? My understanding is that the terms that the kernel sees are fully expanded (though perhaps stored in compressed form, with pointers), but there are annotations in the term that tell the pretty-printer to use a "let" abbreviation. Is that right?

Exactly.

Can one simulate it somewhat by going into proof-term mode, and using the "let" there?

More or less, the "abbreviation" will only be available in proof-term mode. For example, it will not be available if we return to tactic mode.

What are some other problems we have had without "let" in the kernel?

For example, I had problems with the following kind of declaration

theorem ... :=
  let f := ... in
  assert h : P f, from ...,
  begin
      -- here in tactic mode, f is not available, and all occurrences of f are expanded. 
      -- Example: the of h is not (P f)
  end

The summary is: the current trick we use only works for proof-term mode.

[avigad]

Hmmm. Floris, Jakob, Rob, and you have naturally gravitated towards long tactic proofs, and the proofs we do will get longer, so I guess in the long run it will make a difference.

[fpvandoorn]

I hardly use the let expression, and I haven't missed the ability to abbreviate certain terms in a tactic proof. I do see that this can be useful in long proofs, but I don't think that this is the most important feature to focus attention on right now. I also rarely used this feature in Coq.

[mikeshulman]

For what it's worth, I think this is a very important feature. In older versions of Coq the assert tactic was not transparent, and I found this to be very annoying when doing HoTT. When newer versions of Coq made a transparent assert possible, it made for much cleaner proofs. Separating out using a lemma or section is very annoying when you are in the middle of a long proof with lots of hypotheses.

Similarly, it would be nice to have a transparent version of have for forward reasoning, that could be referred back to with this and backquotes.

[fpvandoorn]

I do want to add change my statement from half a year ago. In the last half year I have missed this feature, and I would use it quite often. I still think it's not top priority, though.

[mikeshulman]

Commit 144b570 that mentions this issue appears to claim that it's adding let-expressions to the kernel. It sounded from the above discussion as though the lack of let-expressions in the kernel was the main obstacle to having a transparent let tactic. If the kernel does now have let-expressions, how much work would it be to add a transparent let tactic?

[leodemoura]

@mikeshulman Commit 144b570 was a failed experiment. The Lean kernel does not have let-expressions in the kernel, and we have decided in a separate mail thread we will not add this kernel extension.

Our plan is to change the representation we use for goals in the tactic framework. We would include a “fake" hypothesis of the form (H : T := V), and label occurrences of the term V as H. Then, we would also have to change tactics to treat occurrences of the labeled term V as an "name". For example, the simplifier and rewriter tactics should not go inside V. We would also have to change the elaborator. It needs to create these fake hypotheses and label terms for the tactic framework. The main advantage of this solution is that we don’t have to change the kernels (C++ and Haskell) The disadvantage is that it is a little bit hackish. We have to make sure all tactics respect the “illusion”. It is not a complicated change, but it is quite laborious. This change is on our TODO list, but it is not the main priority right now. @dselsam and I are currently working full-time on automation for Lean.

[mikeshulman]

@leodemoura Thanks for the explanation! Would this or something like it also allow transparent have?

[leodemoura]

Would this or something like it also allow transparent have?

Yes, we will be able to use let (as a transparent have) in proof-term and tactic modes.

[Kha]

@leodemoura I'm trying to understand the issues of the current implementation, but I can't reproduce the problems with entering tactic mode, at least not in a simple example:

example (A B) (f : A → B) (x : A) : B :=
  let y := f x in
  begin
    apply y
  end

While it's true that y is unfolded in the tactics block, this seems to be equally true in proof-term mode: have h : y = y, from _, shows f x = f x as the current goal.

[fpvandoorn]

The problem is with the let tactic. Compare:

example (A B) (f : A → B) (x : A) : f x = f x :=
let y := f x in
eq.refl y

example (A B) (f : A → B) (x : A) : f x = f x :=
begin 
  let y := f x,
  exact eq.refl y 
end

[leodemoura]

There is also one problem that affects the let-term: it is eagerly expanded.

example (a b : nat) : a + b = 0 -> a = 0 :=
assume H, 
let      c := a + b in
have  Hc : c = 0, from H,
begin
   state  -- in the proof state we have Hc : a + b = 0 instead of Hc : c = 0
end

[fpvandoorn]

Now that I think about it, the following does work:

example (A B) (f : A → B) (x : A) : f x = f x :=
begin 
  exact 
  let y := f x in
  begin exact eq.refl y end
end

Maybe we can (temporarily) make the tactic let y : A := t be syntactic sugar for (or act the same as)

exact let y : A := t in begin [...] end

[Kha]

@fpvandoorn I should have clarified that I was referencing Leo's let-term example (if only there was an easy way of quoting Github comments). Either way, the conclusion I wanted to draw is the same as yours: If the term let also works in tactic mode, it seems like there should be a way to make the tactic let semantically equivalent. Your workaround is great, but I think it will break if there are multiple active subgoals.

@leodemoura Coming from Isabelle/Isar, I am actually used to exactly that behavior. But I see that the tactic let is also used to introduce hypotheses that are then rewritten, so I suppose we cannot just make it syntactically transparent. Considering that, wouldn't the issue be solved by introducing a new tactic command that behaves like the term let?

[leodemoura]

@fpvandoorn the trick exact let y : A := t in begin [...] end is better than nothing. The main problems is that it is still being eagerly expanded. Another minor problem is that it is not really a tactic because it relies on begin ... end (e.g., we cannot use begin ... end inside of an orelse or repeat tacticals). Recall that begin ... end blocks cut the search space. A begin ... end block is a construct for grouping sequences of tactics, where each step is a "checkpoint" (aka Prolog cut). Another problem is that y can only be used in terms embedded inside of the begin ... end. For example, suppose we have

let H : a = 0 := ...,
simp  

The tactic simp would not be able to use H : a = 0, since there is no H : a = 0 in the context. So, it would not rewrite a to 0.

@Kha The current let-tactic is building a proof term of the form (fun y : A, ?M) t, where ?M is a placeholder representing the new proof/term to be synthesized after executing the tactic. In the new context, we have y : A, but we don't have t.

Considering that, wouldn't the issue be solved by introducing a new tactic command that behaves like the term let?

Yes, but we would have to store the the fact y : A := t inside of the new goal.

We have the current proposal:

1- Change the representation for goals in Lean. They would contain sequence of declarations H : A and labeled terms y : A := t. In the current implementation, we have only H : A. The labeled terms would be represented as let-value y (t : A), where let-value is just annotation for (t : A) with the name y. These labeled terms are similar to the annotations we already have in Lean. We implement these extensions using the "macro" expressions supported by the kernel. These macros are all expanded when we execute the kernel at trust-level 0. For this one, let-value y (t : A) expands to t.

2- Some tactics contains nested terms (e.g., apply and exact). These terms are elaborated using the goal context at tactic execution time. Actually, the argument for these tactics are not really terms, but pre-terms, since they have not been elaborated yet. To elaborate these pre-terms, we set the elaboration context using the goal. Now, we would also have to replace occurrences of y in the pre-term with let-value y (t : A).

3- We have to modify the pretty printer to print let-value y (t : A) as y (this is easy).

4- We have to adjust all existing tactics to take into account the new representation for goals. For example, simp should be able to use a hypothesis introduced using let. Tactics such as rewrite should not "visit" the nested term (t : A) at let-value y (t : A). Moreover, when we rewrite a let-value hypothesis, we would have to "propagate" the change to all its occurrences.

5- We have to modify the type class resolution procedure to consider local instances of the form let-value y (t : A). Right now, the type class resolution procedure ignores local instances declared using let-terms. This issue has been raised in another thread.

There is nothing technically hard, but it is a lot work.

[Kha]

(Oh, I just found out about the r shortcut for quoting comments. Too bad it doesn't recover formatting.)

Considering that, wouldn't the issue be solved by introducing a new tactic command that behaves like the term let?

Yes, but we would have to store the the fact y : A := t inside of the new goal.

I fear I'm leading the discussion in circles, so please stop me if that is the case, but I still don't see why we need to store the fact for a transparent let (assuming we keep the current, opaque let for all other cases). I've thrown together a quick experiment at https://github.com/Kha/lean/commit/43f14482589da8e65fb31cd5e883332caef8bf7f, which, as expected, breaks at the few places where you need an opaque let, but does allow tactic proofs like the following (which wouldn't work with the exact workaround):

example (A) (x : A) : x = x ∧ x = x :=
begin
  apply and.intro,
  let y := x,
  apply (eq.refl y),
  apply (eq.refl y),
end

[leodemoura]

@Kha your proposal is not perfect, but it is simple. It combines the implementation of the have-tactic with the one for let-terms. You are eagerly expanding y in the pre-terms in the current scope at parsing time. Then, when the let-tactic is executed, it adds an opaque y to the context.

It is a good temporary workaround, but it has the following problems.

• Some y's are expanded eagerly, but the hypothesis y added by the let-tactic is opaque, and after the execution, it is not the case that this opaque y is definitionally equal to x.
• Users will complain that some y's are expanded and others are not when printing the proof state.
• The current let-term (and your suggestion) do not respect dynamic scoping rules in tactic mode. In the following example, the intro Ha is shadowing the Ha : f a = 0. In your approach, the behavior will be different.

example (a b : nat) : b = 0 → f a + b = 0 :=
begin
  have Ha : f a = 0, from f_ax a,
  intro Ha,
    rewrite Ha -- Ha here is (Ha : b = 0)
end

[leodemoura]

@Kha I mistakenly claimed your suggestion uses the existing let-tactic. This is not the case. You used the id tactic instead.

So, we also have the problem of missing hypothesis. For example, in the following example simp uses H to simplify. If we replace the have with a let, the H will not be there. So, the let will not really be a "transparent have" since it is not adding any hypothesis to the proof state.

import data.nat
open nat

constant f : nat → nat
axiom f_ax : ∀ n, f n = 0

example (a b : nat) : f a + b = b :=
begin
  have H : f a = 0, from f_ax a,
  simp
end

[Kha]

I understand that two separate tactics could lead to some confusion, but careful documentation may be able to prevent that. So let me sketch a more complete proposal:

• Tactic let should be transparent and not introduce a hypothesis, i.e. behave just like term let. It should primarily be used to introduce aliases for values, meaning its purpose is the same as in any other functional language. One could argue whether it should be folded back in printed proof states; the Isabelle developers must have had some good reason not to, but I'm assuming implementing it should not be too hard(?)
• For the opaque, fact-introducing variant I'd propose a new tactic note H := expr (name borrowed from Isabelle). However, instead of comparing it to let, I would simply introduce it as a shorthand for have H : <inferred>, from expr and say that it is useful for introducing existing propositions as hypotheses. This should make it clear that the two tactics have quite different scopes of application.

[leodemoura]

@Kha I think your proposal is a good workaround. It addresses many issues. I like the note tactic. @fpvandoorn Does it solve the let-problems you have been having in HoTT? I'm wondering if you also need a transparent let for non-trivial proof terms.

the Isabelle developers must have had some good reason not to, but I'm assuming implementing it should not be too hard(?)

@Kha I think they have the same problem we have. To implement the let properly, they would have to revise the tactic framework and how they represent goals and the proof state. It is not conceptually hard, but it is a lot of work.

[Kha]

@Kha I think your proposal is a good workaround. It addresses many issues. I like the note tactic.

Great to hear! If @fpvandoorn agrees, I'd be happy to implement it.

[leodemoura]

@fpvandoorn Here is a potential scenario that may affect you.

begin
   ...
   let H := non-trivial-term,
   ...
   apply f H
   ...
   apply g H
   ...
end

We would be replacing H with the non-trivial-term (at parsing time), and each tactic using H would have to re-elaborate H. Moreover, the result may be different since the elaboration process depends on the context. For proof-term mode, the problem is minimized since we have one big simultaneous elaboration step. Similarly, in the tactic,

   apply f H H 

we have two copies of H, but they would be elaborated only once, since they are solved in the same elaboration round. To be able to communicate the result of the elaboration between different tactics, we would also have to extend the tactic framework.

[fpvandoorn]

I'm not really sure whether this would satisfy my needs. One thing which I would want is that if I write let H := non-trivial-term the term H will also be used in goals.

One question: when I write let H := non-trivial-term, in tactic mode, non-trivial-term will not be elaborated at all? So when non-trivial-term contains x, and I later write f H, the x will refer to whatever x is in the context at that moment, and not the moment I wrote let? That would be confusing to me, but I don't know how it will play out in practice. Is it possible to elaborate non-trivial-term already as much as possible when I wrote the let tactic? Or is that problematic, since then the term can become ill-typed if the context changes?

I'm wondering if you also need a transparent let for non-trivial proof terms.

Yes, I would probably use it for non-trivial proof terms. For example, I might want to define a functor (consisting of 2 functions and 2 proofs) within a let and then proof that this functor has some nice properties (e.g. it's an equivalence). I would mainly use let so that I can more easily input the functor, and the goal will become clearer when the functor is replaced by a variable.

[leodemoura]

One question: when I write let H := non-trivial-term, in tactic mode, non-trivial-term will not be elaborated at all?

Yes, in @Kha patch, it is not. It is not really a tactic, but a macro.

I later write f H, the x will refer to whatever x is in the context at that moment, and not the moment I wrote let?

Yes. This is also the case for the current let terms. This is what I meant when I said: The current let-term (and your suggestion) do not respect dynamic scoping rules in tactic mode.

Is it possible to elaborate non-trivial-term already as much as possible when I wrote the let tactic?

It is possible, but it is not a simple change. It is also possible to refactor to refactor the tactic framework as I suggested above, but it is laborious.

Or is that problematic, since then the term can become ill-typed if the context changes?

Yes. I think a workaround should be used only if it is very simple to implement. @Kha workaround is not perfect, but it is a small change, and it will address simple cases.

[fpvandoorn]

Yes. I think a workaround should be used only if it is very simple to implement. @Kha workaround is not perfect, but it is a small change, and it will address several cases.

I agree. It does indeed address several cases, so I think we should try it.

[leodemoura]

@Kha has implemented the proposal above, and it has been integrated in the main branch. https://github.com/leanprover/lean/commit/2185ee7e95f27f190b5e3cd26124ef43e684fb73

So, I'm closing this issue. The original problem posted by @rlewis1988 has been addressed. We still have some rough corners (discussed above), but we are currently postponing a permanent solution.

[robertylewis]

This is great, thanks @Kha !

[robertylewis]

@Kha I've come across some strange behavior in the let tactic. I think it would be easy to fix (if you and @leodemoura agree this is the wrong behavior). The following succeeds:

example : true :=
  begin
    let H'' := blah,
    trivial
  end

This one fails where you'd expect ("unknown identifier blah"):

example : true :=
  begin
    let H'' := blah,
    apply H''
  end

Should the argument to let be type checked when the tactic is called? Technically there's nothing really wrong with the first example, but it seems strange.

[Kha]

@rlewis1988 That certainly seems unintuitive, but it is basically the same issue raised by @fpvandoorn above. @leodemoura mentioned that it wouldn't be easy to fix this - and it really would be a workaround on top of a workaround, since it would only be correct when the context between definition and usage of a let doesn't change.

[robertylewis]

Oh, I'm sorry. I thought I looked through the thread to see if this had been brought up, but somehow I missed Floris' post. It's a bit of a shame this is complicated to fix. Once I train myself to use note instead of let, I suspect it won't catch me very often, but it's still quite counterintuitive.