text:
From iris.base_logic.lib Require Export invariants.
From iris.algebra Require Import gset coPset.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.

(* Non-atomic ("thread-local") invariants. *)

Definition na_inv_pool_name := gname.

Class na_invG Σ :=
  na_inv_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
Definition na_invΣ : gFunctors :=
  #[ GFunctor (constRF (prodR coPset_disjR (gset_disjR positive))) ].
Instance subG_na_invG {Σ} : subG na_invΣ Σ → na_invG Σ.
Proof. solve_inG. Qed.

Section defs.
  Context `{invG Σ, na_invG Σ}.

  Definition na_own (p : na_inv_pool_name) (E : coPset) : iProp Σ :=
    own p (CoPset E, GSet ∅).

  Definition na_inv (p : na_inv_pool_name) (N : namespace) (P : iProp Σ) : iProp Σ :=
    (∃ i, ⌜i ∈ (↑N:coPset)⌝ ∧
          inv N (P ∗ own p (CoPset ∅, GSet {[i]}) ∨ na_own p {[i]}))%I.
End defs.

Instance: Params (@na_inv) 3.
Typeclasses Opaque na_own na_inv.

Section proofs.
  Context `{invG Σ, na_invG Σ}.

  Global Instance na_own_timeless p E : Timeless (na_own p E).
  Proof. rewrite /na_own; apply _. Qed.

  Global Instance na_inv_ne p N : NonExpansive (na_inv p N).
  Proof. rewrite /na_inv. solve_proper. Qed.
  Global Instance na_inv_proper p N : Proper ((≡) ==> (≡)) (na_inv p N).
  Proof. apply (ne_proper _). Qed.

  Global Instance na_inv_persistent p N P : Persistent (na_inv p N P).
  Proof. rewrite /na_inv; apply _. Qed.

  Lemma na_inv_iff p N P Q : ▷ □ (P ↔ Q) -∗ na_inv p N P -∗ na_inv p N Q.
  Proof.
    iIntros "#HPQ". rewrite /na_inv. iDestruct 1 as (i ?) "#Hinv".
    iExists i. iSplit; first done. iApply (inv_iff with "[] Hinv").
    iNext; iAlways.
    iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
  Qed.

  Lemma na_alloc : (|==> ∃ p, na_own p ⊤)%I.
  Proof. by apply own_alloc. Qed.

  Lemma na_own_disjoint p E1 E2 : na_own p E1 -∗ na_own p E2 -∗ ⌜E1 ## E2⌝.
  Proof.
    apply wand_intro_r.
    rewrite /na_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]).
  Qed.

  Lemma na_own_union p E1 E2 :
    E1 ## E2 → na_own p (E1 ∪ E2) ⊣⊢ na_own p E1 ∗ na_own p E2.
  Proof.
    intros ?. by rewrite /na_own -own_op pair_op left_id coPset_disj_union.
  Qed.

  Lemma na_own_acc E2 E1 tid :
    E2 ⊆ E1 → na_own tid E1 -∗ na_own tid E2 ∗ (na_own tid E2 -∗ na_own tid E1).
  Proof.
    intros HF. assert (E1 = E2 ∪ (E1 ∖ E2)) as -> by exact: union_difference_L.
    rewrite na_own_union; last by set_solver+. iIntros "[$ $]". auto.
  Qed.

  Lemma na_inv_alloc p E N P : ▷ P ={E}=∗ na_inv p N P.
  Proof.
    iIntros "HP".
    iMod (own_unit (prodUR coPset_disjUR (gset_disjUR positive)) p) as "Hempty".
    iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
    { apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
      apply (gset_disj_alloc_empty_updateP_strong' (λ i, i ∈ (↑N:coPset))).
      intros Ef. exists (coPpick (↑ N ∖ coPset.of_gset Ef)).
      rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
      apply coPpick_elem_of=> Hfin.
      eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
      apply of_gset_finite. }
    simpl. iDestruct "Hm" as %(<- & i & -> & ?).
    rewrite /na_inv.
    iMod (inv_alloc N with "[-]"); last (iModIntro; iExists i; eauto).
    iNext. iLeft. by iFrame.
  Qed.

  Lemma na_inv_open p E F N P :
    ↑N ⊆ E → ↑N ⊆ F →
    na_inv p N P -∗ na_own p F ={E}=∗ ▷ P ∗ na_own p (F∖↑N) ∗
                       (▷ P ∗ na_own p (F∖↑N) ={E}=∗ na_own p F).
  Proof.
    rewrite /na_inv. iIntros (??) "#Hnainv Htoks".
    iDestruct "Hnainv" as (i) "[% Hinv]".
    rewrite [F as X in na_own p X](union_difference_L (↑N) F) //.
    rewrite [X in (X ∪ _)](union_difference_L {[i]} (↑N)) ?na_own_union; [|set_solver..].
    iDestruct "Htoks" as "[[Htoki $] $]".
    iInv "Hinv" as "[[$ >Hdis]|>Htoki2]" "Hclose".
    - iMod ("Hclose" with "[Htoki]") as "_"; first auto.
      iIntros "!> [HP $]".
      iInv N as "[[_ >Hdis2]|>Hitok]".
      + iDestruct (own_valid_2 with "Hdis Hdis2") as %[_ Hval%gset_disj_valid_op].
        set_solver.
      + iSplitR "Hitok"; last by iFrame. eauto with iFrame.
    - iDestruct (na_own_disjoint with "Htoki Htoki2") as %?. set_solver.
  Qed.

  Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N.

  Global Instance into_acc_na p F E N P :
    IntoAcc (X:=unit) (na_inv p N P)
            (↑N ⊆ E ∧ ↑N ⊆ F) (na_own p F) (fupd E E) (fupd E E)
            (λ _, ▷ P ∗ na_own p (F∖↑N))%I (λ _, ▷ P ∗ na_own p (F∖↑N))%I
              (λ _, Some (na_own p F))%I.
  Proof.
    rewrite /IntoAcc /accessor. iIntros ((?&?)) "#Hinv Hown".
    rewrite exist_unit -assoc /=.
    iApply (na_inv_open with "Hinv"); done.
  Qed.
End proofs.

author: izgzhen

repo: iris-coq

save_path: github-repos/coq/izgzhen-iris-coq


Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Specific.solinas64_2e150m3_3limbs.Synthesis.

(* TODO : change this to field once field isomorphism happens *)
Definition carry :
  { carry : feBW_loose -> feBW_tight
  | forall a, phiBW_tight (carry a) = (phiBW_loose a) }.
Proof.
  Set Ltac Profiling.
  Time synthesize_carry ().
  Show Ltac Profile.
Time Defined.

Print Assumptions carry.


text:
Add LoadPath "../metatheory".
Require Export STLC_init.

Ltac gather_atoms ::=
  let A := gather_atoms_with (fun x : vars => x) in
  let B := gather_atoms_with (fun x : var => {{ x }}) in
  let C := gather_atoms_with (fun x : typing_env => dom x) in
  let D1 := gather_atoms_with (fun x => fv_term x) in
  constr:(A \u B \u C \u D1).

(** Mutual induction principles *)
Scheme pval_mut_ind_aux := Induction for pval Sort Prop
with   val_mut_ind_aux  := Induction for val  Sort Prop.
Combined Scheme pval_val_mut_ind from pval_mut_ind_aux, val_mut_ind_aux.

(** Administrative lemmas *)
Lemma var_subst : forall e x, subst_term e x (term_var_f x) = e.
Proof.
intros e x; simpl; destruct (x == x); congruence.
Qed.
Hint Rewrite var_subst : lngen.

Lemma pval_val_regular :
  (forall p, pval p → lc_term p) ∧ (forall v, val v → lc_term v).
Proof.
apply pval_val_mut_ind; eauto.
Qed.

Lemma pval_regular : forall p, pval p → lc_term p.
Proof.
intros; destruct pval_val_regular as [H1 _]; auto.
Qed.

Lemma val_regular : forall v, val v → lc_term v.
Proof.
intros; destruct pval_val_regular as [_ H2]; auto.
Qed.
Hint Resolve pval_regular val_regular.

Lemma red0_regular1 : forall e e', red0 e e' → lc_term e.
Proof.
intros e e' H. destruct H; auto.
Qed.

Lemma red0_regular2 : forall e e', red0 e e' → lc_term e'.
Proof.
intros e e' H; destruct H; eauto with lngen.
Qed.
Hint Resolve red0_regular1 red0_regular2.

Lemma red1_regular1 : forall e e', e ⇝ e' → lc_term e.
Proof.
intros e e' H. induction H; eauto.
Qed.

Lemma red1_regular2 : forall e e', e ⇝ e' → lc_term e'.
Proof.
intros e e' H; induction H; eauto.
Qed.
Hint Resolve red1_regular1 red1_regular2.

Lemma red_star_regular1 : forall e1 e2, e1 ⇝⋆ e2 →
  lc_term e2 → lc_term e1.
Proof.
intros e1 e2 H Hlc; induction H; eauto.
Qed.

Lemma red_star_regular2 : forall e1 e2, e1 ⇝⋆ e2 →
  lc_term e1 → lc_term e2.
Proof.
intros e1 e2 H Hlc; induction H; eauto.
Qed.
Hint Resolve red_star_regular1 red_star_regular2.

Lemma wfterm_regular : forall Γ e τ,
  wfterm Γ e τ → lc_term e.
Proof.
intros Γ e τ H; induction H; auto.
Qed.
Hint Resolve wfterm_regular.

Lemma wfterm_env_uniq : forall Γ e τ,
  wfterm Γ e τ → uniq Γ.
Proof.
intros Γ e τ H. induction H; auto.
pick fresh x. assert (uniq ([(x, t1)] ++ G)) as H1 by auto. inversion H1; auto.
Qed.
Hint Resolve wfterm_env_uniq.

(** Lemmas about values *)
Lemma value_is_normal_aux :
  (forall v, pval v → ~ exists e, v ⇝ e) ∧
  (forall v, val v → ~ exists e, v ⇝ e).
Proof.
apply pval_val_mut_ind; intros; intros [e0 Hred]; inversion Hred; subst; eauto.
inversion H.
inversion H1; subst. inversion p.
inversion H0.
pick fresh x. eapply H; eauto.
Qed.

Lemma value_is_normal : forall v, val v → ~ exists e, v ⇝ e.
Proof.
destruct value_is_normal_aux as [_ Th]. intuition auto.
Qed.

(** Renaming lemmas *)
Lemma pval_val_renaming : forall x y,
  (forall v, pval v → pval (subst_term (term_var_f y) x v)) ∧
  (forall v, val v → val (subst_term (term_var_f y) x v)).
Proof.
intros x y.
apply pval_val_mut_ind; intros; simpl; auto.
Case "var". destruct (x0 == x); auto.
Case "abs". pick fresh z and apply val_abs.
  rewrite subst_term_open_term_wrt_term_var; auto.
Qed.

Lemma val_renaming : forall x y v,
  val v → val (subst_term (term_var_f y) x v).
Proof.
intros x y v H. destruct (pval_val_renaming x y); auto.
Qed.
Hint Resolve val_renaming.

Lemma red0_renaming : forall x y e e', red0 e e' →
  red0 (subst_term (term_var_f y) x e) (subst_term (term_var_f y) x e').
Proof.
intros x y e e' H.
inversion H; subst.
simpl. rewrite subst_term_open_term_wrt_term; auto. apply red0_beta; auto with lngen.
assert (lc_term (subst_term (term_var_f y) x (term_abs t e1))) by auto with lngen; auto.
Qed.
Hint Resolve red0_renaming.

Lemma red1_renaming : forall x y e e', e ⇝ e' →
  (subst_term (term_var_f y) x e) ⇝ (subst_term (term_var_f y) x e').
Proof.
intros x y e e' H.
induction H; subst; simpl; auto.
apply red1_appL; auto with lngen.
apply red1_appR; auto with lngen.
apply red1_abs with (L := L `union` {{x}}); intros z Hz.
replace (term_var_f z) with (subst_term (term_var_f y) x (term_var_f z)) by auto with lngen.
repeat rewrite <- subst_term_open_term_wrt_term; eauto.
Qed.
Hint Resolve red1_renaming.

Lemma red_star_renaming : forall x y e e', e ⇝⋆ e' →
  (subst_term (term_var_f y) x e) ⇝⋆ (subst_term (term_var_f y) x e').
Proof.
intros x y e e' H.
induction H.
apply rt_step; auto.
apply rt_refl.
eapply rt_trans; eauto.
Qed.
Hint Resolve red_star_renaming.

(** Lemmas about [red0], [red1] *)
Lemma red0_subst : forall x e'' e e', lc_term e'' → red0 e e' →
  red0 (subst_term e'' x e) (subst_term e'' x e').
Proof.
intros x e'' e e' Hlc H.
inversion H; subst.
simpl. rewrite subst_term_open_term_wrt_term; auto. apply red0_beta; auto with lngen.
assert (lc_term (subst_term e'' x (term_abs t e1))) by auto with lngen; auto.
Qed.
Hint Resolve red0_subst.

Lemma red1_subst : forall x e'' e e', lc_term e'' → e ⇝ e' →
  (subst_term e'' x e) ⇝ (subst_term e'' x e').
Proof.
intros x e'' e e' Hlc H.
induction H; subst; simpl; auto.
apply red1_appL; auto with lngen.
apply red1_appR; auto with lngen.
apply red1_abs with (L := L `union` {{x}}); intros z Hz.
replace (term_var_f z) with (subst_term e'' x (term_var_f z)) by auto with lngen.
repeat rewrite <- subst_term_open_term_wrt_term; eauto.
Qed.
Hint Resolve red1_subst.

Lemma red1_open : forall L e'' e e',
  lc_term e'' →
  (forall x, x ∉ L → e ^ x ⇝ e' ^ x) →
  e ^^ e'' ⇝ e' ^^ e''.
Proof.
intros L e'' e e' Hlc H.
pick fresh x.
rewrite subst_term_intro with (x1 := x) (e1 := e); auto.
rewrite subst_term_intro with (x1 := x) (e1 := e'); auto.
Qed.
Hint Resolve red1_open.

(* Lemmas about red_star *)
Lemma red_star_context_appL : forall e1 e1' e2,
  lc_term e2 → e1 ⇝⋆ e1' →
  term_app e1 e2 ⇝⋆ term_app e1' e2.
Proof.
intros e1 e1' e2 Hlc Hred.
induction Hred.
apply rt_step; auto.
apply rt_refl.
eapply rt_trans; eauto.
Qed.

Lemma red_star_context_appR : forall e1 e2 e2',
  lc_term e1 → e2 ⇝⋆ e2' →
  term_app e1 e2 ⇝⋆ term_app e1 e2'.
Proof.
intros e1 e2 e2' Hlc Hred.
induction Hred.
apply rt_step; auto.
apply rt_refl.
eapply rt_trans; eauto.
Qed.

Lemma red_star_context_app : forall e1 e1' e2 e2',
  lc_term e1 → lc_term e2 → e1 ⇝⋆ e1' → e2 ⇝⋆ e2' →
  term_app e1 e2 ⇝⋆ term_app e1' e2'.
Proof.
intros e1 e1' e2 e2' Hlc1 Hlc2 Hred1 Hred2.
eapply rt_trans; eauto using red_star_context_appL, red_star_context_appR.
Qed.

Lemma red_star_context_abs : forall L τ e e',
  (forall x, x `notin` L → e ^ x ⇝⋆ e' ^ x) →
  term_abs τ e ⇝⋆ term_abs τ e'.
Proof.
intros L τ e e' H. pick fresh x.
remember (e ^ x) as e1.
remember (e' ^ x) as e1'.
assert (e1 ⇝⋆ e1') as Hred by solve [subst; apply H; auto]. clear H.
generalize dependent x. generalize dependent e'. generalize dependent e.
induction Hred; intros; subst.
Case "step".
apply rt_step.
apply red1_abs with (L := L `union` fv_term e `union` fv_term e'); intros.
rewrite <- var_subst with (e := term_var_f x) (x := x0).
replace e with (subst_term (term_var_f x) x0 e) by auto with lngen.
replace e' with (subst_term (term_var_f x) x0 e') by auto with lngen.
repeat rewrite <- subst_term_open_term_wrt_term; eauto.
Case "refl".
assert (e = e'). eapply open_term_wrt_term_inj; eauto. subst. apply rt_refl.
Case "trans".
apply rt_trans with (y := term_abs τ (close_term_wrt_term x0 y)).
apply IHHred1 with (x := x0); autorewrite with lngen; auto.
apply IHHred2 with (x := x0); autorewrite with lngen; auto.
Qed.
Hint Resolve red_star_context_appL red_star_context_appR red_star_context_app red_star_context_abs.

author: esope


text:
Require Import VST.floyd.proofauto.
Require Import common_predicates.
Require Import tree_free.
From SSL_VST Require Import core.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Definition free_spec :=
  DECLARE _free
          WITH ty: type, x: val
                              PRE  [ (tptr tvoid) ]
                              PROP()
                              PARAMS(x)
                              SEP (data_at_ Tsh ty x)
                              POST [ Tvoid ]
                              PROP()
                              LOCAL()
                              SEP (emp).

Definition tree_free_spec :=
  DECLARE _tree_free
   WITH x: val, s: (list Z), _alpha_549: tree_card
   PRE [ (tptr (Tunion _sslval noattr)) ]
   PROP( is_pointer_or_null((x : val)) )
   PARAMS(x)
   SEP ((tree (x : val) (s : list Z) (_alpha_549 : tree_card)))
   POST[ tvoid ]
   PROP(  )
   LOCAL()
   SEP ().

Definition Gprog : funspecs :=
  ltac:(with_library prog [tree_free_spec; free_spec]).

Lemma body_tree_free : semax_body Vprog Gprog f_tree_free tree_free_spec.
Proof.

start_function.
ssl_open_context.
forward_if.

 - {
assert_PROP (_alpha_549 = tree_card_0) as ssl_card_assert. { entailer!; ssl_dispatch_card. }
ssl_card tree ssl_card_assert .
assert_PROP (((x : val) = nullval)). { entailer!. }
let ssl_var := fresh in assert_PROP(s = ([] : list Z)) as ssl_var; try rewrite ssl_var in *. { entailer!. }
forward; entailer!.

}
 - {
assert_PROP (exists _alpha_545 _alpha_544, _alpha_549 = tree_card_2 _alpha_545 _alpha_544) as ssl_card_assert. { entailer!; ssl_dispatch_card. }
ssl_card tree ssl_card_assert _alpha_545x _alpha_544x.
assert_PROP ((~ ((x : val) = nullval))). { entailer!. }
Intros vx s2x rx s1x lx.
let ssl_var := fresh in assert_PROP(s = ((([(vx : Z)] : list Z) ++ (s1x : list Z)) ++ (s2x : list Z))) as ssl_var; try rewrite ssl_var in *. { entailer!. }
try rename vx into vx2.
forward.
try rename lx into lx2.
forward.
try rename rx into rx2.
forward.
assert_PROP(is_pointer_or_null((lx2 : val))). { entailer!. }
forward_call ((lx2 : val), (s1x : list Z), (_alpha_544x : tree_card)).
assert_PROP(is_pointer_or_null((rx2 : val))). { entailer!. }
forward_call ((rx2 : val), (s2x : list Z), (_alpha_545x : tree_card)).
forward_call (tarray (Tunion _sslval noattr) 3, x).
forward; entailer!.

}

Qed.

author: TyGuS

repo: ssl-vst

save_path: github-repos/coq/TyGuS-ssl-vst


text:
Require Import ZArith MSets MSetAVL.

Module M := MSetAVL.Make(Z_as_OT).

Open Scope Z_scope.

Definition ens1 := M.add 3 (M.add 0 (M.add 2 (M.empty))).
Definition ens2 := M.add 0 (M.add 2 (M.add 4 (M.empty))).
Definition ens3 := M.inter ens1 ens2.
Definition ens4 := M.union ens1 ens2.

Eval vm_compute in (M.mem 2 ens3).
Eval vm_compute in (M.elements ens3).
Eval vm_compute in (M.elements ens4).
Eval vm_compute in M.compare ens3 ens4.

(* Sets by themselves are ugly (proof parts), but who cares *)
Eval vm_compute in ens1.
Eval vm_compute in ens3.
Eval vm_compute in ens4.

(** Some more intense tests. *)

Fixpoint multiples (m:Z)(start:Z)(n:nat) {struct n} : list Z :=
  match n with
   | O => nil
   | S n => start::(multiples m (m+start) n)
  end.

Eval vm_compute in (multiples 2 0 200%nat).

Definition bigens1 := fold_right M.add M.empty (multiples 2 0 400%nat).
Definition bigens2 := fold_right M.add M.empty (multiples 3 0 400%nat).
Time Eval vm_compute in (M.elements (M.inter bigens1 bigens2)).
Time Eval vm_compute in (M.elements (M.union bigens1 bigens2)).

Definition bigens3 := fold_right M.add M.empty (multiples 2 0 (100*100)%nat).
Definition bigens4 := fold_right M.add M.empty (multiples 3 0 (100*100)%nat).
Time Eval vm_compute in (M.cardinal bigens3). (* computation of bigens3 done once and forall *)
Time Eval vm_compute in (M.cardinal bigens4). (* computation of bigens4 done once and forall *)
Time Eval vm_compute in (M.cardinal (M.inter bigens3 bigens4)).
Time Eval vm_compute in (M.cardinal (M.union bigens3 bigens4)).

(* Experimental illustration of the cardinal law: |AUB|+|A^B|=|A|+|B| *)
Time Eval vm_compute in (M.cardinal (M.union bigens3 bigens4)
                                         +M.cardinal (M.inter bigens3 bigens4))%nat.
(*   = 20000%nat
     : nat
*)

author: coq-contribs

repo: fsets

save_path: github-repos/coq/coq-contribs-fsets


text:
Require Import Lang.Syntax.
Require Import Lang.Bindings.
Require Import Lang.Static.
Require Import Lang.BindingsFacts.
Require Import Setoid.
Set Implicit Arguments.

Implicit Types EV HV V L : Set.

(** * Facts about the preorders on effects *)

Section section_eff_facts.
Context (EV HV L : Set).

Lemma se_transitive (𝓔₁ 𝓔₂ 𝓔₃ : eff EV HV L) : se 𝓔₁ 𝓔₂ → se 𝓔₂ 𝓔₃ → se 𝓔₁ 𝓔₃.
Proof.
auto.
Qed.

Lemma se_reflexive (𝓔 : eff EV HV L) : se 𝓔 𝓔.
Proof.
auto.
Qed.

Instance se_PreOrder : PreOrder (fun 𝓔₁ 𝓔₂ => se 𝓔₁ 𝓔₂) := {
  PreOrder_Reflexive  := @se_reflexive ;
  PreOrder_Transitive := @se_transitive ;
}.

Lemma se_nil (𝓔 : eff EV HV L) : se [] 𝓔.
Proof.
induction 𝓔 ; crush.
Qed.

Lemma se_cons_l (e : ef EV HV L) 𝓔1 𝓔2 : se (e :: 𝓔1) 𝓔2 -> se 𝓔1 𝓔2.
Proof.
crush.
Qed.

Lemma se_cons_r (e : ef EV HV L) 𝓔1 𝓔2 : se 𝓔1 𝓔2 -> se 𝓔1 (e :: 𝓔2).
Proof.
crush.
Qed.

Lemma se_app_l (𝓔1 𝓔2 : eff EV HV L) : se 𝓔1 (𝓔1 ++ 𝓔2).
Proof.
crush.
Qed.

Lemma se_app_r (𝓔1 𝓔2 : eff EV HV L) : se 𝓔2 (𝓔1 ++ 𝓔2).
Proof.
crush.
Qed.

Lemma se_app (𝓔1 𝓔2 E : eff EV HV L) : se 𝓔1 E -> se 𝓔2 E -> se (𝓔1 ++ 𝓔2) E.
Proof.
Hint Rewrite in_app_iff.
crush.
Qed.

End section_eff_facts.

(** * Facts about the preorders on types *)

Section section_ty_facts.

Hint Constructors st.
Hint Resolve se_reflexive.

Lemma st_transitive EV HV (T₁ T₂ T₃ : ty EV HV ∅) : st T₁ T₂ → st T₂ T₃ → st T₁ T₃.
Proof.
eauto.
Qed.

Fixpoint st_reflexive EV HV (T : ty EV HV ∅) : st T T.
Proof.
destruct T ; simpl.
+ apply st_unit.
+ apply st_fun ; auto.
+ apply st_efun ; eauto.
+ apply st_hfun ; auto.
Qed.

Instance st_PreOrder EV HV : PreOrder (@st EV HV) := {
  PreOrder_Reflexive  := @st_reflexive EV HV ;
  PreOrder_Transitive := @st_transitive EV HV ;
}.

End section_ty_facts.

Section section_wf_XEnv.

Hint Rewrite concat_empty_r concat_assoc.
Hint Rewrite notin_singleton notin_union dom_empty dom_concat dom_single.
Hint Extern 0 => match goal with
| [ H : empty = _ & _ ~ _ |- _ ] => apply empty_push_inv in H ; crush
| [ H : _ & _ ~ _ = _ & _ ~ _ |- _ ] => apply eq_push_inv in H ; crush
end.

Lemma ok_concat_indom_l EV HV (Ξ Ξ' : XEnv EV HV) :
ok (Ξ & Ξ') → ∀ X, X ∈ dom Ξ → X ∉ dom Ξ'.
Proof.
intros ok_ΞΞ' X HX.
induction Ξ' using env_ind ; [crush|].
rewrite concat_assoc in ok_ΞΞ'.
inversion ok_ΞΞ' ; crush.
Qed.

Lemma wf_XEnv_ok EV HV (Ξ : XEnv EV HV) :
wf_XEnv Ξ → ok Ξ.
Proof.
induction 1 ; constructor ; crush.
Qed.

Lemma wf_XEnv_concat_inv_l EV HV (Ξ Ξ' : XEnv EV HV) :
wf_XEnv (Ξ & Ξ') → wf_XEnv Ξ.
Proof.
induction Ξ' as [ | Ξ'' X [??] ] using env_ind ; [crush|].
rewrite concat_assoc.
inversion 1 ; crush.
Qed.

End section_wf_XEnv.

author: yizhouzhang

repo: abseff-coq

save_path: github-repos/coq/yizhouzhang-abseff-coq


text:
Require Import AutoSep.
Require Import SyntaxExpr.

Require Import StringSet.
Import StringSet.
Require Import FSetProperties.
Module Import SSP := Properties StringSet.

Set Implicit Arguments.

Section TopLevel.

  Variable vars : list string.

  Variable temp_size : nat.

  Variable exprs : list Expr.

  Variable base dst : nat.

  Definition is_state sp vs temps dst dst_buf : HProp :=
    (locals vars vs 0 (sp ^+ $8) *
     array temps (sp ^+ $8 ^+ $(4 * length vars)) *
     array dst_buf (sp ^+ $ dst))%Sep.

  Definition new_pre : assert :=
    x ~> ExX, Ex vs, Ex temps, Ex dst_buf,
    ![^[is_state x#Sp vs temps dst dst_buf] * #0]x /\
    [| length temps = temp_size /\
       length exprs = length dst_buf |].

  Require Import SemanticsExpr.
  Require Import DepthExpr.
  Require Import Max.

  Definition depth := max_list 0 (map depth exprs).

  Require CompileExpr.
  Require Import ListFactsNew.

  Local Open Scope nat.

  Definition runs_to x_pre x :=
    forall specs other vs temps dst_buf,
      interp specs (![is_state x_pre#Sp vs temps dst dst_buf * other ] x_pre)
      -> length temps = temp_size
      -> length exprs = length dst_buf
      -> Regs x Sp = x_pre#Sp /\
      exists changed,
        interp specs (![is_state (Regs x Sp) vs (upd_sublist temps base changed) dst (map (eval vs) exprs) * other ] (fst x_pre, x)) /\
        length changed <= depth.

  Definition post (pre : assert) :=
    st ~> Ex st_pre,
    pre (fst st, st_pre) /\
    [| runs_to (fst st, st_pre) (snd st) |].

  Definition imply (pre new_pre: assert) := forall specs x, interp specs (pre x) -> interp specs (new_pre x).

  Require Import FreeVarsExpr.
  Require Import Union.

  Definition syn_req exprs base :=
    Subset (union_list (map free_vars exprs)) (of_list vars) /\
    base + depth <= temp_size /\
    List.Forall (fun e => DepthExpr.depth e <= depth) exprs.

  Definition verifCond base pre := imply pre new_pre :: syn_req exprs base :: nil.

  Variable imports : LabelMap.t assert.

  Variable imports_global : importsGlobal imports.

  Variable modName : string.

  Definition Seq2 := @Seq_ _ imports_global modName.

  Definition Skip := Straightline_ imports modName nil.

  Fixpoint Seq ls :=
    match ls with
      | nil => Skip
      | a :: ls' => Seq2 a (Seq ls')
    end.

  Definition Strline := Straightline_ imports modName.

  Definition SaveRv lv := Strline (IL.Assign lv (RvLval (LvReg Rv)) :: nil).

  Definition stack_slot (n : nat) := LvMem (Sp + n)%loc.

  Definition compile_expr e n := CompileExpr.compile vars temp_size imports_global modName e n.

  Fixpoint do_compile exprs base dst :=
    match exprs with
      | nil => nil
      | x :: xs =>
        compile_expr x base
          :: SaveRv (stack_slot dst)
          :: do_compile xs base (4 + dst)
    end.

  Definition body := Seq (do_compile exprs base dst).

  Require Import Wrap.

  Opaque mult.

  Definition compile : cmd imports modName.
    refine (Wrap imports imports_global modName body post (verifCond base) _ _).

    Lemma postOk : forall specs exprs base dst pre x,
      interp specs (Postcondition (Seq (do_compile exprs base dst) pre) x)
      -> imply pre (x ~> ExX, Ex vs, Ex temps, Ex dst_buf,
        ![^[is_state x#Sp vs temps dst dst_buf] * #0]x /\
        [| length temps = temp_size /\
          length exprs = length dst_buf |])
      -> syn_req exprs base
      -> exists x0, interp specs (pre (fst x, x0))
        /\ forall specs other vs temps dst_buf,
          interp specs (![is_state (Regs x0 Sp) vs temps dst dst_buf * other ] (fst x, x0))
          -> length temps = temp_size
          -> length exprs = length dst_buf
          -> Regs (snd x) Sp = Regs x0 Sp /\
          exists changed,
            interp specs (![is_state (Regs (snd x) Sp) vs (upd_sublist temps base changed) dst (map (eval vs) exprs) * other ] (fst x, snd x)) /\
            length changed <= depth.
      induction exprs0; post.

      clear_fancy.
      Transparent evalInstrs.
      simpl in H3.
      Opaque evalInstrs.
      injection H3; clear H3; intros; subst.
      descend.
      eauto.
      descend.
      instantiate (1 := nil); simpl.
      destruct dst_buf; simpl in *; auto.
      discriminate.
      simpl; auto.

      apply IHexprs0 in H; clear IHexprs0; auto.
      Focus 2.
      hnf; post.
      apply H0 in H3; clear H0; post.
      unfold is_state in H2.
      assert (interp specs0
        (![locals vars x4 0 (Regs x2 Sp ^+ $ (8)) *
          array x5 (Regs x2 Sp ^+ $ (8) ^+ $ (4 * Datatypes.length vars)) *
          (array x6 (Regs x2 Sp ^+ $ (dst0)) *
          ![fun m : ST.settings * smem => x3 m]) ]
        (fst x0, x2))).
      clear H; clear_fancy.
      step auto_ext.
      clear H2.
      apply H5 in H3; clear H5; post.
      unfold stack_slot in H4.
      clear H; clear_fancy.

      Lemma array_out : forall a p,
        length a > 0
        -> array a p ===> p =*> Array.selN a 0 * array (tl a) (p ^+ $4).
        clear_fancy; destruct a; unfold array; simpl; intros.
        inversion H.
        destruct a.
        sepLemma.
        apply Himp_star_frame; try apply Himp_refl.
        eapply Himp_trans; [ apply ptsto32m_shift_base' | ].
        instantiate (1 := 4); auto.
        apply Himp_refl.
      Qed.

      Lemma change_hyp : forall P Q specs st,
        interp specs (![P] st)
        -> P ===> Q
        -> interp specs (![Q] st).
        intros.
        eapply Imply_sound.
        rewrite sepFormula_eq.
        apply H0.
        rewrite sepFormula_eq in *; auto.
      Qed.

      eapply change_hyp in H5.
      Focus 2.
      apply Himp_star_frame; [ apply Himp_refl | ].
      apply Himp_star_frame; [ | apply Himp_refl ].
      apply array_out; omega.
      destruct x6; simpl in *; try discriminate.
      evaluate auto_ext.
      destruct x0; simpl in *.
      descend.
      replace (Regs x2 Sp ^+ natToW dst0 ^+ natToW 4) with (Regs x2 Sp ^+ natToW (S (S (S (S dst0)))))
        in H9.
      unfold is_state.
      unfold CompileExpr.is_state in H9.
      step auto_ext.
      rewrite H.
      step auto_ext.
      rewrite <- H3.
      step auto_ext.
      rewrite <- wplus_assoc.
      unfold natToW.
      rewrite <- natToWord_plus.
      repeat f_equal.
      omega.
      rewrite length_upd_sublist; auto.
      auto.

      post.
      post.
      eexists; split; eauto.
      intros.
      clear H2.
      unfold is_state in H.
      assert (interp specs0
        (![CompileExpr.is_state vars (Regs x2 Sp) vs temps
          * (array dst_buf (Regs x2 Sp ^+ $ (dst0)) * other ) ]
        (fst x, x2))).
      unfold CompileExpr.is_state.
      clear H0; clear_fancy.
      step auto_ext.
      clear H.
      apply H5 in H2; clear H5.
      generalize H6; intro Hs.
      apply H2 in Hs; clear H2.
      destruct x; simpl in *.
      destruct Hs as [ ? [ ? [ ? [ ? [ ] ] ] ] ].
      simpl in *.
      eapply change_hyp in H2.
      Focus 2.
      apply Himp_star_frame; [ apply Himp_refl | ].
      apply Himp_star_frame; [ | apply Himp_refl ].
      apply array_out; omega.
      unfold stack_slot in H4.
      clear H0; clear_fancy.
      evaluate auto_ext.
      destruct dst_buf; simpl in *; try discriminate.
      assert (interp specs0
        (![is_state (Regs x0 Sp) vs (upd_sublist temps base0 x) (S (S (S (S dst0)))) dst_buf *
          ((Regs x2 Sp ^+ natToW dst0) =*> Regs x1 Rv * other)] (s, x0))).
      unfold is_state.
      unfold CompileExpr.is_state in H9.
      step auto_ext.
      rewrite <- H0.
      unfold natToW.
      rewrite H.
      rewrite <- H0.
      step auto_ext.
      rewrite <- wplus_assoc.
      unfold natToW.
      rewrite <- natToWord_plus.
      replace (dst0 + 4) with (S (S (S (S dst0)))) by omega.
      step auto_ext.
      clear H9.
      apply H3 in H10; clear H3; auto.
      post.
      congruence.

      assert (length (upd_sublist (upd_sublist temps base0 x) base0 x3)
        = length temps).
      repeat rewrite length_upd_sublist; reflexivity.
      eapply CompileExpr.get_changed in H9.
      post.
      descend.
      rewrite <- H12.
      Focus 3.
      instantiate (1 := base0 + max (length x) (length x3)).
      omega.
      Focus 2.
      destruct H1.
      destruct (NPeano.Nat.max_spec (length x) (length x3)); intuition.
      inversion_clear H16.
      omega.
      unfold is_state in *.
      eapply change_hyp.
      Focus 2.
      apply Himp_star_frame; [ | eapply Himp_refl ].
      apply Himp_star_frame; [ eapply Himp_refl | ].

      Lemma array_in : forall a p,
        length a > 0
        -> p =*> Array.selN a 0 * array (tl a) (p ^+ $4) ===> array a p.
        clear_fancy; destruct a; unfold array; simpl; intros.
        inversion H.
        destruct a.
        sepLemma.
        apply Himp_star_frame; try apply Himp_refl.
        eapply Himp_trans; [ | apply ptsto32m_shift_base ].
        instantiate (1 := 4); auto.
        apply Himp_refl.
        auto.
      Qed.

      apply array_in; simpl; auto.
      simpl.
      replace (Regs s0 Sp ^+ $ (dst0) ^+ $ (4))
        with (Regs s0 Sp ^+ ($ (dst0) ^+ $ (4))) by words.
      rewrite <- natToWord_plus.
      replace (dst0 + 4) with (S (S (S (S dst0)))) by omega.
      generalize dependent (map (eval vs) exprs0); intros.
      step auto_ext.
      replace (Regs x2 Sp) with (Regs s0 Sp) by congruence.
      step auto_ext.

      intros.
      repeat rewrite CompileExpr.upd_sublist_unchanged by auto; reflexivity.

      intros.
      generalize (Max.le_max_l (length x) (length x3)).
      generalize (Max.le_max_r (length x) (length x3)); intros.
      repeat rewrite CompileExpr.upd_sublist_unchanged_high by auto; reflexivity.

      rewrite length_upd_sublist; auto.
      unfold syn_req in *; intuition.
      hnf; intros.
      apply H2.
      simpl.
      unfold union_list.
      simpl.

      Lemma In_union_list : forall x exprs0,
        In x (fold_right union empty (map free_vars exprs0))
        -> In x (fold_right union empty (map free_vars exprs0)).
        induction exprs0; simpl; intuition.
      Qed.

      eapply In_union_list with (exprs0 := a :: exprs0); eauto.
      simpl.
      eapply StringFacts.union_iff; eauto.
      inversion H4; auto.
    Qed.

    abstract (unfold verifCond; wrap0;
      match goal with
        | [ H : interp _ _ |- _ ] => eapply postOk in H; post; descend; eauto
      end).

    Lemma verifCondOk : forall exprs base dst pre,
      imply pre (x ~> ExX, Ex vs, Ex temps, Ex dst_buf,
        ![^[is_state x#Sp vs temps dst dst_buf] * #0]x /\
        [| length temps = temp_size /\
          length exprs = length dst_buf |])
      -> syn_req exprs base
      -> vcs (VerifCond (Seq (do_compile exprs base dst) pre)).
      induction exprs0; wrap0.

      Transparent evalInstrs.
      discriminate.
      Opaque evalInstrs.

      clear IHexprs0; clear_fancy.
      hnf; post.
      apply H in H1; clear H; post.
      unfold is_state, CompileExpr.is_state in *.
      assert (interp specs
        (![locals vars x1 0 ((x) # (Sp) ^+ $ (8)) *
          array x2 ((x) # (Sp) ^+ $ (8) ^+ $ (4 * Datatypes.length vars)) *
          (array x3 ((x) # (Sp) ^+ $ (dst0)) *
          ![fun m : ST.settings * smem => x0 m]) ] x)).
      step auto_ext.
      clear H1.
      descend.
      step auto_ext.
      auto.

      unfold syn_req, CompileExpr.syn_req in *; intuition.
      hnf; intros.
      apply H1.
      simpl.
      unfold union_list.
      simpl.

      apply StringFacts.union_iff; auto.
      inversion H3; omega.

      clear IHexprs0; clear_fancy.
      apply H in H3; clear H; post.
      unfold is_state in H1.
      assert (interp specs
        (![locals vars x1 0 (Regs x Sp ^+ $ (8)) *
          array x2 (Regs x Sp ^+ $ (8) ^+ $ (4 * Datatypes.length vars)) *
          (array x3 (Regs x Sp ^+ $ (dst0)) *
          ![fun m : ST.settings * smem => x0 m]) ] (stn, x))).
      step auto_ext.
      clear H1.
      apply H4 in H3; clear H4; post.
      eapply change_hyp in H4.
      Focus 2.
      apply Himp_star_frame; [ apply Himp_refl | ].
      apply Himp_star_frame; [ | apply Himp_refl ].
      apply array_out; omega.
      destruct x3; simpl in *; try discriminate.
      unfold stack_slot in *.
      evaluate auto_ext.

      apply IHexprs0; clear IHexprs0; clear_fancy.
      Focus 2.
      unfold syn_req in *; intuition.
      hnf; intros.
      apply H1.
      simpl.
      unfold union_list; simpl.
      eapply In_union_list with (exprs0 := a :: exprs0); eauto.
      apply StringFacts.union_iff; eauto.
      inversion H3; auto.
      hnf; post.
      apply H in H2; clear H; post.
      unfold is_state in H1.
      assert (interp specs
        (![CompileExpr.is_state vars (Regs x1 Sp) x3 x4
          * (array x5 (Regs x1 Sp ^+ $ (dst0)) * ![fun m : ST.settings * smem => x2 m]) ]
        (fst x, x1))).
      unfold CompileExpr.is_state.
      step auto_ext.
      clear H1.
      apply H4 in H2; clear H4; post.
      eapply change_hyp in H4.
      Focus 2.
      apply Himp_star_frame; [ apply Himp_refl | ].
      apply Himp_star_frame; [ | apply Himp_refl ].
      apply array_out; omega.
      destruct x5; simpl in *; try discriminate.
      unfold stack_slot in *.
      evaluate auto_ext.
      destruct x; simpl in *.
      descend.
      rewrite H4.
      rewrite <- H2.
      unfold is_state.
      unfold CompileExpr.is_state in H9.
      step auto_ext.
      rewrite <- H2.
      rewrite <- wplus_assoc.
      rewrite <- natToWord_plus.
      replace (dst0 + 4) with (S (S (S (S dst0)))) by omega.
      step auto_ext.
      rewrite length_upd_sublist; auto.
      congruence.
    Qed.

    abstract (unfold verifCond; wrap0; eauto using verifCondOk).
  Defined.

End TopLevel.

author: mmcco

repo: Verified-BPF

save_path: github-repos/coq/mmcco-Verified-BPF


text:
From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* ********************* *)

Section Transformer.
  Definition sumt (R:Type) : (Type -> Type) -> Type -> Type :=
    fun m A => m (R + A:Type).
  Definition mult (R:Type) (idx:R) (op:Monoid.law idx)
  : (Type -> Type) -> Type -> Type :=
    fun m A => m (R * A:Type).
  Definition appt (R:Type) : (Type -> Type) -> Type -> Type :=
    fun m A => R -> m A.
  Definition statet (R:Type) : (Type -> Type) -> Type -> Type :=
    fun m A => R -> m (R * A:Type).
End Transformer.

(* ********************* *)

Module Pure.
  Definition Eta (m:Type -> Type) := forall A, A -> m A.

  Record class_of (m:Type -> Type) :=
    Class {
        eta : Eta m;
      }.

  Section ClassDef.
    Structure map := Pack {apply; _: class_of apply}.
    Variable (cF : map).
    Definition class :=
      let: Pack _ c := cF return class_of (apply cF) in c.
  End ClassDef.

  Module Exports.
    Coercion apply : map >-> Funclass.
    Notation pureMap := map.
    Notation Eta := Eta.
    Definition eta T := (eta (class T)).
  End Exports.
End Pure.
Import Pure.Exports.

Section Pure_lemma.
  Variable (m:pureMap).
  Let eta := eta m.
End Pure_lemma.

Definition eq_pureMap (m:Type -> Type) (c d:Pure.class_of m) :=
  forall A, @eta (Pure.Pack c) A =1 @eta (Pure.Pack d) _.

Section Pure_canonicals.
  (* id *)
  Definition id_pure_class_of : Pure.class_of id := Pure.Class (fun A x => x).
  Definition id_pureMap : pureMap :=
    Eval hnf in @Pure.Pack id id_pure_class_of.

  (* comp *)
  Definition comp_pure_class_of (m n:pureMap) :
    Pure.class_of (fun A => m (n A)) :=
    Pure.Class (fun _ => (@eta m _ \o @eta n _)).
  Definition comp_pureMap (m n:pureMap) : pureMap :=
    Eval hnf in @Pure.Pack (fun A => m (n A)) (comp_pure_class_of m n).

  Lemma eta_comp m n :
    @eta (comp_pureMap m n) = fun _ => @eta m _ \o @eta n _.
  Proof. done. Qed.

  (* option *)
  Definition option_pure_class_of : Pure.class_of option :=
    Pure.Class (@Some).
  Canonical option_pureMap : pureMap :=
    Eval hnf in @Pure.Pack option option_pure_class_of.

  Lemma eta_option : @eta option_pureMap = @Some.
  Proof. done. Qed.

  (* seq *)
  Definition seq_pure_class_of : Pure.class_of seq :=
    Pure.Class (fun _ x => [:: x]).
  Canonical seq_pureMap : pureMap :=
    Eval hnf in @Pure.Pack seq seq_pure_class_of.

  Lemma era_seq : @eta seq_pureMap = (fun _ x => [:: x]).
  Proof. done. Qed.

  (* sumt *)
  Definition sumt_pure_class_of R (m:pureMap) : Pure.class_of (sumt R m) :=
    Pure.Class (fun _ x => eta m (inr x)).
  Canonical sumt_pureMap R (m:pureMap) : pureMap :=
    Eval hnf in @Pure.Pack (sumt R m) (sumt_pure_class_of R m).

  (* mult *)
  Definition mult_pure_class_of R (idx:R) (op:Monoid.law idx) (m:pureMap)
    : Pure.class_of (mult op m) :=
    Pure.Class (fun _ x => eta _ (idx,x)).
  Canonical mult_pureMap a (idx:a) (op:Monoid.law idx) (m:pureMap) : pureMap :=
    Eval hnf in @Pure.Pack (mult op m) (mult_pure_class_of op m).

  (* appt *)
  Definition appt_pure_class_of R (m:pureMap) : Pure.class_of (appt R m) :=
    Pure.Class (fun _ x _ => eta _ x).
  Canonical appt_pureMap R (m:pureMap) : pureMap :=
    Eval hnf in @Pure.Pack (appt R m) (appt_pure_class_of R m).

  (* statet *)
  Definition statet_pure_class_of R (m:pureMap) : Pure.class_of (statet R m) :=
    Pure.Class (fun _ x r => eta _ (r,x)).
  Canonical statet_pureMap R (m:pureMap) : pureMap :=
    Eval hnf in @Pure.Pack (statet R m) (statet_pure_class_of R m).
End Pure_canonicals.

(* ********************* *)

Module Functor.
  Definition Functor (m:Type -> Type) := forall A B, (A -> B) -> m A -> m B.

  Record class_of (m:Type -> Type) :=
    Class {
        functor : Functor m;
        _: forall A B (f g:A -> B), f =1 g -> functor f =1 functor g;
        _: forall A x, functor (@id A) x = x;
        _: forall A B C (f:B -> C) (g:A -> B) x,
            functor (f \o g) x = functor f (functor g x)
      }.

  Section ClassDef.
    Structure map := Pack {apply; _: class_of apply}.
    Variable (cF : map).
    Definition class :=
      let: Pack _ c := cF return class_of (apply cF) in c.
  End ClassDef.

  Module Exports.
    Coercion apply : map >-> Funclass.
    Notation functorMap := map.
    Notation Functor := Functor.
    Definition functor T := (functor (class T)).
  End Exports.
End Functor.
Import Functor.Exports.

Section Functor_lemma.
  Variable (m : functorMap).

  Lemma eq_functor : forall A B (f g:A -> B),
      f =1 g -> @functor m _ _ f =1 functor g.
  Proof. by case : m => func []. Qed.

  Lemma functor_id : forall A (x:m A), functor (@id A) x = x.
  Proof. by case : m => func []. Qed.

  Lemma functorD : forall A B C (f:B -> C) (g:A -> B) (x:m A),
      functor (f \o g) x = functor f (functor g x).
  Proof. by case : m => func []. Qed.

  Lemma eq_functor_id A (f:A -> A) :
    f =1 id -> @functor m _ _ f =1 id.
  Proof. move /eq_functor => e x. by rewrite e functor_id. Qed.
End Functor_lemma.

Definition eq_functorMap (m:Type -> Type) (c d:Functor.class_of m) :=
  forall A B,
    @functor (Functor.Pack c) A B =2 @functor (Functor.Pack d) _ _.

Section Functor_canonicals.
  (* id *)
  Definition id_functor_class_of : Functor.class_of id.
  Proof. exact : (@Functor.Class _ (fun _ _ => id)). Defined.
  Definition id_functorMap : functorMap :=
    Eval hnf in @Functor.Pack id id_functor_class_of.

  (* comp *)
  Definition comp_functor_class_of (m n:functorMap) :
    Functor.class_of (fun A => m (n A)).
  Proof.
    apply : (@Functor.Class _ (fun _ _ => @functor m _ _ \o @functor n _ _))
    =>[A B f g fg|A x|A B C f g x]/=.
    - by do 2! apply : eq_functor.
    - apply : eq_functor_id. exact : functor_id.
    - rewrite -functorD. apply : eq_functor => y. exact : functorD.
  Defined.
  Definition comp_functorMap (m n:functorMap) : functorMap :=
    Eval hnf in @Functor.Pack (fun A => m (n A)) (comp_functor_class_of m n).

  Lemma functor_comp m n :
    @functor (comp_functorMap m n) =
    fun _ _ => @functor m _ _ \o @functor n _ _.
  Proof. done. Qed.

  (* option *)
  Definition option_functor_class_of : Functor.class_of option.
  Proof.
    apply : (@Functor.Class
               _ (fun _ _ f o => if o is Some x then Some (f x) else None))
    =>[A B f g fg [x|]|A [x|]|A B C f g [x|]]//.
      by rewrite fg.
  Defined.
  Canonical option_functorMap : functorMap :=
    Eval hnf in @Functor.Pack option option_functor_class_of.

  Lemma functor_option :
    @functor option_functorMap =
    fun _ _ f o => if o is Some x then Some (f x) else None.
  Proof. done. Qed.

  Lemma seq_functor_class_of : Functor.class_of seq.
  Proof.
    apply : (@Functor.Class _ (@map)).
    - exact : eq_map.
    - exact : map_id.
    - exact : map_comp.
  Defined.
  Canonical seq_functorMap : functorMap :=
    Eval hnf in @Functor.Pack seq seq_functor_class_of.

  Lemma functor_seq : @functor seq_functorMap = @map.
  Proof. done. Qed.

  (* sumt *)
  Definition sumt_functor_class_of R (m:functorMap):
    Functor.class_of (sumt R m).
  Proof.
    apply : (@Functor.Class
               _ (fun _ _ f => functor (fun x => match x with
                                                 | inl a => inl a
                                                 | inr x => inr (f x)
                                                 end)))
    =>[A B f g fg|A x|A B C f g x]/=.
    - apply : eq_functor =>[[|x]]//. by rewrite fg.
    - by apply : eq_functor_id =>[[]].
    - rewrite -functorD. by apply : eq_functor =>[[]].
  Defined.
  Canonical sumt_functorMap R (m:functorMap) : functorMap :=
    Eval hnf in @Functor.Pack (sumt R m) (sumt_functor_class_of R m).

  Lemma functor_sumt R m:
    @functor (sumt_functorMap R m) =
    fun _ _ f => functor (fun x => match x with
                                   | inl a => inl a
                                   | inr x => inr (f x)
                                   end).
  Proof. done. Qed.

  (* mult *)
  Definition mult_functor_class_of R (idx:R) (op:Monoid.law idx) (m:functorMap):
    Functor.class_of (mult op m).
  Proof.
    apply : (@Functor.Class
               _ (fun _ _ f => functor (fun rx => match rx with
                                                    (r,x) => (r,f x)
                                                  end)))
    =>[A B f g fg|A x|A B C f g x].
    - apply : eq_functor =>[[r x]]. by rewrite fg.
    - by apply : eq_functor_id =>[[]].
    - rewrite -functorD. by apply : eq_functor =>[[]].
  Defined.
  Canonical mult_functorMap R (idx:R) (op:Monoid.law idx) (m:functorMap) :
    functorMap :=
    Eval hnf in @Functor.Pack (mult op m) (mult_functor_class_of op m).

  Lemma functor_mult R (idx:R) (op:Monoid.law idx) m:
    @functor (mult_functorMap op m) =
    fun _ _ f => functor (fun rx => match rx with (r,x) => (r,f x) end).
  Proof. done. Qed.

  (* appt *)
  (* needed functional extensionality *)
(*
  Definition appt_functor_class_of R (m:functorMap):
    Functor.class_of (appt R m).
  Proof.
    apply : (@Functor.Class _ (fun _ _ f xf x => functor f (xf x)))
    =>[A B f g fg xf||].
*)
End Functor_canonicals.

(* ********************* *)

Module PFunctor.
  Section ClassDef.
    Record class_of (m:Type -> Type) :=
      Class {
          pBase : Pure.class_of m;
          fBase : Functor.class_of m
        }.
    Structure map := Pack {apply; _: class_of apply}.
    Variable (cF:map).
    Definition class :=
      let: Pack _ c := cF return class_of (apply cF) in c.
    Definition pureMap := Pure.Pack (pBase class).
    Definition functorMap := Functor.Pack (fBase class).
  End ClassDef.

  Module Exports.
    Coercion pBase : class_of >-> Pure.class_of.
    Coercion fBase : class_of >-> Functor.class_of.
    Coercion apply : map >-> Funclass.
    Coercion pureMap : map >-> Pure.map.
    Canonical pureMap.
    Coercion functorMap : map >-> Functor.map.
    Canonical functorMap.
    Notation pfunctorMap := map.
  End Exports.
End PFunctor.
Import PFunctor.Exports.

Section PFunctor_lemma.
  Variable (m : pfunctorMap).
End PFunctor_lemma.

Definition eq_pfunctorMap (m:Type -> Type) (c d:PFunctor.class_of m) :=
  eq_pureMap c d /\ eq_functorMap c d.

Section PFunctor_canonicals.
  (* id *)
  Definition id_pfunctor_class_of : PFunctor.class_of id :=
    PFunctor.Class id_pure_class_of id_functor_class_of.
  Definition id_pfunctorMap : pfunctorMap :=
    Eval hnf in @PFunctor.Pack id id_pfunctor_class_of.

  (* comp *)
  Definition comp_pfunctor_class_of (m n:pfunctorMap) :
    PFunctor.class_of (fun A => m (n A)) :=
    PFunctor.Class (comp_pure_class_of m n) (comp_functor_class_of m n).
  Definition comp_pfunctorMap (m n:pfunctorMap) : pfunctorMap :=
    Eval hnf in @PFunctor.Pack (fun A => m (n A)) (comp_pfunctor_class_of m n).

  (* option *)
  Definition option_pfunctor_class_of : PFunctor.class_of option :=
    PFunctor.Class option_pure_class_of option_functor_class_of.
  Canonical option_pfunctorMap : pfunctorMap :=
    Eval hnf in @PFunctor.Pack option option_pfunctor_class_of.

  (* seq *)
  Definition seq_pfunctor_class_of : PFunctor.class_of seq :=
    PFunctor.Class seq_pure_class_of seq_functor_class_of.
  Canonical seq_pfunctorMap : pfunctorMap :=
    Eval hnf in @PFunctor.Pack seq seq_pfunctor_class_of.

  (* sumt *)
  Definition sumt_pfunctor_class_of R (m:pfunctorMap) :
    PFunctor.class_of (sumt R m) :=
    PFunctor.Class (sumt_pure_class_of R m) (sumt_functor_class_of R m).
  Canonical sumt_pfunctorMap R (m:pfunctorMap): pfunctorMap :=
    Eval hnf in @PFunctor.Pack (sumt R m) (sumt_pfunctor_class_of R m).

  (* mult *)
  Definition mult_pfunctor_class_of R (idx:R) (op:Monoid.law idx)
             (m:pfunctorMap) : PFunctor.class_of (mult op m) :=
    PFunctor.Class (mult_pure_class_of op m) (mult_functor_class_of op m).
  Definition mult_pfunctorMap R (idx:R) (op:Monoid.law idx) (m:pfunctorMap)
    : pfunctorMap :=
    Eval hnf in @PFunctor.Pack (mult op m) (mult_pfunctor_class_of op m).
End PFunctor_canonicals.

(* ********************* *)

Module Applicative.
  Definition Applicative (m:Type -> Type)
    := forall A B, m (A -> B) -> m A -> m B.

  Record mixin_of (m:pfunctorMap) :=
    Mixin {
        applicative : Applicative m;
        _: forall A B (f:A -> B),
            applicative (eta _ f) =1 functor f;
        _: forall A B C (f g:A -> B -> C),
            f =2 g ->
            forall x, applicative (functor f x) =1 applicative (functor g x);
        _: forall A B C D (f g:A -> B -> C -> D),
            (forall x, f x =2 g x) ->
            forall x y, applicative (applicative (functor f x) y)
                        =1 applicative (applicative (functor g x) y);
        _: forall A B C (f:m (B -> C)) (g:m (A -> B)) x,
            applicative (applicative (applicative (eta _ comp) f) g) x =
            applicative f (applicative g x);
        _: forall A B (f:A -> B) x,
            applicative (eta _ f) (eta m x) = eta _ (f x);
        _: forall A B (f:m (A -> B)) x,
            applicative f (eta _ x) = functor (@^~ x) f
      }.

  Section ClassDef.
    Record class_of (m:Type -> Type) :=
      Class {
          base : PFunctor.class_of m;
          mixin : mixin_of (PFunctor.Pack base)
        }.
    Structure map := Pack {apply; _: class_of apply}.
    Variable (cF:map).
    Definition class :=
      let: Pack _ c := cF return class_of (apply cF) in c.
    Definition pureMap := Pure.Pack (base class).
    Definition functorMap := Functor.Pack (base class).
    Definition pfunctorMap := PFunctor.Pack (base class).
  End ClassDef.

  Module Exports.
    Coercion base : class_of >-> PFunctor.class_of.
    Coercion mixin : class_of >-> mixin_of.
    Coercion apply : map >-> Funclass.
    Coercion pureMap : map >-> Pure.map.
    Canonical pureMap.
    Coercion functorMap : map >-> Functor.map.
    Canonical functorMap.
    Coercion pfunctorMap : map >-> PFunctor.map.
    Canonical pfunctorMap.
    Notation applicativeMap := map.
    Notation Applicative := Applicative.
    Definition applicative T := (applicative (class T)).
  End Exports.
End Applicative.
Import Applicative.Exports.

Section Applicative_lemma.
  Variable (m:applicativeMap).
  Let eta := eta m.

  Lemma applicative_etal A B (f:A -> B) :
    applicative (eta f) =1 functor f.
  Proof. rewrite /eta. by case : m => func [b []]. Qed.

  Lemma applicativeA A B C :
    forall (f:m (B -> C)) (g:m (A -> B)) x,
      applicative (applicative (applicative (eta comp) f) g) x =
      applicative f (applicative g x).
  Proof. rewrite /eta. by case : m => func [b []]. Qed.

  Lemma applicative_eta_eta A B (f:A -> B) x :
    applicative (eta f) (eta x) = eta (f x).
  Proof. rewrite /eta. by case : m => func [b []]. Qed.

  Lemma applicative_etar A B :
    forall (f:m (A -> B)) x,
      applicative f (eta x) = functor (@^~ x) f.
  Proof. rewrite /eta. by case : m => func [b []]. Qed.

  Definition functor2 A B C (f:A -> B -> C) (x:m A) : m B -> m C :=
    applicative (functor f x).

  Lemma eq_functor2 A B C (f g:A -> B -> C):
    f =2 g -> functor2 f =2 functor2 g.
  Proof.
    rewrite /functor2. case : m => func [b /=[a e0 H e1 e2 e3 e4]].
    exact : H.
  Qed.

  Lemma functor2_eta A B C (f:A -> B -> C) x:
    functor2 f (eta x) =1 functor (f x).
  Proof.
    rewrite /functor2 => y.
      by rewrite -applicative_etal applicative_eta_eta applicative_etal.
  Qed.

  Definition functor3 A B C D (f:A -> B -> C -> D)
             (x:m A) (y:m B) : m C -> m D :=
    applicative (functor2 f x y).

  Lemma eq_functor3 A B C D (f g:A -> B -> C -> D):
    (forall x, f x =2 g x) -> forall x, functor3 f x =2 functor3 g x.
  Proof.
    rewrite /functor3 /functor2. case : m => func [b /=[a e0 e1 H e2 e3 e4]].
    exact : H.
  Qed.

  Lemma functor3_eta A B C D (f:A -> B -> C -> D) x:
    functor3 f (eta x) =2 functor2 (f x).
  Proof.
    rewrite /functor3 => y z. by rewrite functor2_eta.
  Qed.
End Applicative_lemma.

Definition eq_applicativeMap (m:Type -> Type) (c d:Applicative.class_of m) :=
  eq_pfunctorMap c d /\
  forall A B, @applicative (Applicative.Pack c) A B
                =2 @applicative (Applicative.Pack d) _ _.

Section Applicative_canonicals.
  (* id *)
  Definition id_applicative_mixin_of : Applicative.mixin_of id_pfunctorMap.
  Proof.
    exact : (@Applicative.Mixin
               _ ((fun _ _ => id) : Applicative id_pfunctorMap)).
  Defined.
  Definition id_applicative_class_of : Applicative.class_of id :=
    Applicative.Class id_applicative_mixin_of.
  Definition id_applicativeMap : applicativeMap :=
    Eval hnf in @Applicative.Pack id id_applicative_class_of.

  (* comp *)
  Definition comp_applicative_mixin_of (m n:applicativeMap) :
    Applicative.mixin_of (comp_pfunctorMap m n).
  Proof.
    apply : (@Applicative.Mixin
               _ ((fun A B (f:m (n (A -> B)))
                   => functor2 (@applicative _ _ _) f)
                  : Applicative (comp_pfunctorMap _ _)))
              =>/=[A B f x|A B C f g fg x y|A B C D f g fg x y z|
                   A B C f g x|A B f x|A B f x].
    - rewrite functor_comp functor2_eta. apply : eq_functor => y.
      exact : applicative_etal.
    - rewrite functor_comp /= /functor2 -!functorD. apply : eq_functor2.
      exact : eq_functor2.
    - rewrite functor_comp /= /functor2 -!functorD -!applicative_etal.
      rewrite -!applicativeA !applicative_eta_eta !applicative_etal.
      apply : eq_functor3. exact : eq_functor3.
    - rewrite eta_comp /= functor2_eta /functor2 -!applicative_etal.
      do ! (rewrite -applicativeA !applicative_eta_eta).
         rewrite -2!applicativeA applicative_etar -applicative_etal.
         do ! (rewrite -applicativeA !applicative_eta_eta).
            rewrite !applicative_etal.
      apply : eq_functor3. exact : applicativeA.
    - by rewrite eta_comp functor2_eta -applicative_etal !applicative_eta_eta.
    - rewrite functor_comp eta_comp /= /functor2 applicative_etar -functorD.
      apply : eq_functor => y. exact : applicative_etar.
  Defined.
  Definition comp_applicative_class_of (m n:applicativeMap) :
    Applicative.class_of (fun A => m (n A)) :=
    Applicative.Class (comp_applicative_mixin_of m n).
  Definition comp_applicativeMap (m n:applicativeMap) : applicativeMap :=
    Eval hnf in @Applicative.Pack
                  (fun A => m (n A)) (comp_applicative_class_of m n).

  Lemma applicative_comp (m n:applicativeMap):
    @applicative (comp_applicativeMap m n) =
    fun A B (f:m (n (A -> B))) => functor2 (@applicative _ _ _) f.
  Proof. done. Qed.

  Lemma applicative_functor2 (m n:applicativeMap) A B C f:
    @functor2 (comp_applicativeMap m n) A B C f =2 functor2 (functor2 f).
  Proof.
    rewrite /functor2 applicative_comp /functor2 functor_comp => x y /=.
    rewrite -functorD. apply : eq_functor2 =>{x y} x y.
    exact : eq_functor2.
  Qed.

  Lemma applicative_functor3 (m n:applicativeMap) A B C D f x:
    @functor3 (comp_applicativeMap m n) A B C D f x =2 functor3 (functor3 f) x.
  Proof.
    rewrite /functor3 applicative_comp /functor2 functor_comp => y z /=.
    rewrite -!applicative_etal -!applicativeA applicative_eta_eta.
    rewrite -!applicative_etal -applicativeA !applicative_eta_eta.
    rewrite -applicativeA !applicative_eta_eta applicative_etal.
    apply : eq_functor3. exact : eq_functor3.
  Qed.

  (* option *)
  Definition option_applicative_mixin_of:
    Applicative.mixin_of option_pfunctorMap.
  Proof.
    by apply : (@Applicative.Mixin
                  _ (fun _ _ oF ox
                     => if oF is Some f
                        then if ox is Some x then Some (f x) else None
                        else None))
                 =>/=[|A B C f g fg [x|][y|]|A B C D f g fg [x|][y|][z|]|
                      A B C [f|][g|][x|]||]//; rewrite functor_option fg.
  Defined.
  Definition option_applicative_class_of : @Applicative.class_of option :=
    Applicative.Class option_applicative_mixin_of.
  Canonical option_applicativeMap : applicativeMap :=
    Eval hnf in @Applicative.Pack option option_applicative_class_of.

  Lemma applicative_option :
    @applicative option_applicativeMap =
    fun _ _ oF ox => if oF is Some f
                     then if ox is Some x then Some (f x) else None
                     else None.
  Proof. done. Qed.
End Applicative_canonicals.

(* ********************* *)

Module Monad.
  Definition Mu (m:Type -> Type) := forall A, m (m A) -> m A.

  Record mixin_of (m:pfunctorMap) :=
    Mixin {
        mu : Mu m;
        _: forall A (x:m A), mu (eta _ x) = x;
        _: forall A x,
            mu (functor (@eta _ A) x) = x;
        _: forall A x,
            mu (functor (@mu A) x) = mu (mu x)
      }.
  Section ClassDef.
    Record class_of (m:Type -> Type) :=
      Class {
          base : PFunctor.class_of m;
          mixin : mixin_of (PFunctor.Pack base)
        }.
    Structure map := Pack {apply; _: class_of apply}.
    Variable (cF:map).
    Definition class :=
      let: Pack _ c := cF return class_of (apply cF) in c.
    Definition pureMap := Pure.Pack (base class).
    Definition functorMap := Functor.Pack (base class).
    Definition pfunctorMap := PFunctor.Pack (base class).
  End ClassDef.

  Module Exports.
    Coercion base : class_of >-> PFunctor.class_of.
    Coercion mixin : class_of >-> mixin_of.
    Coercion apply : map >-> Funclass.
    Coercion pureMap : map >-> Pure.map.
    Canonical pureMap.
    Coercion functorMap : map >-> Functor.map.
    Canonical functorMap.
    Coercion pfunctorMap : map >-> PFunctor.map.
    Canonical pfunctorMap.
    Notation monadMap := map.
    Notation Mu := Mu.
    Definition mu T := (mu (class T)).
  End Exports.
End Monad.
Import Monad.Exports.

Section Monad_lemma.
  Variable (m : monadMap).
  Let eta := eta m.

  Lemma mu_eta : forall A (x:m A), mu (eta x) = x.
  Proof. rewrite /eta. by case : m => func [b []]. Qed.

  Lemma mu_functor_eta : forall A x, mu (functor (@eta A) x) = x.
  Proof. rewrite /eta. by case : m => func [b []]. Qed.

  Lemma mu_functor_mu : forall A x, mu (functor (@mu m A) x) = mu (mu x).
  Proof. rewrite /eta. by case : m => func [b []]. Qed.
End Monad_lemma.

Definition eq_monadMap (m:Type -> Type) (c d:Monad.class_of m) :=
  [/\ eq_pureMap c d, eq_functorMap c d &
   forall A, @mu (Monad.Pack c) A =1 @mu (Monad.Pack d) _].

Section Monad_canonicals.
  (* id *)
  Definition id_monad_mixin_of : Monad.mixin_of id_pfunctorMap.
  Proof.
    exact : (@Monad.Mixin _ ((fun _ => id) : Mu id_pfunctorMap)).
  Defined.
  Definition id_monad_class_of : Monad.class_of id :=
    Monad.Class id_monad_mixin_of.
  Definition id_monadMap : monadMap :=
    Eval hnf in @Monad.Pack id id_monad_class_of.

  (* option *)
  Definition option_monad_mixin_of : Monad.mixin_of option_pfunctorMap.
  Proof.
      by apply : (@Monad.Mixin _  (fun _ o => if o is Some x then x else None))
      =>[A [x|]|A [x|]|A [x|]].
  Defined.
  Definition option_monad_class_of : Monad.class_of option :=
    Monad.Class option_monad_mixin_of.
  Canonical option_monadMap : monadMap :=
    Eval hnf in @Monad.Pack option option_monad_class_of.

  Lemma mu_option :
    @mu option_monadMap = fun _ o => if o is Some x then x else None.
  Proof. done. Qed.

  (* seq *)
  Lemma seq_monad_mixin_of : Monad.mixin_of seq_pfunctorMap.
  Proof.
    apply : (@Monad.Mixin _ (@flatten))=>/=[||A].
    - exact : cats0.
    - exact : flatten_seq1.
    - elim =>[|x s IHs]//=. by rewrite flatten_cat -IHs.
  Defined.
  Definition seq_monad_class_of : Monad.class_of seq :=
    Monad.Class seq_monad_mixin_of.
  Canonical seq_monadMap : monadMap :=
    Eval hnf in @Monad.Pack seq seq_monad_class_of.

  Lemma mu_seq : @mu seq_monadMap = @flatten.
  Proof. done. Qed.

End Monad_canonicals.

Section Monad_applicative.
  Variable (m:monadMap).
  Definition hApplicative : Applicative m :=
    fun A B f x => mu (functor (fun x => functor (@^~ x) f) x).
  Definition vApplicative : Applicative m :=
    fun A B f x => mu (functor ((@functor _ _ _)^~ x) f).
End Monad_applicative.

Eval compute in (hApplicative [:: (fun x => x.+1); (fun x =>x.+2)] [:: 10; 20]).
(* = [:: 11; 12; 21; 22] *)
Eval compute in (vApplicative [:: (fun x => x.+1); (fun x =>x.+2)] [:: 10; 20]).
(* = [:: 11; 21; 12; 22] *)

Section Monad_applicative_lemma.
  Definition eq_hvApplicative m :=
    forall A B, @hApplicative m A B =2 @vApplicative _ _ _.

  Lemma id_eq_hvApplicative : eq_hvApplicative id_monadMap.
  Proof. done. Qed.

  Lemma option_eq_hvApplicative : eq_hvApplicative option_monadMap.
  Proof. by move => A B [f|] [x|]. Qed.
End Monad_applicative_lemma.

(* ********************* *)

Module Kleisli.
  Record mixin_of (m:monadMap) :=
    Mixin {
        _: forall A B (f:(A -> B)) x,
          functor f (eta m x) = eta _ (f x);
        _: forall A B (f:A -> B) (x:m (m A)),
            functor f (mu x) = mu (functor (functor f) x)
      }.
  Section ClassDef.
    Record class_of (m:Type -> Type) :=
      Class {
          base : Monad.class_of m;
          mixin : mixin_of (Monad.Pack base)
        }.
    Structure map := Pack {apply; _: class_of apply}.
    Variable (cF:map).
    Definition class :=
      let: Pack _ c := cF return class_of (apply cF) in c.
    Definition pureMap := Pure.Pack (base class).
    Definition functorMap := Functor.Pack (base class).
    Definition pfunctorMap := PFunctor.Pack (base class).
    Definition monadMap := Monad.Pack (base class).
  End ClassDef.

  Module Exports.
    Coercion base : class_of >-> Monad.class_of.
    Coercion mixin : class_of >-> mixin_of.
    Coercion apply : map >-> Funclass.
    Coercion pureMap : map >-> Pure.map.
    Canonical pureMap.
    Coercion functorMap : map >-> Functor.map.
    Canonical functorMap.
    Coercion pfunctorMap : map >-> PFunctor.map.
    Canonical pfunctorMap.
    Coercion monadMap : map >-> Monad.map.
    Canonical monadMap.
    Notation kleisliMap := map.
  End Exports.
End Kleisli.
Import Kleisli.Exports.

Section Kleisli_lemma.
  Variable (m:kleisliMap).
  Let eta := eta m.

  Lemma functor_eta : forall A B (f:A -> B) x,
      functor f (eta x) = eta (f x).
  Proof. rewrite /eta. by case m => func [b []]. Qed.

  Lemma functor_mu : forall A B (f:A -> B) (x:m (m A)),
      functor f (mu x) = mu (functor (functor f) x).
  Proof. rewrite /eta. by case : m => func [b []]. Qed.

  (* *)
  Definition Unit := Eta.
  Definition Bind (m:Type -> Type) := forall A B, m A -> (A -> m B) -> m B.

  Definition unit : Unit m := eta.
  Definition bind : Bind m := fun A B x f => mu (functor f x).

  Lemma eq_bind A B (f g:A -> m B) :
    f =1 g -> (@bind _ _)^~ f =1 (@bind _ _)^~ g.
  Proof. move => fg x. by rewrite /bind (eq_functor fg). Qed.

  Lemma bind_unitr A (x:m A) : bind x (@unit _) = x.
  Proof. exact : mu_functor_eta. Qed.

  Lemma bind_unitl A B x (f:A -> m B) : bind (unit x) f = f x.
  Proof. by rewrite /bind /unit functor_eta mu_eta. Qed.

  Lemma bindA A B C x (f:A -> m B) (g:B -> m C) :
    bind (bind x f) g = bind x (fun y => bind (f y) g).
  Proof. by rewrite /bind functor_mu -mu_functor_mu -!functorD. Qed.

  (* hApplicative *)
  Definition hApplicative_mixin_of : Applicative.mixin_of m.
  Proof.
    apply : (@Applicative.Mixin _ (@hApplicative m))
    =>[A B f x|A B C f g fg x y|A B C D f g fg x y z|
       A B C f g x|A B f x|A B f x];
        rewrite /hApplicative /=.
    - by rewrite (eq_functor (g:= @eta _ \o f))
      =>[|y]/=; rewrite ?functor_eta // functorD mu_functor_eta.
    - congr(mu). apply : eq_functor =>{y} y. rewrite -!functorD.
        by apply : eq_functor =>{x} x /=.
    - congr(mu). apply : eq_functor =>{z} z. rewrite !functor_mu. congr(mu).
      rewrite -!functorD. apply : eq_functor =>{y} y /=.
      rewrite -!functorD. apply : eq_functor =>{x} x /=.
      exact : fg.
    - rewrite functor_mu -mu_functor_mu. congr(mu). rewrite -!functorD.
      apply : eq_functor =>{x} x /=. rewrite functor_mu. congr(mu).
      rewrite -!functorD. apply : eq_functor =>{g} g /=.
      rewrite !functor_mu -!functorD.
        by rewrite (eq_functor (g:= @eta _ \o @^~ (g x)))
        =>[|z]/=; rewrite ?functor_eta // functorD mu_functor_eta.
    - by rewrite !functor_eta mu_eta.
    - by rewrite functor_eta mu_eta.
  Defined.
  Definition hApplicative_class_of : Applicative.class_of m :=
    Applicative.Class hApplicative_mixin_of.
  Definition hApplicativeMap : applicativeMap :=
    @Applicative.Pack m hApplicative_class_of.
  Lemma applicative_hApplicative :
    @applicative hApplicativeMap = @hApplicative m.
  Proof. done. Qed.

  (* vApplicative *)
  Definition vApplicative_mixin_of : Applicative.mixin_of m.
  Proof.
    apply : (@Applicative.Mixin _ (@vApplicative m))
    =>[A B f x|A B C f g fg x y|A B C D f g fg x y z|
       A B C f g x|A B f x|A B f x];
        rewrite /vApplicative /=.
    - by rewrite functor_eta mu_eta.
    - congr(mu). rewrite -!functorD. apply : eq_functor =>{x} x /=.
      exact : eq_functor.
    - congr(mu). rewrite !functor_mu -!functorD. congr(mu).
      apply : eq_functor =>{x} x /=. rewrite -!functorD.
      apply : eq_functor =>{y} y /=. apply : eq_functor =>{z} z /=.
      exact : fg.
    - rewrite functor_eta mu_eta functor_mu -mu_functor_mu -!functorD.
      congr(mu). apply : eq_functor =>{f} f /=. rewrite functor_mu -!functorD.
      congr(mu). apply : eq_functor =>{g} g /=. exact : functorD.
    - by rewrite !functor_eta mu_eta.
    - by rewrite (eq_functor (g:= @eta _ \o @^~ x))
      =>[|y]/=; rewrite ?functor_eta // functorD mu_functor_eta.
  Defined.
  Definition vApplicative_class_of : Applicative.class_of m :=
    Applicative.Class vApplicative_mixin_of.
  Definition vApplicativeMap : applicativeMap :=
    @Applicative.Pack m vApplicative_class_of.
  Lemma applicative_vApplicative :
    @applicative vApplicativeMap = @vApplicative m.
  Proof. done. Qed.
End Kleisli_lemma.

Definition eq_kleisliMap (m:Type -> Type) (c d:Kleisli.class_of m) :=
  eq_monadMap c d.

Section Kleisli_canonicals.
  (* id *)
  Definition id_kleisli_mixin_of : Kleisli.mixin_of id_monadMap.
  Proof. exact : Kleisli.Mixin. Defined.
  Definition id_kleisli_class_of : Kleisli.class_of id :=
    Kleisli.Class id_kleisli_mixin_of.
  Definition id_kleisliMap : kleisliMap :=
    Eval hnf in @Kleisli.Pack id id_kleisli_class_of.

  (* option *)
  Definition option_kleisli_mixin_of : Kleisli.mixin_of option_monadMap.
  Proof.
      by apply : Kleisli.Mixin =>[|A B f [[x|]|]].
  Defined.
  Definition option_kleisli_class_of : Kleisli.class_of option :=
    Kleisli.Class option_kleisli_mixin_of.
  Canonical option_kleisliMap : kleisliMap :=
    Eval hnf in @Kleisli.Pack option option_kleisli_class_of.

  (* seq *)
  Definition seq_kleisli_mixin_of : Kleisli.mixin_of seq_monadMap.
  Proof.
    apply : Kleisli.Mixin =>// A B. exact : map_flatten.
  Defined.
  Definition seq_kleisli_class_of : Kleisli.class_of seq :=
    Kleisli.Class seq_kleisli_mixin_of.
  Canonical seq_kleisliMap : kleisliMap :=
    Eval hnf in @Kleisli.Pack seq seq_kleisli_class_of.

  (* sumt *)
  Definition sumt_monad_mixin_of R (m:kleisliMap) :
    Monad.mixin_of (sumt_pfunctorMap R m).
  Proof.
    apply : (@Monad.Mixin
               _ ((fun _ x => mu (functor
                                  (fun x => match x with
                                            | inl r => eta _ (inl r)
                                            | inr x => x
                                            end) x)) : Mu (sumt R m)))
    =>[A x|A x|A x].
    - by rewrite functor_eta mu_eta.
    - rewrite /eta /= -functorD (eq_functor (g:=@eta _ _)) =>[|[r|y]]//.
        by rewrite mu_functor_eta.
    - rewrite functor_mu -mu_functor_mu -!functorD. congr(mu).
      apply : eq_functor =>{x} [[a|x]]//=.
        by rewrite functor_eta mu_eta.
  Defined.
  Definition sumt_monad_class_of R (m:kleisliMap) : Monad.class_of (sumt R m) :=
    Monad.Class (sumt_monad_mixin_of R m).
  Canonical sumt_monadMap R (m:kleisliMap) : monadMap :=
    Eval hnf in @Monad.Pack (sumt R m) (sumt_monad_class_of R m).

  Lemma mu_sumt R m :
    @mu (sumt_monadMap R m) =
    fun _ x => mu (functor (fun x => match x with
                                     | inl r => eta _ (inl r)
                                     | inr x => x
                                     end) x).
  Proof. done. Qed.

  Definition sumt_kleisli_mixin_of R (m:kleisliMap) :
    Kleisli.mixin_of (sumt_monadMap R m).
  Proof.
    apply : Kleisli.Mixin =>[A B f x|A B f x]/=.
    - by rewrite [functor _ _]functor_eta.
    - rewrite [functor _ _]functor_mu functor_sumt /sumt. congr(mu).
      rewrite -!functorD. apply : eq_functor =>{x}[[a|x]]//=.
        by rewrite functor_eta.
  Defined.
  Definition sumt_kleisli_class_of R (m:kleisliMap) :
    Kleisli.class_of (sumt R m) :=
    Kleisli.Class (sumt_kleisli_mixin_of R m).
  Definition sumt_kleisliMap R (m:kleisliMap) : kleisliMap :=
    Eval hnf in @Kleisli.Pack (sumt R m) (sumt_kleisli_class_of R m).

  (* mult *)
  Definition mult_monad_mixin_of R (idx:R) (op:Monoid.law idx) (m:kleisliMap) :
    Monad.mixin_of (mult_pfunctorMap op m).
  Proof.
    apply : (@Monad.Mixin
               _ ((fun _ x =>
                    mu (functor (fun amx =>
                                   match amx with
                                   | (a,mx) =>
                                     functor (fun bx =>
                                                match bx with
                                                | (b,x) => (op a b,x)
                                                end) mx
                                   end) x)) : Mu (mult_pfunctorMap op m)))
              =>/=[A x|A x|A x].
    - rewrite [functor _ _]functor_eta mu_eta.
      rewrite (eq_functor (g:=id)) ?functor_id // =>[[r y]].
        by rewrite Monoid.mul1m.
    - rewrite -functorD (eq_functor (g:=@eta _ _)) ?mu_functor_eta
      =>[|[r y]]//=. by rewrite functor_eta Monoid.mulm1.
    - rewrite functor_mu -mu_functor_mu -!functorD. congr(mu).
      apply : eq_functor =>[[r y]]/=. rewrite functor_mu -!functorD. congr(mu).
      apply : eq_functor =>[[s z]]/=. rewrite -functorD.
      apply : eq_functor =>[[t w]]/=. by rewrite Monoid.mulmA.
  Defined.
  Definition mult_monad_class_of R (idx:R) (op:Monoid.law idx) (m:kleisliMap) :
    Monad.class_of (mult op m) := Monad.Class (mult_monad_mixin_of op m).
  Canonical mult_monadMap R (idx:R) (op:Monoid.law idx) (m:kleisliMap) :
    monadMap := Eval hnf in @Monad.Pack (mult op m) (mult_monad_class_of op m).

  Lemma mu_mult R (idx:R) (op:Monoid.law idx) (m:kleisliMap) :
    @mu (mult_monadMap op m) =
    (fun _ x =>
       mu (functor (fun amx =>
                      match amx with
                      | (a,mx) =>
                        functor (fun bx =>
                                   match bx with
                                   | (b,x) => (op a b,x)
                                   end) mx
                      end) x)).
  Proof. done. Qed.

  Definition mult_kleisli_mixin_of R (idx:R) (op:Monoid.law idx) (m:kleisliMap):
    Kleisli.mixin_of (mult_monadMap op m).
  Proof.
    apply : Kleisli.Mixin =>/=[A B f x|A B f x].
    - by rewrite [functor _ _]functor_eta.
    - rewrite mu_mult functor_mult functor_mu -!functorD. congr(mu).
      apply : eq_functor =>[[r y]]/=. rewrite -!functorD.
        by apply : eq_functor =>[[]].
  Defined.
  Definition mult_kleisli_class_of R (idx:R) (op:Monoid.law idx) (m:kleisliMap):
    Kleisli.class_of (mult op m) := Kleisli.Class (mult_kleisli_mixin_of op m).
  Canonical mult_kleisliMap R (idx:R) (op:Monoid.law idx) (m:kleisliMap) :
    kleisliMap :=
    Eval hnf in @Kleisli.Pack (mult op m) (mult_kleisli_class_of op m).
End Kleisli_canonicals.

(* ********************* *)

Module AKleisli.
  Section ClassDef.
    Record class_of (t:Type -> Type) :=
      Class {
          base : Kleisli.class_of t;
          mixin : Applicative.mixin_of (PFunctor.Pack base)
        }.
    Definition applicative_class_of t (class:class_of t)
      : Applicative.class_of t :=
      Applicative.Class (mixin class).
    Structure map := Pack {apply; _: class_of apply}.
    Variable (cF:map).
    Definition class :=
      let: Pack _ c := cF return class_of (apply cF) in c.
    Definition pureMap := Pure.Pack (base class).
    Definition functorMap := Functor.Pack (base class).
    Definition pfunctorMap := PFunctor.Pack (base class).
    Definition monadMap := Monad.Pack (base class).
    Definition kleisliMap := Kleisli.Pack (base class).
    Definition applicativeMap := Applicative.Pack (applicative_class_of class).
  End ClassDef.

  Module Exports.
    Coercion base : class_of >-> Kleisli.class_of.
    Coercion mixin : class_of >-> Applicative.mixin_of.
    Coercion apply : map >-> Funclass.
    Coercion pureMap : map >-> Pure.map.
    Canonical pureMap.
    Coercion functorMap : map >-> Functor.map.
    Canonical functorMap.
    Coercion pfunctorMap : map >-> PFunctor.map.
    Canonical pfunctorMap.
    Coercion monadMap : map >-> Monad.map.
    Canonical monadMap.
    Coercion kleisliMap : map >-> Kleisli.map.
    Canonical kleisliMap.
    Coercion applicative_class_of : class_of >-> Applicative.class_of.
    Coercion applicativeMap : map >-> Applicative.map.
    Canonical applicativeMap.
    Notation akleisliMap := map.
  End Exports.
End AKleisli.
Import AKleisli.Exports.

Section AKleisli_lemma.
  Variable (m:kleisliMap).

  Definition hkleisli_class_of : AKleisli.class_of m
    := AKleisli.Class (hApplicative_mixin_of m).
  Definition hkleisli : akleisliMap := @AKleisli.Pack m hkleisli_class_of.

  Definition vkleisli_class_of : AKleisli.class_of m
    := AKleisli.Class (vApplicative_mixin_of m).
  Definition vkleisli : akleisliMap := @AKleisli.Pack m vkleisli_class_of.
End AKleisli_lemma.

(* ********************* *)

Module Sequence.
  Definition Sequence (t:Type -> Type) :=
    forall (m:applicativeMap) A, t (m A) -> m (t A).

  Record mixin_of (t:functorMap) :=
    Mixin {
        sequence:Sequence t;
        _:forall (m:applicativeMap) A B (f:A -> B) (x:t (m A)),
            sequence (functor (functor f) x) =
            functor (functor f) (sequence x)
      }.
  Section ClassDef.
    Record class_of (t:Type -> Type) :=
      Class {
          base : Functor.class_of t;
          mixin : mixin_of (Functor.Pack base)
        }.
    Structure map := Pack {apply; _: class_of apply}.
    Variable (cF:map).
    Definition class :=
      let: Pack _ c := cF return class_of (apply cF) in c.
    Definition functorMap := Functor.Pack (base class).
  End ClassDef.

  Module Exports.
    Coercion base : class_of >-> Functor.class_of.
    Coercion mixin : class_of >-> mixin_of.
    Coercion apply : map >-> Funclass.
    Coercion functorMap : map >-> Functor.map.
    Canonical functorMap.
    Notation sequenceMap := map.
    Notation Sequence := Sequence.
    Definition sequence T := sequence (class T).
  End Exports.
End Sequence.
Import Sequence.Exports.

Section Sequence_lemma.
  Variable (t:sequenceMap).

  Lemma sequence_functor_functor :
    forall (m:applicativeMap) A B (f:A -> B) (x:t (m A)),
      sequence (functor (functor f) x) = functor (functor f) (sequence x).
  Proof. by case : t => func [b []]. Qed.
End Sequence_lemma.

Definition eq_sequenceMap (t:Type -> Type) (c d:Sequence.class_of t) :=
  eq_functorMap c d /\
  forall m A,
    @sequence (Sequence.Pack c) m A =1 @sequence (Sequence.Pack d) m _.

Section Sequence_canonicals.
  (* id *)
  Definition id_sequence_mixin_of : Sequence.mixin_of id_functorMap.
  Proof.
    exact : (@Sequence.Mixin _ ((fun _ _ => id) : Sequence id_functorMap)).
  Defined.
  Definition id_sequence_class_of : Sequence.class_of id :=
    Sequence.Class id_sequence_mixin_of.
  Definition id_sequenceMap : sequenceMap :=
    Eval hnf in @Sequence.Pack id id_sequence_class_of.

  (* comp *)
  Definition comp_sequnece_mixin_of (t s:sequenceMap) :
    Sequence.mixin_of (comp_functorMap t s).
  Proof.
    apply : (@Sequence.Mixin
               _ ((fun _ _ => @sequence _ _ _ \o functor (@sequence _ _ _))
                  : Sequence (comp_functorMap t s)))=>/= m A B f x.
    rewrite -sequence_functor_functor -!functorD. congr (sequence).
    apply : eq_functor => y /=. by rewrite sequence_functor_functor.
  Defined.
  Definition comp_sequence_class_of (t s:sequenceMap) :
    Sequence.class_of (fun A => t (s A)) :=
    Sequence.Class (comp_sequnece_mixin_of t s).
  Definition comp_sequenceMap (t s:sequenceMap) : sequenceMap :=
    Eval hnf in @Sequence.Pack (fun A => t (s A)) (comp_sequence_class_of t s).

  Lemma sequence_comp t s :
    @sequence (comp_sequenceMap t s) =
    fun _ _ => @sequence _ _ _ \o functor (@sequence _ _ _).
  Proof. done. Qed.

  (* option *)
  Definition option_sequence_mixin_of : Sequence.mixin_of option_functorMap.
  Proof.
    apply : (@Sequence.Mixin
               _ (fun _ _ o =>
                    if o is Some x then functor (@Some _) x else eta _ None))
    => m A B f [x|]/=.
    - by rewrite -!functorD.
    - by rewrite -applicative_etal applicative_eta_eta.
  Defined.
  Definition option_sequence_class_of : Sequence.class_of option :=
    Sequence.Class option_sequence_mixin_of.
  Canonical option_sequenceMap : sequenceMap :=
    Eval hnf in @Sequence.Pack option option_sequence_class_of.

  Lemma sequence_option :
    @sequence option_sequenceMap =
    fun _ _ o => if o is Some x then functor (@Some _) x else eta _ None.
  Proof. done. Qed.

  (* seq *)
  Definition seq_sequence_mixin_of : Sequence.mixin_of seq_functorMap.
  Proof.
    apply : (@Sequence.Mixin
               _ (fun _ _ => foldr (functor2 cons) (eta _ [::])))
    => m A B f /=.
    elim =>[|x s /=->].
    - by rewrite -applicative_etal applicative_eta_eta.
    - rewrite /functor2 -!applicative_etal -applicativeA applicative_etar.
      do ! rewrite -applicativeA !applicative_eta_eta.
         rewrite !applicative_etal -functorD. exact : eq_functor2.
  Defined.
  Definition seq_sequence_class_of : Sequence.class_of seq :=
    Sequence.Class seq_sequence_mixin_of.
  Canonical seq_sequenceMap : sequenceMap :=
    Eval hnf in @Sequence.Pack seq seq_sequence_class_of.

  Lemma sequence_seq :
    @sequence seq_sequenceMap = fun _ _ => foldr (functor2 cons) (eta _ [::]).
  Proof. done. Qed.

  (* sumt *)
  Definition sumt_sequence_mixin_of R (t:sequenceMap):
    Sequence.mixin_of (sumt_functorMap R t).
  Proof.
    apply : (@Sequence.Mixin
               _ ((fun m _ f =>
                     sequence (functor (fun rma =>
                                          match rma with
                                          | inl r => eta _ (inl r)
                                          | inr ma => @functor m _ _ inr ma
                                          end) f))
                  : Sequence (sumt_functorMap R t)))=>[m A B f x].
    rewrite -sequence_functor_functor -!functorD. congr(sequence).
    apply : eq_functor =>{x} [[r|x]]/=.
    - by rewrite -applicative_etal applicative_eta_eta.
    - rewrite -!functorD. exact : eq_functor.
  Defined.
  Definition sumt_sequence_class_of R (t:sequenceMap) :
    Sequence.class_of (sumt R t) :=
    Sequence.Class (sumt_sequence_mixin_of R t).
  Canonical sumt_sequenceMap R (t:sequenceMap) : sequenceMap :=
    Eval hnf in @Sequence.Pack (sumt R t) (sumt_sequence_class_of R t).

  Lemma sequence_sumt R (t:sequenceMap) :
    @sequence (sumt_sequenceMap R t) =
    fun m _ f => sequence (functor (fun rma => match rma with
                                               | inl r => eta _ (inl r)
                                               | inr ma => @functor m _ _ inr ma
                                               end) f).
  Proof. done. Qed.

  (* mult *)
  Definition mult_sequence_mixin_of R (idx:R) (op:Monoid.law idx)
             (t:sequenceMap): Sequence.mixin_of (mult_functorMap op t).
  Proof.
    apply : (@Sequence.Mixin
               _ ((fun _ _ f =>
                    sequence (functor (fun rma =>
                                         match rma with
                                         | (r,ma) => functor (pair r) ma
                                         end) f)) : Sequence (mult op t)))
    => m A B f x.
    rewrite -sequence_functor_functor -!functorD. congr(sequence).
    apply : eq_functor =>[[r ma]]/=. rewrite -!functorD.
    exact : eq_functor.
  Defined.
  Definition mult_sequence_class_of R (idx:R) (op:Monoid.law idx)
             (t:sequenceMap) : Sequence.class_of (mult op t) :=
    Sequence.Class (mult_sequence_mixin_of op t).
  Canonical mult_sequenceMap R (idx:R) (op:Monoid.law idx) (t:sequenceMap):
    sequenceMap :=
    Eval hnf in @Sequence.Pack (mult op t) (mult_sequence_class_of op t).

  Lemma sequence_mult R (idx:R) (op:Monoid.law idx) (t:sequenceMap) :
    @sequence (mult_sequenceMap op t) =
    fun _ _ f => sequence (functor (fun rma =>
                                      match rma with
                                      | (r,ma) => functor (pair r) ma
                                      end) f).
  Proof. done. Qed.
End Sequence_canonicals.

(* ********************* *)

Module Traversable.
  Definition Traverse (t:Type -> Type) :=
    forall (m:applicativeMap) A B, (A -> m B) -> t A -> m (t B).

  Record mixin_of (t:sequenceMap) :=
    Mixin {
        _: forall (m:Type -> Type) (c d:Applicative.class_of m),
            eq_applicativeMap c d ->
            forall A,
              @sequence t (Applicative.Pack c) A
              =1 @sequence t (Applicative.Pack d) A;
        _: forall A, @sequence t id_applicativeMap A =1 @id _;
        _: forall (m n:applicativeMap) A (x:t (m (n A))),
            @sequence t (comp_applicativeMap _ _) _ x =
            functor (@sequence _ _ _) (sequence x)
      }.
  Section ClassDef.
  Record class_of (t:Type -> Type) :=
    Class {
        base : Sequence.class_of t;
        mixin : mixin_of (Sequence.Pack base)
      }.
    Structure map := Pack {apply; _: class_of apply}.
    Variable (cF : map).
    Definition class :=
      let: Pack _ c := cF return class_of (apply cF) in c.
    Definition functorMap := Functor.Pack (base class).
    Definition sequenceMap := Sequence.Pack (base class).
  End ClassDef.

  Module Exports.
    Coercion base : class_of >-> Sequence.class_of.
    Coercion mixin : class_of >-> mixin_of.
    Coercion apply : map >-> Funclass.
    Coercion functorMap : map >-> Functor.map.
    Canonical functorMap.
    Coercion sequenceMap : map >-> Sequence.map.
    Canonical sequenceMap.
    Notation traverseMap := map.
    Notation Traverse := Traverse.
  End Exports.
End Traversable.
Import Traversable.Exports.

Section Traversable_lemma.
  Variable (t:traverseMap).

  Lemma sequence_eq_applicativeMap : forall m (c d:Applicative.class_of m),
      eq_applicativeMap c d ->
      forall A,
        @sequence t (Applicative.Pack c) A
        =1 @sequence _ (Applicative.Pack d) A.
  Proof. by case : t => func [b []]. Qed.

  Lemma sequence_id : forall A, @sequence t id_applicativeMap A =1 @id _.
  Proof. by case : t => func [b []]. Qed.

  Lemma sequenceD : forall (m n:applicativeMap) A (x:t (m (n A))),
      @sequence t (comp_applicativeMap _ _) _ x =
      functor (@sequence _ _ _) (sequence x).
  Proof. by case : t => func [b []]. Qed.

  Definition traverse : Traverse t := fun _ _ _ f x => sequence (functor f x).

  Lemma traverse_eq_applicativeMap m (c d:Applicative.class_of m) :
    eq_applicativeMap c d ->
    forall A B (f:A -> m B),
      @traverse (Applicative.Pack c) _ _ f
      =1 @traverse (Applicative.Pack d) _ _ f.
  Proof. move => cd A B f x. exact : sequence_eq_applicativeMap. Qed.

  Lemma eq_traverse : forall (m:applicativeMap) A B (f g:A -> m B),
      f =1 g -> traverse f =1 traverse g.
  Proof. rewrite /traverse => m A B f g fg x. by rewrite (eq_functor fg). Qed.

  Lemma traverse_id A B : @traverse id_applicativeMap A B =2 @functor t _ _.
  Proof. rewrite /traverse => f x. by rewrite sequence_id. Qed.

  Lemma traverseD (m n:applicativeMap) A B C (f:B -> m C) (g:A -> n B) x :
    @traverse (comp_applicativeMap _ _) _ _ (functor f \o g) x
    = functor (traverse f) (traverse g x).
  Proof.
    rewrite /traverse sequenceD [functor (_ \o g) _]functorD.
      by rewrite sequence_functor_functor -functorD.
  Qed.

  Lemma traverse_compf (m:applicativeMap) A B C (f:B -> m C) (g:A -> B) x :
    traverse (f \o g) x = traverse f (functor g x).
  Proof. by rewrite /traverse functorD. Qed.

  Lemma traverse_functor_comp
        (m:applicativeMap) A B C (f:B -> C) (g:A -> m B) x :
    traverse (functor f \o g) x = functor (functor f) (traverse g x).
  Proof. by rewrite /traverse functorD sequence_functor_functor. Qed.

  Lemma sequence_def (m:applicativeMap) A (x:t (m A)):
    sequence x = traverse id x.
  Proof. by rewrite /traverse functor_id. Qed.

End Traversable_lemma.

Definition eq_traverseMap (t:Type -> Type) (c d:Traversable.class_of t) :=
  eq_sequenceMap c d.

Section Traversable_canonicals.
  (* id *)
  Definition id_traverse_mixin_of : Traversable.mixin_of id_sequenceMap.
  Proof.
    apply : Traversable.Mixin =>//= m n A x. by rewrite functor_id.
  Defined.
  Definition id_traverse_class_of : Traversable.class_of id :=
    Traversable.Class id_traverse_mixin_of.
  Definition id_traverseMap : traverseMap :=
    Eval hnf in @Traversable.Pack id id_traverse_class_of.

  (* comp *)
  Definition comp_traverse_mixin_of (t s:traverseMap) :
    Traversable.mixin_of (comp_sequenceMap t s).
  Proof.
    apply : Traversable.Mixin =>/=[m c d cd A x|A x|m n A x];
      rewrite sequence_comp /=.
    - rewrite (sequence_eq_applicativeMap cd).
      congr(@sequence t (Applicative.Pack d)). apply : eq_functor => y.
        by rewrite (sequence_eq_applicativeMap cd).
    - rewrite sequence_id. apply : eq_functor_id. exact : sequence_id.
    - rewrite sequenceD functorD -sequence_functor_functor -functorD.
      congr(functor _ (sequence _)). apply : eq_functor => y /=.
      exact : sequenceD.
  Defined.
  Definition comp_traverse_class_of (m n:traverseMap) :
    Traversable.class_of (fun A => m (n A)) :=
    Traversable.Class (comp_traverse_mixin_of m n).
  Definition comp_traverseMap (m n:traverseMap) : traverseMap :=
    Eval hnf in @Traversable.Pack (fun A => m (n A))
                                  (comp_traverse_class_of m n).

  (* option *)
  Definition option_traverse_mixin_of:
    Traversable.mixin_of option_sequenceMap.
  Proof.
    apply : Traversable.Mixin =>/=[m c d cd A [x|]|A [x|]|m n A [x|]]//;
                              rewrite sequence_option.
    - by case : cd =>[[_ ->] _].
    - by case : cd =>[[-> _] _].
    - rewrite -functorD. exact : eq_functor.
    - by rewrite -applicative_etal applicative_eta_eta.
  Defined.
  Definition option_traverse_class_of : Traversable.class_of option :=
    Traversable.Class option_traverse_mixin_of.
  Canonical option_traverseMap : traverseMap :=
    Eval hnf in @Traversable.Pack option option_traverse_class_of.

  (* seq *)
  Lemma eq_foldr T R (f g:T -> R -> R):
    f =2 g -> foldr f =2 foldr g.
  Proof. move => fg z. by elim =>[|x s /=->]. Qed.

  Definition seq_traverse_mixin_of:
    Traversable.mixin_of seq_sequenceMap.
  Proof.
    apply : Traversable.Mixin =>/=[m c d cd A s|A|m n A];
      rewrite sequence_seq.
    - rewrite /functor2. case : cd =>[[-> cdf] cda]. apply : eq_foldr => y z.
        by rewrite cdf cda.
    - by elim =>[|x s /=->].
    - rewrite /functor2 eta_comp functor_comp applicative_comp /=.
      elim =>[|x s /=->]//=.
      + by rewrite -applicative_etal applicative_eta_eta.
      + rewrite /functor2 -functorD -!applicative_etal -applicativeA.
        rewrite applicative_etar !applicative_etal -!functorD -applicative_etal.
        rewrite -applicativeA applicative_eta_eta applicative_etal -functorD.
        exact : eq_functor2.
  Defined.
  Definition seq_traverse_class_of : Traversable.class_of seq :=
    Traversable.Class seq_traverse_mixin_of.
  Canonical seq_traverseMap : traverseMap :=
    Eval hnf in @Traversable.Pack seq seq_traverse_class_of.

  (* sumt *)
  Definition sumt_traverse_mixin_of R (t:traverseMap):
    Traversable.mixin_of (sumt_sequenceMap R t).
  Proof.
    apply : Traversable.Mixin =>/=[m c d cd A x|A x|m n A x];
      rewrite sequence_sumt.
    - rewrite (sequence_eq_applicativeMap cd).
      case : cd =>[[eta_cd fun_cd] app_cd].
      congr(@sequence t (Applicative.Pack d)). apply : eq_functor =>[[r|ma]].
      + exact : eta_cd.
      + exact : fun_cd.
    - rewrite sequence_id. exact : eq_functor_id.
    - rewrite functorD sequenceD. congr(functor).
      rewrite -(@sequence_functor_functor t) -functorD. congr(sequence).
      apply : eq_functor =>[[r|ma]]/=.
      + by rewrite -applicative_etal applicative_eta_eta.
      + rewrite -functorD. exact : eq_functor.
  Defined.
  Definition sumt_traverse_class_of R (t:traverseMap):
    Traversable.class_of (sumt R t) :=
    Traversable.Class (sumt_traverse_mixin_of R t).
  Canonical sumt_traverseMap R (t:traverseMap) : traverseMap :=
    Eval hnf in @Traversable.Pack (sumt R t) (sumt_traverse_class_of R t).

  (* mult *)
  Definition mult_traverse_mixin_of R (idx:R) (op:Monoid.law idx)
             (t:traverseMap): Traversable.mixin_of (mult_sequenceMap op t).
  Proof.
    apply : Traversable.Mixin =>[m c d cd A x|A x|m n A x];
                                  rewrite sequence_mult.
    - rewrite (sequence_eq_applicativeMap cd).
      case : cd =>[[_ fun_cd] _].
      congr(@sequence t (Applicative.Pack d)). apply : eq_functor =>[[r ma]].
      exact : fun_cd.
    - rewrite sequence_id. apply : eq_functor_id. exact : eq_functor_id.
    - rewrite functorD sequenceD. congr(@functor m).
      rewrite -(@sequence_functor_functor t) -functorD. congr(sequence).
      apply : eq_functor =>[[r ma]]/=. rewrite -functorD.
      exact : eq_functor.
  Defined.
  Definition mult_traverse_class_of R (idx:R) (op:Monoid.law idx)
             (t:traverseMap) : Traversable.class_of (mult op t) :=
    Traversable.Class (mult_traverse_mixin_of op t).
  Canonical mult_traverseMap R (idx:R) (op:Monoid.law idx) (t:traverseMap):
    traverseMap :=
    Eval hnf in @Traversable.Pack (mult op t) (mult_traverse_class_of op t).
End Traversable_canonicals.

(* ********************* *)

Module RCompKleisli.
  Record mixin_of (t:kleisliMap) (sequence:Sequence t) :=
    Mixin {
        _: forall (m:akleisliMap) A (x:m A),
          sequence _ _ (eta _ x) = functor (@eta _ _) x;
        _: forall (m:akleisliMap) A (x:t A),
            sequence _ _ (functor (@eta m _) x) = eta _ x;
        _: forall (m:akleisliMap) A (x:t (t (m A))),
            sequence _ _ (mu x) =
            functor (@mu _ _) (sequence _ _ (functor (sequence _ _) x));
        _: forall (m:akleisliMap) A (x:t (m (m A))),
            sequence  _ _ (functor (@mu _ _) x) =
            mu (functor (sequence _ _) (sequence _ _ x))
      }.
  Section ClassDef.
    Record class_of (t:Type -> Type) :=
      Class {
          base : Kleisli.class_of t;
          sMixin : Sequence.mixin_of (Functor.Pack base);
          mixin : @mixin_of (Kleisli.Pack base) (Sequence.sequence sMixin)
        }.
    Definition sequence_class_of t class :=
      Sequence.Class (@sMixin t class).
    Structure map := Pack {apply; _: class_of apply}.
    Variable (cF : map).
    Definition class :=
      let: Pack _ c := cF return class_of (apply cF) in c.
    Definition pureMap := Pure.Pack (base class).
    Definition functorMap := Functor.Pack (base class).
    Definition pfunctorMap := PFunctor.Pack (base class).
    Definition monadMap := Monad.Pack (base class).
    Definition kleisliMap := Kleisli.Pack (base class).
    Definition sequenceMap := Sequence.Pack (sequence_class_of class).
  End ClassDef.

  Module Exports.
    Coercion base : class_of >-> Kleisli.class_of.
    Coercion sMixin : class_of >-> Sequence.mixin_of.
    Coercion mixin : class_of >-> mixin_of.
    Coercion apply : map >-> Funclass.
    Coercion pureMap : map >-> Pure.map.
    Canonical pureMap.
    Coercion functorMap : map >-> Functor.map.
    Canonical functorMap.
    Coercion pfunctorMap : map >-> PFunctor.map.
    Canonical pfunctorMap.
    Coercion monadMap : map >-> Monad.map.
    Canonical monadMap.
    Coercion kleisliMap : map >-> Kleisli.map.
    Canonical kleisliMap.
    Coercion sequence_class_of : class_of >-> Sequence.class_of.
    Coercion sequenceMap : map >-> Sequence.map.
    Canonical sequenceMap.
    Notation rcompKleisliMap := map.
  End Exports.
End RCompKleisli.
Import RCompKleisli.Exports.

Section RCompKleisli_lemma.
  Variable (t:rcompKleisliMap).
  Let sequence := @sequence t.

  Lemma sequence_eta : forall (m:akleisliMap) A (x:m A),
      sequence (eta t x) = functor (@eta _ _) x.
  Proof. rewrite /sequence. by case : t => func [b sm []]. Qed.

  Lemma sequence_functor_eta : forall (m:akleisliMap) A (x:t A),
      sequence (functor (@eta m _) x) = eta m x.
  Proof. rewrite /sequence. by case : t => func [b sm []]. Qed.

  Lemma sequence_mu : forall (m:akleisliMap) A (x:t (t (m A))),
      sequence (@mu t _ x) =
      functor (@mu t _) (sequence (functor (@sequence _ _) x)).
  Proof. rewrite /sequence. by case : t => func [b sm []]. Qed.

  Lemma sequence_functor_mu : forall (m:akleisliMap) A (x:t (m (m A))),
      sequence (functor (@mu _ _) x) =
      mu (functor (@sequence _ _) (sequence x)).
  Proof. rewrite /sequence. by case : t => func [b sm []]. Qed.
End RCompKleisli_lemma.

Definition rcomp_monad_class_of (m:akleisliMap) (t:rcompKleisliMap):
  Monad.class_of (fun A => m (t A)).
Proof.
  apply : (@Monad.Class _ (comp_pfunctor_class_of m t)).
  apply : (@Monad.Mixin
             _ ((fun _ => functor (@mu _ _) \o (@mu _ _) \o
                                  functor (@sequence t m _)) :
                  Mu (comp_pfunctorMap m t)))
            =>/=[A x|A x|A x].
  - rewrite eta_comp /= functor_eta mu_eta sequence_eta -functorD.
    rewrite (eq_functor (g:=id)) ?functor_id =>// y /=.
      by rewrite mu_eta.
  - rewrite functor_comp eta_comp /= -functorD.
    rewrite (eq_functor (g:= @eta m _ \o functor (@eta t _)))=>[|y]/=.
    + rewrite functorD mu_functor_eta -functorD.
      rewrite (eq_functor (g:=id)) ?functor_id =>// y /=.
        by rewrite mu_functor_eta.
    + by rewrite functorD sequence_functor_eta.
  - rewrite !functor_mu -!functorD -mu_functor_mu -functorD. congr(mu).
    apply : eq_functor =>{x} x /=.
    rewrite 2!functorD sequence_functor_functor sequence_functor_mu.
    rewrite !functor_mu sequence_functor_functor -!functorD. congr(mu).
    apply : eq_functor =>{x} x /=.
    rewrite sequence_mu -!functorD. apply : eq_functor =>{x} x /=.
      by rewrite mu_functor_mu.
Defined.

Definition rcomp_kleisli_class_of (m:akleisliMap) (t:rcompKleisliMap):
  Kleisli.class_of (fun A => m (t A)).
Proof.
  apply : (@Kleisli.Class _ (rcomp_monad_class_of m t)).
  apply : Kleisli.Mixin =>/=[A B f x|A B f x].
  - by rewrite functor_comp eta_comp /= !functor_eta.
  - rewrite !functor_comp /mu /= -!functorD.
    rewrite (eq_functor (g:= @mu t _ \o functor (functor f)))
    =>[|y]/=; [|by rewrite functor_mu].
    rewrite (eq_functor
               (g:=functor (functor (functor f)) \o @sequence t m _))
    =>[|y]/=; [|by rewrite sequence_functor_functor].
    rewrite 2!functorD. congr (functor). by rewrite functor_mu.
Defined.
Definition rcomp_kleisliMap (m:akleisliMap) (t:rcompKleisliMap) :=
  Eval hnf in @Kleisli.Pack (fun A => m (t A)) (rcomp_kleisli_class_of m t).

Definition rcomp_hkleisliMap (m:kleisliMap) (t:rcompKleisliMap) :=
  rcomp_kleisliMap (hkleisli m) t.
Definition rcomp_vkleisliMap (m:kleisliMap) (t:rcompKleisliMap) :=
  rcomp_kleisliMap (vkleisli m) t.

Section RCompKleisli_canonicals.
  (* id *)
  Definition id_rcompKleisli_mixin_of :
    @RCompKleisli.mixin_of
      id_kleisliMap (Sequence.sequence id_sequence_mixin_of).
  Proof.
      by apply : RCompKleisli.Mixin
                   =>/=[m A x||m A x|m A x]//; rewrite !functor_id.
  Defined.
  Definition id_rcompKleisli_class_of : RCompKleisli.class_of id :=
    RCompKleisli.Class id_rcompKleisli_mixin_of.
  Definition id_rcompKleisliMap : rcompKleisliMap :=
    Eval hnf in @RCompKleisli.Pack id id_rcompKleisli_class_of.

  (* option *)
  Definition option_rcompKleisli_mixin_of :
    @RCompKleisli.mixin_of
      option_kleisliMap (Sequence.sequence option_sequence_mixin_of).
  Proof.
    apply : RCompKleisli.Mixin =>[|m A [x|]|m A [[x|]|]|m A [x|]]//=.
    - by rewrite functor_eta.
    - rewrite -!functorD. exact : eq_functor.
    - by rewrite -functorD functor_eta.
    - by rewrite functor_eta.
    - by rewrite functor_mu -functorD.
    - by rewrite functor_eta mu_eta.
  Defined.
  Definition option_rcompKleisli_class_of : RCompKleisli.class_of option :=
    RCompKleisli.Class option_rcompKleisli_mixin_of.
  Definition option_rcompKleisliMap : rcompKleisliMap :=
    Eval hnf in @RCompKleisli.Pack option option_rcompKleisli_class_of.
(*
  (* seq *)
  Definition seq_rcompKleisli_mixin_of :
    @RCompKleisli.mixin_of
      seq_kleisliMap (Sequence.sequence seq_sequence_mixin_of).
  Proof.
    apply : RCompKleisli.Mixin =>/=[m A x|m A|m A|m A]//=;
    rewrite /functor2.
    - by rewrite /functor2 applicative_etar -functorD.
    - elim =>[|x s /=->]//. by rewrite applicative_etar !functor_eta.
    - rewrite /mu /=. elim =>[|s ss IHss]/=.
      + by rewrite functor_eta.
      + rewrite foldr_cat IHss foldr_map -!applicative_etal -applicativeA.
        rewrite applicative_eta_eta !applicative_etal -functorD.
        elim : s {IHss} =>[|x s /=->]//=.
        * rewrite functor_eta applicative_etal /=. exact : eq_functor.
        * rewrite -!applicative_etal -2!applicativeA !applicative_etal.
          rewrite applicative_etar -!functorD -applicative_etal.
          rewrite -applicativeA applicative_eta_eta applicative_etal.
          rewrite -functorD. exact : eq_functor3.
    - elim =>[|x s /=->]//=.
      + by rewrite functor_eta mu_eta.
      + rewrite -!applicative_etal -applicativeA applicative_eta_eta.
        rewrite !applicative_etal -functorD.
 *)

  (* sumt *)
  Definition sumt_rcompKleisli_mixin_of R (t:rcompKleisliMap):
    @RCompKleisli.mixin_of
      (sumt_kleisliMap R t) (Sequence.sequence (sumt_sequence_mixin_of R t)).
  Proof.
    apply : RCompKleisli.Mixin =>[m A x|m A x|m A x|m A x]/=.
    - by rewrite functor_eta [in RHS]functorD sequence_eta.
    - rewrite -functorD -sequence_functor_eta. congr(@sequence t).
      apply : eq_functor =>[[r|a]]//=. by rewrite functor_eta.
    - rewrite functor_mu sequence_mu [in RHS]functorD. congr(functor).
      rewrite -(@sequence_functor_functor t) -!functorD. congr(sequence).
      apply : eq_functor =>[[r|y]]/=.
      + by rewrite !functor_eta sequence_eta functor_eta.
      + by rewrite -functorD eq_functor_id.
    - rewrite [in RHS]functorD -(@sequence_functor_functor t).
      rewrite -sequence_functor_mu -!functorD. congr(@sequence t).
      apply : eq_functor =>[[r|ma]]/=.
      + by rewrite functor_eta mu_eta.
      + by rewrite -functorD functor_mu.
  Defined.
  Definition sumt_rcompKleisli_class_of R (t:rcompKleisliMap) :
    RCompKleisli.class_of (sumt R t) :=
    RCompKleisli.Class (sumt_rcompKleisli_mixin_of R t).
  Definition sumt_rcompKleisliMap R (t:rcompKleisliMap) : rcompKleisliMap :=
    Eval hnf in @RCompKleisli.Pack (sumt R t) (sumt_rcompKleisli_class_of R t).

  (* mult *)
  Definition mult_rcompKleisli_mixin_of R (idx:R) (op:Monoid.law idx)
             (t:rcompKleisliMap):
    @RCompKleisli.mixin_of
      (mult_kleisliMap op t) (Sequence.sequence (mult_sequence_mixin_of op t)).
  Proof.
    apply : RCompKleisli.Mixin =>[m A x|m A x|m A x|m A x]/=.
    - by rewrite functor_eta sequence_eta -functorD.
    - rewrite -functorD -sequence_functor_eta. congr(@sequence t).
      apply : eq_functor =>[[r ma]]/=. by rewrite functor_eta.
    - rewrite functor_mu sequence_mu [in RHS]functorD. congr(functor).
      rewrite -(@sequence_functor_functor t) -!functorD. congr(sequence).
      apply : eq_functor =>[[r ma]]/=. rewrite -!functorD.
      rewrite (eq_functor
                 (g:=functor
                       (fun bx : _ * _ => let (b,x) := bx in (op r b,x))))=>//.
      rewrite -sequence_functor_functor -functorD. congr(sequence).
      apply : eq_functor =>[[s a]]/=. by rewrite -functorD.
    - rewrite [in RHS]functorD -(@sequence_functor_functor t).
      rewrite -sequence_functor_mu -!functorD. congr(@sequence t).
      apply : eq_functor =>[[r ma]]/=. by rewrite functor_mu -functorD.
  Defined.
  Definition mult_rcompKleisli_class_of R (idx:R) (op:Monoid.law idx)
             (t:rcompKleisliMap) : RCompKleisli.class_of (mult op t) :=
    RCompKleisli.Class (mult_rcompKleisli_mixin_of op t).
  Definition mult_rcompKleisliMap R (idx:R) (op:Monoid.law idx)
             (t:rcompKleisliMap) : rcompKleisliMap :=
    Eval hnf in
      @RCompKleisli.Pack (mult op t) (mult_rcompKleisli_class_of op t).
End RCompKleisli_canonicals.

author: nekonistyle

repo: monad-in-Coq