Search code examples
coqtheorem-proving

Simple identity in Coq

I am probably missing something fundamental.

I can prove the following "identity":

Theorem identity_simple : forall a : Prop, a -> a.

With intro. intro. assumption..

However, I can't seem to prove:

Theorem identity : forall a : Prop, a.

Of course I can do intro, but that leaves me with:

a : Prop
_________(1/1)
a

With which I do not know what to do.
The first form seems redundant, to state that for all a, a implies a.

Solution 
  • forall a : Prop, a -> a.

    reads as "given the proof of some proposition a we can construct a proof of the same proposition". Which is true, since we can just return the original proof.

    Let's check it with Coq:

    Print identity_simple.
(* 
output:

identity_simple = fun (a : Prop) (H : a) => H
     : forall a : Prop, a -> a
*)

    the proof term fun (a : Prop) (H : a) => H expresses exactly the described behavior.

    The first form seems redundant, to state that for all a, a implies a.

    You are right in some sense -- it is pretty obvious. You can think of it as a test -- if you cannot prove it then there must be something wrong with the logic.

    forall a : Prop, a.

    reads as "we can construct a proof of any proposition". Which is not true, since for example, you cannot construct the proof of False (in the empty context). And that would be a disaster -- we wouldn't want to use a logic in which everything is provable.