CODEWITHSUNDEEP
coq
user181407
user181407

Reputation: 235

Coq tactic that adds the value of an inductive term to the context

Just to give a simple example of this issue I keep running into, suppose I wish to prove forall f : nat -> bool, exists i j, i<>j /\ f i = f j. The obvious thing to do is check the values of f 0, f 1, f 2, and proceed accordingly. However, if I simply say destruct (f 0), Coq doesn't modify the goal, since f 0 doesn't occur as a subterm. Therefore, I don't have the information I want about what value f 0 is currently taking. Ideally, I would like for Coq to add a witness H : f 0 = false to the context so I can keep track of it.

What I've been doing to get around these issues is to prove an auxiliary lemma bool_destruct : forall b : bool, b = false \/ b = true. Now, if I say destruct (bool_destruct (f 0)) Coq will add the desired H to the context. Naturally, this is tedious when you have to prove this sort of lemma for each inductive type. Thus, I'm wondering if there is a nice tactic that handles these sorts of situations.

Upvotes: 2

Views: 135

Answers (1)

ejgallego
ejgallego

Reputation: 6852

The destruct tactic already supports what you want:

destruct (f 0) eqn:f_is0.

Your idea of using bool_destruct is not as bad as you make it to be, for instance, a similar idea plus a pattern generalization feature of the case tactic is used in math-comp to provide custom destruct views.

Upvotes: 4

Related Questions