Search code examples
coq

Coq : replace hypothesis into implication

I am learning Coq and I encountered an issue : how can I switch from that context

HA : A
HABC : A -> B -> C

to this one ?

HA : B -> C

I tried apply and rewrite tactics but it did not work.

Thank you for your help !

Solution

  • You need to apply HABC to HA to yield a witness of B -> C, which, by the way, it would make more sense to name HBC than HA, already used. Using ssreflect, you could write:

    From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma foo A B C (HA : A) (HABC : A -> B -> C) : false.
Proof.
have HBC := HABC HA.

    If you want to keep the HA name, one way to do it would be to replace the have with

    have {HA} HA := HABC HA.

    where the {HA} clears HA from the environment so that you can reuse the HA name right way for the result of the application.