Hello. I have some lemmas with existentials in the conclusion. For example, suppose I have :

```
Lemma foo: forall a b c,
Hyp1 ->
Hyp2 ->
....
Hyp n ->
exists bar, pred bar
```

I want to introduce `bar`

and `pred bar`

in my context by applying `foo`

. I also want the universally quantified variables and hypotheses to be introduced as subgoals.

Is there an idiomatic SSReflect way to do this?

I know that stdpp has a tactic for this (`opose proof`

). Is there a similar tactic in SSReflect?

Note that `have foo as [bar Hbar]`

does not work because the forall quantified variables are not fed to the lemma.

Maybe `have [bar bar_pred] := foo ... .`

if I understand what you want. Or `have /foo[bar bar_pred] := ... .`

when foo applies on one thing.

`have [bar bar_pred] := foo`

does not work for me because then I have to explicitly provide all the arguments to `foo`

. I want to avoid that and instead want that the hypotheses `foo`

relies on to be added as subgoals

I think Kimaya wants to do something like this.

```
(* Intentionally repetitive and very annoying *)
Section A.
Variable X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 : Type.
Variable f1 : X1 -> X2 -> X3 -> X4 -> X5 -> X6 -> X7 -> X8 -> X9 -> X10 -> Prop.
Variable f2 : X1 -> X2 -> X3 -> X4 -> X5 -> X6 -> X7 -> X8 -> X9 -> X10 -> Prop.
Variable f3 : X1 -> X2 -> X3 -> X4 -> X5 -> X6 -> X7 -> X8 -> X9 -> X10 -> Prop.
Variable Y : Type.
Variable p1 p2 p3 : Y -> Prop.
Lemma foo :
forall x1 x2 x3 x4 x5 x6 x7 x8 x9 x10,
f1 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->
f2 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->
f3 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->
exists y, p1 y /\ p2 y /\ p3 y.
Proof.
(* some proof *)
Admitted.
End A.
(* Let's use [foo]. *)
Section B.
Variable X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 : Type.
Variable f : X1 -> X2 -> X3 -> X4 -> X5 -> X6 -> X7 -> X8 -> X9 -> X10 -> Prop.
Hypothesis H : forall x1 x2 x3 x4 x5 x6 x7 x8 x9 x10, f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10.
Variable (x1 : X1) (x2 : X2) (x3 : X3) (x4 : X4) (x5 : X5) (x6 : X6) (x7 : X7) (x8 : X8) (x9 : X9) (x10 : X10).
Variable Y : Type.
Variable p1 : Y -> Prop.
Lemma bar1 :
exists y, p1 y.
Proof.
(* Not clear how to destruct [foo] right away. *)
Fail (have [y PP] := foo _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 _ _ _).
Abort.
Lemma bar2 :
exists y, p1 y.
Proof.
(* [apply H] does most of the work of figuring out foo's arguments *)
unshelve (edestruct foo as [y [A [B C]]]; try apply H); auto.
exists y; apply A.
Qed.
Lemma bar3 :
exists y, p1 y.
Proof.
(* In this case, [opose proof] works the same way as edestruct. *)
unshelve (opose proof foo as [y [A [B C]]]; try apply H); auto.
exists y; apply A.
Qed.
End B.
```

Looks to me like an XY problem, you should probably rather try to reduce the number of arguments of `foo`

by grouping them in meaningful objects. Automatic inference with things like typeclasses and implicit arguments could also help but beware of spaghetti code.

Maybe our point is not clear because the example got a little too convoluted. Sorry for that.

I agree that in general there should be more bundling up of the hypotheses.

However I do not think it is uncommon to be in a situation where there exists a lemma that has a disjunction or existential in the conclusion and the lemma relies on some hypothesis that perhaps you want dismissed using some automation such as hints database or lia.

In such cases I would want to use some tactic that puts all the universally quantified dependencies of the lemma as subgoals (thus allowing calling some automation tactics on them) and directly gives the user the conclusion to destruct.

Do you disagree that such a tactic would be required /useful?

I am also open to any other suggestions that might eliminate the need for this type of tactic in the first place.

I understand something that could avoid having to type `have [x Px] := exists x, P x. \n apply: foo. \n subproofs`

may seem attractive. But you have to be careful when designing such a tactic, so that it doesn't lead to overly brittle proofs. It's hard to reach a good balance between typing less when writing the proof and painful efforts to fix the proof over and over in the future because it's not robust enough. Saving a bit of time now can easily lead to huge wastes in the future. ssreflect may seem a bit restrictive sometimes, but when put to good use, experience shows that it can help designing very robust and easy to maintain proofs.

Last updated: Jul 23 2024 at 20:01 UTC