Require Import kat normalisation rewriting kat_tac.

Local Infix " ;" := (dot _ _ _) (left associativity, at level 40): ra_terms.

Lemma rmov_x_str `{L: monoid.laws} `{Hl: STR ≪ l} {n} (x e: X n n):
  x;e ≡ e;x → x;e^* ≡ e^*;x.
Proof. apply str_move. Qed.

Lemma rmov_x_itr `{L: monoid.laws} `{Hl: STR ≪ l} {n} (x e: X n n):
  x;e ≡ e;x → x;e^+ ≡ e^+;x.
Proof. apply itr_move. Qed.

Lemma rmov_x_pls `{L: monoid.laws} `{Hl: CUP ≪ l} {n m} x y (e f: X n m):
  x;e ≡ e;y → x;f ≡ f;y → x;(e+f) ≡ (e+f);y.
Proof. intros. ra_normalise. now apply cup_weq. Qed.

Lemma rmov_x_dot `{L: monoid.laws} {n m p} x y z (e: X n m) (f: X m p):
  x;e ≡ e;y → y;f ≡ f;z → x;(e;f) ≡ (e;f);z.
Proof. intros He Hf. rewrite dotA, He, <-dotA, Hf. apply dotA. Qed.

Lemma rmov_x_1 `{L: monoid.laws} {n} (x: X n n): x;1 ≡ 1;x.
Proof. ra. Qed.

Lemma rmov_x_0 `{L: monoid.laws} `{Hl:BOT ≪ l} {n m p q} (x: X n m) (y: X p q): x;0 ≡ 0;y.
Proof. ra. Qed.

Lemma rmov_x_cap `{L: laws} {n} (x: X n n) a b:
  x;[a] ≡ [a];x → x;[b] ≡ [b];x → x;[a ⊓ b] ≡ [a ⊓ b];x.
Proof. hkat. Qed.

Lemma rmov_x_cup `{L: laws} {n} (x: X n n) a b:
  x;[a] ≡ [a];x → x;[b] ≡ [b];x → x;[a ⊔ b] ≡ [a ⊔ b];x.
Proof. hkat. Qed.

Lemma rmov_x_neg `{L: laws} {n} (x: X n n) a:
  x;[a] ≡ [a];x → x;[!a] ≡ [!a];x.
Proof. hkat. Qed.

Lemma rmov_inj `{L: laws} {n} (a b: tst n): [a]⋅[b] ≡ [b]⋅[a].
Proof. kat. Qed.

Ltac solve_rmov :=
  first
    [ eassumption
    | symmetry; eassumption
    | eapply rmov_x_dot
    | apply rmov_x_pls
    | apply rmov_x_str
    | apply rmov_x_itr
    | apply rmov_x_cap
    | apply rmov_x_cup
    | apply rmov_x_neg
    | apply rmov_inj
    | apply rmov_x_1
    | apply rmov_x_0 ]; solve_rmov.

Ltac rmov1 x :=
  rewrite ?dotA;
  
  match goal with
    | |- context [@dot ?X ?n ?n ?m x ?e] ⇒
      let H := fresh "H" in
      let y := fresh "y" in
      evar (y: car (X m m));
      assert (H: x;e ≡ e;y) by (subst y; solve_rmov);
      rewrite H; subst y; clear H
    | |- context [@dot ?X _ ?n ?m (?f;x) ?e] ⇒
      let H := fresh "H" in
      let y := fresh "y" in
      evar (y: car (X m m));
      assert (H: x;e ≡ e;y) by (subst y; solve_rmov);
      rewrite <-(dotA f x e), H; subst y; clear H
  end.

Ltac lmov1 x :=
  rewrite <-?dotA;
  
  match goal with
    | |- context [@dot ?X ?m ?n ?n ?e x] ⇒
      let H := fresh "H" in
      let y := fresh "y" in
      evar (y: car (X m m));
      assert (H: y;e ≡ e;x) by (subst y; solve_rmov);
      rewrite <-H; subst y; clear H
    | |- context [@dot ?X ?m _ _ ?e (x;?f)] ⇒
      let H := fresh "H" in
      let y := fresh "y" in
      evar (y: car (X m m));
      assert (H: y;e ≡ e;x) by (subst y; solve_rmov);
      rewrite (dotA e x f), <-H; subst y; clear H
  end.