Simp and funext

Stream: lean4

[Patrick Johnson]

When rewriting under binders, simp seems to be applying funext on the function from the binder being rewriten, not on the rewriting theorem itself. Is there a specific reason for that?

Each theorem marked as @[simp] can be reduced to funext normal form before adding to the simp set. For example, ∀ (P Q : Prop), ¬(P ∧ Q) ↔ ¬P ∨ ¬Q can be reduced to (λ (P Q : Prop) => ¬(P ∧ Q)) = (λ (P Q : Prop) => ¬P ∨ ¬Q) and if we try to simplify the statement ∀ (A B : Prop), true ∨ ¬(A ∧ B) using that theorem, simp would interpret it as ∀ (A B : Prop), true ∨ f A B where f is the LHS of the rewriting theorem. This should save a lot of time during simplification and shorten the resulting proof size.

Are there any flaws with this idea?

[Mario Carneiro]

this would turn every rewriting problem into a higher order rewriting problem, which is a lot harder and would significantly reduce successful rewrites

[Mario Carneiro]

For instance, what if the goal was ∀ (B A : Prop), true ∨ ¬(A ∧ B) instead? simp would then normalize the expression to ∀ (B A : Prop), true ∨ (λ (B A : Prop) => ¬(A ∧ B)) B A which no longer matches the normalized equation in the simp set

[Mario Carneiro]

Or maybe it would normalize to ∀ (B A : Prop), (λ (B A : Prop) => true ∨ ¬(A ∧ B)) B A instead which doesn't look at all like the equation in the simp set

[Patrick Johnson]

For non-dependent functions, abstracting the LHS away shouldn't be hard at all. The LHS is λ (P Q : Prop) => ¬(P ∧ Q), so we have pattern ¬(?P ∧ ?Q) in the simp decision tree. If the goal is ∀ (B A : Prop), true ∨ ¬(A ∧ B), simp would visit each subexpression and try to match against some pattern from the decision tree. When it sees ¬(A ∧ B), simp would replace it with (λ (P Q : Prop) => ¬(P ∧ Q)) A B, so the goal would become ∀ (B A : Prop), true ∨ (λ (P Q : Prop) => ¬(P ∧ Q)) A B as expected.

[Reid Barton]

I don't see how this is effectively different from just instantiating the simp lemma instead

[Patrick Johnson]

By not using funext when simplifying and therefore shortening the resulting proof term.

[Reid Barton]

But I don't understand why funext would be involved in the first place

[Reid Barton]

Oh you mean for rewriting under binders?

[Patrick Johnson]

The point I'm trying to make is that after reducing to funext normal form, we can replace lambda arguments from the LHS with metavariables and store the pattern in the global simp decision tree. When matching a term against the decision tree, we would keep track of metavariable assignments for each path (and the number of paths we follow would be proportional to the number of metavariables, which can be considered a constant). Not sure how hard it would be to implement this though.

[Reid Barton]

It's an interesting idea although it's not clear to me whether the resulting proof is meaningfully smaller or easier to check; seems like you trade funext for a more complicated motive to eq.rec

[Patrick Johnson]

In the set theoretic theorem prover I'm developing, after implementing this simplification algorithm the performance increased significantly, and proof terms turned out to be shorter. So I thought maybe we can implement something similar in Lean as well. But on the other hand, Lean is dependently typed, so it's hard to know in advance whether this algorithm would bring any benefit.