True in Goal State Coq

Question

While attempting to prove All in Software Foundations Volume 1, Logic.v, I came across a proof state of simply True. I.e. my proof state looks like:

T : Type 
P : T -> Prop
H : forall x : T, False -> P 
==================================
(1/1)
True 

I understand that simply using reflexivity should get my to my goal. But, I don't understand why, or what it means for the proof state to simply be True. What does this mean? And why does reflexivity work here?

Answer 1

You can ask Coq to print the definition of any term: Print True.

The response is:

Inductive True : Prop :=  I : True.

From this response, we see that True is a proposition, and that I is (by fiat) a proof of True.

When you have something like H : forall x : T, False -> P in your context above, it means H is a proof of forall x : T, False -> P, so that if your goal were to be forall x : T, False -> P then you could prove this goal using the command exact H.

In general, whenever you have H : P where P is a proposition, then H is a proof of P.

Accordingly, in this case, you have I : True, and your goal is True, so you can prove this goal using the command exact I.

Answer 2

Looks to be an undocumented but harmless behaviour of reflexivity (see the doc). For such a goal, I usually call easy (constructor or split work too).