Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] a question about 'case' tactic (used with an inductive predicate)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] a question about 'case' tactic (used with an inductive predicate)


Chronological Thread 
  • From: Cedric Auger <sedrikov AT gmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] a question about 'case' tactic (used with an inductive predicate)
  • Date: Wed, 11 Feb 2015 22:52:23 +0100



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




Archive powered by MHonArc 2.6.18.

Top of Page