Extra lemmas for simplification support

From Tealeaves Require Export
  Theory.DecoratedTraversableMonad
  Misc.Prop
  Tactics.Debug.

Import DecoratedTraversableMonad.UsefulInstances.
Import Classes.Kleisli.Theory.DecoratedTraversableMonad.

#[local] Generalizable Variables G A B C.
#[local] Set Implicit Arguments.

Import Monoid.Notations.

Import Monoid.Notations.

Lemma eq_pair_preincr: forall (n: nat) {A} (a: A),
    eq (S n, a) ⦿ 1 = eq (n, a).
forall (n : nat) (A : Type) (a : A),
eq (S n, a) ⦿ 1 = eq (n, a)
Proof.
forall (n : nat) (A : Type) (a : A),
eq (S n, a) ⦿ 1 = eq (n, a)
  intros.
n: nat
A: Type
a: A
eq (S n, a) ⦿ 1 = eq (n, a)
  ext [n' a'].
n: nat
A: Type
a: A
n': nat
a': A
(eq (S n, a) ⦿ 1) (n', a') = ((n, a) = (n', a'))
  unfold preincr, compose, incr.
n: nat
A: Type
a: A
n': nat
a': A
((S n, a) = (1 ● n', a')) = ((n, a) = (n', a'))
  apply propositional_extensionality.
n: nat
A: Type
a: A
n': nat
a': A
(S n, a) = (1 ● n', a') <-> (n, a) = (n', a')
  rewrite pair_equal_spec.
n: nat
A: Type
a: A
n': nat
a': A
S n = 1 ● n' /\ a = a' <-> (n, a) = (n', a')
  rewrite pair_equal_spec.
n: nat
A: Type
a: A
n': nat
a': A
S n = 1 ● n' /\ a = a' <-> n = n' /\ a = a'
  intuition.
Qed.

Section section.

  Context {E : Type} {T : Type -> Type} `{Mapdt E T}.

  Lemma Forall_ctx_to_mapdReduce :
    forall {A t} (f: E * A -> Prop),
      Forall_ctx f t = mapdReduce f t.
E: Type
T: Type -> Type
H: Mapdt E T
forall (A : Type) (t : T A) (f : E * A -> Prop),
Forall_ctx f t = mapdReduce f t
  Proof.
E: Type
T: Type -> Type
H: Mapdt E T
forall (A : Type) (t : T A) (f : E * A -> Prop),
Forall_ctx f t = mapdReduce f t
    reflexivity.
  Qed.
  Lemma mapdReduce_to_Forall_ctx :
    forall {A t} (f: E * A -> Prop),
      mapdReduce f t = Forall_ctx f t.
E: Type
T: Type -> Type
H: Mapdt E T
forall (A : Type) (t : T A) (f : E * A -> Prop),
mapdReduce f t = Forall_ctx f t
  Proof.
E: Type
T: Type -> Type
H: Mapdt E T
forall (A : Type) (t : T A) (f : E * A -> Prop),
mapdReduce f t = Forall_ctx f t
    reflexivity.
  Qed.

  Lemma exists_false_false
    `{DecoratedTraversableFunctor E T}:
    forall {A} (t: T A),
      mapdReduce (op := Monoid_op_or) (unit := Monoid_unit_false)
        (const False) t = False.
E: Type
T: Type -> Type
H, H0: Mapdt E T
H1: DecoratedTraversableFunctor E T
forall (A : Type) (t : T A),
mapdReduce (const False) t = False
  Proof.
E: Type
T: Type -> Type
H, H0: Mapdt E T
H1: DecoratedTraversableFunctor E T
forall (A : Type) (t : T A),
mapdReduce (const False) t = False
    intros.
E: Type
T: Type -> Type
H, H0: Mapdt E T
H1: DecoratedTraversableFunctor E T
A: Type
t: T A
mapdReduce (const False) t = False
    rewrite mapdReduce_through_toctxlist.
E: Type
T: Type -> Type
H, H0: Mapdt E T
H1: DecoratedTraversableFunctor E T
A: Type
t: T A
(mapReduce (const False) ∘ toctxlist) t = False
    unfold compose.
E: Type
T: Type -> Type
H, H0: Mapdt E T
H1: DecoratedTraversableFunctor E T
A: Type
t: T A
mapReduce (const False) (toctxlist t) = False induction (toctxlist t).
E: Type
T: Type -> Type
H, H0: Mapdt E T
H1: DecoratedTraversableFunctor E T
A: Type
t: T A
mapReduce (const False) nil = False
E: Type
T: Type -> Type
H, H0: Mapdt E T
H1: DecoratedTraversableFunctor E T
A: Type
t: T A
a: E * A
e: list (E * A)
IHe: mapReduce (const False) e = False
mapReduce (const False) (a :: e) = False
    -
E: Type
T: Type -> Type
H, H0: Mapdt E T
H1: DecoratedTraversableFunctor E T
A: Type
t: T A
mapReduce (const False) nil = False reflexivity.
    -
E: Type
T: Type -> Type
H, H0: Mapdt E T
H1: DecoratedTraversableFunctor E T
A: Type
t: T A
a: E * A
e: list (E * A)
IHe: mapReduce (const False) e = False
mapReduce (const False) (a :: e) = False cbn.
E: Type
T: Type -> Type
H, H0: Mapdt E T
H1: DecoratedTraversableFunctor E T
A: Type
t: T A
a: E * A
e: list (E * A)
IHe: mapReduce (const False) e = False
(pure cons ● const False a)
● mapReduce (const False) e = False rewrite IHe.
E: Type
T: Type -> Type
H, H0: Mapdt E T
H1: DecoratedTraversableFunctor E T
A: Type
t: T A
a: E * A
e: list (E * A)
IHe: mapReduce (const False) e = False
(pure cons ● const False a) ● False = False do 2 unfold transparent tcs.
E: Type
T: Type -> Type
H, H0: Mapdt E T
H1: DecoratedTraversableFunctor E T
A: Type
t: T A
a: E * A
e: list (E * A)
IHe: mapReduce (const False) e = False
((False \/ const False a) \/ False) = False propext;
                        intuition.
  Qed.

End section.

Lemma binddt_ret:
  forall {W : Type} {T G : Type -> Type}
    `{DecoratedTraversableMonad W T}
    `{Applicative G},
      forall (A B : Type) (f : W * A -> G (T B)) (a: A),
        binddt f (ret a) = f (Ƶ, a).
forall (W : Type) (T G : Type -> Type)
  (op : Monoid_op W) (unit0 : Monoid_unit W)
  (Return_inst : Return T)
  (Bindd_T_inst : Binddt W T T),
DecoratedTraversableMonad W T ->
forall (Map_G : Map G) (Pure_G : Pure G)
  (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : W * A -> G (T B)) (a : A),
binddt f (ret a) = f (Ƶ, a)
Proof.
forall (W : Type) (T G : Type -> Type)
  (op : Monoid_op W) (unit0 : Monoid_unit W)
  (Return_inst : Return T)
  (Bindd_T_inst : Binddt W T T),
DecoratedTraversableMonad W T ->
forall (Map_G : Map G) (Pure_G : Pure G)
  (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : W * A -> G (T B)) (a : A),
binddt f (ret a) = f (Ƶ, a)
  intros.
W: Type
T, G: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
a: A
binddt f (ret a) = f (Ƶ, a)
  compose near a.
W: Type
T, G: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
a: A
(binddt f ∘ ret) a = (f ∘ pair Ƶ) a
  rewrite kdtm_binddt0.
W: Type
T, G: Type -> Type
op: Monoid_op W
unit0: Monoid_unit W
Return_inst: Return T
Bindd_T_inst: Binddt W T T
H: DecoratedTraversableMonad W T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: W * A -> G (T B)
a: A
(f ∘ ret) a = (f ∘ pair Ƶ) a
  reflexivity.
Qed.

(** * Basic rewriting lemmas *)
(******************************************************************************)
Module Basics.

  Ltac rewrite_with_any :=
    match goal with
    | [H : _ = _ |- _] => rewrite H
    | [H : forall _, _ |- _] => progress rewrite H by now trivial
    end.

  Ltac normalize_fns :=
    ltac_trace "normalize_fns";
    match goal with
    | |- context[?f ∘ id] =>
        change (f ∘ id) with f
    | |- context[(id ∘ ?f)] =>
        change (id ∘ f) with f
    end.

  Ltac normalize_fns_in H :=
    match goal with
    | H: context[?f ∘ id] |- _ =>
        change (f ∘ id) with f in H
    | H: context[(id ∘ ?f)] |- _ =>
        change (id ∘ f) with f in H
    end.

  Ltac normalize_id :=
    ltac_trace "normalize_id";
    match goal with
    | |- context[id ?t] =>
        change (id t) with t
    end.

  Ltac normalize_id_in :=
    match goal with
    | H: context[id ?t] |- _ =>
        change (id t) with t in H
    end.

  Ltac simplify_monoid_units :=
    ltac_trace "simplify_monoid_units";
    match goal with
    | |- context[Ƶ ● ?m] =>
        rewrite (monoid_id_l m)
    | |- context[?m ● Ƶ] =>
        rewrite (monoid_id_r m)
    end.

  Ltac simplify_monoid_units_in H :=
    match goal with
    | H: context[Ƶ ● ?m] |- _ =>
        rewrite (monoid_id_l m) in H
    | H: context[?m ● Ƶ] |- _ =>
        rewrite (monoid_id_r m) in H
    end.

  Ltac simplify_preincr_zero :=
    ltac_trace "simplify_preincr_zero";
    match goal with
    | |- context[(?f ⦿ Ƶ)] =>
        rewrite (preincr_zero f)
    | |- context[(?f ⦿ ?x)] =>
        (* test whether x can be resolved as some Ƶ *)
        let T := type of x in
        change x with (Ƶ:T);
        rewrite preincr_zero
    end.

End Basics.

(** * Simplifying applicative functors *)
(******************************************************************************)
Module SimplApplicative.

  Ltac find_functor_instance G :=
    match goal with
    | H: Functor G |- _ => idtac
    | |- _ => fail
    end.

  Ltac find_applicative_instance G :=
    match goal with
    | H: Applicative G |- _ => idtac
    | |- _ => fail
    end.

  Ltac infer_applicative_functors :=
    repeat match goal with
      | H: Applicative ?G |- _ =>
          (* See coq refman 8.20 Note about assert_fails *)
          assert_fails (idtac; find_functor_instance G);
          assert (Functor G) by (now inversion H)
      | H: ApplicativeMorphism ?G1 ?G2 ?ϕ |- _ =>
          (assert_fails (idtac; find_applicative_instance G1);
           assert (Applicative G1) by now inversion H)
          || (assert_fails (idtac; find_applicative_instance G2);
             assert (Applicative G2) by now inversion H)
      end.

  (** ** Identity applicative *)
  (******************************************************************************)
  Ltac simplify_applicative_I :=
    ltac_trace "simplify_applicative_I";
    match goal with
    | |- context[pure (F := fun A => A) ?x] =>
        change (pure (F := fun A => A) x) with x
    | |- context[ap (fun A => A) ?x ?y] =>
        change (ap (fun A => A) x y) with (x y)
    end.

  Ltac simplify_applicative_I_in :=
    match goal with
    | H: context[pure (F := fun A => A) ?x] |- _ =>
        change (pure (F := fun A => A) x) with x
    | H: context[ap (fun A => A) ?x ?y] |- _ =>
        change (ap (fun A => A) x y) with (x y)
    end.

  (** ** Identity maps *)
  (******************************************************************************)
  Ltac simplify_map_I :=
    ltac_trace "simplify_map_I";
    match goal with
    | |- context[map (F := fun A => A) ?f] =>
        unfold_ops @Map_I
    end.

  Ltac simplify_map_I_in :=
    match goal with
    | H: context[map (F := fun A => A) ?f] |- _ =>
        unfold map in H;
        unfold Map_I in H
    end.

End SimplApplicative.

Export Basics.
Export SimplApplicative.