{{ message }}

Instantly share code, notes, and snippets.

lthms/AlgebraicDatatype.v Secret

Last active Jun 29, 2020
 (** * Why are Algebraic Datatypes “Algebraic?” *) (** Functional programming languages feature “algebraic” datatypes. #
# *) (** ** [(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 <>, whose canonical form (in terms of [prod] and [sum]) is <>. The result type of the fold function is <>. *) 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.” *)