Search code examples
coqcoq-tactic

Coq use refine with bi-implication

I'm not sure how to word my question, because I'm new to coq. I want to use refine with a theorem that includes bi-implication. Example code:

Parameters A B C : Prop.

Theorem t1:
  A -> B -> C.
Admitted.

Theorem t2:
  A -> B <-> C.
Admitted.

Theorem test1:
  A -> B -> C.
Proof.
  intros.
  refine (t1 _ _).
  assumption.
  assumption.
Qed.

Theorem test2:
  A -> B -> C.
Proof.
  intros A B.
  refine (t2 _ _).

t1 and t2 are theorems I want to use in refine. t1 works how i expect (shown in test1). But i have a problem with t2. The error I get is:

Ltac call to "refine (uconstr)" failed.
Error: Illegal application (Non-functional construction): 
The expression "t2 ?a" of type "Top.B <-> C"
cannot be applied to the term
 "?y" : "?T"
Not in proof mode.

What I have tried is something like this:

Theorem test3:
  A -> B -> C.
Proof.
  intros.
  cut (B <-> C).
  firstorder.
  refine (t2 _).
  assumption.
Qed.

But with longer props and proofs, it becomes a bit messy. (Also I have to prove the bi-implication myself). Can I use t2 and get its subgoals in a simpler way?

Thanks

Solution

  • A <-> B is defined as (A -> B) /\ (B -> A) so you can project with proj1, proj2:

    Theorem test2:
  A -> B -> C.
Proof.
  intros A B.
  refine (proj1 (t2 _) _).