The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

Just to flesh out the previous email a bit more:

Inductive ibubble (A:Type) : nat -> forall B:Type, B -> B -> Type :=
| ibubble_base : forall x0 y0:A, ibubble A 0 A x0 y0
| build_ibubble : forall (n:nat) (B:Type) (xn yn:B),
    ibubble A n B xn yn -> forall xn1 yn1 : xn = yn,
    ibubble A (S n) (xn = yn) xn1 yn1.
Inductive bubble (A:Type) (n:nat) : Type :=
| bubble_existT : forall (B:Type) (xn yn:B),
    ibubble A n B xn yn -> bubble A n.

Implicit Arguments ibubble_base [[A]].
Implicit Arguments build_ibubble [[A] [n] [B] [xn] [yn]].
Implicit Arguments bubble_existT [[A] [n] [B] [xn] [yn]].

Definition bubble_half_type {A:Type} {n:nat} (b:bubble A n) : Type :=
match b with
| bubble_existT B _ _ _ => B
end.

Definition bubble_bottom {A:Type} {n:nat} (b:bubble A n) :
  bubble_half_type b :=
match b with
| bubble_existT _ xn _ _ => xn
end.

Definition bubble_top {A:Type} {n:nat} (b:bubble A n) :
  bubble_half_type b :=
match b with
| bubble_existT _ _ yn _ => yn
end.

Definition bubble_base {A:Type} (x0 y0:A) : bubble A 0 :=
  bubble_existT (ibubble_base x0 y0).

Definition build_bubble {A:Type} {n:nat} (b:bubble A n) :
  bubble_bottom b = bubble_top b ->
  bubble_bottom b = bubble_top b -> bubble A (S n) :=
match b with
| bubble_existT _ xn yn b' => fun xn1 yn1 : xn=yn =>
              bubble_existT (build_ibubble b' xn1 yn1)
end.

Definition my_bubble_rect (A:Type) (P: forall n:nat, bubble A n -> Type)
  (Pbase : forall x0 y0:A, P 0 (bubble_base x0 y0))
  (Pbuild : forall (n:nat) (b:bubble A n), P n b ->
     forall (xn1 yn1:bubble_bottom b = bubble_top b),
       P (S n) (build_bubble b xn1 yn1))
  (n:nat) (b:bubble A n) : P n b.
Proof.
destruct b.
induction i.
exact (Pbase x0 y0).
exact (Pbuild n (bubble_existT i) IHi xn1 yn1).
Defined.

Therefore, bubble acts as if it were an inductive type with constructors 
bubble_base and build_bubble.  (Which of course can't be done literally, 
since 
you'd have to define bubble_bottom and bubble_top simultaneously.)
-- 
Daniel Schepler