Supongamos que ya he probado algún teorema en coq, y luego quiero presentarlo como una hipótesis en la prueba de otro teorema. ¿Hay una manera sucinta de hacer esto?

La necesidad de esto generalmente surge cuando quiero hacer algo como una prueba de casos. Y he descubierto que una forma de hacer esto esassert La declaración del teorema, y ​​luego probarlo de inmediato, pero esto parece un poco engorroso. Por ejemplo tiendo a escribir cosas como:

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.

Pero ¿hay una manera más fácil que tener que escribir el conjuntoassert [statement] by apply [theorem] ¿cosa?