AlgebraicDatatype.v

(** * Why are Algebraic Datatypes “Algebraic?” *)

(** Functional programming languages feature “algebraic” datatypes.

    #<div id="generate-toc"></div># *)

(** ** [(Type, sum, prod)] forms a Ring  *)

(** *** [Type] Equivalence *)

Inductive type_equiv (α β : Type) : Prop :=
| mk_type_equiv (f : α -> β) (g : β -> α)
               (equ1 : forall (x : α), x = g (f x))
               (equ2 : forall (x : β), x = f (g x))
  : type_equiv α β.

Arguments mk_type_equiv [α β].

Infix "==" := type_equiv (at level 72).
Infix ">>>" := (fun f g x => g (f x)) (at level 70).

From Coq Require Import Setoid Equivalence Morphisms.

Lemma type_equiv_refl {α} : α == α.

Proof.
  now apply (mk_type_equiv (@id α) (@id α)).
Qed.

Lemma type_equiv_sym {α β} (equ : α == β) : β == α.

Proof.
  destruct equ.
  apply (mk_type_equiv g f equ2 equ1).
Qed.

Lemma type_equiv_trans {α β γ} (equ1 : α == β) (equ2 : β == γ)
  : α == γ.

Proof.
  destruct equ1, equ2.
  apply (mk_type_equiv (f >>> f0) (g0 >>> g)).
  + intros x.
    rewrite <- equ2.
    rewrite <- equ1.
    reflexivity.
  + intros x.
    rewrite <- equ0.
    rewrite <- equ3.
    reflexivity.
Qed.

#[refine]
Instance type_equiv_Equivalence : Equivalence type_equiv :=
  {}.

Proof.
  + intros x.
    apply type_equiv_refl.
  + intros x y.
    apply type_equiv_sym.
  + intros x y z.
    apply type_equiv_trans.
Qed.

(** *** [Type] is an Abelian Group under [sum] *)

Instance sum_Proper
  : Proper (type_equiv ==> type_equiv ==> type_equiv) sum.

Proof.
  add_morphism_tactic.
  intros α α' equ1 β β' equ2.
  destruct equ1, equ2.
  apply (mk_type_equiv (fun x => match x with
                                | inl x => inl (f x)
                                | inr x => inr (f0 x)
                                end)
                      (fun x => match x with
                                | inl x => inl (g x)
                                | inr x => inr (g0 x)
                                end)).
  + intros [x|y]; cbn.
    ++ rewrite <- equ1; auto.
    ++ rewrite <- equ2; auto.
  + intros [x|y]; cbn.
    ++ rewrite <- equ0; auto.
    ++ rewrite <- equ3; auto.
Qed.

Definition sum_invert {α β} (x : α + β) : β + α :=
  match x with
  | inl x => inr x
  | inr x => inl x
  end.

Lemma sum_com {α β} : α + β == β + α.

Proof.
  apply (mk_type_equiv sum_invert sum_invert);
    intros [x|x]; reflexivity.
Qed.

(** *** [Type] is a Monoid under [prod] *)

Instance prod_Proper
  : Proper (type_equiv ==> type_equiv ==> type_equiv) prod.

Proof.
  add_morphism_tactic.
  intros α α' equ1 β β' equ2.
  destruct equ1, equ2.
  apply (mk_type_equiv (fun x => (f (fst x), f0 (snd x)))
                      (fun x => (g (fst x), g0 (snd x)))).
  + intros [x y]; cbn.
    rewrite <- equ1.
    rewrite <- equ2.
    reflexivity.
  + intros [x y]; cbn.
    rewrite <- equ0.
    rewrite <- equ3.
    reflexivity.
Qed.


Inductive Empty := .

Notation "∅" := Empty.

Definition from_empty (α : Type) (x : ∅) : α :=
  match x with end.

Definition unwrap_left_or {α β} (f : β -> α) (x : α + β)
  : α :=
  match x with
  | inl x => x
  | inr x => f x
  end.

Lemma sum_neutral (α : Type) : α == α + ∅.

Proof.
  apply (mk_type_equiv inl
                      (unwrap_left_or (from_empty α)));
    auto.
  intros [x|x]; auto.
  destruct x.
Qed.

Definition prod_invert {α β} (x : α * β) : β * α :=
  (snd x, fst x).

Lemma prod_com {α β} : α * β == β * α.

Proof.
  apply (mk_type_equiv prod_invert prod_invert);
    intros [x y]; reflexivity.
Qed.

Lemma prod_neutral (α : Type) : α * unit == α.

Proof.
  apply (mk_type_equiv fst (fun x => (x, tt))).
  + intros [x []]; reflexivity.
  + intros x; reflexivity.
Qed.

Lemma prod_annihilate (α : Type) : α * ∅ == ∅.

Proof.
  apply (mk_type_equiv (snd >>> from_empty ∅)
                      (from_empty (α * ∅))).
  + intros [_ []].
  + intros [].
Qed.

Lemma prod_sum_distr (α β γ : Type)
  : α * (β + γ) == α * β + α * γ.

Proof.
  apply (mk_type_equiv (fun x => match x with
                                | (x, inr y) => inr (x, y)
                                | (x, inl y) => inl (x, y)
                                end)
                      (fun x => match x with
                                | inr (x, y) => (x, inr y)
                                | inl (x, y) => (x, inl y)
                                end)).
  + intros [x [y | y]]; auto.
  + intros [[x y] | [x y]]; auto.
Qed.

(** ** Reasoning with Types *)

(** *** [list] Canonical Form *)

From Coq Require Import List.
Import ListNotations.

Lemma list_equiv (α : Type)
  : list α == unit + α * list α.

Proof.
  apply (mk_type_equiv (fun x => match x with
                                | [] => inl tt
                                | x :: rst => inr (x, rst)
                                end)
                      (fun x => match x with
                                | inl _ => []
                                | inr (x, rst) => x :: rst
                                end)).
  + intros [| x rst]; reflexivity.
  + intros [[] | [x rst]]; reflexivity.
Qed.

(** *** Automatic Folding Functions *)

Ltac fold_args b a r :=
  lazymatch a with
  | unit =>
    exact r
  | b =>
    exact (r -> r)
  | (?c + ?d)%type =>
    exact (ltac:(fold_args b c r) * ltac:(fold_args b d r))%type
  | (b * ?c)%type =>
    exact (r -> ltac:(fold_args b c r))
  | (?c * ?d)%type =>
    exact (c -> ltac:(fold_args b d r))
  | ?a =>
    exact (a -> r)
  end.

Ltac currying a :=
  match a with
  | ?a * ?b -> ?c => exact (a -> ltac:(currying (b -> c)))
  | ?a => exact a
  end.

(** We introduce [fold_type INPUT CANON_FORM OUTPUT], a tactic to compute the
    type of the fold function of the type <<INPUT>>, whose canonical form (in
    terms of [prod] and [sum]) is <<CANON_FORM>>. The result type of the fold
    function is <<OUTPUT>>. *)

Ltac fold_type b a r :=
  exact (ltac:(currying (ltac:(fold_args b a r) -> r))).

Definition fold_list_type (α β : Type) : Type :=
  ltac:(fold_type (list α) (unit + α * list α)%type β).

(** Here is the definition of [fold_list_type], as outputed by [Print
    foldl_list_type].

<<
fold_list_type = fun α β : Type => β -> (α -> β -> β) -> β
     : Type -> Type -> Type
>> *)

(** *** Equivalent Datatypes *)

(** The existence of the empty list complexifies the implementation of “simple”
    functions such as [head]. We can introduce a variant of [list] which does
    not suffer the same issue, by modifying the [nil] constructor so that it
    expects one argument. *)

Inductive non_empty_list (α : Type) :=
| ne_cons : α -> non_empty_list α -> non_empty_list α
| ne_singleton : α -> non_empty_list α.

Arguments ne_cons [α].
Arguments ne_singleton [α].

Definition ne_head {α} (l : non_empty_list α) : α :=
  match l with
  | ne_singleton x => x
  | ne_cons x _ => x
  end.

(** The canonical form of [non_empty_list] is very similar to [list]’s. The only
    difference is we that Similarly to [list], we can replace [unit] by [α]. *)

Lemma ne_list_equiv (α : Type)
  : non_empty_list α == α + (α * non_empty_list α).

Proof.
  apply (mk_type_equiv
           (fun x => match x with
                     | ne_cons x rst => inr (x, rst)
                     | ne_singleton x => inl x
                     end)
           (fun x => match x with
                     | inr (x, rst) => ne_cons x rst
                     | inl x => ne_singleton x
                     end)).
  + intros [x rst | x]; reflexivity.
  + intros [x | [x rst]]; reflexivity.
Qed.

(** But we can also demonstrate the relation between [list] and
    [non_empty_list], which reveals an alternative implemantion of
    [non_empty_list].  More precisely, we can prove that [forall (α : Type),
    non_empty_list α == α * list α]. *)

(* begin details : Auxiliary functions *)
Fixpoint non_empty_list_of_list {α} (x : α) (l : list α)
  : non_empty_list α :=
  match l with
  | y :: rst => ne_cons x (non_empty_list_of_list y rst)
  | [] => ne_singleton x
  end.

#[local]
Fixpoint list_of_non_empty_list {α} (l : non_empty_list α)
  : list α :=
  match l with
  | ne_cons x rst => x :: list_of_non_empty_list rst
  | ne_singleton x => [x]
  end.

Fixpoint prod_list_of_non_empty_list {α} (l : non_empty_list α)
  : α * list α :=
  match l with
  | ne_singleton x => (x, [])
  | ne_cons x rst => (x, list_of_non_empty_list rst)
  end.
(* end details *)

Lemma ne_list_list_equiv (α : Type)
  : non_empty_list α == α * list α.

Proof.
  apply (mk_type_equiv
           prod_list_of_non_empty_list
           (fun x => non_empty_list_of_list (fst x) (snd x))).
  + intros [x rst|x]; auto.
    cbn.
    revert x.
    induction rst; intros x; auto.
    cbn; now rewrite IHrst.
  + intros [x rst].
    cbn.
    destruct rst; auto.
    change (non_empty_list_of_list x (α0 :: rst))
      with (ne_cons x (non_empty_list_of_list α0 rst)).
    replace (α0 :: rst)
      with (list_of_non_empty_list
              (non_empty_list_of_list α0 rst)); auto.
    revert α0.
    induction rst; intros y; [ reflexivity | cbn ].
    now rewrite IHrst.
Qed.

(** So, yeah. datatypes are “algebraic.” *)