gcongr for implication

Stream: mathlib4

[Daniel Weber]

How hard would it be to modify gcongr to support implication? I imagine it utilizing stuff like docs#forall_imp, docs#Exists.imp, docs#And.imp, docs#Or.imp, docs#Not.imp, but also more specific stuff like a ≤ b → c ≤ d → (b < c → a < d), and there could be a macro for revert h; gcongr or apply (_ : _ → _) h; gcongr as a weaker form of convert

[Floris van Doorn]

I think that would be nice! It's probably a bit of work to implement, since implication is not a constant, and so has to be special-cased.

[Daniel Weber]

I'll try to implement it

[Daniel Weber]

Is there a definition fun (a b : Prop) ↦ a → b somewhere?

[Kyle Miller]

Since you're talking about metaprogramming, what what sort of function do you mean? Literally some sort of Imp declaration (which you can write as (· → ·) by the way), or something to construct implications when metaprogramming?

[Daniel Weber]

Just some sort of Imp declaration, so I'd only have to convert implications to it and then it's a relation

[Daniel Weber]

I encountered a problem that gcongr introduces all hypothesis to the main goal it produces, but when the main goal is actually an implication we don't want to introduce the last hypothesis. Is there a version of docs#Lean.MVarId.introsWithBinderIdents I can use to introduce all variables except the last one?

[Kyle Miller]

After some looking, I don't see any Imp-like function. Depending on where this is in the code, you might consider special-casing implications in the code so that implication still acts like a relation.

[Kyle Miller]

For your introsWithBinderIndents question, is that function already in the gcongr code, or are you using it because you happen to have BinderIdents? Usually I see docs#Lean.MVarId.intros in tactics. Too bad it's not public, but in the module where it's defined there's a function getIntrosSize you could use, and then use that for docs#Lean.MVarId.introN

[Daniel Weber]

That's the function already in the code

[Kyle Miller]

I see. I also see that introsWithBinderIdents makes use of getIntrosSize to compute how many times to intro. Anyway, the answer is very very likely "no" to you question about there being any pre-existing function that does intros-but-one.

I guess your idea to use an Imp function would help here, to be able to hide that it's an implication.

[Daniel Weber]

I see, then I'll copy introsWithBinderIdents but edit it to use getIntrosSize - 1

[Kyle Miller]

How about instead making introNWithBinderIdents that takes in a number of variables to intro, then implement introsWithBinderIdents in terms of that.

[Daniel Weber]

I managed to get it to (seemingly) work for stuff like (∃ x, a x ∧ b x) → ∃ x, c x ∧ d x, but there's a problem with docs#forall_imp - it sees it as (∀ (a : α), p a) → ((a : α) → q a) and then complains that (a : α) → q a isn't a valid relation. Is there a better solution to that than trying all suffixes as a possible RHS?

[Jireh Loreaux]

Are you reimplementing docs#Mathlib.Tactic.Peel.peel ?

[Daniel Weber]

I'm trying to implement it as part of gcongr

[Heather Macbeth]

There's actually a version of this (with special-casing of implication, done as a separate attribute @[grw], but basically the same idea) implemented on branch#HM-grw-attribute:
https://github.com/leanprover-community/mathlib4/blob/ef82c2de29ac2f582687c38f809f199ed3373698/Mathlib/Tactic/GRW/Core.lean#L39-L60

[Heather Macbeth]

The history of that branch is that it was going to be a follow-up to #8167, which never got merged (there was a slow review process and we lost the original author).

[Heather Macbeth]

@Daniel Weber, any chance you would like to adopt #8167?

[Daniel Weber]

I don't think I could do it well, it seems quite complex and I don't know metaprogramming well