test failure at chapter 04

[soonhokong]

ERROR executing 04_Quantifiers_and_Equality.org.16.lean, for in_code_block block starting at 320, 

produced output:

04_Quantifiers_and_Equality.org.16.lean:5:0: error: unifier maximum number of steps (20000) exceeded,
the maximum number of steps can be increased by setting the option unifier.max_steps 
(remark: the unifier uses higher order unification and unification-hints, which may trigger non-termination

import data.nat
open nat eq.ops algebra

example (x y : ℕ) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
have H1 : (x + y) * (x + y) = (x + y) * x + (x + y) * y, from !left_distrib,
have H2 : (x + y) * (x + y) = x * x + y * x + (x * y + y * y),
  from !right_distrib ▸ !right_distrib ▸ H1,
!add.assoc⁻¹ ▸ H2

[soonhokong]

Having set_option unifier.max_steps 40000 is a solution (but maybe not a good one). Another possibility is to introduce an intermediate step as follows:

import data.nat
open nat eq.ops algebra

example (x y : ℕ) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
have H1 : (x + y) * (x + y) = (x + y) * x + (x + y) * y, from (left_distrib (x + y) x y),
have H2 : (x + y) * (x + y) = x * x + y * x + (x + y) * y, from !right_distrib ▸ H1,
have H3 : (x + y) * (x + y) = x * x + y * x + (x * y + y * y), from !right_distrib ▸ H2,
  !add.assoc⁻¹ ▸ H3

[leodemoura]

@avigad @soonhokong I think we should avoid examples that use ▸. This is an anti-pattern. It generates fragile proofs that are hard to maintain. In the future, I want to completely disallow terms such as !right_distrib ▸ !right_distrib ▸ H1.

I know that in Chapter 4, tactics were not introduced yet. But, we can introduce just the rewrite tactic. Another option is to provide the argument to right_distrib explicitly, and avoid the ! notation.

[soonhokong]

Closed by d9aa276de23086f70db5065297309e668baaa1a2