The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

Hi all,

In the (very abstracted example of a) lemma below, is there a way to
prove the result without writing "nat" or "x = y"?

What I'd like is to be able to write something like
specialize (H _).
    admit.
specialize (H _).
    admit.
specialize (H _).
    admit.
specialize (H _).
    admit.
apply H.
(i.e. turn the first thing H wants into a new goal).


Lemma Lem : forall (x : nat), (x = 3).
Proof.
intros.
assert (forall (y : nat), (x = y) ->
        forall (z : nat), (x = z) -> (x = 3)).
    admit.

(* Suppose we are here, "nat"s can be shown to exist, and "x = y"
   and "x = z" are provable (we'll just pretend and use admit).
   How can we write this proof without writing "nat" or "x = y"?
   (in a real proof, "nat" and "x = y" would be large expressions I don't
   want to have to repeat) *)

assert (y : nat).
    admit.
specialize (H y).
assert (EQ : x = y).
    admit.
specialize (H EQ).
assert (z : nat).
    admit.
specialize (H z).
apply H.
    admit.
Qed.


Thanks
Ian