Approximating inductive types

ApproxNat.v

Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.Morphisms.

Fail Inductive X : Type := BAD : (X -> X) -> X.

Definition natF (T : Type) : Type :=
  T + unit.

(* We define approximation using a fixpoint which computes a Type
 * by repeatedly applying a function. The base case is the empty set.
 *)
Fixpoint approx (F : Type -> Type) (n : nat) : Type :=
  match n with
  | 0 => Empty_set
  | S n => F (approx F n)
  end.

Record Mu (F : Type -> Type) := mkMu
{ depth : nat
; value : approx F depth }.
Arguments depth {_} _.
Arguments value {_} _.
Arguments mkMu {_} _ _.

(* Using the approximation, natural numbers can be written by pairing
 * the depth of the approximation and a value of the approximation.
 *)
Definition Nat := Mu natF.
Definition mkNat := @mkMu natF.

Definition NatO : Nat := @mkNat 1 (inr tt).
Definition NatS (n : Nat) : Nat :=
  mkNat (S n.(depth)) (inl n.(value)).
(* It is important to note that the [S] in the depth is
 * *not* the successor. We need one extra level of approximation
 * in order to represent numbers that are 1 larger.
 *)

(* Inductive types are isomorphic to their unfoldings, i.e.
 *   natF Nat ~ Nat
 * We represent this with two functions:
 * - into : natF Nat -> Nat
 * - outof : Nat -> natF Nat
 *)

(* [into] is straightforward *)
Definition into (n : natF Nat) : Nat :=
  match n with
  | inl n' => NatS n'
  | inr tt => NatO
  end.

(* [outof] is a bit more complex. We are going to use the
 * Functorial nature of [natF] to "close" the recursive
 * occurances of our values converting them from [approx natF n]
 * to [Nat].
 *)
Class Functor (F : Type -> Type) : Type :=
{ fmap : forall {T U}, (T -> U) -> F T -> F U }.

Instance Functor_natF : Functor natF :=
{ fmap := fun _T _U f x =>
            match x with
            | inl x => inl (f x)
            | inr x => inr x
            end }.


Definition outof (n : Nat) : natF Nat :=
  match n.(depth) as a return approx natF a -> natF Nat with
  | 0 => fun x : Empty_set => match x with end
  | S a' => fun x : natF (approx natF a') =>
    (* This packs up the recursive instances *)
    fmap (fun n : approx natF a' => mkNat a' n) x
  end n.(value).

(* It is easy to prove part of the isomorphism. *)
Theorem outof_into : forall (n : natF Nat),
  outof (into n) = n.
Proof.
  destruct n; simpl.
  { destruct n; reflexivity. }
  { destruct u. reflexivity. }
Qed.

(* However, going the other way is unprovable.
 * The reason is that, with our representation,
 * there are multiple representations of a single number.
 * For example, 0 can be represented as [existT (S n) (inr tt)]
 * for *any* [n].
 *)
Theorem into_outof : forall (n : Nat),
  into (outof n) = n.
Proof.
  destruct n.
  simpl. destruct depth0.
  { elimtype Empty_set. assumption. }
  { destruct value0.
    { reflexivity. }
    { simpl. destruct u.
      (* Unprovable! *)
Abort.

(* In order to solve this problem, we need to define a
 * more permissive equivalence relation for [Nat].
 *)

Section approx_equiv.
  (* We can define this generically for an approximation of any
   * type function [F] by constructing a relation recursively
   * given the approximation levels.
   *)
  Variable F : Type -> Type.

  (* The central piece is the following 2nd order, heterogeneous relation.
   * [RF] takes a relation (r) between two types [T] and [U] and returns a
   * relation between [F T] and [F U]. Note that [r] is the relation used
   * to compare recursive instances of the structure.
   *)
  Variable RF : forall T U, (T -> U -> Prop) -> F T -> F U -> Prop.
  (* Using this, we can construct a approximation for the relation
   * from [RF]. Note that the only case that matters is the one where
   * there are levels of the approximation remaining since in all other
   * instances we can derive a contradiction.
   *)
  Fixpoint approx_Eq {n m} {struct n} : approx F n -> approx F m -> Prop :=
    match n as n , m as m return approx F n -> approx F m -> Prop with
    | 0 , 0 => fun a b : Empty_set => match a with end
    | 0 , S m' => fun (a : Empty_set) _ => match a with end
    | S n' , 0 => fun _ (b : Empty_set) => match b with end
    | S n' , S m' => @RF _ _ (@approx_Eq n' m')
    end.

  (* The next three definitions prove that [approx_Eq] inherits the
   * Reflexive, Symmetric, and Transitive nature of [RF]. The defintions
   * are slightly longer than usual since we need to define the
   * 2nd order analogs to each of the properties.
   *
   * NOTE: These properties are all homogeneous since the properties are
   * only meaningful for homogeneous relations.
   *)
  Theorem Refl_approx_Eq {n}
          {Rrf : forall T (R: T -> T -> Prop), Reflexive R ->
                                               Reflexive (@RF T T R)}
  : Reflexive (@approx_Eq n n).
  Proof.
    red. induction n.
    { destruct x. }
    { simpl. intros.
      eapply Rrf. red. intros. eapply IHn. }
  Qed.

  Theorem Sym_approx_Eq {n}
          {Srf : forall T (R: T -> T -> Prop), Symmetric R ->
                                               Symmetric (@RF T T R)}
  : Symmetric (@approx_Eq n n).
  Proof.
    induction n; eauto.
    { red. destruct x. }
  Qed.

  Theorem Trans_approx_Eq {n}
          {Trf : forall T (R: T -> T -> Prop), Transitive R ->
                                               Transitive (@RF T T R)}
  : Transitive (@approx_Eq n n).
  Proof.
    induction n; eauto.
  Qed.

End approx_equiv.

Arguments approx_Eq {F} RF {n m} _ _ : rename.

(* Now we can define the equivalence relation for [natF].
 *)
Section natF_eq.
  Variables T U : Type.
  Variable RTU : T -> U -> Prop.

  Inductive NatF_eq : natF T -> natF U -> Prop :=
  | Oinr : NatF_eq (inr tt) (inr tt)
  | Oinl : forall a b, RTU a b -> NatF_eq (inl a) (inl b).
End natF_eq.

(* and we can use it to prove that equal numbers are equal. *)
Goal approx_Eq NatF_eq (NatS NatO).(value) (NatS NatO).(value).
Proof.
  compute. constructor. constructor.
Qed.

(* Note that the relation is agnostic to the level of the approximation. *)
Goal approx_Eq NatF_eq
     (inl (inr tt) : approx natF 10)
     (inl (inr tt) : approx natF 100).
Proof.
  constructor. constructor.
Qed.

(* We can define [Nat_eq] to simply unpack the approximations. *)
Definition Nat_eq (a b : Nat) : Prop :=
  approx_Eq NatF_eq a.(value) b.(value).

Lemma Refl_NatF_eq : forall (T : Type) (R : T -> T -> Prop),
   Reflexive R -> Reflexive (NatF_eq T T R).
Proof.
  red. destruct x; try constructor; eauto.
  destruct u. constructor.
Qed.

(* Using [Nat_eq], we can prove that [into] and [outof] form
 * an isomorphism.
 *)
Theorem Nat_eq_outof_into : forall (n : natF Nat),
  NatF_eq _ _ Nat_eq (outof (into n)) n.
Proof.
  destruct n; simpl.
  { constructor. unfold Nat_eq.
    simpl. eapply Refl_approx_Eq.
    clear. intros.
    red. destruct x.
    - constructor. apply H.
    - destruct u. constructor. }
  { destruct u. simpl. constructor. }
Qed.

Theorem Nat_eq_into_outof : forall (n : Nat),
  Nat_eq (into (outof n)) n.
Proof.
  destruct n.
  simpl. destruct depth0.
  { elimtype Empty_set. assumption. }
  { destruct value0.
    { simpl. unfold NatS. simpl.
      unfold Nat_eq. apply Refl_approx_Eq. eapply Refl_NatF_eq. }
    { simpl. destruct u.
      red. simpl.
      unfold approx_Eq. simpl.
      constructor. } }
Qed.

(** "Pattern Matching" **)
(* Non-dependent Pattern matching comes directly from the implementation of
 * 'outof'
 *)
Definition match_nat (n : Nat) (retT : Type)
           (case_zero : retT)
           (case_S : Nat -> retT)
: retT :=
  match outof n with
  | inl n => case_S n
  | inr tt => case_zero
  end.

(* To define recursion, we build our recursion on the approximation depth.
 * The non-dependent version is not too tricky. The implementation is
 * parametric in the underlying type function defining the inductive type
 * *as long as it is a Functor*
 *)
Section approx.
  Variable F : Type -> Type.
  Context {FunctorF : Functor F}.
  Variable Ret : Type.

  Variable f : F Ret -> Ret.

  Fixpoint approx_rec (n : nat) : approx F n -> Ret :=
    match n as n return approx F n -> Ret with
    | 0 => fun x : Empty_set => match x with end
    | S n => fun x : F (approx F n) =>
               f (fmap (F:=F) (approx_rec n) x)
    end.
End approx.

(* We can instantiate the definition for natural numbers with a simple
 * function.
 *)
Definition Nat_rec {T} (f : natF T -> T) (n : Nat) : T :=
  approx_rec natF T f n.(depth) n.(value).

(* We can also easily define the recursion that does the pattern match for us
 *)
Definition Nat_rec' {T} (case0 : T) (caseS : T -> T) (n : Nat) : T :=
  approx_rec natF T (fun x => match x with
                              | inl x => caseS x
                              | inr _ => case0
                              end) n.(depth) n.(value).

(* Defining functions *)
Definition Nat_plus (a b : Nat) : Nat :=
  Nat_rec (fun x => match x with
                    | inl x => NatS x
                    | inr tt => b
                    end) a.

(* ...and computing with them works in the usual way. *)
Eval compute in Nat_plus NatO (NatS (NatS NatO)).

(** Dependent Pattern Matching and Folds **)

(* The key to doing dependent pattern matching is to ensure that the return
 * type does not depend on the depth of the approximation. We'll just focus
 * on the specialization to natural numbers for now.
 *)
Section dep_match_Nat.
  Variable ResT : Nat -> Type.
  Variable Proper_ResT : forall a b,
      Nat_eq a b ->
      (ResT a -> ResT b) * (ResT b -> ResT a).

  Local Definition Nat_eq_zero : forall n m a b,
      Nat_eq (mkNat (S n) (inr a)) (mkNat (S m) (inr b)).
  Proof.
    unfold Nat_eq. simpl.
    intros. destruct a; destruct b; constructor.
  Defined.

  Variable case_zero : ResT NatO.
  Variable case_S    : forall n : Nat, ResT (NatS n).

  Definition case_natF_dep (d : nat)
  : forall v : approx natF d, ResT (mkNat d v) :=
    match d as d
          return forall x : approx natF d, ResT (mkNat d x)
    with
    | 0 => fun x : Empty_set => match x with end
    | S n => fun x : natF (approx natF n) =>
               match x with
               | inl x => case_S (mkNat n x)
               | inr _ =>
                 fst (Proper_ResT _ _ (Nat_eq_zero _ _ _ _)) case_zero
               end
    end.

  Definition case_Nat_dep (n : Nat) : ResT n :=
    match n as v return ResT v with
    | mkMu d v => case_natF_dep d v
    end.
End dep_match_Nat.

(* We can generalize the pattern match to a fold using a fixpoint *)
Section dep_fold_Nat.
  Variable ResT : Nat -> Type.
  Variable Proper_ResT : forall a b,
      Nat_eq a b ->
      (ResT a -> ResT b) * (ResT b -> ResT a).
  Variable case_zero : ResT NatO.
  Variable case_S : forall n : Nat, ResT n -> ResT (NatS n).

  Fixpoint approx_natF_rec_dep (d : nat)
  : forall v : approx natF d, ResT (mkNat d v) :=
    match d as d
          return forall v : approx natF d, ResT (mkNat d v)
    with
    | 0 => fun v : Empty_set => match v with end
    | S d => fun v : natF (approx natF d) =>
               match v with
               | inl v' => case_S (mkNat d v') (approx_natF_rec_dep d v')
               | inr _ =>
                 fst (Proper_ResT _ _ (Nat_eq_zero _ _ _ _)) case_zero
               end
    end.

  Definition Nat_rec_dep (v : Nat) : ResT v :=
    match v as v return ResT v with
    | mkMu d v => approx_natF_rec_dep d v
    end.
End dep_fold_Nat.