Tealeaves.Classes.Multisorted.Theory.Targeted
From Tealeaves Require Import
Classes.Multisorted.DecoratedTraversableMonad
Classes.Multisorted.Theory.Container
Categories.TypeFamily
Functors.List
Functors.Constant.
Import TypeFamily.Notations.
Import Product.Notations.
Import Monoid.Notations.
#[local] Generalizable Variables A B C F G W S T K.
Classes.Multisorted.DecoratedTraversableMonad
Classes.Multisorted.Theory.Container
Categories.TypeFamily
Functors.List
Functors.Constant.
Import TypeFamily.Notations.
Import Product.Notations.
Import Monoid.Notations.
#[local] Generalizable Variables A B C F G W S T K.
(* TODO: Define a version that works for applicative effects. *)
(*
[program] Definition btga `{ix: Index} `{Map F} `{Pure F} `{Mult F} {A W: Type} (T: K -> Type -> Type) `{! MReturn T} (j: K) (f: W * A -> F (T j A)): forall (k: K), W * A -> F (T k A) := fun k '(w, a) => if k == j then f (w, a) else pure ∘ mret T k a. *)
Require Import Coq.Program.Equality.
#[program] Definition btgd `{ix: Index} {A W: Type}
{T: K → Type → Type} `{! MReturn T}
(j: K) (f: W × A → T j A): ∀ (k: K), W × A → T k A :=
fun k '(w, a) ⇒ if k == j then f (w, a) else mret T k a.
#[program] Definition btg `{ix: Index} {A: Type}
{T: K → Type → Type} `{! MReturn T}
(j: K) (f: A → T j A): ∀ (k: K), A → T k A :=
fun k ⇒ if k == j then f else mret T k.
Require Import Coq.Program.Equality.
Section btg_lemmas.
Context
`{ix: Index}.
Context
`{MReturn T}
{W A: Type}.
Lemma btgd_eq: ∀ k (f: W × A → T k A),
btgd k f k = f.
Proof.
introv. unfold btgd. ext [w a].
compare values k and k.
dependent destruction DESTR_EQ.
cbn. reflexivity.
Qed.
Lemma btgd_neq: ∀ {k j} (f: W × A → T j A),
k ≠ j → btgd j f k = mret T k ∘ extract (W := (W ×)).
Proof.
introv. unfold btgd. intro hyp. ext [w a].
compare values k and j.
Qed.
Lemma btgd_id (j: K):
btgd (A := A) j
(mret T j ∘ extract (W := (W ×))) = mret T ◻ allK extract.
Proof.
unfold btgd. ext k [w a]. compare values k and j.
Qed.
Lemma btg_eq: ∀ k (f: A → T k A),
btg k f k = f.
Proof.
introv. unfold btg.
compare values k and k.
dependent destruction DESTR_EQ.
cbn. reflexivity.
Qed.
Lemma btg_neq: ∀ {k j} (f: A → T j A),
k ≠ j → btg j f k = mret T k.
Proof.
introv. unfold btg. intro hyp.
compare values k and j.
Qed.
Lemma btg_id (j: K):
btg (A := A) j (mret T j) = mret T.
Proof.
unfold btg. ext k. compare values k and j.
Qed.
End btg_lemmas.
(*
[program] Definition btga `{ix: Index} `{Map F} `{Pure F} `{Mult F} {A W: Type} (T: K -> Type -> Type) `{! MReturn T} (j: K) (f: W * A -> F (T j A)): forall (k: K), W * A -> F (T k A) := fun k '(w, a) => if k == j then f (w, a) else pure ∘ mret T k a. *)
Require Import Coq.Program.Equality.
#[program] Definition btgd `{ix: Index} {A W: Type}
{T: K → Type → Type} `{! MReturn T}
(j: K) (f: W × A → T j A): ∀ (k: K), W × A → T k A :=
fun k '(w, a) ⇒ if k == j then f (w, a) else mret T k a.
#[program] Definition btg `{ix: Index} {A: Type}
{T: K → Type → Type} `{! MReturn T}
(j: K) (f: A → T j A): ∀ (k: K), A → T k A :=
fun k ⇒ if k == j then f else mret T k.
Require Import Coq.Program.Equality.
Section btg_lemmas.
Context
`{ix: Index}.
Context
`{MReturn T}
{W A: Type}.
Lemma btgd_eq: ∀ k (f: W × A → T k A),
btgd k f k = f.
Proof.
introv. unfold btgd. ext [w a].
compare values k and k.
dependent destruction DESTR_EQ.
cbn. reflexivity.
Qed.
Lemma btgd_neq: ∀ {k j} (f: W × A → T j A),
k ≠ j → btgd j f k = mret T k ∘ extract (W := (W ×)).
Proof.
introv. unfold btgd. intro hyp. ext [w a].
compare values k and j.
Qed.
Lemma btgd_id (j: K):
btgd (A := A) j
(mret T j ∘ extract (W := (W ×))) = mret T ◻ allK extract.
Proof.
unfold btgd. ext k [w a]. compare values k and j.
Qed.
Lemma btg_eq: ∀ k (f: A → T k A),
btg k f k = f.
Proof.
introv. unfold btg.
compare values k and k.
dependent destruction DESTR_EQ.
cbn. reflexivity.
Qed.
Lemma btg_neq: ∀ {k j} (f: A → T j A),
k ≠ j → btg j f k = mret T k.
Proof.
introv. unfold btg. intro hyp.
compare values k and j.
Qed.
Lemma btg_id (j: K):
btg (A := A) j (mret T j) = mret T.
Proof.
unfold btg. ext k. compare values k and j.
Qed.
End btg_lemmas.
#[export] Hint Rewrite @btg_eq @btg_id @btgd_eq @btgd_id: tea_tgt.
#[export] Hint Rewrite @tgtd_eq @tgtd_eq @tgtd_id: tea_tgt.
#[export] Hint Rewrite @btgd_neq @btg_neq using auto: tea_tgt.
#[export] Hint Rewrite @btgd_eq @btg_eq @btg_id @btgd_id: tea_tgt_eq.
#[export] Hint Rewrite @tgtd_eq @tgt_eq @tgt_id: tea_tgt_eq.
#[export] Hint Rewrite @btgd_neq @btg_neq using auto: tea_tgt_neq.
#[export] Hint Rewrite @tgtd_neq: tea_tgt_neq.
#[export] Hint Rewrite @tgtd_eq @tgtd_eq @tgtd_id: tea_tgt.
#[export] Hint Rewrite @btgd_neq @btg_neq using auto: tea_tgt.
#[export] Hint Rewrite @btgd_eq @btg_eq @btg_id @btgd_id: tea_tgt_eq.
#[export] Hint Rewrite @tgtd_eq @tgt_eq @tgt_id: tea_tgt_eq.
#[export] Hint Rewrite @btgd_neq @btg_neq using auto: tea_tgt_neq.
#[export] Hint Rewrite @tgtd_neq: tea_tgt_neq.
(* For now we ignore traversals because we don't need them for
System F. *)
(********************************************************************)
Definition kbindd {A} `(f: W × A → T j A): U A → U A
:= mbindd U (btgd j f).
Definition kbind `(f: A → T j A): U A → U A
:= mbind U (btg j f).
Definition kmapd `(f: W × A → A): U A → U A :=
mmapd U (tgtd j f).
Definition kmap `(f: A → A): U A → U A :=
mmap U (tgt j f).
Section traversals.
Context `{Applicative G}.
Definition tgtdt
{A} (k: K) (f: W × A → G A): W × A -k→ G A :=
fun j '(w, a) ⇒ if k == j then f (w, a) else pure a.
Definition tgtdt_def
{A B} (k: K) (f def: W × A → G B): W × A -k→ G B :=
fun j ⇒ if k == j then f else def.
Definition tgtt {A} (k: K) (f: A → G A): A -k→ G A :=
fun j ⇒ if k == j then f else pure.
Definition tgtt_def {A B} (k: K) (f def: A → G B): A -k→ G B :=
fun j ⇒ if k == j then f else def.
Definition kmapdt `(f: W × A → G A): U A → G (U A) :=
mmapdt U G (tgtdt j f).
Definition ktraverse `(f: A → G A): U A → G (U A) :=
mmapt U G (tgtt j f).
Lemma kmapdt_to_mmapdt `(f: W × A → G A):
kmapdt f = mmapdt U G (tgtdt j f).
Proof.
reflexivity.
Qed.
Lemma kmapt_to_mtraverse `(f: A → G A):
ktraverse f = mmapt U G (tgtt j f).
Proof.
reflexivity.
Qed.
End traversals.
Section special_cases.
Context
{A: Type}.
System F. *)
(********************************************************************)
Definition kbindd {A} `(f: W × A → T j A): U A → U A
:= mbindd U (btgd j f).
Definition kbind `(f: A → T j A): U A → U A
:= mbind U (btg j f).
Definition kmapd `(f: W × A → A): U A → U A :=
mmapd U (tgtd j f).
Definition kmap `(f: A → A): U A → U A :=
mmap U (tgt j f).
Section traversals.
Context `{Applicative G}.
Definition tgtdt
{A} (k: K) (f: W × A → G A): W × A -k→ G A :=
fun j '(w, a) ⇒ if k == j then f (w, a) else pure a.
Definition tgtdt_def
{A B} (k: K) (f def: W × A → G B): W × A -k→ G B :=
fun j ⇒ if k == j then f else def.
Definition tgtt {A} (k: K) (f: A → G A): A -k→ G A :=
fun j ⇒ if k == j then f else pure.
Definition tgtt_def {A B} (k: K) (f def: A → G B): A -k→ G B :=
fun j ⇒ if k == j then f else def.
Definition kmapdt `(f: W × A → G A): U A → G (U A) :=
mmapdt U G (tgtdt j f).
Definition ktraverse `(f: A → G A): U A → G (U A) :=
mmapt U G (tgtt j f).
Lemma kmapdt_to_mmapdt `(f: W × A → G A):
kmapdt f = mmapdt U G (tgtdt j f).
Proof.
reflexivity.
Qed.
Lemma kmapt_to_mtraverse `(f: A → G A):
ktraverse f = mmapt U G (tgtt j f).
Proof.
reflexivity.
Qed.
End traversals.
Section special_cases.
Context
{A: Type}.
Lemma kbind_to_kbindd (f: A → T j A):
kbind f = kbindd (f ∘ extract (W := (W ×))).
Proof.
unfold kbind, kbindd. rewrite mbind_to_mbindd.
fequal. ext k [w a].
unfold vec_compose, compose; cbn.
compare values k and j.
- autorewrite with tea_tgt_eq. easy.
- autorewrite with tea_tgt_neq. easy.
Qed.
Lemma kmapd_to_kbindd (f: W × A → A):
kmapd f = kbindd (mret T j ∘ f).
Proof.
unfold kmapd, kbindd. rewrite mmapd_to_mbindd.
fequal. ext k [w a].
unfold vec_compose, compose.
cbn. compare values k and j.
Qed.
Lemma kmap_to_kbindd (f: A → A):
kmap f = kbindd (mret T j ∘ f ∘ extract (W := (W ×))).
Proof.
unfold kmap, kbindd. rewrite mmap_to_mbindd.
fequal. ext k [w a].
unfold vec_compose, compose. cbn.
compare values k and j. cbn.
now autorewrite with tea_tgt_eq.
now autorewrite with tea_tgt_neq.
Qed.
kbind f = kbindd (f ∘ extract (W := (W ×))).
Proof.
unfold kbind, kbindd. rewrite mbind_to_mbindd.
fequal. ext k [w a].
unfold vec_compose, compose; cbn.
compare values k and j.
- autorewrite with tea_tgt_eq. easy.
- autorewrite with tea_tgt_neq. easy.
Qed.
Lemma kmapd_to_kbindd (f: W × A → A):
kmapd f = kbindd (mret T j ∘ f).
Proof.
unfold kmapd, kbindd. rewrite mmapd_to_mbindd.
fequal. ext k [w a].
unfold vec_compose, compose.
cbn. compare values k and j.
Qed.
Lemma kmap_to_kbindd (f: A → A):
kmap f = kbindd (mret T j ∘ f ∘ extract (W := (W ×))).
Proof.
unfold kmap, kbindd. rewrite mmap_to_mbindd.
fequal. ext k [w a].
unfold vec_compose, compose. cbn.
compare values k and j. cbn.
now autorewrite with tea_tgt_eq.
now autorewrite with tea_tgt_neq.
Qed.
Lemma kmap_to_kmapd (f: A → A):
kmap f = kmapd (f ∘ extract (W := (W ×))).
Proof.
unfold kmap, kbind.
unfold kmapd. rewrite mmap_to_mmapd.
fequal. ext k.
unfold vec_compose.
compare values j and k.
now autorewrite with tea_tgt_eq.
now autorewrite with tea_tgt_neq.
Qed.
kmap f = kmapd (f ∘ extract (W := (W ×))).
Proof.
unfold kmap, kbind.
unfold kmapd. rewrite mmap_to_mmapd.
fequal. ext k.
unfold vec_compose.
compare values j and k.
now autorewrite with tea_tgt_eq.
now autorewrite with tea_tgt_neq.
Qed.
Lemma kmap_to_kbind (f: A → A):
kmap f = kbind (mret T j ∘ f).
Proof.
unfold kmap, kbind.
rewrite mmap_to_mbind.
fequal. ext k.
unfold vec_compose.
compare values j and k.
now autorewrite with tea_tgt_eq.
now autorewrite with tea_tgt_neq.
Qed.
End special_cases.
End DTM_targeted.
kmap f = kbind (mret T j ∘ f).
Proof.
unfold kmap, kbind.
rewrite mmap_to_mbind.
fequal. ext k.
unfold vec_compose.
compare values j and k.
now autorewrite with tea_tgt_eq.
now autorewrite with tea_tgt_neq.
Qed.
End special_cases.
End DTM_targeted.
Definition compose_kdm
`{ix: Index}
{W: Type}
{T: K → Type → Type}
`{mn_op: Monoid_op W}
`{mn_unit: Monoid_unit W}
`{∀ k, MBind W T (T k)}
`{! MReturn T}
{j: K}
{A: Type}
(g: W × A → T j A)
(f: W × A → T j A): W × A → T j A :=
fun '(w, a) ⇒ kbindd (T j) j (g ∘ incr w) (f (w, a)).
Infix "⋆kdm" := compose_kdm (at level 40).
Section DecoratedMonad.
Context
(U: Type → Type)
`{MultiDecoratedTraversablePreModule W T U}
`{! MultiDecoratedTraversableMonad W T}
{j: K}
{A: Type}.
Theorem kbindd_id:
kbindd U j (mret T j ∘ extract) = @id (U A).
Proof.
intros. unfold kbindd. rewrite <- (mbindd_id U).
fequal. ext k [w a]. cbn. compare values k and j.
Qed.
Theorem kbindd_kbindd_eq: ∀ (g: W × A → T j A) (f: W × A → T j A),
kbindd U j g ∘ kbindd U j f =
kbindd U j (g ⋆kdm f).
Proof.
intros. unfold kbindd. rewrite (mbindd_mbindd U).
fequal. ext k [w a]. cbn. compare values k and j.
- cbn. unfold kbindd. fequal. ext k [w' a'].
compare values k and j.
- compose near a on left. rewrite mbindd_comp_mret.
cbn. compare values k and j.
Qed.
Theorem kbindd_kbindd_neq:
∀ {i: K} (Hneq: j ≠ i)
(g: W × A → T i A) (f: W × A → T j A),
kbindd U i g ∘ kbindd U j f =
mbindd U (btgd i g ⋆dm btgd j f).
Proof.
intros. unfold kbindd. now rewrite (mbindd_mbindd U).
Qed.
kbindd U j (mret T j ∘ extract) = @id (U A).
Proof.
intros. unfold kbindd. rewrite <- (mbindd_id U).
fequal. ext k [w a]. cbn. compare values k and j.
Qed.
Theorem kbindd_kbindd_eq: ∀ (g: W × A → T j A) (f: W × A → T j A),
kbindd U j g ∘ kbindd U j f =
kbindd U j (g ⋆kdm f).
Proof.
intros. unfold kbindd. rewrite (mbindd_mbindd U).
fequal. ext k [w a]. cbn. compare values k and j.
- cbn. unfold kbindd. fequal. ext k [w' a'].
compare values k and j.
- compose near a on left. rewrite mbindd_comp_mret.
cbn. compare values k and j.
Qed.
Theorem kbindd_kbindd_neq:
∀ {i: K} (Hneq: j ≠ i)
(g: W × A → T i A) (f: W × A → T j A),
kbindd U i g ∘ kbindd U j f =
mbindd U (btgd i g ⋆dm btgd j f).
Proof.
intros. unfold kbindd. now rewrite (mbindd_mbindd U).
Qed.
Theorem kbindd_comp_mret_eq: ∀ (f: W × A → T j A) (a: A),
kbindd (T j) j f (mret T j a) = f (Ƶ, a).
Proof.
intros. unfold kbindd. compose near a on left.
rewrite (mbindd_comp_mret).
now autorewrite with tea_tgt_eq.
Qed.
Theorem kbindd_comp_mret_neq:
∀ (i: K) (Hneq: j ≠ i)
(f: W × A → T j A) (a: A),
kbindd (T i) j f (mret T i a) = mret T i a.
Proof.
intros. unfold kbindd. compose near a on left.
rewrite (mbindd_comp_mret).
now autorewrite with tea_tgt_neq.
Qed.
kbindd (T j) j f (mret T j a) = f (Ƶ, a).
Proof.
intros. unfold kbindd. compose near a on left.
rewrite (mbindd_comp_mret).
now autorewrite with tea_tgt_eq.
Qed.
Theorem kbindd_comp_mret_neq:
∀ (i: K) (Hneq: j ≠ i)
(f: W × A → T j A) (a: A),
kbindd (T i) j f (mret T i a) = mret T i a.
Proof.
intros. unfold kbindd. compose near a on left.
rewrite (mbindd_comp_mret).
now autorewrite with tea_tgt_neq.
Qed.
Lemma kmapd_kbindd: ∀
(g: W × A → A) (f: W × A → T j A),
kmapd U j g ∘ kbindd U j f =
kbindd U j (fun '(w, a) ⇒ kmapd (T j) j (g ∘ incr w) (f (w, a))).
Proof.
intros. rewrite kmapd_to_kbindd.
rewrite kbindd_kbindd_eq. fequal.
unfold compose_kdm. ext [w a].
now rewrite kmapd_to_kbindd.
Qed.
Lemma kbind_kbindd: ∀
(g: A → T j A) (f: W × A → T j A),
kbind U j g ∘ kbindd U j f = kbindd U j (kbind (T j) j g ∘ f).
Proof.
intros. rewrite kbind_to_kbindd. rewrite kbindd_kbindd_eq.
fequal. unfold compose_kdm. ext [w a].
reassociate →. rewrite extract_incr. now rewrite kbind_to_kbindd.
Qed.
Lemma kmap_kbindd: ∀
(g: A → A) (f: W × A → T j A),
kmap U j g ∘ kbindd U j f =
kbindd U j (fun '(w, a) ⇒ kmap (T j) j g (f (w, a))).
Proof.
intros. unfold kmap, kbindd. rewrite mmap_to_mbindd.
rewrite (mbindd_mbindd U). fequal. ext k [w a].
compare values j and k.
- autorewrite with tea_tgt_eq.
rewrite mmap_to_mbindd. fequal.
ext k' [w' a']. unfold compose; cbn. reflexivity.
- autorewrite with tea_tgt_neq.
unfold vec_compose, compose; cbn.
compose near a on left.
rewrite (mbindd_comp_mret).
rewrite tgt_neq; auto.
Qed.
Lemma kbindd_kmapd: ∀
(g: W × A → T j A) (f: W × A → A),
kbindd U j g ∘ kmapd U j f =
kbindd U j (fun '(w, a) ⇒ g (w, f (w, a))).
Proof.
intros. rewrite kmapd_to_kbindd.
rewrite kbindd_kbindd_eq. fequal.
ext (w, a). unfold compose; cbn.
rewrite kbindd_comp_mret_eq. unfold compose; cbn.
now simpl_monoid.
Qed.
Lemma kbindd_kbind: ∀
(g: W × A → T j A) (f: A → T j A),
kbindd U j g ∘ kbind U j f =
kbindd U j (fun '(w, a) ⇒ kbindd (T j) j (g ∘ incr w) (f a)).
Proof.
intros. rewrite kbind_to_kbindd. now rewrite kbindd_kbindd_eq.
Qed.
(* TODO <<kbindd_kmap>> *)
End DecoratedMonad.
(g: W × A → A) (f: W × A → T j A),
kmapd U j g ∘ kbindd U j f =
kbindd U j (fun '(w, a) ⇒ kmapd (T j) j (g ∘ incr w) (f (w, a))).
Proof.
intros. rewrite kmapd_to_kbindd.
rewrite kbindd_kbindd_eq. fequal.
unfold compose_kdm. ext [w a].
now rewrite kmapd_to_kbindd.
Qed.
Lemma kbind_kbindd: ∀
(g: A → T j A) (f: W × A → T j A),
kbind U j g ∘ kbindd U j f = kbindd U j (kbind (T j) j g ∘ f).
Proof.
intros. rewrite kbind_to_kbindd. rewrite kbindd_kbindd_eq.
fequal. unfold compose_kdm. ext [w a].
reassociate →. rewrite extract_incr. now rewrite kbind_to_kbindd.
Qed.
Lemma kmap_kbindd: ∀
(g: A → A) (f: W × A → T j A),
kmap U j g ∘ kbindd U j f =
kbindd U j (fun '(w, a) ⇒ kmap (T j) j g (f (w, a))).
Proof.
intros. unfold kmap, kbindd. rewrite mmap_to_mbindd.
rewrite (mbindd_mbindd U). fequal. ext k [w a].
compare values j and k.
- autorewrite with tea_tgt_eq.
rewrite mmap_to_mbindd. fequal.
ext k' [w' a']. unfold compose; cbn. reflexivity.
- autorewrite with tea_tgt_neq.
unfold vec_compose, compose; cbn.
compose near a on left.
rewrite (mbindd_comp_mret).
rewrite tgt_neq; auto.
Qed.
Lemma kbindd_kmapd: ∀
(g: W × A → T j A) (f: W × A → A),
kbindd U j g ∘ kmapd U j f =
kbindd U j (fun '(w, a) ⇒ g (w, f (w, a))).
Proof.
intros. rewrite kmapd_to_kbindd.
rewrite kbindd_kbindd_eq. fequal.
ext (w, a). unfold compose; cbn.
rewrite kbindd_comp_mret_eq. unfold compose; cbn.
now simpl_monoid.
Qed.
Lemma kbindd_kbind: ∀
(g: W × A → T j A) (f: A → T j A),
kbindd U j g ∘ kbind U j f =
kbindd U j (fun '(w, a) ⇒ kbindd (T j) j (g ∘ incr w) (f a)).
Proof.
intros. rewrite kbind_to_kbindd. now rewrite kbindd_kbindd_eq.
Qed.
(* TODO <<kbindd_kmap>> *)
End DecoratedMonad.
(* TODO <<kbind_kmapd>> *)
(* TODO <<kmapd_kbind>> *)
Section DecoratedFunctor.
Context
(U: Type → Type)
`{MultiDecoratedTraversablePreModule W T U}
`{! MultiDecoratedTraversableMonad W T}
{j: K}.
Context
(U: Type → Type)
`{MultiDecoratedTraversablePreModule W T U}
`{! MultiDecoratedTraversableMonad W T}
{j: K}.
Theorem kmapd_id: ∀ A,
kmapd U j extract = @id (U A).
Proof.
intros. unfold kmapd.
rewrite <- (mmapd_id U).
fequal. ext k. compare values j and k.
- now autorewrite with tea_tgt.
- now autorewrite with tea_tgt.
Qed.
Theorem kmapd_kmapd: ∀ A,
∀ (g: W × A → A) (f: W × A → A),
kmapd U j g ∘ kmapd U j f =
kmapd U j (fun '(w, a) ⇒ g (w, f (w, a))).
Proof.
intros. unfold kmapd.
rewrite (mmapd_mmapd U). fequal.
ext k [w a]. compare values j and k.
- now autorewrite with tea_tgt.
- now autorewrite with tea_tgt_neq.
Qed.
kmapd U j extract = @id (U A).
Proof.
intros. unfold kmapd.
rewrite <- (mmapd_id U).
fequal. ext k. compare values j and k.
- now autorewrite with tea_tgt.
- now autorewrite with tea_tgt.
Qed.
Theorem kmapd_kmapd: ∀ A,
∀ (g: W × A → A) (f: W × A → A),
kmapd U j g ∘ kmapd U j f =
kmapd U j (fun '(w, a) ⇒ g (w, f (w, a))).
Proof.
intros. unfold kmapd.
rewrite (mmapd_mmapd U). fequal.
ext k [w a]. compare values j and k.
- now autorewrite with tea_tgt.
- now autorewrite with tea_tgt_neq.
Qed.
Lemma kmapd_comp_mret_eq: ∀ A,
∀ (f: W × A → A) (a: A),
kmapd (T j) j f (mret T j a) = mret T j (f (Ƶ, a)).
Proof.
intros. unfold kmapd. rewrite mmapd_comp_mret.
now autorewrite with tea_tgt.
Qed.
Lemma kmapd_comp_mret_neq: ∀ A,
∀ (k: K) (neq: k ≠ j) (f: W × A → A) (a: A),
kmapd (T k) j f (mret T k a) = mret T k a.
Proof.
intros. unfold kmapd. rewrite mmapd_comp_mret.
now autorewrite with tea_tgt_neq.
Qed.
(* TODO <<kmap_kmapd>> *)
(* TODO <<kmapd_kmap>> *)
End DecoratedFunctor.
∀ (f: W × A → A) (a: A),
kmapd (T j) j f (mret T j a) = mret T j (f (Ƶ, a)).
Proof.
intros. unfold kmapd. rewrite mmapd_comp_mret.
now autorewrite with tea_tgt.
Qed.
Lemma kmapd_comp_mret_neq: ∀ A,
∀ (k: K) (neq: k ≠ j) (f: W × A → A) (a: A),
kmapd (T k) j f (mret T k a) = mret T k a.
Proof.
intros. unfold kmapd. rewrite mmapd_comp_mret.
now autorewrite with tea_tgt_neq.
Qed.
(* TODO <<kmap_kmapd>> *)
(* TODO <<kmapd_kmap>> *)
End DecoratedFunctor.
Definition compose_km
`{ix: Index}
{W: Type}
{T: K → Type → Type}
`{∀ k, MBind W T (T k)}
`{! MReturn T}
{j: K}
{A: Type}
(g: A → T j A)
(f: A → T j A): A → T j A :=
(kbind (T j) j g ∘ f).
Infix "⋆km" := compose_km (at level 40).
Section Monad.
Context
(U: Type → Type)
`{MultiDecoratedTraversablePreModule W T U}
`{! MultiDecoratedTraversableMonad W T}
{j: K}.
`{ix: Index}
{W: Type}
{T: K → Type → Type}
`{∀ k, MBind W T (T k)}
`{! MReturn T}
{j: K}
{A: Type}
(g: A → T j A)
(f: A → T j A): A → T j A :=
(kbind (T j) j g ∘ f).
Infix "⋆km" := compose_km (at level 40).
Section Monad.
Context
(U: Type → Type)
`{MultiDecoratedTraversablePreModule W T U}
`{! MultiDecoratedTraversableMonad W T}
{j: K}.
Theorem kbind_id: ∀ A,
kbind U j (mret T j) = @id (U A).
Proof.
intros. unfold kbind.
rewrite <- (mbind_id U). fequal.
ext k. compare values j and k.
- now autorewrite with tea_tgt_eq.
- now autorewrite with tea_tgt_neq.
Qed.
Theorem kbind_kbind: ∀ A,
∀ (g f: A → T j A),
kbind U j g ∘ kbind U j f =
kbind U j (g ⋆km f).
Proof.
intros. unfold kbind.
rewrite (mbind_mbind U). fequal.
ext k a. compare values j and k.
- now autorewrite with tea_tgt_eq.
- autorewrite with tea_tgt_neq.
rewrite (mbind_comp_mret k).
now autorewrite with tea_tgt_neq.
Qed.
kbind U j (mret T j) = @id (U A).
Proof.
intros. unfold kbind.
rewrite <- (mbind_id U). fequal.
ext k. compare values j and k.
- now autorewrite with tea_tgt_eq.
- now autorewrite with tea_tgt_neq.
Qed.
Theorem kbind_kbind: ∀ A,
∀ (g f: A → T j A),
kbind U j g ∘ kbind U j f =
kbind U j (g ⋆km f).
Proof.
intros. unfold kbind.
rewrite (mbind_mbind U). fequal.
ext k a. compare values j and k.
- now autorewrite with tea_tgt_eq.
- autorewrite with tea_tgt_neq.
rewrite (mbind_comp_mret k).
now autorewrite with tea_tgt_neq.
Qed.
Lemma kbind_comp_mret_eq: ∀ A,
∀ (f: A → T j A) (a: A),
kbind (T j) j f (mret T j a) = f a.
Proof.
intros. unfold kbind. rewrite mbind_comp_mret.
now autorewrite with tea_tgt_eq.
Qed.
Lemma kbind_comp_mret_neq: ∀ A,
∀ (i: K) (Hneq: j ≠ i) (f: A → T j A) (a: A),
kbind (T i) j f (mret T i a) = mret T i a.
Proof.
intros. unfold kbind. rewrite mbind_comp_mret.
now autorewrite with tea_tgt_neq.
Qed.
(* TODO <<kmap_kbind>> *)
(* TODO <<kbind_kmap>> *)
End Monad.
∀ (f: A → T j A) (a: A),
kbind (T j) j f (mret T j a) = f a.
Proof.
intros. unfold kbind. rewrite mbind_comp_mret.
now autorewrite with tea_tgt_eq.
Qed.
Lemma kbind_comp_mret_neq: ∀ A,
∀ (i: K) (Hneq: j ≠ i) (f: A → T j A) (a: A),
kbind (T i) j f (mret T i a) = mret T i a.
Proof.
intros. unfold kbind. rewrite mbind_comp_mret.
now autorewrite with tea_tgt_neq.
Qed.
(* TODO <<kmap_kbind>> *)
(* TODO <<kbind_kmap>> *)
End Monad.
Section Functor.
Context
(U: Type → Type)
`{MultiDecoratedTraversablePreModule W T U}
`{! MultiDecoratedTraversableMonad W T}
{j: K}.
Context
(U: Type → Type)
`{MultiDecoratedTraversablePreModule W T U}
`{! MultiDecoratedTraversableMonad W T}
{j: K}.
Theorem kmap_id: ∀ A,
kmap U j (@id A) = @id (U A).
Proof.
intros. unfold kmap.
rewrite <- (mmap_id U).
fequal. ext k. compare values k and j.
now autorewrite with tea_tgt_eq.
now autorewrite with tea_tgt_neq.
Qed.
Theorem kmap_kmap: ∀ (A: Type) (g f: A → A),
kmap U j g ∘ kmap U j f = kmap U j (g ∘ f).
Proof.
intros. unfold kmap.
rewrite (mmap_mmap U). fequal.
ext k.
rewrite vec_compose_k.
compare values j and k.
- now autorewrite with tea_tgt_eq.
- now autorewrite with tea_tgt_neq.
Qed.
kmap U j (@id A) = @id (U A).
Proof.
intros. unfold kmap.
rewrite <- (mmap_id U).
fequal. ext k. compare values k and j.
now autorewrite with tea_tgt_eq.
now autorewrite with tea_tgt_neq.
Qed.
Theorem kmap_kmap: ∀ (A: Type) (g f: A → A),
kmap U j g ∘ kmap U j f = kmap U j (g ∘ f).
Proof.
intros. unfold kmap.
rewrite (mmap_mmap U). fequal.
ext k.
rewrite vec_compose_k.
compare values j and k.
- now autorewrite with tea_tgt_eq.
- now autorewrite with tea_tgt_neq.
Qed.
Lemma kmap_comp_kret_eq {A}:
∀ (f: A → A) (a: A),
kmap (T j) j f (mret T j a) = mret T j (f a).
Proof.
intros. unfold kmap. rewrite mmap_comp_mret.
now rewrite tgt_eq.
Qed.
Lemma kmap_comp_kret_neq {A}:
∀ (i: K) (Hneq: j ≠ i) (f: A → A) (a: A),
kmap (T i) j f (mret T i a) = mret T i a.
Proof.
intros. unfold kmap. rewrite mmap_comp_mret.
rewrite tgt_neq; auto.
Qed.
End Functor.
∀ (f: A → A) (a: A),
kmap (T j) j f (mret T j a) = mret T j (f a).
Proof.
intros. unfold kmap. rewrite mmap_comp_mret.
now rewrite tgt_eq.
Qed.
Lemma kmap_comp_kret_neq {A}:
∀ (i: K) (Hneq: j ≠ i) (f: A → A) (a: A),
kmap (T i) j f (mret T i a) = mret T i a.
Proof.
intros. unfold kmap. rewrite mmap_comp_mret.
rewrite tgt_neq; auto.
Qed.
End Functor.
Module Notations.
Infix "⋆dtm" := compose_dtm (at level 40): tealeaves_scope.
Infix "⋆kdm" := compose_kdm (at level 40): tealeaves_scope.
Infix "⋆km" := compose_km (at level 40): tealeaves_scope.
End Notations.
Import Container.Notations.
Infix "⋆dtm" := compose_dtm (at level 40): tealeaves_scope.
Infix "⋆kdm" := compose_kdm (at level 40): tealeaves_scope.
Infix "⋆km" := compose_km (at level 40): tealeaves_scope.
End Notations.
Import Container.Notations.
Section DTM_membership_targetted.
Context
(U: Type → Type)
`{MultiDecoratedTraversablePreModule W T U}
`{! MultiDecoratedTraversableMonad W T}.
Context
(j: K)
{A: Type}.
Context
(U: Type → Type)
`{MultiDecoratedTraversablePreModule W T U}
`{! MultiDecoratedTraversableMonad W T}.
Context
(j: K)
{A: Type}.
Lemma inmd_kbindd_eq_iff1:
∀ `(f: W × A → T j A) (t: U A) (wtotal: W) (a2: A),
(wtotal, (j, a2)) ∈md kbindd U j f t →
∃ (w1 w2: W) (a1: A),
(w1, (j, a1)) ∈md t ∧ (w2, (j, a2)) ∈md f (w1, a1)
∧ wtotal = w1 ● w2.
Proof.
introv hyp. unfold kbindd in hyp.
apply (inmd_mbindd_iff1 U) in hyp.
destruct hyp as [k1 [w1 [w2 [a [hyp1 [hyp2 hyp3]]]]]]. subst.
compare values j and k1.
+ ∃ w1 w2 a. splits.
{ auto. }
{ rewrite btgd_eq in hyp2. auto. }
{ reflexivity. }
+ rewrite btgd_neq in hyp2; auto.
unfold compose in hyp2; cbn in hyp2.
rewrite inmd_mret_iff in hyp2. destructs hyp2.
subst. contradiction.
Qed.
Lemma inmd_kbindd_eq_iff2:
∀ `(f: W × A → T j A) (t: U A) (wtotal: W) (a2: A),
(∃ (w1 w2: W) (a1: A),
(w1, (j, a1)) ∈md t ∧ (w2, (j, a2)) ∈md f (w1, a1)
∧ wtotal = w1 ● w2) →
(wtotal, (j, a2)) ∈md kbindd U j f t.
Proof.
introv [w1 [w2 [a1 hyp]]]. destructs hyp. unfold kbindd.
apply (inmd_mbindd_iff2 U).
∃ j w1 w2 a1. rewrite btgd_eq. auto.
Qed.
Theorem inmd_kbindd_eq_iff:
∀ `(f: W × A → T j A) (t: U A) (wtotal: W) (a2: A),
(wtotal, (j, a2)) ∈md kbindd U j f t ↔
∃ (w1 w2: W) (a1: A),
(w1, (j, a1)) ∈md t ∧ (w2, (j, a2)) ∈md f (w1, a1)
∧ wtotal = w1 ● w2.
Proof.
split; auto using inmd_kbindd_eq_iff1, inmd_kbindd_eq_iff2.
Qed.
Lemma inmd_kbindd_neq_iff1:
∀ (i: K) (Hneq: j ≠ i) `(f: W × A → T j A)
(t: U A) (wtotal: W) (a2: A),
(wtotal, (i, a2)) ∈md kbindd U j f t →
(wtotal, (i, a2)) ∈md t ∨
(∃ (w1 w2: W) (a1: A),
(w1, (j, a1)) ∈md t ∧
(w2, (i, a2)) ∈md f (w1, a1) ∧
wtotal = w1 ● w2).
Proof.
introv ? hyp. unfold kbindd in hyp.
apply (inmd_mbindd_iff1 U) in hyp.
destruct hyp as [k1 [w1 [w2 [a [hyp1 [hyp2 hyp3]]]]]]. subst.
compare values j and k1.
+ right. ∃ w1 w2 a. rewrite btgd_eq in hyp2. splits; auto.
+ left. rewrite btgd_neq in hyp2; auto.
unfold compose in hyp2. cbn in hyp2.
rewrite inmd_mret_iff in hyp2. destructs hyp2; subst.
simpl_monoid. auto.
Qed.
Lemma inmd_kbindd_neq_iff2:
∀ (i: K) (Hneq: j ≠ i) `(f: W × A → T j A)
(t: U A) (wtotal: W) (a2: A),
(wtotal, (i, a2)) ∈md t ∨
(∃ (w1 w2: W) (a1: A),
(w1, (j, a1)) ∈md t ∧
(w2, (i, a2)) ∈md f (w1, a1) ∧
wtotal = w1 ● w2) →
(wtotal, (i, a2)) ∈md kbindd U j f t.
Proof.
introv ? hyp. destruct hyp as [hyp | hyp].
- apply (inmd_mbindd_iff2 U). ∃ i wtotal Ƶ a2.
splits.
{ auto. }
{ rewrite btgd_neq; auto. unfold compose; cbn.
rewrite inmd_mret_iff; auto. }
{ now simpl_monoid. }
- destruct hyp as [w1 [w2 [a1 [hyp1 [hyp2 hyp3]]]]]. subst.
apply (inmd_mbindd_iff2 U).
∃ j w1 w2 a1. rewrite btgd_eq. auto.
Qed.
Theorem inmd_kbindd_neq_iff:
∀ (i: K) (Hneq: j ≠ i) `(f: W × A → T j A)
(t: U A) (wtotal: W) (a2: A),
(wtotal, (i, a2)) ∈md kbindd U j f t ↔
(wtotal, (i, a2)) ∈md t ∨
(∃ (w1 w2: W) (a1: A),
(w1, (j, a1)) ∈md t ∧
(w2, (i, a2)) ∈md f (w1, a1) ∧
wtotal = w1 ● w2).
Proof.
split; auto using inmd_kbindd_neq_iff1, inmd_kbindd_neq_iff2.
Qed.
∀ `(f: W × A → T j A) (t: U A) (wtotal: W) (a2: A),
(wtotal, (j, a2)) ∈md kbindd U j f t →
∃ (w1 w2: W) (a1: A),
(w1, (j, a1)) ∈md t ∧ (w2, (j, a2)) ∈md f (w1, a1)
∧ wtotal = w1 ● w2.
Proof.
introv hyp. unfold kbindd in hyp.
apply (inmd_mbindd_iff1 U) in hyp.
destruct hyp as [k1 [w1 [w2 [a [hyp1 [hyp2 hyp3]]]]]]. subst.
compare values j and k1.
+ ∃ w1 w2 a. splits.
{ auto. }
{ rewrite btgd_eq in hyp2. auto. }
{ reflexivity. }
+ rewrite btgd_neq in hyp2; auto.
unfold compose in hyp2; cbn in hyp2.
rewrite inmd_mret_iff in hyp2. destructs hyp2.
subst. contradiction.
Qed.
Lemma inmd_kbindd_eq_iff2:
∀ `(f: W × A → T j A) (t: U A) (wtotal: W) (a2: A),
(∃ (w1 w2: W) (a1: A),
(w1, (j, a1)) ∈md t ∧ (w2, (j, a2)) ∈md f (w1, a1)
∧ wtotal = w1 ● w2) →
(wtotal, (j, a2)) ∈md kbindd U j f t.
Proof.
introv [w1 [w2 [a1 hyp]]]. destructs hyp. unfold kbindd.
apply (inmd_mbindd_iff2 U).
∃ j w1 w2 a1. rewrite btgd_eq. auto.
Qed.
Theorem inmd_kbindd_eq_iff:
∀ `(f: W × A → T j A) (t: U A) (wtotal: W) (a2: A),
(wtotal, (j, a2)) ∈md kbindd U j f t ↔
∃ (w1 w2: W) (a1: A),
(w1, (j, a1)) ∈md t ∧ (w2, (j, a2)) ∈md f (w1, a1)
∧ wtotal = w1 ● w2.
Proof.
split; auto using inmd_kbindd_eq_iff1, inmd_kbindd_eq_iff2.
Qed.
Lemma inmd_kbindd_neq_iff1:
∀ (i: K) (Hneq: j ≠ i) `(f: W × A → T j A)
(t: U A) (wtotal: W) (a2: A),
(wtotal, (i, a2)) ∈md kbindd U j f t →
(wtotal, (i, a2)) ∈md t ∨
(∃ (w1 w2: W) (a1: A),
(w1, (j, a1)) ∈md t ∧
(w2, (i, a2)) ∈md f (w1, a1) ∧
wtotal = w1 ● w2).
Proof.
introv ? hyp. unfold kbindd in hyp.
apply (inmd_mbindd_iff1 U) in hyp.
destruct hyp as [k1 [w1 [w2 [a [hyp1 [hyp2 hyp3]]]]]]. subst.
compare values j and k1.
+ right. ∃ w1 w2 a. rewrite btgd_eq in hyp2. splits; auto.
+ left. rewrite btgd_neq in hyp2; auto.
unfold compose in hyp2. cbn in hyp2.
rewrite inmd_mret_iff in hyp2. destructs hyp2; subst.
simpl_monoid. auto.
Qed.
Lemma inmd_kbindd_neq_iff2:
∀ (i: K) (Hneq: j ≠ i) `(f: W × A → T j A)
(t: U A) (wtotal: W) (a2: A),
(wtotal, (i, a2)) ∈md t ∨
(∃ (w1 w2: W) (a1: A),
(w1, (j, a1)) ∈md t ∧
(w2, (i, a2)) ∈md f (w1, a1) ∧
wtotal = w1 ● w2) →
(wtotal, (i, a2)) ∈md kbindd U j f t.
Proof.
introv ? hyp. destruct hyp as [hyp | hyp].
- apply (inmd_mbindd_iff2 U). ∃ i wtotal Ƶ a2.
splits.
{ auto. }
{ rewrite btgd_neq; auto. unfold compose; cbn.
rewrite inmd_mret_iff; auto. }
{ now simpl_monoid. }
- destruct hyp as [w1 [w2 [a1 [hyp1 [hyp2 hyp3]]]]]. subst.
apply (inmd_mbindd_iff2 U).
∃ j w1 w2 a1. rewrite btgd_eq. auto.
Qed.
Theorem inmd_kbindd_neq_iff:
∀ (i: K) (Hneq: j ≠ i) `(f: W × A → T j A)
(t: U A) (wtotal: W) (a2: A),
(wtotal, (i, a2)) ∈md kbindd U j f t ↔
(wtotal, (i, a2)) ∈md t ∨
(∃ (w1 w2: W) (a1: A),
(w1, (j, a1)) ∈md t ∧
(w2, (i, a2)) ∈md f (w1, a1) ∧
wtotal = w1 ● w2).
Proof.
split; auto using inmd_kbindd_neq_iff1, inmd_kbindd_neq_iff2.
Qed.
Corollary inmd_kbind_eq_iff:
∀ `(f: A → T j A) (t: U A) (wtotal: W) (a2: A),
(wtotal, (j, a2)) ∈md kbind U j f t ↔
∃ (w1 w2: W) (a1: A),
(w1, (j, a1)) ∈md t ∧ (w2, (j, a2)) ∈md f a1
∧ wtotal = w1 ● w2.
Proof.
intros. rewrite kbind_to_kbindd. now rewrite (inmd_kbindd_eq_iff).
Qed.
Corollary inmd_kbind_neq_iff:
∀ (i: K) (Hneq: j ≠ i) `(f: A → T j A) (t: U A) (wtotal: W) (a2: A),
(wtotal, (i, a2)) ∈md kbind U j f t ↔
(wtotal, (i, a2)) ∈md t ∨
(∃ (w1 w2: W) (a1: A),
(w1, (j, a1)) ∈md t ∧ (w2, (i, a2)) ∈md f a1
∧ wtotal = w1 ● w2).
Proof.
intros. rewrite kbind_to_kbindd. rewrite inmd_kbindd_neq_iff; auto.
unfold compose. cbn. easy.
Qed.
Corollary inmd_kmapd_eq_iff:
∀ `(f: W × A → A) (t: U A) (w: W) (a2: A),
(w, (j, a2)) ∈md kmapd U j f t ↔
∃ (a1: A), (w, (j, a1)) ∈md t ∧ a2 = f (w, a1).
Proof.
intros. unfold kmapd. rewrite (inmd_mmapd_iff U).
now rewrite tgtd_eq.
Qed.
Corollary inmd_kmapd_neq_iff:
∀ (i: K) (Hneq: j ≠ i) `(f: W × A → A) (t: U A) (w: W) (a2: A),
(w, (i, a2)) ∈md kmapd U j f t ↔
(w, (i, a2)) ∈md t.
Proof.
intros. unfold kmapd. rewrite (inmd_mmapd_iff U).
rewrite tgtd_neq; auto. cbn. split.
- intros [a [hyp eq]]; subst. auto.
- intros hyp. now (∃ a2).
Qed.
Corollary inmd_kmap_eq_iff:
∀ `(f: A → A) (t: U A) (w: W) (a2: A),
(w, (j, a2)) ∈md kmap U j f t ↔
∃ (a1: A), (w, (j, a1)) ∈md t ∧ a2 = f a1.
Proof.
intros. unfold kmap. rewrite (inmd_mmap_iff U).
now rewrite tgt_eq.
Qed.
Corollary inmd_kmap_neq_iff:
∀ (i: K) (Hneq: j ≠ i) `(f: A → A) (t: U A) (w: W) (a2: A),
(w, (i, a2)) ∈md kmap U j f t ↔
(w, (i, a2)) ∈md t.
Proof.
intros. unfold kmap. rewrite (inmd_mmap_iff U).
rewrite tgt_neq; auto. split.
- intros [a [hyp eq]]; subst. auto.
- intros hyp. now (∃ a2).
Qed.
∀ `(f: A → T j A) (t: U A) (wtotal: W) (a2: A),
(wtotal, (j, a2)) ∈md kbind U j f t ↔
∃ (w1 w2: W) (a1: A),
(w1, (j, a1)) ∈md t ∧ (w2, (j, a2)) ∈md f a1
∧ wtotal = w1 ● w2.
Proof.
intros. rewrite kbind_to_kbindd. now rewrite (inmd_kbindd_eq_iff).
Qed.
Corollary inmd_kbind_neq_iff:
∀ (i: K) (Hneq: j ≠ i) `(f: A → T j A) (t: U A) (wtotal: W) (a2: A),
(wtotal, (i, a2)) ∈md kbind U j f t ↔
(wtotal, (i, a2)) ∈md t ∨
(∃ (w1 w2: W) (a1: A),
(w1, (j, a1)) ∈md t ∧ (w2, (i, a2)) ∈md f a1
∧ wtotal = w1 ● w2).
Proof.
intros. rewrite kbind_to_kbindd. rewrite inmd_kbindd_neq_iff; auto.
unfold compose. cbn. easy.
Qed.
Corollary inmd_kmapd_eq_iff:
∀ `(f: W × A → A) (t: U A) (w: W) (a2: A),
(w, (j, a2)) ∈md kmapd U j f t ↔
∃ (a1: A), (w, (j, a1)) ∈md t ∧ a2 = f (w, a1).
Proof.
intros. unfold kmapd. rewrite (inmd_mmapd_iff U).
now rewrite tgtd_eq.
Qed.
Corollary inmd_kmapd_neq_iff:
∀ (i: K) (Hneq: j ≠ i) `(f: W × A → A) (t: U A) (w: W) (a2: A),
(w, (i, a2)) ∈md kmapd U j f t ↔
(w, (i, a2)) ∈md t.
Proof.
intros. unfold kmapd. rewrite (inmd_mmapd_iff U).
rewrite tgtd_neq; auto. cbn. split.
- intros [a [hyp eq]]; subst. auto.
- intros hyp. now (∃ a2).
Qed.
Corollary inmd_kmap_eq_iff:
∀ `(f: A → A) (t: U A) (w: W) (a2: A),
(w, (j, a2)) ∈md kmap U j f t ↔
∃ (a1: A), (w, (j, a1)) ∈md t ∧ a2 = f a1.
Proof.
intros. unfold kmap. rewrite (inmd_mmap_iff U).
now rewrite tgt_eq.
Qed.
Corollary inmd_kmap_neq_iff:
∀ (i: K) (Hneq: j ≠ i) `(f: A → A) (t: U A) (w: W) (a2: A),
(w, (i, a2)) ∈md kmap U j f t ↔
(w, (i, a2)) ∈md t.
Proof.
intros. unfold kmap. rewrite (inmd_mmap_iff U).
rewrite tgt_neq; auto. split.
- intros [a [hyp eq]]; subst. auto.
- intros hyp. now (∃ a2).
Qed.
Theorem in_kbindd_eq_iff:
∀ `(f: W × A → T j A) (t: U A) (a2: A),
(j, a2) ∈m kbindd U j f t ↔
∃ (w1: W) (a1: A),
(w1, (j, a1)) ∈md t ∧ (j, a2) ∈m f (w1, a1).
Proof.
intros. rewrite inmd_iff_in.
setoid_rewrite inmd_iff_in.
setoid_rewrite inmd_kbindd_eq_iff.
split.
- intros [w [w1 [w2 [a1 [hyp1 [hyp2 hyp3]]]]]].
eexists. eexists. split; eauto.
- intros [w [a1 [hyp1 [w2 hyp2]]]].
repeat eexists; eauto.
Qed.
Theorem in_kbindd_neq_iff:
∀ (i: K) (Hneq: j ≠ i) `(f: W × A → T j A) (t: U A) (a2: A),
(i, a2) ∈m kbindd U j f t ↔
(i, a2) ∈m t ∨
(∃ (w1: W) (a1: A),
(w1, (j, a1)) ∈md t ∧ (i, a2) ∈m f (w1, a1)).
Proof.
intros. rewrite inmd_iff_in.
setoid_rewrite inmd_iff_in.
setoid_rewrite inmd_kbindd_neq_iff; auto.
split.
- intros [w [hyp | hyp]].
+ left. eauto.
+ right. destruct hyp as [w1 [w2 [a1 [hyp1 [hyp2 hyp3]]]]].
repeat eexists; eauto.
- intros [hyp | hyp].
+ destruct hyp as [w hyp]. eexists. left. eauto.
+ destruct hyp as [w1 [a1 [hyp1 [w2 hyp2]]]].
eexists. right. repeat eexists; eauto.
Qed.
Corollary in_kbind_eq_iff:
∀ `(f: A → T j A) (t: U A) (a2: A),
(j, a2) ∈m kbind U j f t ↔
∃ (a1: A),
(j, a1) ∈m t ∧ (j, a2) ∈m f a1.
Proof.
intros. rewrite kbind_to_kbindd. rewrite (in_kbindd_eq_iff).
setoid_rewrite inmd_iff_in at 2.
unfold compose. cbn. firstorder.
Qed.
Corollary in_kbind_neq_iff:
∀ (i: K) (Hneq: j ≠ i) `(f: A → T j A) (t: U A) (a2: A),
(i, a2) ∈m kbind U j f t ↔
(i, a2) ∈m t ∨
(∃ (a1: A),
(j, a1) ∈m t ∧ (i, a2) ∈m f a1).
Proof.
intros. rewrite kbind_to_kbindd. rewrite in_kbindd_neq_iff; auto.
split.
- intros [hyp|hyp].
+ now left.
+ right. unfold compose in hyp. cbn in hyp.
destruct hyp as [? [a1 [hyp1 hyp2]]].
apply inmd_implies_in in hyp1. eauto.
- intros [hyp|hyp].
+ now left.
+ right.
destruct hyp as [a1 [hyp1 hyp2]].
rewrite inmd_iff_in in hyp1. destruct hyp1 as [w1 hyp1].
∃ w1 a1. auto.
Qed.
Corollary in_kmapd_eq_iff:
∀ `(f: W × A → A) (t: U A) (a2: A),
(j, a2) ∈m kmapd U j f t ↔
∃ (w: W) (a1: A), (w, (j, a1)) ∈md t ∧ a2 = f (w, a1).
Proof.
intros. unfold kmapd. rewrite (in_mmapd_iff U).
now rewrite tgtd_eq.
Qed.
Corollary in_kmapd_neq_iff:
∀ (i: K) (Hneq: j ≠ i) `(f: W × A → A) (t: U A) (a2: A),
(i, a2) ∈m kmapd U j f t ↔
(i, a2) ∈m t.
Proof.
intros. unfold kmapd. rewrite (in_mmapd_iff U).
rewrite tgtd_neq; auto. cbn. split.
- intros [w [a [hyp eq]]]; subst.
eapply inmd_implies_in; eauto.
- intros hyp. rewrite inmd_iff_in in hyp.
destruct hyp as [w hyp]. eauto.
Qed.
Corollary in_kmap_eq_iff:
∀ `(f: A → A) (t: U A) (a2: A),
(j, a2) ∈m kmap U j f t ↔
∃ (a1: A), (j, a1) ∈m t ∧ a2 = f a1.
Proof.
intros. unfold kmap. rewrite (in_mmap_iff U).
now rewrite tgt_eq.
Qed.
Corollary in_kmap_neq_iff:
∀ (i: K) (Hneq: j ≠ i) `(f: A → A) (t: U A) (a2: A),
(i, a2) ∈m kmap U j f t ↔
(i, a2) ∈m t.
Proof.
intros. unfold kmap. rewrite (in_mmap_iff U).
rewrite tgt_neq; auto. split.
- intros [a [hyp ?]]; subst. assumption.
- intros; now (∃ a2).
Qed.
End DTM_membership_targetted.
∀ `(f: W × A → T j A) (t: U A) (a2: A),
(j, a2) ∈m kbindd U j f t ↔
∃ (w1: W) (a1: A),
(w1, (j, a1)) ∈md t ∧ (j, a2) ∈m f (w1, a1).
Proof.
intros. rewrite inmd_iff_in.
setoid_rewrite inmd_iff_in.
setoid_rewrite inmd_kbindd_eq_iff.
split.
- intros [w [w1 [w2 [a1 [hyp1 [hyp2 hyp3]]]]]].
eexists. eexists. split; eauto.
- intros [w [a1 [hyp1 [w2 hyp2]]]].
repeat eexists; eauto.
Qed.
Theorem in_kbindd_neq_iff:
∀ (i: K) (Hneq: j ≠ i) `(f: W × A → T j A) (t: U A) (a2: A),
(i, a2) ∈m kbindd U j f t ↔
(i, a2) ∈m t ∨
(∃ (w1: W) (a1: A),
(w1, (j, a1)) ∈md t ∧ (i, a2) ∈m f (w1, a1)).
Proof.
intros. rewrite inmd_iff_in.
setoid_rewrite inmd_iff_in.
setoid_rewrite inmd_kbindd_neq_iff; auto.
split.
- intros [w [hyp | hyp]].
+ left. eauto.
+ right. destruct hyp as [w1 [w2 [a1 [hyp1 [hyp2 hyp3]]]]].
repeat eexists; eauto.
- intros [hyp | hyp].
+ destruct hyp as [w hyp]. eexists. left. eauto.
+ destruct hyp as [w1 [a1 [hyp1 [w2 hyp2]]]].
eexists. right. repeat eexists; eauto.
Qed.
Corollary in_kbind_eq_iff:
∀ `(f: A → T j A) (t: U A) (a2: A),
(j, a2) ∈m kbind U j f t ↔
∃ (a1: A),
(j, a1) ∈m t ∧ (j, a2) ∈m f a1.
Proof.
intros. rewrite kbind_to_kbindd. rewrite (in_kbindd_eq_iff).
setoid_rewrite inmd_iff_in at 2.
unfold compose. cbn. firstorder.
Qed.
Corollary in_kbind_neq_iff:
∀ (i: K) (Hneq: j ≠ i) `(f: A → T j A) (t: U A) (a2: A),
(i, a2) ∈m kbind U j f t ↔
(i, a2) ∈m t ∨
(∃ (a1: A),
(j, a1) ∈m t ∧ (i, a2) ∈m f a1).
Proof.
intros. rewrite kbind_to_kbindd. rewrite in_kbindd_neq_iff; auto.
split.
- intros [hyp|hyp].
+ now left.
+ right. unfold compose in hyp. cbn in hyp.
destruct hyp as [? [a1 [hyp1 hyp2]]].
apply inmd_implies_in in hyp1. eauto.
- intros [hyp|hyp].
+ now left.
+ right.
destruct hyp as [a1 [hyp1 hyp2]].
rewrite inmd_iff_in in hyp1. destruct hyp1 as [w1 hyp1].
∃ w1 a1. auto.
Qed.
Corollary in_kmapd_eq_iff:
∀ `(f: W × A → A) (t: U A) (a2: A),
(j, a2) ∈m kmapd U j f t ↔
∃ (w: W) (a1: A), (w, (j, a1)) ∈md t ∧ a2 = f (w, a1).
Proof.
intros. unfold kmapd. rewrite (in_mmapd_iff U).
now rewrite tgtd_eq.
Qed.
Corollary in_kmapd_neq_iff:
∀ (i: K) (Hneq: j ≠ i) `(f: W × A → A) (t: U A) (a2: A),
(i, a2) ∈m kmapd U j f t ↔
(i, a2) ∈m t.
Proof.
intros. unfold kmapd. rewrite (in_mmapd_iff U).
rewrite tgtd_neq; auto. cbn. split.
- intros [w [a [hyp eq]]]; subst.
eapply inmd_implies_in; eauto.
- intros hyp. rewrite inmd_iff_in in hyp.
destruct hyp as [w hyp]. eauto.
Qed.
Corollary in_kmap_eq_iff:
∀ `(f: A → A) (t: U A) (a2: A),
(j, a2) ∈m kmap U j f t ↔
∃ (a1: A), (j, a1) ∈m t ∧ a2 = f a1.
Proof.
intros. unfold kmap. rewrite (in_mmap_iff U).
now rewrite tgt_eq.
Qed.
Corollary in_kmap_neq_iff:
∀ (i: K) (Hneq: j ≠ i) `(f: A → A) (t: U A) (a2: A),
(i, a2) ∈m kmap U j f t ↔
(i, a2) ∈m t.
Proof.
intros. unfold kmap. rewrite (in_mmap_iff U).
rewrite tgt_neq; auto. split.
- intros [a [hyp ?]]; subst. assumption.
- intros; now (∃ a2).
Qed.
End DTM_membership_targetted.