Benedikt Ahrens and Régis Spadotti— Terminal semantics for codata types in intensional Martin-Löf type theory
Table of contents
Index
Require Import Category.Setoids.
Require Import Category.Types.
Require Import Category.Types_Setoids.
Require Import Category.RComod.
Require Import Category.RComonad.
Require Import Category.Stream.Category.
Require Import Category.Stream.Axioms.
Require Import Theory.Category.
Require Import Theory.InitialTerminal.
Require Import Theory.Functor.
Require Import Theory.RelativeComonad.
Require Import Theory.Comodule.
Require Import Theory.Product.
Require Import Theory.PrecompositionWithProduct.
Require Import Theory.PushforwardComodule.

Generalizable All Variables.

Stream is terminal in Streams

Module StreamTerminal (Import Ax : StreamAxioms).

-∼- is an equivalence relation

  Lemma bisim_refl : ∀ {A} {s : Stream A}, s ∼ s.
  Show proof.
    intros. apply bisim_intro with (R ≔ λ s₁ s₂ ∙ s₁ = s₂); [clean_hyps; intros..|auto].
    - subst; reflexivity.
    - subst; reflexivity.

  Lemma bisim_sym : ∀ {A} {s₁ s₂ : Stream A}, s₁ ∼ s₂ → s₂ ∼ s₁.
  Show proof.
    intros.
    apply bisim_intro with (R ≔ λ s₁ s₂ ∙ s₂ ∼ s₁); [clean_hyps; intros..|auto].
    - symmetry; now apply bisim_head.
    - now apply bisim_tail.

  Lemma bisim_trans : ∀ {A} {s₁ s₂ s₃ : Stream A}, s₁ ∼ s₂ → s₂ ∼ s₃ → s₁ ∼ s₃.
  Show proof.
    intros.
    apply bisim_intro with (R ≔ λ s₁ s₃ ∙ ∃ s₂, s₁ ∼ s₂ ∧ s₂ ∼ s₃);
    [clean_hyps; intros.. | eauto].
    - destruct H as (? & ? & ?).
      etransitivity. eapply bisim_head; eauto.
      now apply bisim_head.
    - destruct H as (? & ? & ?).
      eexists; split; eapply bisim_tail; eauto.

  Instance bisim_equiv : ∀ {A}, Equivalence (@bisim A).
  Show proof.
    constructor; repeat intro.
    - now apply bisim_refl.
    - now apply bisim_sym.
    - eapply bisim_trans; eauto.

  Lemma eq_bisim : ∀ {A} {s₁ s₂ : Stream A}, s₁ = s₂ → s₁ ∼ s₂.
  Show proof.
    intros. now rewrite H.

Stream as a setoid

  Program Definition STREAM (A : Type) : Setoids.Obj ≔
    Setoids.make ⦃ Carrier ≔ Stream A ; Equiv ≔ bisim ⦄.

head & tail are setoids morphisms

  Lemma head_cong : ∀ {A} {s₁ s₂ : Stream A}, s₁ ∼ s₂ → head s₁ = head s₂.
  Show proof.
    intros A s₁ s₂ eq_s₁s₂. now apply bisim_head.

  Lemma tail_cong : ∀ {A} {s₁ s₂ : Stream A}, s₁ ∼ s₂ → tail s₁ ∼ tail s₂.
  Show proof.
    intros A s₁ s₂ eq_s₁s₂. now apply bisim_tail.

  Program Definition 𝒉𝒆𝒂𝒅 {A} : STREAM A ⇒ 𝑬𝑸 A ≔ Setoids.Morphism.make head.
head-cong
  Show proof.
    now apply head_cong.

  Program Definition 𝒕𝒂𝒊𝒍 {A} : STREAM A ⇒ STREAM A ≔ Setoids.Morphism.make tail.
tail-cong
  Show proof.
    now apply tail_cong.

Cosubstitution for streams

  Definition cosubst {A B : 𝑻𝒚𝒑𝒆} (f : Stream A ⇒ B) : Stream A ⇒ Stream B ≔
    corec f tail.

Stream is a relative comonad over EQ

  Obligation Tactic ≔ idtac.
  Program Definition 𝑺𝒕𝒓 : ‵ 𝑹𝑪𝒐𝒎𝒐𝒏𝒂𝒅 𝑬𝑸 ′ ≔
    RelativeComonad.make⦃ T≔ STREAM
    ; counit≔ λ X ∙ 𝒉𝒆𝒂𝒅
    ; cobind≔ λ X Y ∙ λ f ↦ Setoids.Morphism.make (cosubst f) ⦄.
cosubst-cong
  Show proof.
    intros.
    apply bisim_intro with (λ s₁ s₂ ∙ ∃ x y, x ∼ y ∧ s₁ = cosubst f x ∧ s₂ = cosubst f y)
    ; [clean_hyps; intros..|eauto].
    - destruct H as (x & y & eq_xy & → & ->).
      unfold cosubst. repeat rewrite head_corec.
      now rewrite eq_xy.
    - destruct H as (x & y & eq_xy & → & ->).
      ∃ (tail x). ∃ (tail y).
      split; [|split].
      + now apply bisim_tail.
      + unfold cosubst at 1. rewrite tail_corec. reflexivity.
      + unfold cosubst at 1. rewrite tail_corec. reflexivity.
cosubst-cong₂
  Show proof.
    intros X Y f g eq_fg x y eq_xy. simpl.
    apply bisim_intro with (λ s₁ s₂ ∙ ∃ x y, x ∼ y ∧ s₁ = cosubst f x ∧ s₂ = cosubst g y); [intros..|eauto].
    - destruct H as (x' & y' & eq_xy' & → & ->).
      unfold cosubst; repeat rewrite head_corec.
      etransitivity. eapply (Setoids.cong f). apply eq_xy'.
      now apply eq_fg.
    - destruct H as (x' & y' & eq_xy' & → & ->).
      ∃ (tail x'). ∃ (tail y').
      split; [|split].
      + now apply bisim_tail.
      + unfold cosubst at 1. rewrite tail_corec. reflexivity.
      + unfold cosubst at 1. rewrite tail_corec. reflexivity.
cobind-counit
  Show proof.
    simpl. intros.
    apply bisim_intro with (λ s₁ s₂ ∙ ∃ x y, x ∼ y ∧ s₁ = cosubst head x ∧ s₂ = y); [clean_hyps; intros..|eauto].
    - destruct H as (x & y & eq_xy & → & ->).
      unfold cosubst; rewrite head_corec; now apply head_cong.
    - destruct H as (x & y & eq_xy & → & ->).
      ∃ (tail x). ∃ (tail y).
      split; [|split].
      + now apply bisim_tail.
      + unfold cosubst at 1. rewrite tail_corec. reflexivity.
      + reflexivity.
counit-cobind
  Show proof.
    repeat intro. rewrite H. simpl. unfold cosubst. now rewrite head_corec.
cobind-cobind
  Show proof.
    intros X Y Z f g x y eq_xy. rewrite <- eq_xy. clear y eq_xy. simpl.
    apply bisim_intro with (λ s₁ s₂ ∙ ∃ x, s₁ = cosubst g (cosubst f x) ∧ s₂ = cosubst (λ y ∙ g (cosubst f y)) x);
    [clean_hyps; intros..|eauto].
    - destruct H as (x & → & ->).
      unfold cosubst. repeat rewrite head_corec. reflexivity.
    - destruct H as (x & → & ->).
      ∃ (tail x). split.
      + unfold cosubst. now do 2 rewrite tail_corec.
      + unfold cosubst. now rewrite tail_corec.

Stream coalgebra

  Program Definition 𝑻𝒂𝒊𝒍 : ‵ [𝑺𝒕𝒓] ⇒ [𝑺𝒕𝒓] ′ ≔
    Comodule.make ⦃ α ≔ λ A ∙ Setoids.Morphism.make 𝒕𝒂𝒊𝒍 ⦄.
tail-cong
  Show proof.
    intros A x y eq_xy; now rewrite eq_xy.
α-commutes
  Show proof.
    intros C D f x y eq_xy. rewrite eq_xy. apply eq_bisim. simpl. unfold cosubst. now rewrite tail_corec.

  Program Definition 𝑺𝑻𝑹 : ‵ 𝑺𝒕𝒓𝒆𝒂𝒎 ′ ≔
    Stream.make ⦃ T ≔ 𝑺𝒕𝒓 ; tail ≔ 𝑻𝒂𝒊𝒍 ⦄.

𝑺𝑻𝑹 is a terminal object

  Section Defs.

    Variable (Tr : 𝑺𝒕𝒓𝒆𝒂𝒎).

    Notation T≔ (Stream.T Tr).
    Notation "'T⋅tail'"≔ (Stream.tail Tr _).
    Notation "'T⋅tail[' A ]"≔ (Stream.tail Tr A) (only parsing).
    Notation STR≔ (Stream.T 𝑺𝑻𝑹).
    Notation "'STR⋅tail'"≔ (Stream.tail 𝑺𝑻𝑹 _).
    Notation "'STR⋅tail[' A ]"≔ (Stream.tail 𝑺𝑻𝑹 A) (only parsing).

    Local Notation "a ∼ b" ≔ (SEquiv a b).

    Definition tau {A} : T A → STR A ≔ corec T⋅counit T⋅tail.

    Lemma head_tau : ∀ A (t : T A), STR⋅counit (tau t) = T⋅counit t.
    Show proof.
      intros. unfold tau. simpl. now rewrite head_corec.

    Lemma tail_tau : ∀ A (t : T A), STR⋅tail (tau t) = tau (T⋅tail t).
    Show proof.
      intros. unfold tau. simpl. now rewrite tail_corec.

    Lemma tau_cong : ∀ A (x y : T A), x ∼ y → tau x ∼ tau y.
    Show proof.
      intros.
      apply bisim_intro with (λ s₁ s₂ ∙ ∃ x y, x ∼ y ∧ s₁ = tau x ∧ s₂ = tau y);
      [clean_hyps; intros..|eauto].
      - destruct H as (x & y & eq_xy & → & ->).
        unfold tau. repeat rewrite head_corec. now rewrite eq_xy.
      - destruct H as (x & y & eq_xy & → & ->).
        ∃ (T⋅tail x). ∃ (T⋅tail y). split; [|split].
        + now rewrite eq_xy.
        + unfold tau. now rewrite tail_corec.
        + unfold tau. now rewrite tail_corec.

    Program Definition Tau {A} : T A ⇒ STR A ≔
      Setoids.Morphism.make tau.
tau-cong
    Show proof.
      intros. now apply tau_cong.

    Lemma tau_counit : ∀ A (t t' : T A), t ∼ t' → T⋅counit t ∼ STR⋅counit (tau t').
    Show proof.
      intros A t t' eq_tt'. rewrite eq_tt'. simpl. unfold tau. now rewrite head_corec.

    Lemma tau_cobind : ∀ A B (f : STR A ⇒ 𝑬𝑸 B) x y, x ∼ y → Tau (T⋅cobind (f ∘ Tau) x) ∼ STR⋅cobind f (Tau y).
    Show proof.
      intros A B f x y eq_xy. rewrite <- eq_xy. clear y eq_xy.
      apply bisim_intro with (λ s₁ s₂ ∙ ∃ x, s₁ ∼ Tau (T⋅cobind (f ∘ Tau) x) ∧ s₂ ∼ STR⋅cobind f (Tau x));
      [clean_hyps;intros..|eauto].
      - destruct H as (x & ? & ?).
        etransitivity. eapply head_cong. apply H.
        symmetry; etransitivity. eapply head_cong; apply H0.
        simpl. unfold tau, cosubst. repeat rewrite head_corec.
        symmetry. etransitivity. apply (counit_cobind T). reflexivity.
        reflexivity.
      - destruct H as (x & ? & ?).
        ∃ (T⋅tail x). split.
        etransitivity. eapply tail_cong. apply H.
        simpl. unfold tau. repeat rewrite tail_corec.
        apply tau_cong. etransitivity. apply (α_commutes (Stream.tail Tr)). reflexivity.
        simpl. reflexivity.
        etransitivity. eapply tail_cong. apply H0.
        simpl. unfold tau, cosubst. repeat rewrite tail_corec. reflexivity.
      - ∃ x; split; reflexivity.

  End Defs.

◯ is a morphism of triangles
  Program Definition ◯ (T : 𝑺𝒕𝒓𝒆𝒂𝒎) : T ⇒ 𝑺𝑻𝑹 ≔
    Stream.make ⦃ τ ≔ RelativeComonad.make ⦃ τ ≔ λ A ∙ Tau T ⦄ ⦄.
τ-counit
  Show proof.
    repeat intro. now apply tau_counit.
τ-cobind
  Show proof.
    repeat intro. now apply tau_cobind.
τ-commutes
  Show proof.
    repeat intro. rewrite H. simpl. unfold tau. repeat rewrite tail_corec. reflexivity.

𝑺𝑻𝑹 is a terminal object
  Program Definition Terminality : Terminal 𝑺𝒕𝒓𝒆𝒂𝒎 ≔
    Terminal.make⦃ one≔ 𝑺𝑻𝑹
    ; top≔ ◯ ⦄.
top-unique
  Show proof.
    intros A f X x y eq_xy. rewrite <- eq_xy. clear y eq_xy. simpl.
    apply bisim_intro with (λ s₁ s₂ ∙ ∃ x, s₁ ∼ ⟨f⟩ _ x ∧ s₂ ∼ tau A x); [clean_hyps; intros..|].
    - destruct H as (? & ? & ?).
      etransitivity. eapply head_cong. apply H.
      symmetry; etransitivity. eapply head_cong. apply H0.
      unfold tau. rewrite head_corec. symmetry. etransitivity. symmetry. apply (◯_counit (Stream.τ f)).
      reflexivity. reflexivity.
    - destruct H as (? & ? & ?).
      ∃ (Stream.tail A _ x). split.
      + etransitivity. eapply tail_cong. apply H.
        etransitivity. symmetry. eapply (Stream.τ_commutes f). reflexivity.
        reflexivity.
      + etransitivity. eapply tail_cong. apply H0.
        unfold tau. rewrite tail_corec. reflexivity.
    - ∃ x. split; reflexivity.

End StreamTerminal.
Benedikt Ahrens and Régis Spadotti— Terminal semantics for codata types in intensional Martin-Löf type theory
Table of contents
Index