The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2015-02-11 20:37 GMT+01:00 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?

​Yes:

In your hypothesis, you have:

H : even (S (S (S (S (S O)))))

and your goal is:

even ​(S (S (S (S (S (S (S O)))))))

When you run "case H", Coq will replace all occurrences of the index (the nat in "nat -> Prop" of even) it finds in the goal (other hypotheses are not affected, unless one of them uses directly H, in which case an error is returned; this is the main difference I see with destruct, where all hypotheses can be affected even if they do not use H).

Thus you could think of case as a "two steps tactic".

First it abstract its index (note that parameters, ie. arguments left of ':' in the inductive definition, are unaffected), then it replaces it with what it can find in the constructors of the inductives.

Intermediate step:

​H : even <Hole 0>

and your goal is:

even ​(S (S <Hole 0>))

​

​First case (replace <Hole 0> with O as told by the even_O constructor)​:

​|- even (S (S O)) (* ie. even 2 *)​

​​Second case (replace <Hole 0> with S (S n) as told by the even_SS constructor, needs introduction of n and even n)​:

​|- forall n, even n -> even (S (S (S (S n))))

​

 

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