congr and forward dependencies

Stream: lean4

[Jakob von Raumer]

Going off from this issue, I wondered if there's any use of having a version/option for the congr tactic (be it inside or outside of conv) which does not skip arguments with forward dependencies, in order to do definitional rewriting. I think the default should still be that they're skipped, otherwise we lose all compatibility with Lean 3' s congr, but maybe an option would be good?

[Mario Carneiro]

My suggestion: @2 in enter and related functions means "second argument including implicits/dependents"

[Sebastian Ullrich]

we lose all compatibility with Lean 3' s congr

That's not exactly been a design concern so far. And I would be quite surprised if it broke more than a handful proofs in mathlib.

[Mario Carneiro]

In any case it's easy enough to work around incompatibilities by providing a congr' in mathlib4

[Mario Carneiro]

I think counting or not counting implicit arguments would make a big difference in enter since it would offset the numbering, but mathlib doesn't have enter

[Sebastian Ullrich]

Oh counting all arguments should definitely use a separate syntax. Obscure syntax for obscured data.

[Mario Carneiro]

Does enter work with names for named arguments?

[Mario Carneiro]

i.e. enter x to enter f (x: Nat) : Nat

[Sebastian Ullrich]

It doesn't, but that would be nice as well, yes

[Mario Carneiro]

I think that's probably better for getting to implicit args than counting since it creates a dependency on ordering of implicits

[Mario Carneiro]

also the argument numbering should be 1-based, with 0 meaning to rewrite the head function (I think the first of those is implemented but not the second)

[Jakob von Raumer]

enter's arguments are 1-based right now

[Mario Carneiro]

good, just checking

[Mario Carneiro]

the 0 = head thing is how it's done in mathematica and it's fairly intuitive

[Jakob von Raumer]

I think we all agree on the implicits... for the fwd deps, I'll add
an option

 private def congrApp (mvarId : MVarId) (lhs rhs : Expr) (skipFwdDeps := true) : MetaM (List MVarId) :=
...

which enter and arg set to false

[Mario Carneiro]

I don't think skipping forward dependencies should ever be a thing, it's not obvious from the call expression itself whether an argument is dependent or not

[Mario Carneiro]

instead it should just reject if you try to rewrite at an argument you can't rewrite at

[Jakob von Raumer]

Yes, that's my idea as well. And there's a point to doing definitional rewrites, too

[Mario Carneiro]

It is not at all simple to do definitional rewrites with congr though, because you can't introduce a metavariable and subgoal for the definitional equality

[Mario Carneiro]

You would need an extension of the tactic monad itself to support |- a === b defeq goals

[Jakob von Raumer]

Is that also if we only open a goal for the first of the two dependent args?

[Jakob von Raumer]

The type check of the rhs kind of has to happen after the congr mvar is filled in...

[Mario Carneiro]

right

[Mario Carneiro]

Something like f a b = f ?a' b doesn't typecheck

[Mario Carneiro]

or rather, it will probably immediately force ?a' := a so you don't get a subgoal

[Mario Carneiro]

the "extended tactic monad" I mentioned would have a way to encode this as f a b = f ?a' ?b with "and by the way set ?b := b once it typechecks"

[Jakob von Raumer]

proposed a fix