CODEWITHSUNDEEP
coq
ax_fer
ax_fer

Reputation: 13

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 !

Upvotes: 0

Views: 143

Answers (1)

Pierre Jouvelot
Pierre Jouvelot

Reputation: 923

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.

Upvotes: 1

Related Questions