Coq use refine with bi-implication

Question

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

Yeah, but I'm trying to use a more complex theorem, just wanted to post a simple example. — mdatsev
if you do destruct (t2 A). you will get H: B->C and H1: C->B in the context. Then you can use H to solve your goal. And the reason you can't use refine (t2 _ _) is that t2 is of type A->(B<->C), notice the parentheses. — larsr
I was hoping for maybe some smart tactic that is able to use B<->C to prove B->C and use it in refine somehow — mdatsev

Li-yao Xia Li-yao Xia · Accepted Answer · 2020-03-04T22:22:04

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 _) _).

Coq use refine with bi-implication

1 Answers