The Coq mailing list

[anoun AT labri.fr]

Hi all,
Can anybody tell me which kind of goals the tactic firstorder manage to solve
I tried to use it to prove automaticaly some first order formulas defined in a
finite domain but failed to do so

Examples:
========

Inductive try:Set:=|t1|t2|t3.

Definition pred1 (t:try):Prop:=
match t with
|t1=>True
|_=>False
end.

Definition pred2 (t:try):Prop:=
match t with
|_ =>True
end.

Lemma lem1:(exists x:try, pred1 x).
firstorder.
(* the goal is not changed *)
....

Lemma lem2:forall (x:try), pred2 x.
firstorder.
Qed.

Otherwise, Is there a complete tactic which solves first order formulas 
defined
in finite domains?

Thanks for your help!
Houda

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.