Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Introduce previously proved theorem as hypothesis

Tags:

Suppose that I have already proved some theorem in coq, and later I want to introduce it as a hypothesis in the proof of another theorem. Is there a succinct way to do this?

The need for this typically arises for me when I want to do something like a proof by cases. And I've discovered that one way to do this is to assert the statement of the theorem, and then immediately prove it, but this seems kind of cumbersome. For example I tend to write things like:

Require Import Arith.EqNat.  Definition Decide P := P \/ ~P.  Theorem decide_eq_nat: forall x y: nat, Decide (x = y). Proof.   intros x y. remember (beq_nat x y) as b eqn:E. destruct b.     left. apply beq_nat_eq. assumption.     right. apply beq_nat_false. symmetry. assumption. Qed.  Theorem silly: forall x y: nat, x = y \/ x <> y. Proof.   intros x y.   assert (Decide (x = y)) as [E|N] by apply decide_eq_nat.     left. assumption.     right. assumption. Qed. 

But is there an easier way than having to type the whole assert [statement] by apply [theorem] thing?

like image 712
Juan A. Navarro Avatar asked Feb 15 '13 23:02

Juan A. Navarro


1 Answers

You can use pose proof theorem_name as X., where X is the name you want to introduce.


If you're going to destruct it right away, you can also: destruct (decide_eq_nat x y).

like image 142
Ptival Avatar answered Sep 28 '22 08:09

Ptival