CODEWITHSUNDEEP
coq
Zheng Cheng
Zheng Cheng

Reputation: 400

Prove existential quantifier using Coq

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:

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,

Thanks!

Upvotes: 3

Views: 3246

Answers (2)

Daniel Schepler
Daniel Schepler

Reputation: 3103

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.

Upvotes: 3

ejgallego
ejgallego

Reputation: 6852

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.

Upvotes: 4

Related Questions