Nat.sub =?= HSub.hSub

Stream: mathlib4

[Thomas Murrills]

What's the right way to check (on the meta/expression level) that a particular HSub.hSub is (or is not) Nat.sub?

They're not defeq: Nat.sub is not defeq to @HSub.hSub.{0, 0, 0} Nat Nat Nat (@instHSub.{0} Nat instSubNat). (Is this a transparency issue, maybe?)

(This is for the norm_num extension for Nat.sub, if the context is helpful!)

[Thomas Murrills]

Though, Nat.sub a b is defeq to HSub.hSub a b. What's going on there?

[Mario Carneiro]

you have to unfold instances to see them as refl:

example : @HSub.hSub.{0, 0, 0} Nat Nat Nat (@instHSub.{0} Nat instSubNat) = Nat.sub :=
  by with_reducible rfl -- fail
example : @HSub.hSub.{0, 0, 0} Nat Nat Nat (@instHSub.{0} Nat instSubNat) = Nat.sub :=
  by with_reducible_and_instances rfl -- ok
example : @HSub.hSub.{0, 0, 0} Nat Nat Nat (@instHSub.{0} Nat instSubNat) = Nat.sub :=
  rfl -- ok

[Mario Carneiro]

which makes sense since instSubNat is an instance, and not a reducible definition

[Thomas Murrills]

ok, I see! instances have a separate transparency which is not seen through by default in isDefeq? Hmmm...I take it rfl uses a different transparency than isDefeq by default then?

[Thomas Murrills]

is there a general rule describing what uses what transparency?

[Mario Carneiro]

no, rfl and isDefEq use the current transparency set in the MetaM monad

[Mario Carneiro]

with_reducible (the tactic combinator) and withReducible (the function) change this setting to .reducible instead of whatever is inherited

[Thomas Murrills]

do tactics set a different initial transparency than you'd see in e.g. norm_num extensions then? this makes sense, I'm just wondering why they're different in different places

[Mario Carneiro]

that's why with_reducible is able to change the behavior of the rfl tactic in this example

[Mario Carneiro]

The default transparency is .default, normally tactics will be running in that context

[Mario Carneiro]

norm_num extensions are also running with the same inherited transparency

[Mario Carneiro]

I don't know what code you are talking about specifically though

[Thomas Murrills]

interesting, guard <|← withNewMCtxDepth <| isDefEq f q(Nat.sub) fails (guard <|← withNewMCtxDepth <| withReducibleAndInstances <| isDefEq f q(Nat.sub) succeeds) when evaluated pretty much at the top of evalSub

[Thomas Murrills]

(aside: do I need the new metavariable context depth? I couldn't see any metavariables that might be accidentally set but just wanted to be sure)

[Mario Carneiro]

the metavariables in question are in f

[Mario Carneiro]

you don't want the user to have a HSub.hSub ?A ?inst 1 2 expression where calling norm_num assigns ?A := Nat just because we decided to see whether we can evaluate it as Nat.sub

[Mario Carneiro]

I think it would be better to use HSub.hSub (\alpha := Nat) instead of Nat.sub here since that's the more common expression to find

[Thomas Murrills]

re: mvars, makes sense! unification is pretty strong, then...

[Thomas Murrills]

Mario Carneiro said:

I think it would be better to use HSub.hSub (\alpha := Nat) instead of Nat.sub here since that's the more common expression to find

hmm, are we sure no one ever gives another HSub instance for Nat though? after all HSub.hSub : Nat → Nat → Int would make sense, and I wouldn't want to try the Nat.sub part of the extension for that

[Mario Carneiro]

the two expressions are defeq, it's just that you will more often see nat subtraction expressed using - than Nat.sub

[Thomas Murrills]

right, I just want to guard against false positives if there's another HSub instance

[Mario Carneiro]

so this would avoid having to unfold the instance unless it is a weird instance

[Thomas Murrills]

or maybe setting all three parameters to Nat would be safe

[Mario Carneiro]

that expression (inside Qq) will elaborate it at tactic declaration time, to the Nat.sub instance

[Mario Carneiro]

you can mouse over the expression and observe that all three parameters are set regardless

[Mario Carneiro]

if a Nat -> Nat -> Int instance was added, it wouldn't change anything unless it was added upstream of NormNum.Basic, and even then it would probably not be selected since the Nat -> Nat -> Nat instance is a default instance

[Thomas Murrills]

ah, it's a dependency and elaboration time thing, got it

[Thomas Murrills]

(unless we changed the default instance in mathlib...which might be nice...one day...far in the future... :upside_down:) (but, yeah, I see your point! makes sense)

[Thomas Murrills]

also btw I traced it and apparently norm_num extensions run under .reducible transparency, at least when using norm_num1, which I suppose makes intuitive sense, since we don't want to be diving too deep into things. the more you know.

[Thomas Murrills]

(also I guess simp is run before norm_num extensions when using norm_num? I don't get any norm_num traces in some cases when I delete the 1. interesting.)

[Mario Carneiro]

who is setting that transparency?

[Mario Carneiro]

I didn't see any such things in NormNum.Core, but I didn't look in simp

[Thomas Murrills]

I didn't see anything in Core either, so I figured simp—I'll take a look

[Mario Carneiro]

Simp.main calls withSimpConfig which uses withReducible

[Thomas Murrills]

ok, !4#1997 works! (@Heather Macbeth) (but I wonder if my style is off re: how I structured the branches.)

[Thomas Murrills]

oh, re: github comment on !4#1997, what's the best way to separate the PR dependency @Mario Carneiro after having set it up like this? honestly I have no experience with this kind of thing unfortunately. ("delete it all and make a new PR" is my go-to strategy.)

But, if it helps, only the 2 commits at the end belong to this PR.

[Mario Carneiro]

as long as you retain the branch name, you don't need to close/make a new PR, no matter how much git surgery you do

[Mario Carneiro]

I would try doing a rebase to master, there is a way to say "move all the commits from HEAD~2 to now onto master"

[Mario Carneiro]

Another way to clear all the history is to git reset master, which resets the branch to master (undoing all your commits) but without actually changing the files in the working directory, so you end up in a state as if you had just made all the changes and they are awaiting staging/commit. So you can go through the changes, revert anything that you don't want in the PR, and then make a single commit with everything you do want

[Thomas Murrills]

ok, I'll google how to spell that and/or just do some copy-pasting! (Nat.sub is so small compared to ofScientific)

btw the point of the dependency was to make it easy to work on top of this branch with all finished features for @Heather Macbeth—but, I guess merging is possible? 😅 maybe it would be best to make a non-PR'd branch norm_num-all or something which stayed up to date with all finished but not-yet-merged features

[Mario Carneiro]

I think you should let Heather do that locally, assuming there are no nontrivial interactions between the PRs

[Mario Carneiro]

if there are, then they should probably be dependent PRs

[Thomas Murrills]

I think this one can be separated

[Thomas Murrills]

however, ofScientific is used for teaching prior to Nat.sub, so it's "higher priority" in a sense

[Thomas Murrills]

also I'm not sure how it works for teaching—a branch might be useful if all students are using it or something. but I'll let Heather direct what should happen here

[Mario Carneiro]

it's also a lot harder to review :P

[Thomas Murrills]

lol true

[Mario Carneiro]

the commit history of that PR is also in shambles, there are a ton of things which seem to be from old branches

[Thomas Murrills]

right—I'll try to fix that later! for now !4#1997 seems to be cleaned up

[Thomas Murrills]

When you say it should be a separate norm_num extension: do we match against _ - _, Sub.sub _ _, Nat.sub _ _ in the new extension?

[Heather Macbeth]

Mario Carneiro said:

I think you should let Heather do that locally, assuming there are no nontrivial interactions between the PRs

Yup, I'm maintaining a branch
https://github.com/leanprover-community/mathlib4/tree/hrmacbeth-math2001
which has all the un-merged features I need (currently !4#1707, !4#1897, !4#1999, and I will add in !4#1997!)

[Mario Carneiro]

Thomas Murrills said:

When you say it should be a separate norm_num extension: do we match against _ - _, Sub.sub _ _, Nat.sub _ _ in the new extension?

(_ : Nat) - _, Sub.sub (_ : Nat) _, Nat.sub _ _

[Thomas Murrills]

ah...that transparency issue is actually a problem for most of the extensions (e.g. Mul.mul doesn't work)

[Thomas Murrills]

do we prepend each defeq check with withReducibleAndInstances or do we do multiple defeq checks? (is || short-circuited at the stage of evaluation we need it to be?)

[Thomas Murrills]

also, separate PR or just deal with it in this PR?

[Mario Carneiro]

we could put withReducibleAndInstances in the norm_num harness

[Thomas Murrills]

hmm, you mean set the transparency in norm_num right before the eval? like this?

/-- A simp plugin which calls `NormNum.eval`. -/
def tryNormNum? (post := false) (e : Expr) : SimpM (Option Simp.Step) := do
  try return some (.done (← withReducibleAndInstances <| eval e post))
  catch _ => return none

(not sure what you mean by harness tbh, just going off vibes :upside_down:)

[Thomas Murrills]

that definitely works, so I'll commit it to !4#1997, and if we don't like it we can revert it

[Mario Carneiro]

probably better to put it on the norm_num eval itself (line 527 ext.eval e in derive)

[Thomas Murrills]

cool, done :)

[Thomas Murrills]

btw, cleaned up ofScientific !4#1707
Mario Carneiro said:

the commit history of that PR is also in shambles, there are a ton of things which seem to be from old branches

history has been rewritten and that PR now has just 13 commits. :)