iterate until no change

Stream: metaprogramming / tactics

[Damiano Testa]

Dear All,

I am a complete beginner with writing tactics, so I am very unsure whether what I ask is meaningful or not.

In trying to convert a procedure to compute degree of polynomials into a tactic, I would like to iterate a code-block until the initial state and the final one are the same. How can I do this? Below is a silly #mwe.

Thanks!

import tactic

example {a b : ℕ} : a + b = 0 :=
begin
-- this loops forever
  iterate { rw [add_comm, add_comm] },
end

[Damiano Testa]

(Fun fact, if you remove the import tactic, then iterate seems to stop quickly and possibly behave as I hoped it would.)

[Damiano Testa]

(The difference in behaviour between iterate with or without the import appears to be that with the import iterate seems to pause at each step and make sure that it has not already proven the goal.)

[Damiano Testa]

Actually, I am not sure about the difference: I think that one iterate has an explicit bound on the number of iterations, the other does not. Then there is a mix about rw that I did not know.

[Floris van Doorn]

I think tactic#repeat does what you want. It stops applying the tactic if it doesn't change the goal (or fails)

[Damiano Testa]

I am not sure what is going on, but this does not work (and in my use-case repeat also does not work):

meta def reprw : tactic unit :=
`[
  repeat { rw [add_comm] }
]

example {a b : ℕ} : a + b = b + a :=
begin
  reprw, -- ends as it started saying that there are unsolved goals
end

[Damiano Testa]

I meant to say: I am using this iterate not to solve the goal, but to massage it, so that after I can continue processing it.

[Arthur Paulino]

tactic#squeeze_simp has this behavior as well

[Floris van Doorn]

This works for me:

import tactic
meta def reprw : tactic unit :=
`[
  repeat { rw [add_comm] }
]

example {a b : ℕ} : a + b = b + a :=
begin
  reprw -- solves goal
end

Note: you need some kind of import, in order for add_comm to exist.

[Damiano Testa]

Ok, I'll continue investigating! I suspect that I minimised my example too much.

[Damiano Testa]

I find not getting an error for the add_comm very confusing!

[Floris van Doorn]

Note: a good way to debug issues with repeat is to just copy the tactic a couple of times and see where you get the first error:

example {a b : ℕ} : a + b = b + a :=
begin
  rw [add_comm], rw [add_comm], rw [add_comm]
end

[Arthur Paulino]

same_result is the function that you might want

[Floris van Doorn]

Damiano Testa said:

I find not getting an error for the add_comm very confusing!

This is a feature(?) of repeat: it will execute the tactic until the first time the tactic raises an error. The tactic raises an error the first time is applied, since it doesn't know what add_comm is.

[Damiano Testa]

Ok, thank you both for your help!

[Floris van Doorn]

You can also use docs#tactic.repeat1 (doesn't have an interactive version, I believe):

import tactic
meta def reprw : tactic unit :=
tactic.repeat1 `[rw [foobar]]

example {a b : ℕ} : a + b = b + a :=
begin
  reprw -- unknown identifier 'foobar'
end