CODEWITHSUNDEEP
polymorphismcoqdecidableparameterized-types
user287393
user287393

Reputation: 1251

Parameterizing a proposition over other parameterized propositions of unknown arity in Coq

I want to define a parameterized proposition decidable that talks about the decidability of other parameterized propositions. To take a common example, even is a parameterized proposition that takes 1 parameter of type nat, and it is decidable. lt is a parameterized proposition that takes 2 parameters of type nat, and it is also decidable. I want decidable to be such that decidable even and decidable lt are both provable propositions.

The main difficulty in definining decidable is specifying its type. It must accept any parameterized proposition of type A -> B -> C -> ... Z -> Prop, where A...Z are types and their total number is arbitrary.

Here's my first attempt:

Inductive decidable { X : Type } ( P : X ) : Prop :=
| d_0 : X = Prop -> P \/ ~ P -> decidable X P   
| d_1 : forall ( Y Z : Type ), ( X = Y -> Z ) 
  -> ( forall ( y : Y ), decidable Z ( P y ) )
  -> decidable X P.

I thought it should be OK to use P \/ ~ P as a premise in d_0 because Coq would be smart enough to figure out that P : Prop, given the prior premise X = Prop. It's not.

So right now I can't find any way around spelling out the whole ugly thing: if I want to say that some P : A -> B -> C -> ... Z -> Prop is decidable, it must be written forall ( a : A ) ( b : B ) ( c : C ) ... ( z : Z ), P a b c ... z \/ ~ P a b c ... z. Ugh.

But maybe I'm missing something. Maybe there's some neat trick I've overlooked due to my rudimentary knowledge of Coq polymorphism.

Any suggestions?

Upvotes: 0

Views: 193

Answers (1)

user3551663
user3551663

Reputation: 

Require Import Coq.Arith.Even.

You'll need a heterogeneous list of types. It only contains types but the types may be from different universes.

Inductive list : Type :=
  | nil : list
  | cons : Type -> list -> list.

This function takes a list of sets and returns the type of the predicates that vary over these sets. I don't know how to generalize this function to accept any list of sorts (Prop, Type 1, Type 2, ...).

Fixpoint predicate (l1 : list) : Type :=
  match l1 with
  | nil => Prop
  | cons t1 l2 => t1 -> predicate l2
  end.

Eval simpl in predicate (cons bool nil).
Eval simpl in predicate (cons bool (cons nat nil)).

This function takes a list of sets and a predicate that varies over these sets, and asserts that the predicate is decidable.

Fixpoint decidable (l1 : list) : predicate l1 -> Prop :=
  match l1 with
  | nil => fun p1 => p1 \/ ~ p1
  | cons t1 l2 => fun p1 => forall x1, decidable l2 (p1 x1)
  end.

Eval simpl in decidable (cons nat nil) even.
Eval simpl in decidable (cons nat (cons nat nil)) le.
Eval simpl in decidable (cons nat (cons Prop (cons Set (cons Type nil)))).

Upvotes: 2

Related Questions