Rewrite tactic fails to match equality when both sides are lambda terms

[melanie-taprogge]

Summary

The rewrite tactic fails to match an equality proposition when both sides of the equality are lambda terms.

The minimal-example.zip demonstrates this:

• Repro.lp: using two symbols l r : τ (a ⤳ o), Lambdapi fails to apply the rewrite tactic to the goal

  (λ x : τ a, l x) = (λ x : τ a, r x)

  with =_sym [(a ⤳ o)].
• ReproExplicit.lp: the same example, but with =_sym fully instantiated with both lambda terms.

Both files fail to check. In the explicit version, Lambdapi reports that the selected equality does not match an identical-looking equality:

[ReproExplicit.lp:18:2-22:22] [(λ x, l x) = (λ x, r x)] doesn't match [(λ x, l x) = (λ x, r x)].

Note that this issue is not caused by the current limitation of the rewrite tactic that does not allow for it to be applied under binders, but instead it prevents the rewrite tactic to operate on lambda terms.

How to reproduce

cd minimal-example
lambdapi check Repro.lp
lambdapi check ReproExplicit.lp

Expected behavior

The rewrite should match the selected equality with lambda terms on both sides, and both files should check.

Actual behavior

Checking Repro.lp fails with:

[Repro.lp:18:2-40] [(λ x, l x) = (λ x, r x)] doesn't match [$x = $y].

Checking ReproExplicit.lp fails with:

[ReproExplicit.lp:18:2-22:22] [(λ x, l x) = (λ x, r x)] doesn't match [(λ x, l x) = (λ x, r x)].

Observed version

Observed with Lambdapi 3.0.0-145-g4ef4527.

[fblanqui]

Hi. With flag "print_implicits" on, the goal is: π (¬ (@= (a ⤳d (λ _, o)) (λ x, l x) (λ x, r x))).
As you can see, for some reason, the inferred type of λ x, l x and λ x, r x is a ⤳d (λ _, o) which you try to match with a ⤳ o. These two terms are equivalent but not syntactically equal, and matching in the rewrite tactic is syntactic.
One way to circumvent that problem is to do simplify ⤳d before calling rewrite.

To avoid this, we could include some reduction in the matching algorithm.

[melanie-taprogge]

Hi. With flag "print_implicits" on, the goal is: π (¬ (@= (a ⤳d (λ _, o)) (λ x, l x) (λ x, r x))). As you can see, for some reason, the inferred type of λ x, l x and λ x, r x is a ⤳d (λ _, o) which you try to match with a ⤳ o. These two terms are equivalent but not syntactically equal, and matching in the rewrite tactic is syntactic. One way to circumvent that problem is to do simplify ⤳d before calling rewrite.

To avoid this, we could include some reduction in the matching algorithm.

Thank you for looking into it. Yes, indeed, adding the simplification step should work for the instances where this occurs on my benchmark. It may still make sense to add a reduction in the matching, as you suggested.