From Tealeaves Require Export
  Functors.List
  Functors.Early.Environment
  Classes.Kleisli.Theory.DecoratedTraversableFunctor.

Import Subset.Notations.
Import DecoratedContainerFunctor.Notations.
Import List.ListNotations.
Import Monoid.Notations.

Section env_instance.

  Context {E: Type}.

  #[export] Instance ToCtxset_env: ToCtxset E (env E) :=
    fun (A: Type) (s: env E A) ⇒
      tosubset (F := list) s.

  #[export] Instance Compat_ToCtxset_Mapdt_env:
    Compat_ToCtxset_Mapdt E (env E).
  Proof.
    unfold Compat_ToCtxset_Mapdt.
    unfold ToCtxset_env.
    unfold ToCtxset_Mapdt.
    ext A l.
    unfold mapdReduce.
    unfold mapdt.
    unfold Mapdt_env.
    induction l.
    - reflexivity.
    - destruct a as [e a].
      rewrite tosubset_list_cons.
      cbn.
      unfold_ops @Pure_const @Map_const.
      unfold_ops @Monoid_op_subset @Monoid_unit_subset.
      rewrite IHl.
      fequal.
      simpl_subset.
      reflexivity.
  Qed.

  Lemma toctxset_env_nil: ∀ (A: Type),
      toctxset (F := env E) (@nil (E × A)) = subset_empty.
  Proof.
    reflexivity.
  Qed.

  Lemma toctxset_env_one: ∀ (A: Type) (e: E) (a: A),
      toctxset (F := env E) [(e, a)] = {{ (e, a) }}.
  Proof.
    intros. unfold_ops @ToCtxset_env.
    simpl_list. simpl_subset.
    reflexivity.
  Qed.

  Lemma toctxset_env_cons: ∀ (A: Type) (e: E) (a: A) (l: env E A),
      toctxset (F := env E) ((e, a) :: l) =
        {{(e, a)}} ∪ (toctxset l).
  Proof.
    reflexivity.
  Qed.

  Lemma toctxset_env_app: ∀ (A: Type) (l1 l2: env E A),
      toctxset (F := env E) (l1 ++ l2) =
        toctxset l1 ∪ toctxset l2.
  Proof.
    intros. unfold_ops @ToCtxset_env.
    simpl_list.
    reflexivity.
  Qed.

  #[export] Instance Natural_ToCtxset_env:
    Natural (@toctxset E (env E) _).
  Proof.
    constructor.
    - try typeclasses eauto.
    - typeclasses eauto.
    - unfold_ops @ToCtxset_env.
      intros.
      rewrite ctxset_map_spec.
      rewrite (natural (A := E × A)
                 (B := E × B)
                 (ϕ := @tosubset list _)).
      rewrite env_map_spec.
      reflexivity.
  Qed.

  #[export] Instance DecoratedHom_toctxset_env:
    DecoratedHom E (env E) (ctxset E) (@toctxset E (env E) _).
  Proof.
    constructor. intros.
    ext Γ [e b].
    unfold_ops @ToCtxset_env @Mapd_ctxset.
    unfold compose.
    induction Γ.
    - cbn. propext.
      + intros [a [contra heq]]. contradiction.
      + contradiction.
    - destruct a as [e' a].
      change_right ((e', f (e', a)) = (e, b) ∨ (e, b) ∈d mapd f Γ).
      setoid_rewrite <- IHΓ; clear IHΓ.
      autorewrite with tea_list.
      propext.
      + intros [a' [[Hin|Hin] Heq]].
        × left.
          autorewrite with tea_set in ×.
          now inversion Hin; subst.
        × right.
          now (∃ a').
      + intros [Heq | [a' [Hin Heq]]].
        × inversion Heq; subst. ∃ a.
          autorewrite with tea_set.
          intuition.
        × ∃ a'.
          autorewrite with tea_set.
          intuition.
  Qed.

End env_instance.