upstreaming simps to Std

Stream: mathlib4

[Scott Morrison]

@Floris van Doorn, I would really like to make simps available to everyone, outside Mathlib. I've verified that it is easy to extract: #8140 does a slight import cleanup result from checking this.

Would you have any objection if I did this? (Anyone else?)

[Floris van Doorn]

That sounds good to me!

[Johan Commelin]

@Scott Morrison I don't know what I'm talking about, but I noticed that you are removing a use of q. I thought we generally tried to use Qq whenever possible?

But I guess Std can't depend on Qq, because Qq already depends on Std?

[Eric Wieser]

Qq doesn't depend on Std

[Eric Wieser]

Also, I think there's an open PR that fixes a bug in simps; it would be nice to get that merged before upstreaming

[Johan Commelin]

Do you mean

WIP: try to fix simps not failing when reaching a term is not a constructor #2936

[Eric Wieser]

Last time the Qq thing came up I think we were stalled by Gabriel having no time; I think now that the repo ownership has transferred, that's slightly less of a concern

[Eric Wieser]

#7707 is the one I had in mind

[Mario Carneiro]

Speaking of which, I've been thinking about upstreaming Qq to Std

[Johan Commelin]

In that case, this change to simps should maybe not be made?

[Eric Wieser]

Mario Carneiro said:

Speaking of which, I've been thinking about upstreaming Qq to Std

This sounds like a much better option than de-Qqing mathlib tactics; though I think we should:

• merge the open Qq PRs first
• make sure to merge the histories git merge --allow-unrelated to ensure Gabriel keeps all the credit / commit logs

[Johan Commelin]

@Mario Carneiro How concrete are you Qq-upstreaming plans?
@Scott Morrison How urgent is upstreaming simps to Std for you/FRO?

[Mario Carneiro]

I was thinking about bringing it up for discussion, not much more concrete than that

[Mario Carneiro]

it's definitely appropriate for Std, and it's going to be a bigger problem the more mathlib tactics we upstream because many of them use Qq

[Johan Commelin]

For now, could Std just start depending on Qq? Or is that too weird?

[Mario Carneiro]

It would most likely take the form of making Qq live in some new module like Std.Tactic.Qq, copying the contents in

[Mario Carneiro]

Std doesn't have any dependencies and the plan is to keep it that way, although we can consider alternatives

[Eric Wieser]

What's the issue with adding dependencies to Std? If the plan is to eventually merge the packages anyway, that doesn't sound too bad in the meantime.

[Mario Carneiro]

I was talking long term

[Mario Carneiro]

Sure, we could do it as a temporary measure but I don't really see the point since inlining is also fairly easy

[Mario Carneiro]

I don't see any forthcoming technical solutions to being able to automatically inline Qq in Std

[Eric Wieser]

We should probably check @Gabriel Ebner is happy with that outcome

[Mario Carneiro]

The main reason I want to avoid dependencies is because it means fewer moving parts for all downstream packages

[Scott Morrison]

I think this whole discussion is a bit off-track. :-)

The use of Qq in simps was completely trivial: I replaced it with literally a single call to mkConst.

[Scott Morrison]

If #7707 is going to happen soon it is fine to wait for it. But if it's more than a couple of days I'd prefer that we just continue with the upstreaming, and move #7707 over afterwards.

[Scott Morrison]

Entirely separately from upstreaming simps, we can talk about Qq in Std. :-)

Leo has previously expressed opposition to moving Qq into Std, or indeed having too many tactics relying on it. So I think this question is a complicated one that may not be resolvable quickly.

[Scott Morrison]

Okay, std#347 is the upstreaming of @[simps]. It can happen before or after #7707, either way will just patch up the second PR.

[Mario Carneiro]

Scott Morrison said:

Entirely separately from upstreaming simps, we can talk about Qq in Std. :-)

Leo has previously expressed opposition to moving Qq into Std, or indeed having too many tactics relying on it. So I think this question is a complicated one that may not be resolvable quickly.

Okay, I will hold off and also bring this up with him. Qq is definitely not the most bullet-proof implementation, but I think the ideas are sound and I really would not want to do any serious expr building over known types without it or an equivalent.

[Scott Morrison]

My only real complaint is that there are sometimes weird hard-to-diagnose errors binding universe levels.

I think (don't quote me?) Leo was concerned in part that it might be too easy for users to write non-performant Expr matching code, when a few getAppFnArgs would suffice?

For Expr building, quote4 is indispensable, I agree!

[Mario Carneiro]

yeah the expr match stuff is pretty expensive

[Mario Carneiro]

obviously the goal is to have expr match syntax which elaborates to calls to getAppFnArgs and friends

[Mario Carneiro]

I think we could have a Std.Experimental folder and put Qq.Match in it. This folder would not be included in import Std but it would be useful for allowing more things to be upstreamed faster before we are ready to commit to the API

[Eric Wieser]

Scott Morrison said:

I think (don't quote me?) Leo was concerned in part that it might be too easy for users to write non-performant Expr matching code, when a few getAppFnArgs would suffice?

The flip side of this is that code that doesn't use Qq can end up behaving incorrectly around reducible definitions, as it can end up performing exact rather than reducible matches.

[Jannis Limperg]

Does QQ do matching up to reducible computation by default? Can you get it to do syntactic matching as well?

[Eric Wieser]

My understanding was that it only did reducible matching (and that that's in some sense a feature; you don't ever want to match things like instances syntactically)

[Jannis Limperg]

Makes sense; reducible matching should certainly be the default.

[Gabriel Ebner]

Scott Morrison said:

I think (don't quote me?) Leo was concerned in part that it might be too easy for users to write non-performant Expr matching code, when a few getAppFnArgs would suffice?

Indeed, the matching part of quote4 is not great. It does its job as a tech demo amazingly, but I completely agree that there's massive performance issues. My plan was to automatically generate matching code using whnfR+getAppArgs+isDefEq (without unification), roughly approximating what the discrimination tree module does. But I never found the time to implement it.

[Gabriel Ebner]

There's two other big issues with the match syntax. First, there's no way to distinguish pattern variables from antiquotations. For example, in let x : Q(Nat) := 42; match y with | ~q($x + $y) => .... Should $x bind a fresh variable, or should it check that the lhs is defeq to 42?

[Gabriel Ebner]

Second, the macros in that file are wild. :smile: