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?
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.
@Joshua Grosso I know some examples can be written by recursion instead, but that’s unusual... except it always happens with logical relations.
And in that case, there is usuallty something that you can do induction over.
but I agree with Jasper — concrete examples please, there are too many ways.
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".
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.
Joshua Grosso said:
The only solution I can think of is to make a separate
Fixpoint
that creates aProp
ensuring a giventy
is valid (and figure out how to appease the termination checker), but my hope is that I can makety
'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).
Wait, how would you get the expected elimination scheme? Unless you turn ty’s into a sigma type.
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).
Re validity, there shouldn’t be any problem with the termination checker: the validity checker is plain structural recursion:
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.
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