The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

Hi,

While continuing the quest to understand what 'case' tactic means, I have 
tried this:

        Inductive even : nat -> Prop :=
        | even_O : even 0
        | even_SS : forall n : nat, even n -> even (S (S n)).

and then:

        (* the goal itself is pointless --- I am just curious about 'case' 
tactic *)
        Goal even 5 -> even 7.
        Proof.
          intro H.
          case H.

I see that Coq generates two subgoals:

        even 2

        forall n : nat, even n -> even (S (S (S (S n))))

In this particular case, I am not so much interested whether the subgoals are 
provable (they are) and how do the subproofs look like (trivial)
but I would like to understand how did Coq computed these subgoals.
(presumably from the original goal, the context and the chosen tactic)

Does anyone know?

Thanks a lot in advance for help with this.
--
Matej