CODEWITHSUNDEEP
coqcoq-tactic
psquid
psquid

Reputation: 829

How do I simplify a hypothesis of the form True -> P in Coq?

If I have a hypothesis in my proof context that looks like H: True -> P and I want to convert it to H: P, what's the easiest way to do this? I tried simpl in H but it does nothing, and the only way I've found is the extremely unsatisfactory pose proof (H Coq.Init.Logic.I) as H. Isn't there a simpler way?

Upvotes: 4

Views: 667

Answers (1)

Théo Winterhalter
Théo Winterhalter

Reputation: 5108

There are two ways to work with this, besides using pose proof.

Using specialize.

This tactics allows you to provide arguments to you hypotheses. In you case you could do

specialize (H I).

or even

specialize H with (1 := I).

and you can use as if you want to create a copy rather than instantiate H directly.

Using forward.

I think this is what you want here. forward H. will ask you to prove the first hypothesis of H. So you will do something like this:

forward H.
- auto.
- (* Then resume with H : P *)

but you can also provide it with a (goal-closing) tactic:

forward H by auto.
(* Now you have one goal, and H has type P *)

forward is—as of yet—not part of the standard library. It can however be defined pretty easily (here is the definition from the MetaCoq library).

Ltac forward_gen H tac :=
  match type of H with
  | ?X -> _ => let H' := fresh in assert (H':X) ; [tac|specialize (H H'); clear H']
  end.

Tactic Notation "forward" constr(H) := forward_gen H ltac:(idtac).
Tactic Notation "forward" constr(H) "by" tactic(tac) := forward_gen H tac.

Note that simpl here doesn't work because it's not really a tactic to simplify hypotheses in the usual sense, it's really just a tactic to apply some computation rules, it basically evaluates the goal or the hypothesis you apply it on. True -> P does not reduce to P because it would then take one fewer argument.

Upvotes: 5

Related Questions