Prove existential quantifier using Coq

Question

Assuming we have an inductive data structure and some predicate over it:

Inductive A : EClass :=
   X | Y .

Definition P (a: A) : bool :=
 match a with
   X => true
 | Y => false
 end.

Then, I formulate a theorem to say there exists an element a such that P a returns true:

Theorem test :
 exists a: A, P a.

There are probably various ways of doing it, I am thinking how to use case analysis to prove it, in my mind, it works something like this:

remember there are 2 ways A can be constructed
try each way one by one, stop if we find a witness such that P a holds.

My Coq code looks like:

evar (a: A). (* introduce a candidate to manipulate *)
destruct a eqn: case_A. (* case analysis *)
  - (* case where a = X *) 
    exists a.
    rewrite case_A.
    done.  
  - (* case where a = Y *) 
    (* stuck *)

My question is that,

is my prove strategy logically flawed?
if not, my Coq is the problem, how can I convey to Coq that my job is done is I find one witness? might be I should not destruct?

Thanks!

ejgallego · Accepted Answer · 2017-09-24 13:27:31Z

4

Yes, your proof is flawed! All that you need is to provide the witness first:

Inductive A := X | Y .

Definition P (a: A) : bool := match a with X => true | Y => false end.

Theorem test : exists a: A, P a = true.
Proof. now exists X. Qed.

If you do case analysis first, you'll get into a dead-end.

answered Sep 24, 2017 at 13:27

ejgallego

6,8721 gold badge17 silver badges31 bronze badges

Sign up to request clarification or add additional context in comments.

Comments

Daniel Schepler · Accepted Answer · 2017-09-26 00:22:05Z

Here is a rough framework that demonstrates how you might program a Coq tactic to try all elements of a finite type as witnesses.

(* Typeclass to register an enumeration of elements of a type. *)
Class Enumeration (A:Type) :=
enumerate : list A.
Arguments enumerate A [Enumeration].

(* Typeclass to register decision procedures to determine whether
   a given proposition is true or false. *)
Class Decision (P:Prop) :=
decide : {P} + {~P}.
Arguments decide P [Decision].

(* Given a Coq list l, execute tactic t on every element of
   l until we get a success. *)
Ltac try_list l t :=
match (eval hnf in l) with
| @cons _ ?hd ?tl => (t hd || try_list tl t)
end.
(* Tactic for "proof by reflection": use a decision procedure, and
   if it returns "true", then extract the proof from the result. *)
Ltac by_decision :=
match goal with
|- ?P => let res := (eval hnf in (decide P)) in
         match res with
         | left ?p => exact p
         end
end.
(* Combination to try to prove an (exists x:A, P) goal by trying
   to prove P by reflection for each element in an enumeration of A. *)
Ltac try_enumerate :=
match goal with
|- @ex ?A ?P =>
  try_list (enumerate A)
    ltac:(fun x => exists x; by_decision)
end.

(* Demonstration on your example *)
Inductive A := X | Y.
Instance A_enum : Enumeration A :=
cons X (cons Y nil).
Instance bool_eq_dec : forall x y:bool,
  Decision (x = y).
Proof.
intros. red. decide equality.
Defined.

Definition P (a:A) : bool :=
match a with
| X => true
| Y => false
end.

Goal exists a:A, P a = true.
Proof.
try_enumerate.
Qed.

Collectives™ on Stack Overflow

Prove existential quantifier using Coq

2 Answers 2

Comments

Comments

Your Answer

Hot Network Questions

Collectives™ on Stack Overflow

2 Answers 2

Comments

Comments

Your Answer

Sign up or log in

Post as a guest

Related