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.

(** * Decorated Container Instance for <<env>> *)
(**********************************************************************)
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).
E: Type
Compat_ToCtxset_Mapdt E (env E)
  Proof.
E: Type
Compat_ToCtxset_Mapdt E (env E)
    unfold Compat_ToCtxset_Mapdt.
E: Type
ToCtxset_env = ToCtxset_Mapdt
    unfold ToCtxset_env.
E: Type
(fun (A : Type) (s : env E A) => tosubset s) =
ToCtxset_Mapdt
    unfold ToCtxset_Mapdt.
E: Type
(fun (A : Type) (s : env E A) => tosubset s) =
(fun A : Type => mapdReduce ret)
    ext A l.
E, A: Type
l: env E A
tosubset l = mapdReduce ret l
    unfold mapdReduce.
E, A: Type
l: env E A
tosubset l = mapdt ret l
    unfold mapdt.
E, A: Type
l: env E A
tosubset l =
Mapdt_env E (const (E * A -> Prop)) Map_const
  Pure_const Mult_const A False ret l
    unfold Mapdt_env.
E, A: Type
l: env E A
tosubset l = mapdt_env E (const (E * A -> Prop)) ret l
    induction l.
E, A: Type
tosubset [] =
mapdt_env E (const (E * A -> Prop)) ret []
E, A: Type
a: E * A
l: list (E * A)
IHl: tosubset l = mapdt_env E (const (E * A -> Prop)) ret l
tosubset (a :: l) =
mapdt_env E (const (E * A -> Prop)) ret (a :: l)
    -
E, A: Type
tosubset [] =
mapdt_env E (const (E * A -> Prop)) ret [] reflexivity.
    -
E, A: Type
a: E * A
l: list (E * A)
IHl: tosubset l = mapdt_env E (const (E * A -> Prop)) ret l
tosubset (a :: l) =
mapdt_env E (const (E * A -> Prop)) ret (a :: l) destruct a as [e a].
E, A: Type
e: E
a: A
l: list (E * A)
IHl: tosubset l = mapdt_env E (const (E * A -> Prop)) ret l
tosubset ((e, a) :: l) =
mapdt_env E (const (E * A -> Prop)) ret ((e, a) :: l)
      rewrite tosubset_list_cons.
E, A: Type
e: E
a: A
l: list (E * A)
IHl: tosubset l = mapdt_env E (const (E * A -> Prop)) ret l
{{(e, a)}} ∪ tosubset l =
mapdt_env E (const (E * A -> Prop)) ret ((e, a) :: l)
      cbn.
E, A: Type
e: E
a: A
l: list (E * A)
IHl: tosubset l = mapdt_env E (const (E * A -> Prop)) ret l
{{(e, a)}} ∪ tosubset l =
(pure cons ● map (pair e) (ret (e, a)))
● mapdt_env E (const (E * A -> Prop)) ret l
      unfold_ops @Pure_const @Map_const.
E, A: Type
e: E
a: A
l: list (E * A)
IHl: tosubset l = mapdt_env E (const (E * A -> Prop)) ret l
{{(e, a)}} ∪ tosubset l =
(Ƶ ● ret (e, a))
● mapdt_env E (const (E * A -> Prop)) ret l
      unfold_ops @Monoid_op_subset @Monoid_unit_subset.
E, A: Type
e: E
a: A
l: list (E * A)
IHl: tosubset l = mapdt_env E (const (E * A -> Prop)) ret l
{{(e, a)}} ∪ tosubset l =
∅ ∪ ret (e, a)
∪ mapdt_env E (const (E * A -> Prop)) ret l
      rewrite IHl.
E, A: Type
e: E
a: A
l: list (E * A)
IHl: tosubset l = mapdt_env E (const (E * A -> Prop)) ret l
{{(e, a)}} ∪ mapdt_env E (const (E * A -> Prop)) ret l =
∅ ∪ ret (e, a)
∪ mapdt_env E (const (E * A -> Prop)) ret l
      fequal.
E, A: Type
e: E
a: A
l: list (E * A)
IHl: tosubset l = mapdt_env E (const (E * A -> Prop)) ret l
{{(e, a)}} = ∅ ∪ ret (e, a)
      simpl_subset.
E, A: Type
e: E
a: A
l: list (E * A)
IHl: tosubset l = mapdt_env E (const (E * A -> Prop)) ret l
{{(e, a)}} = ret (e, a)
      reflexivity.
  Qed.

  (** ** Rewriting Rules for <<toctxset>> *)
  (********************************************************************)
  Lemma toctxset_env_nil: forall (A: Type),
      toctxset (F := env E) (@nil (E * A)) = subset_empty.
E: Type
forall A : Type, toctxset [] = ∅
  Proof.
E: Type
forall A : Type, toctxset [] = ∅
    reflexivity.
  Qed.

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

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

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

  (** ** Naturality *)
  (********************************************************************)
  #[export] Instance Natural_ToCtxset_env:
    Natural (@toctxset E (env E) _).
E: Type
Natural (@toctxset E (env E) ToCtxset_env)
  Proof.
E: Type
Natural (@toctxset E (env E) ToCtxset_env)
    constructor.
E: Type
Functor (env E)
E: Type
Functor (ctxset E)
E: Type
forall (A B : Type) (f : A -> B),
map f ∘ toctxset = toctxset ∘ map f
    -
E: Type
Functor (env E) try typeclasses eauto.
    -
E: Type
Functor (ctxset E) typeclasses eauto.
    -
E: Type
forall (A B : Type) (f : A -> B),
map f ∘ toctxset = toctxset ∘ map f unfold_ops @ToCtxset_env.
E: Type
forall (A B : Type) (f : A -> B),
map f ∘ (fun s : env E A => tosubset s) =
(fun s : env E B => tosubset s) ∘ map f
      intros.
E, A, B: Type
f: A -> B
map f ∘ (fun s : env E A => tosubset s) =
(fun s : env E B => tosubset s) ∘ map f
      rewrite ctxset_map_spec.
E, A, B: Type
f: A -> B
map (map f) ∘ (fun s : env E A => tosubset s) =
(fun s : env E B => tosubset s) ∘ map f
      rewrite (natural (A := E * A)
                 (B := E * B)
                 (ϕ := @tosubset list _)).
E, A, B: Type
f: A -> B
tosubset ∘ map (map f) =
(fun s : env E B => tosubset s) ∘ map f
      rewrite env_map_spec.
E, A, B: Type
f: A -> B
tosubset ∘ map (map f) =
(fun s : env E B => tosubset s) ∘ map (map f)
      reflexivity.
  Qed.

  (** ** <<toctxset>> is a Homomorphism of Decorated Functors *)
  (********************************************************************)
  #[export] Instance DecoratedHom_toctxset_env:
    DecoratedHom E (env E) (ctxset E) (@toctxset E (env E) _).
E: Type
DecoratedHom E (env E) (ctxset E)
  (@toctxset E (env E) ToCtxset_env)
  Proof.
E: Type
DecoratedHom E (env E) (ctxset E)
  (@toctxset E (env E) ToCtxset_env)
    constructor.
E: Type
forall (A B : Type) (f : E * A -> B),
mapd f ∘ toctxset = toctxset ∘ mapd f intros.
E, A, B: Type
f: E * A -> B
mapd f ∘ toctxset = toctxset ∘ mapd f
    ext Γ [e b].
E, A, B: Type
f: E * A -> B
Γ: env E A
e: E
b: B
(mapd f ∘ toctxset) Γ (e, b) =
(toctxset ∘ mapd f) Γ (e, b)
    unfold_ops @ToCtxset_env @Mapd_ctxset.
E, A, B: Type
f: E * A -> B
Γ: env E A
e: E
b: B
((fun (s : ctxset E A) '(e, b) =>
  exists a : A, s (e, a) /\ f (e, a) = b)
 ∘ (fun s : env E A => tosubset s)) Γ (e, b) =
((fun s : env E B => tosubset s) ∘ mapd f) Γ (e, b)
    unfold compose.
E, A, B: Type
f: E * A -> B
Γ: env E A
e: E
b: B
(exists a : A, tosubset Γ (e, a) /\ f (e, a) = b) =
tosubset (mapd f Γ) (e, b)
    induction Γ.
E, A, B: Type
f: E * A -> B
e: E
b: B
(exists a : A, tosubset [] (e, a) /\ f (e, a) = b) =
tosubset (mapd f []) (e, b)
E, A, B: Type
f: E * A -> B
a: E * A
Γ: list (E * A)
e: E
b: B
IHΓ: (exists a : A, tosubset Γ (e, a) /\ f (e, a) = b) =
tosubset (mapd f Γ) (e, b)
(exists a0 : A,
   tosubset (a :: Γ) (e, a0) /\ f (e, a0) = b) =
tosubset (mapd f (a :: Γ)) (e, b)
    -
E, A, B: Type
f: E * A -> B
e: E
b: B
(exists a : A, tosubset [] (e, a) /\ f (e, a) = b) =
tosubset (mapd f []) (e, b) cbn.
E, A, B: Type
f: E * A -> B
e: E
b: B
(exists a : A, False /\ f (e, a) = b) = False propext.
E, A, B: Type
f: E * A -> B
e: E
b: B
(exists a : A, False /\ f (e, a) = b) -> False
E, A, B: Type
f: E * A -> B
e: E
b: B
False -> exists a : A, False /\ f (e, a) = b
      +
E, A, B: Type
f: E * A -> B
e: E
b: B
(exists a : A, False /\ f (e, a) = b) -> False intros [a [contra heq]].
E, A, B: Type
f: E * A -> B
e: E
b: B
a: A
contra: False
heq: f (e, a) = b
False contradiction.
      +
E, A, B: Type
f: E * A -> B
e: E
b: B
False -> exists a : A, False /\ f (e, a) = b contradiction.
    -
E, A, B: Type
f: E * A -> B
a: E * A
Γ: list (E * A)
e: E
b: B
IHΓ: (exists a : A, tosubset Γ (e, a) /\ f (e, a) = b) =
tosubset (mapd f Γ) (e, b)
(exists a0 : A,
   tosubset (a :: Γ) (e, a0) /\ f (e, a0) = b) =
tosubset (mapd f (a :: Γ)) (e, b) destruct a as [e' a].
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
IHΓ: (exists a : A, tosubset Γ (e, a) /\ f (e, a) = b) =
tosubset (mapd f Γ) (e, b)
(exists a0 : A,
   tosubset ((e', a) :: Γ) (e, a0) /\ f (e, a0) = b) =
tosubset (mapd f ((e', a) :: Γ)) (e, b)
      change_right ((e', f (e', a)) = (e, b) \/ (e, b) ∈d mapd f Γ).
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
IHΓ: (exists a : A, tosubset Γ (e, a) /\ f (e, a) = b) =
tosubset (mapd f Γ) (e, b)
(exists a0 : A,
   tosubset ((e', a) :: Γ) (e, a0) /\ f (e, a0) = b) =
((e', f (e', a)) = (e, b) \/ (e, b) ∈d mapd f Γ)
      setoid_rewrite <- IHΓ; clear IHΓ.
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
(exists a0 : A,
   tosubset ((e', a) :: Γ) (e, a0) /\ f (e, a0) = b) =
((e', f (e', a)) = (e, b) \/
 (exists a : A, tosubset Γ (e, a) /\ f (e, a) = b))
      autorewrite with tea_list.
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
(exists a0 : A,
   ({{(e', a)}} ∪ tosubset Γ) (e, a0) /\ f (e, a0) = b) =
((e', f (e', a)) = (e, b) \/
 (exists a : A, tosubset Γ (e, a) /\ f (e, a) = b))
      propext.
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
(exists a0 : A,
   ({{(e', a)}} ∪ tosubset Γ) (e, a0) /\ f (e, a0) = b) ->
(e', f (e', a)) = (e, b) \/
(exists a : A, tosubset Γ (e, a) /\ f (e, a) = b)
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
(e', f (e', a)) = (e, b) \/
(exists a : A, tosubset Γ (e, a) /\ f (e, a) = b) ->
exists a0 : A,
  ({{(e', a)}} ∪ tosubset Γ) (e, a0) /\ f (e, a0) = b
      +
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
(exists a0 : A,
   ({{(e', a)}} ∪ tosubset Γ) (e, a0) /\ f (e, a0) = b) ->
(e', f (e', a)) = (e, b) \/
(exists a : A, tosubset Γ (e, a) /\ f (e, a) = b) intros [a' [[Hin|Hin] Heq]].
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
a': A
Hin: {{(e', a)}} (e, a')
Heq: f (e, a') = b
(e', f (e', a)) = (e, b) \/
(exists a : A, tosubset Γ (e, a) /\ f (e, a) = b)
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
a': A
Hin: tosubset Γ (e, a')
Heq: f (e, a') = b
(e', f (e', a)) = (e, b) \/
(exists a : A, tosubset Γ (e, a) /\ f (e, a) = b)
        *
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
a': A
Hin: {{(e', a)}} (e, a')
Heq: f (e, a') = b
(e', f (e', a)) = (e, b) \/
(exists a : A, tosubset Γ (e, a) /\ f (e, a) = b) left.
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
a': A
Hin: {{(e', a)}} (e, a')
Heq: f (e, a') = b
(e', f (e', a)) = (e, b)
          autorewrite with tea_set in *.
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
a': A
Hin: (e', a) = (e, a')
Heq: f (e, a') = b
(e', f (e', a)) = (e, b)
          now inversion Hin; subst.
        *
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
a': A
Hin: tosubset Γ (e, a')
Heq: f (e, a') = b
(e', f (e', a)) = (e, b) \/
(exists a : A, tosubset Γ (e, a) /\ f (e, a) = b) right.
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
a': A
Hin: tosubset Γ (e, a')
Heq: f (e, a') = b
exists a : A, tosubset Γ (e, a) /\ f (e, a) = b
          now (exists a').
      +
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
(e', f (e', a)) = (e, b) \/
(exists a : A, tosubset Γ (e, a) /\ f (e, a) = b) ->
exists a0 : A,
  ({{(e', a)}} ∪ tosubset Γ) (e, a0) /\ f (e, a0) = b intros [Heq | [a' [Hin Heq]]].
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
Heq: (e', f (e', a)) = (e, b)
exists a0 : A,
  ({{(e', a)}} ∪ tosubset Γ) (e, a0) /\ f (e, a0) = b
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
a': A
Hin: tosubset Γ (e, a')
Heq: f (e, a') = b
exists a0 : A,
  ({{(e', a)}} ∪ tosubset Γ) (e, a0) /\ f (e, a0) = b
        *
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
Heq: (e', f (e', a)) = (e, b)
exists a0 : A,
  ({{(e', a)}} ∪ tosubset Γ) (e, a0) /\ f (e, a0) = b inversion Heq; subst.
E, A, B: Type
f: E * A -> B
a: A
Γ: list (E * A)
e: E
Heq: (e, f (e, a)) = (e, f (e, a))
exists a0 : A,
  ({{(e, a)}} ∪ tosubset Γ) (e, a0) /\
  f (e, a0) = f (e, a) exists a.
E, A, B: Type
f: E * A -> B
a: A
Γ: list (E * A)
e: E
Heq: (e, f (e, a)) = (e, f (e, a))
({{(e, a)}} ∪ tosubset Γ) (e, a) /\
f (e, a) = f (e, a)
          autorewrite with tea_set.
E, A, B: Type
f: E * A -> B
a: A
Γ: list (E * A)
e: E
Heq: (e, f (e, a)) = (e, f (e, a))
((e, a) = (e, a) \/ tosubset Γ (e, a)) /\
f (e, a) = f (e, a)
          intuition.
        *
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
a': A
Hin: tosubset Γ (e, a')
Heq: f (e, a') = b
exists a0 : A,
  ({{(e', a)}} ∪ tosubset Γ) (e, a0) /\ f (e, a0) = b exists a'.
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
a': A
Hin: tosubset Γ (e, a')
Heq: f (e, a') = b
({{(e', a)}} ∪ tosubset Γ) (e, a') /\ f (e, a') = b
          autorewrite with tea_set.
E, A, B: Type
f: E * A -> B
e': E
a: A
Γ: list (E * A)
e: E
b: B
a': A
Hin: tosubset Γ (e, a')
Heq: f (e, a') = b
((e', a) = (e, a') \/ tosubset Γ (e, a')) /\
f (e, a') = b
          intuition.
  Qed.

End env_instance.