Stream: math-comp users

Topic: Specializing lemmas before using


view this post on Zulip Kimaya Bedarkar (Apr 04 2024 at 08:54):

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.

view this post on Zulip Pierre Roux (Apr 04 2024 at 09:47):

Maybe have [bar bar_pred] := foo ... . if I understand what you want. Or have /foo[bar bar_pred] := ... . when foo applies on one thing.

view this post on Zulip Kimaya Bedarkar (Apr 04 2024 at 10:06):

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

view this post on Zulip Sergey Bozhko (Apr 04 2024 at 10:21):

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.

view this post on Zulip Pierre Roux (Apr 04 2024 at 10:31):

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.

view this post on Zulip Kimaya Bedarkar (Apr 04 2024 at 10:45):

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?

view this post on Zulip Kimaya Bedarkar (Apr 04 2024 at 10:47):

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

view this post on Zulip Pierre Roux (Apr 10 2024 at 08:52):

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