Предположим, что я уже доказал некоторую теорему в coq, а позже я хочу представить ее как гипотезу при доказательстве другой теоремы. Есть ли лаконичный способ сделать это?
Потребность в этом обычно возникает для меня, когда я хочу сделать что-то вроде доказательства по случаям. И я обнаружил, что одним из способов сделать это является assert утверждение теоремы, а затем сразу же доказать это, но это кажется громоздким. Например, я предпочитаю писать такие вещи, как:
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.
Но есть ли более простой способ, чем набрать целую вещь assert [statement] by apply [theorem]?
