feat: icombine

[alvinylt]

Description

Implements the icombine tactic, available in three formats:

• icombine <hypotheses> as <pattern>
• icombine <hypotheses> gives <pattern>
• icombine <hypotheses> as <pattern> gives <pattern>

Addresses #359.

The functions iCombineAsCore and iCombineGivesCore utilise the type classes CombineSepAs and CombineSepGives, respectively. Since these two functions already handle the list of hypotheses recursively, there is no need to rely on type classes for recursion.

The following type classes and type class instances are all located under the ProofMode directory.

Type class in Lean	Located within the Lean codebase in	Corresponding type class in Rocq	Located within the Rocq codebase in
CombineSepAs	Classes.lean	CombineSepAs	classes.v
CombineSepGives	Classes.lean	CombineSepGives	classes.v

Four instances of the type class CombineSepAs are named combine_sep_as_* instead combine_sep_gives_* in Rocq. Their Lean counterparts are named combineSepGives_* for consistency.

Type class instance in Lean	Located within the Lean codebase in	Corresponding type class instance in Rocq	Located within the Rocq codebase in
combineSepAs_default	Instances.lean	maybe_combine_sep_as_default	classes.v
combineSepAs_affinely	Instances.lean	maybe_combine_sep_as_affinely	class_instances.v
combineSepAs_intuitionistically	Instances.lean	maybe_combine_sep_as_intuitionistically	class_instances.v
combineSepAs_absorbingly	Instances.lean	maybe_combine_sep_as_absorbingly	class_instances.v
combineSepAs_persistently	Instances.lean	maybe_combine_sep_as_persistently	class_instances.v
combineSepAs_later	InstancesLater.lean	maybe_combine_sep_as_later	class_instances_later.v
combineSepAs_laterN	InstancesLater.lean	maybe_combine_sep_as_laterN	class_instances_later.v
combineSepAs_except0	InstancesLater.lean	maybe_combine_sep_as_except_0	class_instances_later.v
combineSepGives_affinely	Instances.lean	combine_sep_as_affinely	class_instances.v
combineSepGives_intuitionistically	Instances.lean	combine_sep_as_intuitionistically	class_instances.v
combineSepGives_absorbingly	Instances.lean	combine_sep_as_absorbingly	class_instances.v
combineSepGives_persistently	Instances.lean	combine_sep_as_persistently	class_instances.v
combineSepGives_later	InstancesLater.lean	maybe_combine_sep_gives_later	class_instances_later.v
combineSepGives_laterN	InstancesLater.lean	maybe_combine_sep_gives_laterN	class_instances_later.v
combineSepGives_except0	InstancesLater.lean	maybe_combine_sep_gives_except_0	class_instances_later.v

The tactic should exhibit the following behaviour, consistent with that in Rocq (correct me if I am wrong):

• If all propositions being combined exist in the intuitionistic context, then the resultant combined proposition also exists in the intuitionistic context.
• Propositions in the intuitionistic context can be used as arguments of the tactic multiple times. For example, if we have HP : P in the intuitionistic context, then icombine HP HP HP as HNew results in HNew : P ∗ P ∗ P being introduced.
• Propositions in the spatial context, by contrast, cannot be used multiple times, so the tactic throws an error in that case.
• If some propositions are in the intuitionistic context while others are in the spatial context, then the resultant combined proposition is in the spatial context. For example, if we have HP : P and HQ : Q in the intuitionistic context as well as HR : R in the spatial context, then icombine HR HQ HP HR as HNew produces Hnew : R ∗ Q ∗ P ∗ R in the spatial context.
• Right associativity: even though propositions are combined from left to right in the order of tactic arguments, combining P, Q and R should give P ∗ Q ∗ R instead of (P ∗ Q) ∗ R.

Regarding the last point, it appears that this is handled automatically by the type class instance for recursion in Rocq. Since recursion is handled by iCombineAsCore in Lean instead, we currently have the type class instance combineSepAs_assoc for this purpose.

Checklist

• My code follows the mathlib naming and code style conventions
• I have updated PORTING.md as appropriate
• I have added my name to the authors section of any appropriate files

[MackieLoeffel]

Thanks for the PR! I had a brief look over it and added some comments.

[MackieLoeffel]

I am surprised that you can use ∧, I was expecting && as the boolean version.

Also does this lemma correspond to a lemma in Rocq? If so, please add a rocq_alias annotation.

[alvinylt]

It looks like p1 and p2 are forced into being p1 = true and p2 = true when ∧ is used as a connective. I have updated the lemma to use && instead; both formulations work with my implementation.

I'm not aware of a comparable lemma in the Rocq codebase, but I've added it into this file since the lemma hold generically. Otherwise I guess we can also place the lemma directly in Combine.lean instead.

[MackieLoeffel]

Instead of writing this function as a recursive function, I recommend that you define a CombineState and then an function that combines the CombineState with one Ident. I think this should allow you to get rid of some of the duplication in this function. You can for example look at the revert tactic for how to do this.

[alvinylt]

I have now restructured the code to handle the hypotheses iteratively with the mutable state instead of recursively, so there is no need for new idents at every iteration anymore.

In the original iCombineAsCore, there was pattern matching on the list of hypotheses hs, and for the case when hs was in the form h1 :: h2 :: htail, there was pattern matching on htail. This is no longer necessary with the current iterative approach, which means there is also no need for repeated pattern matching on matchBool p1 and matchBool p2.

[alvinylt]

The elab definitions for icombine ... as ... and icombine ... gives ... now initialises the mutable state and handles the loop over the list of hypotheses, similar to how it is done in the iclear tactic.

[MackieLoeffel]

It is not ideal to do this in two separate calls to iCombineGivesCore and iCombineAsCore. Instead, it would be better to have a single iCombineGivesAsCore function that does both at the same time.

[alvinylt]

How about defining the icombine ... as ... gives ... syntax as a macro?

macro "icombine" idents:(colGt ident)* "as" colGt patAs:icasesPat "gives" colGt patGives:icasesPat : tactic =>
  `(tactic| (icombine $idents* gives $patGives; icombine $idents* as $patAs))

So this appears to be the simplest way to define icombine ... as ... gives ... without being repetitive as the elab definitions for icombine ... as ... and icombine ... give ... now involve more than calling a helper function.

[lzy0505]

I believe this draft PR was accidentally closed because it was intended to merge into the branch of a PR that was merged. I cannot reopen this PR because the target branch has been deleted.
@alvinylt Could you open a new PR and select master as the target branch?

[alvinylt]

@lzy0505 A new pull request (#392) has been reopened. I'm refactoring the code to handle the list of hypotheses iteratively (and using the CombineState structure) instead of recursively to avoid the need for a new ident at every iteration. This should be ready by the end of today.

[markusdemedeiros]

Apologies for closing this!