Stream: Coq users

Topic: term_ltac as a subgoal (Beginner question)

Tiara Sinlo (Jan 26 2024 at 22:35):

Is it possible to have a term like ltac:(some_tactic) where Coq will infer the type but let me prove it as a subgoal? Or, less generally, suppose I want to go from

  Hpq : P -> Q
  ============================
  True

to

  Hq : Q
  ============================
  True

Some options I know of would be

1. lapply Hpq., which is akward to do for more than one argument (lapply H;[clear H; intro H; lapply H|]?)
2. assert P as Hp by admit. specialize (Hpq Hp). Here you have to specify the type of Hp
3. specialize (Hpq ltac:(some_tac)).This doesn't give you interactivity

These are all kind of suboptimal and I would really want to specify it as a term and prove it in a subgoal, like a mix of 1 and 3.
I kind of have the feeling that there was some ssreflect feature where you could do something like

move/(_ #) in Hpq.

which would give a situation like in lapply Hpq but I might have dreamt that one up...

Paolo Giarrusso (Jan 26 2024 at 22:45):

I'd recommend opose proof (Hpq _) from stdpp https://gitlab.mpi-sws.org/iris/stdpp/-/blob/dd93e4c3b23f25b208a6adaabacdb97c73c0059d/stdpp/tactics.v#L593

Paolo Giarrusso (Jan 26 2024 at 22:45):

Or opose proof* Hpq

Paolo Giarrusso (Jan 26 2024 at 22:47):

The latter will produce a subgoal for each premise of Hpq; the former will only turn underscore into subgoals, at least if the passed term has a non-dependent function type. (Goals for forall quantifiers are turned into evars that appear in other goals)

Tiara Sinlo (Jan 26 2024 at 23:03):

ospecialize (Hpq _) is pretty much 100% what I had in mind, thanks a lot!

Tiara Sinlo (Jan 26 2024 at 23:03):

Would be nice to have this directly in ssreflect as well

Last updated: Oct 13 2024 at 01:02 UTC