Elim a double negation hypothesis in Coq Proof Assistant?

Question

Could anyone explain to me why do we have to prove ~A after elim Ha.?

Before "elim Ha"

1 subgoals
 A : Prop
 Ha : ~ ~ A
______________________________________(1/1)
 A

After

1 subgoals
 A : Prop
 Ha : ~ ~ A
______________________________________(1/1)
 ~ A

Is it right that means ~~A true, ~A true -> A true?

In my knowledge, I only know the rule ~E is ~A true, A true -> FalseHood true

Answer 1

In Coq, ~ P is a notation for P -> False. If I'm not mistaken, using elim on an hypothesis of the shape ~ P is the same as directly using False_rect (you can Print False_rect for more info) with P as an input.

Doing so, you say to Coq "I know that P holds, so using P -> False, I can derive a proof of False" which closes the goal by contradiction. That's why each time you elim a ~ P, Coq asks you to provide a proof of P. In your case, P is ~ A.