catching errors?

Stream: metaprogramming / tactics

[Damiano Testa]

Dear All,

I am working on the tactic that rearranges sums.

The tactic applied to an expression, recurses into the expression until it finds a sum. It then decomposes each sum into summands and rearranges them according to what the user specifies.

My problem is that the tactic will fail is at least one of the summands that appear in the whole expression does not contain one of the terms specified by the user. Is there a way to get the tactic to succeed if on at least one of the found sums it succeeds?

Here is an example of what I would like to work. Suppose that you want to prove the equality

  1 + 3 = 2 + 2

You think, if only I could commute the 1 and the 3, then I would be done. So, you call the move_add tactic saying move_add 1. The tactic looks at the expression, finds that 1 + 3 and 2 + 2 are sums and tries to rearrange them, putting 1 to the right of each sum. On 1 + 3 it succeeds, on the 2 + 2 it fails.

I would like the tactic to perform the substitution on the branch where it succeeded and ignore the error from the other branch.

Is there a way to do this?

Thanks!

[Arthur Paulino]

@Damiano Testa do you have the permalink to recurse_on_expr? It might be insightful for those who can help

[Damiano Testa]

Sure, this is where the recursion recurse_on_expr takes place.

(Line 127 of the file, if the link does not get you there.)

[Damiano Testa]

While trying to wrap my head around this, I would like to know if this is possible or meaningless.

docs#tactic.unify checks if two expressions can be unified, succeeds if they do and returns a tactic unit.

My understanding of this is that I can either use the information that the unification is available or else all computations stop.

Is it possible to continue the computation instead?

In my use-case, I have two lists of expressions and I want to produce the sublist of the first list of terms that unify with some element of the second list.

Right now, I can extract such a sublist only in the case in which all elements of the first list unify with elements of the second one. In the remaining case, Lean stops computing.

[Eric Rodriguez]

I think some of the monadic filters are what you want here. iirc, mfilter has this behaviour?

[Eric Rodriguez]

or maybe some of the <$>-like operators, but I'm rustier than a nail with tetanus on those

[Damiano Testa]

The way I filter the list is exactly using mfilter, but the computation appears to stop when there is a no match.

[Damiano Testa]

The mfilter allows me to take a list and obtain a tactic list, but I have not been able to get it to go past a failure.

[Damiano Testa]

(unless of course I also have another bug somewhere else that is the responsible for the stopping of computation)

[Damiano Testa]

I should probably learn what <$> is, then.

[Eric Rodriguez]

oh, do you mean if the list is completely empty?

[Damiano Testa]

No, in my tests I have a list with some unification and some non-unification.

[Damiano Testa]

I'm happy to receive an empty list, in case nothing unifies. In fact, I want the empty list, instead of no computation!

[Damiano Testa]

For instance, if I try this on [a,b] and want to extract the terms that unify with [a,c], I get a list, if b unifies to either a or c and nothing otherwise.

[Mario Carneiro]

@Damiano Testa Your code for recurse_on_expr does not take into account bound variables: The case | (expr.lam _ _ _ e) := recurse_on_expr e will expose free variables (expr.var), and you can't call lean builtin tactics like pp on such terms

[Mario Carneiro]

The | e := e.get_app_args.mmap' recurse_on_expr case is going to cause your tactic to fail if any of the branches fail, which is probably not correct for a "search" tactic

[Damiano Testa]

Ah, Mario, thanks! Could you also tell me how to expose bound variables and how to fix the issue with failing branches?

Thanks!

[Mario Carneiro]

I'm not totally clear on how you want this code to work in the first place, so it's hard to suggest a replacement. To find the first tactic that succeeds and exit early, use docs#tactic.first instead of mmap'

[Mario Carneiro]

Regarding bound variables, you need to use instantiate when you enter a binder. src#tactic.generalize_proofs has an example

[Mario Carneiro]

but the surrounding stuff depends on what you want to do when you enter the binders

[Mario Carneiro]

@Damiano Testa

[Damiano Testa]

Ok, thanks, I'll try.

What I want is for the code to scan the expression, identify all exprs that are a sum and, whenever one expr is a sum, start performing the rest of the code.

E.g. if the expr is f (a + b + c) = d +e I would like the recursion to isolate a + b + c and d + e and on each continue with the rest of the code.

[Damiano Testa]

(The bound variables issue is secondary, I think, since I have not started testing with that yet)

[Mario Carneiro]

does "the rest of the code" produce a value? How should that value be incorporated into the overall proof?

[Mario Carneiro]

Why is a + b not listed in your list?

[Damiano Testa]

If I run move_add [a] on (a + b + c) = d +e I would like the result to be (b + c + a) = d +e (assuming d and e do not unify with a).

[Damiano Testa]

a + b is not listed, since I want the recursion to stop with it find the first has_add.add which would have been has_add.add (a+b) c.

[Damiano Testa]

(I want the recursion to stop here, but continue until it finds all first occurrences of has_add.add.)

[Mario Carneiro]

all first occurrences sounds like a contradiction

[Mario Carneiro]

is this an early exit or not?

[Mario Carneiro]

what happens if the first bit of code changes the expression?

[Damiano Testa]

probably, since the other occurrences will be on different branches, they will still take place, right?

[Mario Carneiro]

whether they take place or not is up to you

[Damiano Testa]

I would like them to take place, then

[Mario Carneiro]

so it sounds like you want to apply congr recursively

[Mario Carneiro]

unless the lhs is a a + b expression

[Damiano Testa]

Ok, I'll try with congr instead of the recursion with the matching

[Damiano Testa]

Here is an example showing what works and what I would like to work. This takes place on the latest version of the branch aa_sort (be47fbe30956ab08b9a3f864e5e26cdea698c0e3)

import tactic.move_add  -- to get `move_add`
import algebra.group.basic  -- to get basic lemmas about `comm_semigroup`s

--  What happens to hypothesis h₁ after the first `move_add` is what I aim for in all subsequent blocks
example (a b c d : ℕ) (h₁ : b + c + a = d + a + b) (h₂ : b + c + a = d + a + b)
  (h₃ : b + c + a = d + a + b) : true :=
begin
  -- rearranges both sides: I like this!
  move_add [← a, ← b] at h₁,

  -- only rearranges the lhs: I would like to also move the rhs `a` and `b`
  -- ignoring the `c` there.
  move_add [← a, ← b, c] at h₂,

  -- does nothing: I would want this to behave as the succession of the next two tactics
  move_add [a, b, c, d] at h₃,

  -- first rearranges the lhs to `a + b + c`, then rearranges the rhs to `a + b + d`
  -- I like the final result, but I would have wanted to achieve it with the single `move_add [a, b, c, d]`
  -- of the previous block.
  move_add [a, b, c] at h₃,
  move_add [a, b, d] at h₃,
  trivial
end

[Mario Carneiro]

Can you formulate the intended algorithm in prose? Not just examples. This will help you get the right control flow

[Damiano Testa]

The user provides an input: a list of terms, marked as "left" or "right" via the presence or absence of ←.
move_add scans the target expression (say the goal), stopping the first time that it reaches a term that is a sum, creating a list of expressions that are all sums of something, all embedded at various levels in the initial goal. (I am hoping that this is the meaning of recurse_on_expr.)

Once this is done, it goes through this list, one element at a time. For each element, it extracts the summands, i.e. iteratively decomposes each expression as a sum of two terms, until the atoms are no longer sums of anything. (This should be get_summands.)

Finally, it works on each list of summands. On any given list, it purges out of the list provided by the user, the terms that do not unifiy with a summand (being careful about repetitions, though I think that this is not the issue right now), and then tries to do the substitution sorted_sum. If it succeeds on the current goal (after potentially having modified the goal with the previous steps), then great, do it and continue! If it fails, then skip this element and move on to the next.

[Damiano Testa]

I hope that this clarifies what I would like to achieve!

[Mario Carneiro]

Now can you explain what it is currently doing differently from your explanation, and why it does so?

[Mario Carneiro]

hint: if find_in2 fails then unify_list fails then list.combined fails then sorted_sum fails so the <|> skip in recurse_on_expr will skip that whole subterm

[Mario Carneiro]

so I'm guessing you want to catch find_in2 failure in unify_list in order to skip missing subterms in the list

[Damiano Testa]

Mario, thank you so much! I will look at this when I am back at a computer.

Can you also give me a hint on what command to catch errors?

[Damiano Testa]

Mario, thank you so much for your help! At the moment, I think that the tactic is running as I want it to run!

It is currently not reporting any errors ever, which may be debatable. I will do some more testing to make sure that the current version is likely to be correct, even when pushed to extremes, but otherwise, I am happy to start dealing with more detailed comments: I will remove the WIP tag.

[Mario Carneiro]

Regarding error reporting, I would say:

• If a certain expression is never used (in any subterm in any hypothesis), report an error
• If the goal does not change, report an error

[Damiano Testa]

Mario, I made the tactic produce a message informing the user of which goals do not change after applying the tactic.

To address the other kind of error, an expression provided by the user not actually being needed, I am at a loss.
I could catch this, by looping over all sublists of expressions given by the user and seeing whether they produce the same results, but this seems inefficient. It might be something used by (the currently non-existing) move_add? or squeeze_move_add.

[Damiano Testa]

I could easily catch expressions that never unify, that is probably easy. However, once the unified, they will play a (possibly useless) role in some of the rewrites that appear later in the code. They will be embedded in side-goals that simp proves and then rewritten to change a local hypothesis/target.

[Damiano Testa]

I think that it would be enough to check the following.

The user-provided list of expressions determines a permutation of the list of expressions computed as a result of applying get_summands.

The user could provide the full permutation, or could simply specify which elements they want to appear first or last and then let Lean figure out the permutation. I suspect that by finding which user expressions are not needed, I would have to solve the question of deciding whether a list of expressions is minimal among the ones that realize the same final permutation.

[Damiano Testa]

However, I might even argue that this kind of minimization may not be desirable. For instance, providing the full permutation, specifying exactly which term goes where in the final expression is a very natural thing to do. The error would certainly tell you that some variable need not be provided, since, after all, a permutation on n elements is determined by what it does to n-1 elements.

E.g. if I want to change a + b + c to c + a + b I could simply say move_add [c, a, b]. I would achieve the same result by saying move_add [a, b], since once a + b is the right end of the sum, c must be the beginning.

My preference would be to not require Lean to compute such minima, at least not as a default behaviour.

[Damiano Testa]

To conclude: I think that adding a check on whether an expression provided by the user never unifies is reasonable. However, once a variable unifies and the corresponding goal changes, then the tactic should not report any error.

[Damiano Testa]

If desired, I could implement a squeeze_move_add that tries to find a minimal sublist of expressions that generates the same effect, but I would not want this to be the default behaviour.

[Mario Carneiro]

Damiano Testa said:

To conclude: I think that adding a check on whether an expression provided by the user never unifies is reasonable. However, once a variable unifies and the corresponding goal changes, then the tactic should not report any error.

Yes, this is what I meant. If the supplied term does not match any subterm it should be an error, but if it matches it should not be an error even if the tactic doesn't move it anywhere.

[Damiano Testa]

Ok, assuming CI builds, I think that the current version

• does what I want,
• reports errors,
• has some tests!