Stream: Coq users

Topic: Using tactic for automated proof checks of logic problems

view this post on Zulip Ben (May 18 2021 at 15:23):

Hi all, firstly I am very sorry for this beginner question.
I am trying to reproduce a simple Prolog example in Coq but I am struggling.

I want to use the firstorder tactic to see if there is a proof for a number of proposition or not (which are deduced). I can do this for single proposition of Ancestor and ~Ancestor using Goal. Now I would like to check this for all possible relations and note for which Ancestor or ~Ancestor relation it is able to find proofs using the firstorder tactic.

Is there a way to automate the goal proposition dynamically and check for proof? Do I need to write a python script that creates multiple files? Is there a way to access Coq inside another language?
I would really appreciate any help of how you would approach something like this. I have attached my code below.

Thanks,
Ben 

Section Ancestor.
Variable Person : Set.
Variable sue : Person.
Variable diana  : Person.
Variable john  : Person.
Variable edna  : Person.
Variable paul  : Person.
Variable francis  : Person.
Variable john2 : Person.
Variable john3  : Person.
Variable john4  : Person.
Variable joe  : Person.
Variable jennifer  : Person.
Variable juliet  : Person.
Variable janice  : Person.
Variable joey  : Person.
Variable tom  : Person.
Variable bonnie  : Person.
Variable katie  : Person.

Variable Parent : Person -> Person -> Prop.
Variable Ancestor : Person -> Person -> Prop.

Hypothesis data1 : Parent sue diana.
Hypothesis data2 : Parent john diana.
Hypothesis data3 : Parent sue bonnie.
Hypothesis data4 : Parent john bonnie.
Hypothesis data5 : Parent sue tom.
Hypothesis data6 : Parent john tom.
Hypothesis data7 : Parent diana katie.
Hypothesis data8 : Parent paul katie.
Hypothesis data9 : Parent edna sue.
Hypothesis data10 : Parent john2 sue.
Hypothesis data11 : Parent edna john3.
Hypothesis data12 : Parent john2 john3.
Hypothesis data13 : Parent francis john.
Hypothesis data14 : Parent john4 john.
Hypothesis data15 : Parent francis janice.
Hypothesis data16 : Parent john4 janice.
Hypothesis data17 : Parent janice jennifer.
Hypothesis data18 : Parent joe jennifer.
Hypothesis data19 : Parent janice juliet.
Hypothesis data20 : Parent joe juliet.
Hypothesis data21 : Parent janice joey.
Hypothesis data22 : Parent joe joey.

Hypothesis ax1 : forall x, ~Parent x x.
Hypothesis ax2 : forall x, ~Ancestor x x.
Hypothesis ax3 : forall x y, Parent x y -> Ancestor x y.
Hypothesis ax4 : forall x y, Parent x y -> ~Parent y x.
Hypothesis ax5 : forall w x y z, Parent w x /\ Parent y x -> ~Parent z x.
Hypothesis ax6 : forall x y z, ~Parent x y /\ Parent y z -> ~Ancestor x z.

Goal ~Ancestor francis john.
firstorder.
Qed.

view this post on Zulip Paolo Giarrusso (May 19 2021 at 04:19):

One can loop over the hypotheses in Ltac using "match goal", and probably with careful use of "fail N", but I fear you might need to interrupt invocations of firstorder that loop; IIRC, there exists a timeout tactic, but I've never used it with much success. If you generate multiple files and run coqc on each, at least you can run processes in parallel and kill those that don't terrminate.

Last updated: Sep 25 2023 at 12:01 UTC