feat: icombine

[alvinylt]

Description

This reopens the accidentally closed pull request #388.

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 combineAsProofModeHyp and combineGivesProofModeHyp 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 the iterative process is handled by combineGivesProofModeHyp 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]

Can you get rid of this boolean by special casing the 0 argument case and if there is at least one hypothesis, initialize this structure with the first hypothesis?

[MackieLoeffel]

What are pf and pf1 and why are both necessary?

[MackieLoeffel]

Can you combine CombineGivesState and CombineAsState into a single state and also combine the two combine... functions such that one needs to do a single pass instead of two like in Rocq? I thought there was a comment in the Rocq version explaining why they need to do it in a single pass.

[MackieLoeffel]

I am not sure if this instance fully solves the problem. Can you instead call instance search in a different order in the tactic to get the behavior we want? E.g. by reversing order in which the list of hypothesis is processed?