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.
```

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: Jun 23 2024 at 23:01 UTC