coq very nearly has induction-recursion

IRExample.v

(** 
Dybjer and Setzer provide a logical framework in which Induction-Recursion — 
mutual definition of an (A : Type) and a (B : A -> V), in which constructors for A can talk about values of B, and B is defined by case analysis on members of A — 
becomes equivalent to supposing initial algebras for certain functors on { X : Set & X -> V }.  However, this latter family is, up to equivalences over V, the same as ordinary maps V -> Set.  The universal case, in which V = Set, becomes somewhat trickier, for universe level reasons.

In any case, here is one way to define a "large" universe ("large" in the sense: we allow all externally definable functions) with naturals, dependent sums, and dependent products.  A more careful presentation might work on a fibration over functions,
 { AB : Type * Type & fst AB -> snd AB } -> Type
instead, but good luck with that.
*)

Inductive over : Type -> Type :=
 nu : over nat
 | pi (x : Set) (cd : over x) (f : x -> Set) (of : forall t : x, over (f t))
  : over (forall t : x, f t)
 | si (x : Set) (cd : over x) (f : x -> Set) (of : forall t : x, over (f t))
  : over (sigT f).

Definition U_over := { t : Type & over t }.

Lemma N_to_N : over (nat -> nat).
Proof.
  apply pi.
  apply nu.
  intro.
  apply nu.
Defined.

Fixpoint varargs (n : nat) : Set :=
  match n with
  | O => nat
  | S m => nat -> (varargs m) end.

Fixpoint o_v_a (n : nat) : over (varargs n) :=
  match n return over (varargs n) with
  | O => nu
  | S m => pi nat nu _ (fun _ => o_v_a m) end.

Definition Over_VarArgs : over (forall n, varargs n) := pi nat nu varargs o_v_a.

Fixpoint varLength (n : nat) : Set :=
  match n with
  | O => nat
  | S m => sigT (fun _ : nat => varLength m) end.

Fixpoint o_v_l (n : nat) : over (varLength n) :=
  match n return over (varLength n) with
  | O => nu
  | S m => si nat nu _ (fun _ => o_v_l m) end.

Definition Over_ListNat : over (sigT varLength) :=
  si nat nu varLength o_v_l.


(** Another example, weakly sorted lists ; 
  we might try to argue: there is an empty sorted list

   snil : sl
   
  and there is a sorted list 
  
   scons (m : nat) (ll : sl) (ord : follows m ll) : sl
  
  where (follows : nat -> sl -> Type) is defined by induction over sl
  
   follows m snil = Unit 
  
  and
  
   follows m (scons n ll ordn) = m >= n
  
  sl is then equivalent to a disjoint union
   { snil } ∪ { m : nat * sl & follows (fst m) (snd m) }
  
  this example doesn't quite work as wanted, in that snil isn't part of the sigma ---
  a simple adjustment of "follows" can be found by making it explicit:
  
  follows' m ll = m >= (max ll)
  where now (max ll) is defined by cases
  
  max snil' = 0
  max (scons' m ll ord) = m
  
  Now sl' really is a sigma, of
  { x : nat & { ll : sl' & max ll = x } }

  hence the IR definition looks like  
  
 *)

Inductive HasMax : nat -> Type :=
  | snil : HasMax 0
  | scons m n (H : HasMax n) : (m >= n) -> HasMax m.

Definition sortedList := sigT HasMax.