Strict positivity requirement · Miscellaneous

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?

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.

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.

Paolo Giarrusso (Sep 11 2020 at 03:08):

Paolo Giarrusso (Sep 11 2020 at 03:09):

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

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.

Kenji Maillard (Sep 11 2020 at 06:41):

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

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.

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

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:

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.

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

Stream: Miscellaneous

Topic: Strict positivity requirement

Joshua Grosso (Sep 10 2020 at 22:37):