repeat

Stream: new members

[Bolton Bailey]

The documentation for repeat says: "... the tactic is applied recursively to all the generated subgoals until it eventually fails. The recursion stops in a subgoal when the tactic has failed to make progress."

Which is it: Is it applied recursively until it fails, or until it fails to make progress?

[Notification Bot]

Bolton Bailey has marked this topic as unresolved.

[Bolton Bailey]

I'll reopen this thread and ask again because I just don't understand what I'm seeing.
The code I'm working on is a bit too complicated to post an mwe, so hopefully you can bear with me. In the code below, I get an output with two different goals. It reports the error error: solve1 tactic failed, focused goal has not been solved on the final closing bracket. This suggests to me that at the very least , lines 4-6 below are not causing an error. But when I comment those lines out and rerun the program, I get a different output, which only has one goal, (but still says the same error that the goal is not solved by the final bracket).

This makes no sense to me, because, based om my reading of docs#repeat, if the middle three lines don't cause a failure, the output of t, repeat { t, }, should be the same as repeat { t, },. What gives?

{
  simp only [*] with integral_domain_simp at *,

  try {simp only [] with integral_domain_simp at *},
  try {clear found_zero}, -- clear "found_zero" if present
  done <|> begin cases ‹_ ∨ _› with found_zero found_zero; rw found_zero at *, end,

  repeat {
    try {simp only [] with integral_domain_simp at *},
    try {clear found_zero}, -- clear "found_zero" if present
    done <|> begin cases ‹_ ∨ _› with found_zero found_zero; rw found_zero at *, end },
}

[Mario Carneiro]

I would suggest replacing repeat with iterate n for different values of n and see for which values it succeeds

[Mario Carneiro]

It is worth noting that begin ... end in tactic mode is the same as { ... }. In particular, it will fail if you haven't closed the goal at the end of the block

[Mario Carneiro]

This looks like an error reporting bug:

theorem foo : true ∧ true :=
begin
  done <|> {
    refine ⟨trivial, _⟩,
  }, -- the error is actually here

  -- uncommenting this doesn't work
  -- refine trivial,

end -- but it is reported here

[Mario Carneiro]

So what is really happening is that your first begin cases line is failing and the repeat never runs

[Bolton Bailey]

Mario Carneiro said:

It is worth noting that begin ... end in tactic mode is the same as { ... }. In particular, it will fail if you haven't closed the goal at the end of the block

This is certainly good to know.

[Mario Carneiro]

You should use id { ... } instead to group tactics without the implicit done at the end

[Bolton Bailey]

Sorry, what does id do?

[Mario Carneiro]

it's a tactic combinator like try

[Mario Carneiro]

it does nothing, it's the identity function

[Mario Carneiro]

but the { ... } is part of the syntax, so it doesn't count as regular focusing brackets

[Bolton Bailey]

So you mean I should use

iterate 2 id {
  try {simp only [] with integral_domain_simp at *},
  try {clear found_zero}, -- clear "found_zero" if present
  id {cases ‹_ ∨ _› with found_zero found_zero; rw found_zero at *}, },

And this will cause it to not fail if the goal is completed by the second line?

[Mario Carneiro]

The braces after iterate 2 { ... } are also part of the syntax

[Mario Carneiro]

so that's not well formed

[Mario Carneiro]

Immediately after iterate 2 though, you already have a tactic block argument, so you don't need the id

[Mario Carneiro]

It's useful in things like done <|> id { ... }

[Bolton Bailey]

iterate 2  {
  try {simp only [] with integral_domain_simp at *},
  try {clear found_zero}, -- clear "found_zero" if present
  done <|> id {cases ‹_ ∨ _› with found_zero found_zero; rw found_zero at *}, },

[Mario Carneiro]

you can probably replace done <|> id ... with try ... in this case

[Bolton Bailey]

Wouldn't that loop forever with repeat?

[Mario Carneiro]

yes it would

[Mario Carneiro]

I think done would as well though

[Mario Carneiro]

if there are no goals then it will just spin with done succeeding every time

[Bolton Bailey]

See the very first comment in this thread. The docs for repeat should probably be changed to not say "when the tactic has failed to make progress."

[Mario Carneiro]

"make progress" isn't something lean knows how to detect

[Bolton Bailey]

Exactly my point

[Mario Carneiro]

it assumes that tactics fail when they fail to make progress

[Mario Carneiro]

which is generally true of front end tactics

[Bolton Bailey]

But not of all tactics, as I realized to my confusion a few weeks ago.

[Mario Carneiro]

If you use the more explicit structural tactics like done and try that's not quite true anymore

[Bolton Bailey]

Ok, I am confused again. iterate { fail_if_success { done }, ... } succeeds in producing 5 new simpler goals in 2 minutes or so. But repeat { fail_if_success { done }, ... } and repeat { ... } both seem to hang, taking at least 5 minutes. Why would these behave differently?

[Notification Bot]

Bolton Bailey has marked this topic as unresolved.

[Mario Carneiro]

It would really help if you made #mwe's for this stuff

[Mario Carneiro]

Why are these tactics taking minutes? You aren't supposed to exhaust the recursion limit

[Bolton Bailey]

Yes, sorry about that. Let me try to make a simpler mwe.

[Bolton Bailey]

Part of the problem is there is a lot of code earlier on in the file that takes a while to run which generates these equations, and it's hard to separate that time from the time taken by the tactics we are talking about.

[Mario Carneiro]

You seem to think that the actual content of the blocks doesn't matter, so make a MWE with a simpler block

[Mario Carneiro]

my examples use split and trivial which is usually good enough for interesting branching patterns

[Mario Carneiro]

If you need an expensive tactic, use sleep

[Mario Carneiro]

I wonder if I should #xy your problem though. This all looks very case-bashy and you haven't even shown what the goal is, but it looks like you are factoring a polynomial? I'm like 80% sure there is a better proof approach that involves specifying the factorization

[Bolton Bailey]

The problem is I keep making MWEs with simpler blocks and the error doesn't manifest.

[Mario Carneiro]

Your block doesn't seem to reference any lemmas except whatever is in integral_domain_simp, so why not just have a big list of sorry lemmas and then your theorem statement? That will at least skip the top of the file

[Mario Carneiro]

You can also use trace_state to see how the evaluation is progressing btw. How deep is this recursion?

[Mario Carneiro]

Isn't it simpler to just use iterate 3 or something?

[Bolton Bailey]

Let me try to answer all these questions:

[Bolton Bailey]

What I am trying to do is to prove that a collection of ~50 equations over an integral domain implies a goal equation.

[Mario Carneiro]

how in the world did that happen

[Bolton Bailey]

This problem arises in the context of the proof of soundness of a cryptographic construction called a SNARK.

[Mario Carneiro]

ah, well that explains it

[Mario Carneiro]

I hope you have done everything possible to simplify the problem before the main proof

[Mario Carneiro]

for example, if two of the equations imply a third equation that is more useful

[Mario Carneiro]

breaking big proofs into small pieces is good for a bunch of reasons

[Bolton Bailey]

Indeed, I have been working on this in parallel: I could try to look at the paper proof carefully and see if I could reduce the number of equations. Unfortunately, this doesn't bode well for being able to generalize to other constructions.

[Mario Carneiro]

in what way do you want to generalize?

[Bolton Bailey]

I want to generalize to other SNARK constructions, which have different sets of equations.

[Bolton Bailey]

If I hard-code in "these 30 equations are not necessary" then I have to do that every time in the future.

[Mario Carneiro]

I don't mean to reduce the number of equations, I mean to factor the 50 lemmas -> 1 conclusion proof into a tree like 10 x (5 equations -> 1 concl) -> 2 equations -> 1 concl

[Mario Carneiro]

It sounds like you want a general mechanism to prove theorems in this language

[Mario Carneiro]

in which case you should write a custom tactic for it

[Bolton Bailey]

I considered this.

[Bolton Bailey]

The nsatz tactic from coq seems to do what I would want.

[Bolton Bailey]

I expect writing a whole tactic from scratch to resolve these equations would be harder to do though.

[Mario Carneiro]

I don't think you need to be so ambitious as that

[Mario Carneiro]

I mean a tactic to coordinate calls to simp only and rw

[Mario Carneiro]

i.e. what you are doing already

[Mario Carneiro]

you just handle the goal manipulation and control flow

[Bolton Bailey]

I guess I don't understand how what you are suggesting is different from what I'm doing.

[Mario Carneiro]

You will have much better control over the equations and recursion ordering. It's hard to demonstrate because you still haven't shown a #mwe

[Bolton Bailey]

Ok, here's an mwe I'm working on where iterate and repeat behave differently

import data.nat.basic

section my_section

lemma zero_eq_zero : 0 = 0 ↔ true :=
begin
  simp only [eq_self_iff_true],
end

example (a b c d e f : ℕ) (h1 : a = 0 ∨ b = 0) (h2 : d * e = a) : b * d * f * e = 0
:=
begin

  iterate {
    fail_if_success { done },
    try {simp only [mul_eq_zero, zero_mul, mul_zero, zero_eq_zero, or_true, true_or] at *},
    try {clear found_zero}, -- clear "found_zero" if present
    done <|> id {cases ‹_ ∨ _› with found_zero found_zero; rw found_zero at *}, },

end

end my_section

[Mario Carneiro]

But it sounds like you just haven't tried writing tactics before, it's not as hard as you think and they can be as simple or complicated as you like. You should watch Rob's metaprogramming tutorial

[Mario Carneiro]

Note that iterate and repeat are different tactics that do different things, as I mentioned. So it's not that much of a surprise that they act differently

[Mario Carneiro]

the difference is basically iterate {tac} = tac, iterate {tac} while repeat {tac} = tac; repeat {tac}

[Mario Carneiro]

The all_goals behavior of repeat is important for this example. This works:

begin
  iterate {
    fail_if_success { done },
    all_goals {
      try {simp only [mul_eq_zero, zero_mul, mul_zero, zero_eq_zero, or_true, true_or] at *},
      try {clear found_zero}, -- clear "found_zero" if present
      done <|> id {cases ‹_ ∨ _› with found_zero found_zero; rw found_zero at *} } },
end

[Bolton Bailey]

Mario Carneiro said:

But it sounds like you just haven't tried writing tactics before, it's not as hard as you think and they can be as simple or complicated as you like. You should watch Rob's metaprogramming tutorial

I have watched it through twice. It seems like every time I encounter a pitfall, I have to watch it again.

[Mario Carneiro]

If you hit any issues when writing tactics feel free to ask here

[Mario Carneiro]

Most tactics prefer to be called on one goal, and repeat does that, but iterate just calls tac repeatedly and doesn't care if the first invocation produced many subgoals

[Bolton Bailey]

Mario Carneiro said:

the difference is basically iterate {tac} = tac, iterate {tac} while repeat {tac} = tac; repeat {tac}

I have never read any formal documentation for the difference between , and ;. I honestly don't understand the difference between these definitions. Shouldn't they be the same?

[Bolton Bailey]

It seems like both of those definitions are just "recursively apply tac on all subgoals, creating a branching tree of subgoals until you reach failure".

[Mario Carneiro]

That's what ; does

[Mario Carneiro]

, means do tac1, then do tac2

[Mario Carneiro]

tac1; tac2 means do tac1, then focus on each goal produced by tac1 and do tac2 in that state, then join all the goals that result

[Bolton Bailey]

Ok, I understand the difference between , and ; I think. But that doesn't explain why iterate fails in a situation where repeat closes all goals.

[Bolton Bailey]

Here's my logic: If repeat closes all goals, then essentially what it did to solve those goals is just to apply tac over and over, to whatever goal was on top of the stack at the time. If that succeeds, shouldn't iterate do the same thing?

[Bolton Bailey]

I'm trying to get a better understanding by reading lean's definition of iterate. I reached this auxiliary function

/--
`iterate_at_most' n t` repeats `t` `n` times or until `t` fails.
-/
meta def iterate_at_most' : nat → tactic unit → tactic unit
| 0        t := skip
| (succ n) t := do
  (some _) ← try_core t | skip,
  iterate_at_most' n t

What does the | between try_core t and skip do? This is one of those things that might have been covered in Rob Lewis course, but I can't remember all the details.

[Mario Carneiro]

If the pattern doesn't match, it will run the thing on the other side of the | and skip the rest of the block

[Mario Carneiro]

so here that means that if try_core t returns none (i.e. t fails) then the tactic terminates with success

[Mario Carneiro]

Bolton Bailey said:

Here's my logic: If repeat closes all goals, then essentially what it did to solve those goals is just to apply tac over and over, to whatever goal was on top of the stack at the time. If that succeeds, shouldn't iterate do the same thing?

Tactics are called on the entire tactic state, which includes the full list of goals, not just the one on top

[Mario Carneiro]

Most tactics by convention only modify the top goal and leave the others alone, but not all

[Mario Carneiro]

in particular, done acts differently if there are "side goals" after the main goal

[Mario Carneiro]

because if the main goal is done then done will still fail because the side goals aren't

[Bolton Bailey]

Ok, so then does a goal disappear when it is finished?

[Bolton Bailey]

If I have two goals in my state that can both by finished by tac, and I call tac, tac, does that finish all goals?

[Bolton Bailey]

Ok, I finally see why my mwe fails with iterate: the try {simp only [mul_eq_zero, zero_mul, mul_zero, zero_eq_zero, or_true, true_or] at *}, closes a goal, and then done <|> id {cases ‹_ ∨ _› with found_zero found_zero; rw found_zero at *}, }, is applied to a different goal

[Bolton Bailey]

This is what was confusing.

[Mario Carneiro]

Bolton Bailey said:

If I have two goals in my state that can both by finished by tac, and I call tac, tac, does that finish all goals?

Yes, assuming tac only acts on the first goal

[Bolton Bailey]

Is there a way to say "apply this list of tactics as if the top goal was the only goal in the environment"

[Bolton Bailey]

I thought this was accomplished with { ... } or id { ... }, but neither of those make the iterate mwe succeed.

[Mario Carneiro]

here's a tactic that I think represents the control flow you are going for:

open tactic
meta def mysatz : tactic unit := do
  `[simp only [mul_eq_zero, zero_mul, mul_zero, zero_eq_zero, or_true, true_or]
    at * {fail_if_unchanged := ff}],
  _::_ ← get_goals | skip,
  `[cases ‹_ ∨ _› with found_zero found_zero]; (do
    `[rw found_zero at *; clear found_zero],
    mysatz)

example (a b c d e f : ℕ) (h1 : a = 0 ∨ b = 0) (h2 : d * e = a) : b * d * f * e = 0 :=
by mysatz

[Mario Carneiro]

Bolton Bailey said:

Is there a way to say "apply this list of tactics as if the top goal was the only goal in the environment"

focus { tac }

[Bolton Bailey]

Yep, that works.

[Bolton Bailey]

Ok, in the code you just posted, there are at least 3 things I am unfamiliar with.

[Bolton Bailey]

I guess "fail_if_unchaged" is pretty self-explanatory.

[Mario Carneiro]

It's basically equivalent to the try { simp only ... } you wrote, but this gives better errors

[Bolton Bailey]

What is _::_ <- get_goals | skip?

[Mario Carneiro]

same thing as the | from before

[Mario Carneiro]

it's fail_if_success done

[Mario Carneiro]

actually scratch that

[Mario Carneiro]

if there are no goals, then it succeeds and terminates mysatz

[Mario Carneiro]

If we let the cases run, then it would cause our tactic to fail

[Mario Carneiro]

in other words, this covers the case where the simp closes the goal

[Bolton Bailey]

Right, ok

[Mario Carneiro]

Regarding goal handling, this is a "regular" tactic, it assumes there is one goal to start and closes the goal or fails

[Mario Carneiro]

we can assume the simp only doesn't create goals so there is only one goal at the cases

[Mario Carneiro]

and we use ; after cases to run the succeeding block twice, on the two subgoals, and ensure we have only one goal

[Mario Carneiro]

crucially, after the rw, clear we call mysatz recursively

[Mario Carneiro]

this causes a branching tree of invocations, like what repeat gives you

[Mario Carneiro]

actually, we should probably use ; instead of , before the recursive call, because the rw might also close the goal

[Bolton Bailey]

Ok, I understand. One more question, for my own edification. In my version of mysatz (creatively named integral_domain_tactic, and which was bugges for other reasons), instead of using the first ; I was doing

...
do `[cases_type or],
        trace "cases_type or succeeds"
       -- If cases_type or succeeds, call tactic recursively
        `[integral_domain_tactic],
        `[integral_domain_tactic])
        -- If cases_type or fails, rewrite using more powerful simp

Does this also work in principle, because cases_type or always returns two subgoals, or is it flawed somehow?

[Bolton Bailey]

I expect the answer is "it would probably work, but ; to do recursive subcalls is more elegant".

[Mario Carneiro]

It's a little riskier, because if the first integral_domain_tactic doesn't close the goal because of bugs or otherwise, then the second integral_domain_tactic will get a weird state

[Bolton Bailey]

Right, I see.
I'm taking a break, thanks so much for all your help!

[Bolton Bailey]

Unfortunately, I'm realizing the mysatz tactic above is not doing quite what I want it to. After the _::_ ← get_goals | skip, line, it might be the case that there are no ∨ present in the hypotheses. In this case, I would like the tactic to gracefully just return the state at that point as a goal, rather than fail. I'm looking at the try_coreand match syntax to try to resolve this, but I'm not having much luck. Anyone able to help? This is what I have

meta def integral_domain_tactic : tactic unit := do
  `[simp only [] with integral_domain_simp
    at * {fail_if_unchanged := ff}],
  try `[cases_type* true false],
  _::_ ← get_goals | skip, -- If no goals left (get goals is an empty list) then skip
  -- Otherwise try to recurse on an ∨.
  -- I still think this may be wrong. If there is no or, we ought to stop at this point
  cases_success <- try_core `[cases ‹_ ∨ _› with found_zero found_zero],
  match cases_success with
  | some _ := do all_goals { `[rw found_zero at *, clear found_zero], integral_domain_tactic }
  | none := skip

[Bolton Bailey]

It doesn't work to put ; after the try core either. Lean complains that it doesn't know the identifier cases_success

[Bolton Bailey]

Actually nevermind, after playing with it a few more minutes, I found

meta def integral_domain_tactic : tactic unit := do
  `[simp only [] with integral_domain_simp
    at * {fail_if_unchanged := ff}],
  try `[cases_type* true false],
  _::_ ← get_goals | skip, -- If no goals left (get goals is an empty list) then skip
  -- Otherwise try to recurse on an ∨.
  -- I still think this may be wrong. If there is no or, we ought to stop at this point
  cases_success <- try_core `[cases ‹_ ∨ _› with found_zero found_zero],
  match cases_success with
  | some _ := do all_goals' `[rw found_zero at *, clear found_zero, integral_domain_tactic]
  | none := skip
  end

Seems to work. I'll let you all know if anything else comes up.