Skip to content

Instantly share code, notes, and snippets.

@lthms

lthms/AlgebraicDatatype.v Secret

Last active Jun 29, 2020
Embed
What would you like to do?
(** * 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.” *)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.