coqpowerset

Tower of powersets

I would like to define a family of types PowersetTower : Type -> nat -> Type such that:

  1. PowersetTower A 0 = A
  2. PowersetTower A (n+1) = Ensemble (PowersetTower A n) (that is, PowersetTower A n -> Prop)

Is that possible? One idea would be something like

Inductive PowersetTower : Type -> nat -> Type :=
| base : forall (A : Type), PowersetTower A 0
| step : forall (A : Type) (n : nat), (PowersetTower A n -> Prop) -> PowersetTower A (S n)
.

but here Coq complains about the non-strictly-positive occurrence of PowersetTower in the constructor step. However, it is PowersetTower A n that occurs on the left-hand-side of the arrow, and not PowersetTower A (S n), so why does Coq forbid this? It seems OK to me, because I am defining 'larger' types using 'smaller' ones. Would this definition cause a problem if accepted (perhaps using the bypass_check(positivity) attribute)?

Solution

  • I think what you want to define is not an inductive family indexed on n, but a type depending on n. You can do this by recursion:

    Fixpoint PowersetTower (A : Type) (n : nat) : Type :=
  match n with
    | 0 => A
    | S n' => (PowersetTower A n') -> Prop
  end.

    And this is a perfectly valid recursion on n, since it is always smaller in recursive calls – although the returned term happens to be a type, but this is all the salt of dependent types.