`loom_intro` tactic does not behave

[volodeyka]

Sometimes loom_solve tactic leaves out residual goals with weird hypothesis like

i_1 : { fst := l, snd := r } = { fst := i, snd := r_1 }

As in

loom/CaseStudies/Velvet/VelvetExamples/Examples_Total.lean

Line 191 in 2372de9

loom_solve <;> auto [*]

Which means that loom_intro does not work properly. We should debug and fix this

[volodeyka]

After looking into this issue, I realized that it happens because of the new support for match statements.
The problem is that when wpgen_app sees a match statement, it destructs the expression being matched and introduces equalities about it to the context. This is exactly where i_1hypothesis is coming from
@zqy1018, I guess you are reporting the space for a future optimisation here to remove redundant equalities:

loom/Loom/MonadAlgebras/WP/Matcher.lean

Line 200 in 2372de9

TODO This optimization is not implemented yet.

How hard would be to implement something like that? Or maybe at least give proper names to such generated equalities?

[zqy1018]

This is somehow unrelated to the redundant equality issue. If you print sqrt_bn.match_1, then you will see:

def sqrt_bn.match_1.{u_1} : (motive :
    MProdWithNames ℕ (WithName ℕ (Lean.Name.anonymous.mkStr "r")) (Lean.Name.anonymous.mkStr "l") → Sort u_1) →
  (r : MProdWithNames ℕ (WithName ℕ (Lean.Name.anonymous.mkStr "r")) (Lean.Name.anonymous.mkStr "l")) →
    ((l : ℕ) → (r : WithName ℕ (Lean.Name.anonymous.mkStr "r")) → motive { fst := l, snd := r }) → motive r :=
fun motive r h_1 ↦ MProdWithNames.casesOn r fun fst snd ↦ h_1 fst snd

The equality appears because r is the discriminant, and this equality relates the arguments of motive to r. Such equalities are required in some proofs of recursive programs (see the comment in Loom/MonadAlgebras/WP/Matcher.lean for details), so in general I don't think it would easy to eliminate them.

It should be possible, though, to include some tactics in loom_solve to find such equalities and do injection on them.

[volodeyka]

@zqy1018 Maybe we can apply injection theorems at the level of theorem generation (i.e. by running simp)?
At the bare minimum, we should annotate this motive hypothesis using WithName too