Impredicative encoding of mutual inductive types

gistfile1.coq

(* Must be ran with -impredicative-set *)

(* This files briefly demonstrates that the impredicative encoding of
   inductive fixed point (μα.F α is encoded as ∀α.(F α→α)→α) can also
   be used for mutual inductive types. The inductive definition is
   represented as a binary eliminator E α β, (α and β being
   placeholder for the respective types), the first type is then
   ∀αβ.E α β→α, the second one ∀αβ.E α β→β.

   In the non-mutual case, an eliminator is simply F α→α. However, in
   the mutually inductive case, given by two functor F₁ α β and
   F₂ α β, an eliminator must be able to eliminate on both functors,
   and is hence given by (F₁ α β→α)×(F₂ α β→β). *)

(*** Natural numbers ***)

Module Nat.

 Record nat_iterator (A:Set) := {
   succ : A->A ;
   zero : A
 }.

 Definition Nat := forall (A:Set), nat_iterator A -> A.

 Definition nat_nat : nat_iterator Nat := {|
   succ := fun (n:Nat) A (i:nat_iterator A) => i.(succ A) (n A i);
   zero := fun A i => i.(zero A)
 |}.

End Nat.


(*** Even and odd numbers ***)

Module EO.

 Record eo_iterator (A B:Set) := {
   zero : A ;
   succ_o : A -> B ;
   succ_e : B -> A
 }.

 Definition Even := forall A B:Set, eo_iterator A B -> A.

 Definition Odd := forall A B:Set, eo_iterator A B -> B.

 Definition eo_eo : eo_iterator Even Odd := {|
    zero := fun A B i => i.(zero A B) ;
    succ_o e := fun A B i => i.(succ_o A B) (e A B i) ;
    succ_e o := fun A B i => i.(succ_e A B) (o A B i)
 |}.

End EO.