Search code examples
coq

In Coq, is there a way to get rid of "useless" preconditions in a hypothesis?

Sometimes due to a combination of the remember and induction tactics, I end up with hypothesis that look like a bit like this:

Heqa: a = Foo b
IH1: a = Foo b -> bla_bla_bla
IH2: a = Foo b -> ble_ble_ble

Is there a quick way to get those useless a = Foo b preconditions in IH1 and IH2 out of the way? The only way to do that that I can think of is very verbose and repetitive:

assert (IH1': a = Foo b). { apply Heqa. }
apply IH1 in IH1'. clear IH1. rename IH1' into IH1.

assert (IH2': a = Foo b). { apply Heqa. }
apply IH2 in IH2'. clear IH2. rename IH2' into IH2.
Solution

  • You can use the specialize tactic:

    specialize (IH1 Heqa).
specialize (IH2 Heqa).

    will get you

    Heqa: a = Foo b
IH1: bla_bla_bla
IH2: ble_ble_ble

    which seems is what you want.

    specialize applies some arguments to a hypothesis and rewrites it.

    By the way, using a somewhat similar tactic pose proof we can keep the original hypothesis intact. More details can be found here.