Stream: Coq users

Topic: repo for testing positivity check implementation

view this post on Zulip walker (Apr 26 2023 at 16:07):

is there somewhere where I can get tests for all the corner-cases for positivity checker ?

I am specifying a set of positivity checker rules following coq's version without mutual induction, and I want to test that my specs work as I think they should, I already tested natural numbers, lists and vectors are in the way ... but is there a repoistory of tests with all possible corner cases so I can catch errors early before I get stuck somewhere in the proofs ?

Also It is a little bit painful trying to construct the syntax tree by hand (example below) is there a coq library that just accepts grammer and give me ast in form of my custom inductive type?

Example of how I construct and prove positivity of the S constructor of nat:

Example nat_ctors : InductiveConstructors 0.
Proof.
apply: cons.
    by exists (Build_InductiveConstructor "O"%string (induct "nat")).
apply: cons.
    by exists (Build_InductiveConstructor "S"%string (term.pi (induct "nat") (induct "nat"))).
apply: nil.
Defined.

Example natT := mkInductiveType "nat"%string Cempty Closedu0 nat_ctors.

Example S_is_positive: natT |+> term.pi (induct "nat") (induct "nat").
Proof.
apply: Positivity_pi;
    last by apply: O_is_positive.
apply: StrictPositivity_base => //=.
by rewrite PIn_empty_false_iff.
Qed.

view this post on Zulip walker (Apr 26 2023 at 16:08):

walker said:

is there somewhere where I can get tests for all the corner-cases for positivity checker ?

I am specifying a set of positivity checker rules following coq's version without mutual induction, and I want to test that my specs work as I think they should, I already tested natural numbers, lists and vectors are in the way ... but is there a repoistory of tests with all possible corner cases so I can catch errors early before I get stuck somewhere in the proofs ?

Also It is a little bit painful trying to construct the syntax tree by hand (example below) is there a coq library that just accepts grammer and give me ast in form of my custom inductive type?

Example of how I construct and prove positivity of the S constructor of nat. It will be nice if I can automate the construction part so I write many tests:

Example nat_ctors : InductiveConstructors 0.
Proof.
apply: cons.
    by exists (Build_InductiveConstructor "O"%string (induct "nat")).
apply: cons.
    by exists (Build_InductiveConstructor "S"%string (term.pi (induct "nat") (induct "nat"))).
apply: nil.
Defined.

Example natT := mkInductiveType "nat"%string Cempty Closedu0 nat_ctors.

Example S_is_positive: natT |+> term.pi (induct "nat") (induct "nat").
Proof.
apply: Positivity_pi;
    last by apply: O_is_positive.
apply: StrictPositivity_base => //=.
by rewrite PIn_empty_false_iff.
Qed.

Last updated: Oct 13 2024 at 01:02 UTC