Stream: Miscellaneous

Topic: Strict positivity requirement


view this post on Zulip Joshua Grosso (Sep 10 2020 at 22:37):

If I have an Inductive definition which violates the strict positivity requirement, are there any general heuristics for how to alternately encode my datatype such that Coq will accept it? Or, in general, is this not possible?

view this post on Zulip Jasper Hugunin (Sep 10 2020 at 23:31):

The strict positivity requirement prevents writing definitions which allow you to prove false, so there is no completely general way to get an equivalent datatype for every non strictly positive definition. However, if you can share your concrete example, people around here can probably help you either understand why it would let you prove false or come up with a way of encoding it.

view this post on Zulip Paolo Giarrusso (Sep 11 2020 at 03:06):

@Joshua Grosso I know some examples can be written by recursion instead, but that’s unusual... except it always happens with logical relations.

view this post on Zulip Paolo Giarrusso (Sep 11 2020 at 03:08):

And in that case, there is usuallty something that you can do induction over.

view this post on Zulip Paolo Giarrusso (Sep 11 2020 at 03:09):

but I agree with Jasper — concrete examples please, there are too many ways.

view this post on Zulip Joshua Grosso (Sep 11 2020 at 05:27):

I'm trying to make a datatype that represents a type in the simply-typed lambda-calculus with variant types added in. My initial attempt works (where a variant is represented as an associative array from constructor names to wrapped types):

Inductive ty : Type :=
| Arrow : ty -> ty -> ty
| Unit : ty
| Variant : list (string * ty) -> ty.

But, let's say I want to make the type a bit stronger, i.e. enforce uniqueness of constructor names. My naïve attempt was:

Definition keys (A : Type) : list (string * A) -> list string := map fst.

Inductive ty : Type :=
| Arrow : ty -> ty -> ty
| Unit : ty
| Variant : forall l : list (string * ty), NoDup (keys l) -> ty.

but this fails with: Non strictly positive occurrence of "ty" in "forall l : list (string * ty), NoDup (keys l) -> ty".

view this post on Zulip Joshua Grosso (Sep 11 2020 at 05:29):

The only solution I can think of is to make a separate Fixpoint that creates a Prop ensuring a given ty is valid (and figure out how to appease the termination checker), but my hope is that I can make ty's valid by construction.

view this post on Zulip Kenji Maillard (Sep 11 2020 at 06:41):

Joshua Grosso said:

The only solution I can think of is to make a separate Fixpoint that creates a Prop ensuring a given ty is valid (and figure out how to appease the termination checker), but my hope is that I can make ty's valid by construction.

That's probably the simplest solution. You could then implement "smart" constructors with the type above, and prove that the expected elimination scheme for ty holds (the one with a NoDup hypothesis in the Variant case).

view this post on Zulip Paolo Giarrusso (Sep 11 2020 at 11:28):

Wait, how would you get the expected elimination scheme? Unless you turn ty’s into a sigma type.

view this post on Zulip Paolo Giarrusso (Sep 11 2020 at 11:30):

While you’re here, the same problem applies to embedding data structures, if they contain validity predicates. Do you want a dictionary instead of an association list? Tough luck, usually — I’ve stuck with association lists. (Some dictionary libraries might offer “raw” variants without embedded validity).

view this post on Zulip Paolo Giarrusso (Sep 11 2020 at 11:32):

Re validity, there shouldn’t be any problem with the termination checker: the validity checker is plain structural recursion:

view this post on Zulip Paolo Giarrusso (Sep 11 2020 at 11:36):

Fixpoint valid_ty (T : ty) : Prop :=
match T with
| Variant Ts => Forall (fun (k, T) => valid_ty T) Ts /\ NoDup (keys Ts)
| Unit => True
| Arrow T1 T2 => valid_ty T1 /\ valid_ty T2
end.

view this post on Zulip Joshua Grosso (Sep 11 2020 at 13:54):

Very good points all, thank you both! I'll go the Fixpoint route then (not sure why I thought there was a termination issue, I must've done something wrong last time).


Last updated: Dec 05 2023 at 05:01 UTC