CODEWITHSUNDEEP
coqproofquantifiersnegation
jaam
jaam

Reputation: 970

Proof by counterexample in Coq

After proving tens of lemmas in propositional and predicate calculus (some more challenging than others but generally still provable on an intro-apply-destruct autopilot) I hit one starting w/ ~forall and was immediately snagged. Clearly, my understanding and knowledge of Coq was lacking. So, I'm asking for a low-level Coq technique for proving statements of the general form

~forall A [B].., C -> D.  
exists A [B].., ~(C -> D).

In words, I'm hoping for a general Coq recipy for setting up and firing counterexamples. (The main reason for quantifying over functions above is that it's a (or the) primitive connective in Coq.) If you want examples, I suggest e.g.

~forall P Q: Prop, P -> Q.
~forall P: Prop, P -> ~P.

There is a related question which neither posed nor answered mine, so I suppose it's not a duplicate.

Upvotes: 5

Views: 1099

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

Recall that ~ P is defined as P -> False. In other words, to show such a statement, it suffices to assume P and derive a contradiction. The crucial point is that you are allowed to use P as a hypothesis in any way you like. In the particular case of universally quantified statements, the specialize tactic might come in handy. This tactic allows us to instantiate a universally quantified variable with a particular value. For instance,

Goal ~ forall P Q, P -> Q.
Proof.
  intros contra.
  specialize (contra True False). (* replace the hypothesis 
                                     by [True -> False] *)
  apply contra. (* At this point the goal becomes [True] *)
  trivial.
Qed.

Upvotes: 6

Related Questions