Library UniMath.Tactics.Abmonoids_Tactics

Author: Michael A. Warren. Date: Spring 2015. Description: Some tactics for abelian monoids.

Require Import UniMath.Algebra.Monoids_and_Groups
               UniMath.Tactics.Utilities
               UniMath.Tactics.Monoids_Tactics.

I. Definitions.

Because rewrite seems to have handling the two scopes multmonoid and addmonoid, the following definitions are for arbitrary commutative operations.

Definition isabsemigrop {X : hSet} (opp : binop X) :=
  (isassoc opp) ** (iscomm opp).

Definition abmonoid_to_absemigr (M : abmonoid) : isabsemigrop (@op M) :=
  dirprodpair (@assocax M) (@commax M).

Definition absemigr_perm021 :
  ∏ X : hSet, ∏ opp : binop X, ∏ is : isabsemigrop opp,
  ∏ n0 n1 n2,
    opp (opp n0 n1) n2 = opp (opp n0 n2) n1 :=
  λ X opp is n0 n1 n2,
    pathscomp0
      (pathscomp0
         ((pr1 is) n0 n1 n2)
         (maponpaths (λ z, opp n0 z) ((pr2 is) n1 n2)))
      (pathsinv0 ((pr1 is) n0 n2 n1)).

Definition abmonoid_perm021 :=
  λ M : abmonoid, absemigr_perm021 M (@op M) (abmonoid_to_absemigr M).

Definition absemigr_perm102 :
  ∏ X : hSet, ∏ opp : binop X, ∏ is : isabsemigrop opp,
  ∏ n0 n1 n2,
    opp (opp n0 n1) n2 = opp (opp n1 n0) n2 :=
  λ X opp is n0 n1 n2, maponpaths (λ z, opp z n2) ((pr2 is) n0 n1).

Definition abmonoid_perm102 :=
  λ M : abmonoid, absemigr_perm102 M (@op M) (abmonoid_to_absemigr M).

Definition absemigr_perm120 :
  ∏ X : hSet, ∏ opp : binop X, ∏ is : isabsemigrop opp,
  ∏ n0 n1 n2,
    opp (opp n0 n1) n2 = opp (opp n2 n0) n1 :=
  λ X opp is n0 n1 n2,
    pathscomp0 ((pr2 is) (opp n0 n1) n2) (pathsinv0 ((pr1 is) n2 n0 n1)).

Definition abmonoid_perm120 :=
  λ M : abmonoid, absemigr_perm120 M (@op M) (abmonoid_to_absemigr M).

Definition absemigr_perm201 :
  ∏ X : hSet, ∏ opp : binop X, ∏ is : isabsemigrop opp,
  ∏ n0 n1 n2,
    opp (opp n0 n1) n2 = opp (opp n1 n2) n0 :=
  λ X opp is n0 n1 n2,
    pathscomp0 ((pr1 is) n0 n1 n2) ((pr2 is) n0 (opp n1 n2)).

Definition abmonoid_perm201 :=
  λ M : abmonoid, absemigr_perm201 M (@op M) (abmonoid_to_absemigr M).

Definition absemigr_perm210 :
  ∏ X : hSet, ∏ opp : binop X, ∏ is : isabsemigrop opp,
  ∏ n0 n1 n2,
    opp (opp n0 n1) n2 = opp (opp n2 n1) n0 :=
  λ X opp is n0 n1 n2,
    pathscomp0 (absemigr_perm102 X opp is n0 n1 n2)
               (absemigr_perm120 X opp is n1 n0 n2).

Definition abmonoid_perm210 :=
  λ M : abmonoid, absemigr_perm210 M (@op M) (abmonoid_to_absemigr M).

II. Tactics for rearranging words.

We employ the following naming conventions. By default a tactics given pertain only to equations and operate by default on the left-hand side of equations. Those that operate on both left- and right-hand sides of the goal are suffixed with _goal. Tactics that operate on the left-hand side of equations occurring as hypotheses are suffixed with _in. Those that operate on both left- and right-hand sides of equations occurring as hypotheses are suffixed with _both_in. Those that opexrate on all sides of goals and hypotheses are suffixed with _all.
TODO: More general version.
Ltac absemigr_ternary_perm X opp is s t u :=
  let f := eval hnf in opp in
      match goal with
        | |- ?lhs = ?rhs ⇒
          match lhs with
            | context[f (f t s) u] ⇒
              rewrite (absemigr_perm102 X f is t s u); idtac
            | context[f (f t u) s] ⇒
              rewrite (absemigr_perm120 X f is t u s); idtac
            | context[f (f u s) t] ⇒
              rewrite (absemigr_perm201 X f is u s t); idtac
            | context[f (f u t) s] ⇒
              rewrite (absemigr_perm210 X f is u t s); idtac
            | context[f (f s u) t] ⇒
              rewrite (absemigr_perm021 X f is s u t); idtac
            | context[f (f (f ?x t) s) u] ⇒
              rewrite (pr1 is x t s); rewrite (pr1 is x (f t s) u);
              rewrite (absemigr_perm102 X f is t s u);
              rewrite <- (pr1 is x (f s t) u);
              rewrite <- (pr1 is x s t); idtac
            | context[f (f (f ?x t) u) s] ⇒
              rewrite (pr1 is x t u); rewrite (pr1 is x (f t u) s);
              rewrite (absemigr_perm120 X f is t u s);
              rewrite <- (pr1 is x (f s t) u);
              rewrite <- (pr1 is x s t); idtac
            | context[f (f (f ?x u) s) t] ⇒
              rewrite (pr1 is x u s); rewrite (pr1 is x (f u s) t);
              rewrite (absemigr_perm201 X f is u s t);
              rewrite <- (pr1 is x (f s t) u);
              rewrite <- (pr1 is x s t); idtac
            | context[f (f (f ?x u) t) s] ⇒
              rewrite (pr1 is x u t); rewrite (pr1 is x (f u t) s);
              rewrite (absemigr_perm210 X f is u t s);
              rewrite <- (pr1 is x (f s t) u);
              rewrite <- (pr1 is x s t); idtac
            | context[f (f (f ?x s) u) t] ⇒
              rewrite (pr1 is x s u); rewrite (pr1 is x (f s u) t);
              rewrite (absemigr_perm021 X f is s u t);
              rewrite <- (pr1 is x (f s t) u);
              rewrite <- (pr1 is x s t); idtac
          end
      end.

Ltac abmonoid_ternary_perm M :=
  absemigr_ternary_perm M (@op M) (abmonoid_to_absemigr M).

Local Open Scope addmonoid.

Ltac abmonoid_not_word M s :=
  match s with
    | ?x + ?y ⇒ fail 1
    | _ ⇒ idtac
  end.

Ltac abmonoid_not_at_front M t s :=
  match t with
    | s ⇒ fail 1
    | context[s + ?x] ⇒ fail 1
    | _ ⇒ idtac
  end.

Ltac abmonoid_not_at_back M t s :=
  match t with
    | s ⇒ fail 1
    | ?x + s ⇒ fail 1
    | _ ⇒ idtac
  end.

Ltac abmonoid_move_to_back M s :=
  repeat
    let lhs := get_current_lhs in
    abmonoid_not_at_back M lhs s;
      match lhs with
        | s + ?x ⇒ rewrite (commax M s x)
        | context[?x + s + ?y] ⇒
          rewrite (abmonoid_perm021 M x s y)
        | context[s + ?x + ?y] ⇒
          rewrite (abmonoid_perm201 M s x y)
      end.

Ltac abmonoid_move_to_back_in M H s :=
  repeat
    let lhs := get_current_lhs_in H in
    abmonoid_not_at_back M lhs s;
      match lhs with
        | s + ?x ⇒ rewrite (commax M s x) in H
        | context[?x + s + ?y] ⇒
          rewrite (abmonoid_perm021 M x s y) in H
        | context[s + ?x + ?y] ⇒
          rewrite (abmonoid_perm201 M s x y) in H
      end.

Ltac abmonoid_move_to_front M s :=
  repeat
    let lhs := get_current_lhs in
    abmonoid_not_at_front M lhs s;
      match lhs with
        | context[?x + s] ⇒
          abmonoid_not_word M x; rewrite (commax M x s)
        | context[?x + ?y + s] ⇒ abmonoid_not_word M y;
            rewrite (abmonoid_perm021 M x y s)
      end.

Ltac abmonoid_move_to_front_in M H s :=
  repeat
    let lhs := get_current_lhs_in H in
    abmonoid_not_at_front M lhs s;
      match lhs with
        | context[?x + s] ⇒
          abmonoid_not_word M x; rewrite (commax M x s) in H
        | context[?x + ?y + s] ⇒ abmonoid_not_word M y;
            rewrite (abmonoid_perm021 M x y s) in H
      end.

Ltac abmonoid_move_to_front_goal M s :=
  repeat
    let rhs := get_current_rhs in
    abmonoid_not_at_front M rhs s;
      match rhs with
        | context[?x + s] ⇒
          abmonoid_not_word M x; rewrite (commax M x s)
        | context[?x + ?y + s] ⇒ abmonoid_not_word M y;
            rewrite (abmonoid_perm021 M x y s)
      end.

Ltac abmonoid_move_to_front_both_in M H s :=
  repeat
    let rhs := get_current_rhs_in H in
    abmonoid_not_at_front M rhs s;
      match rhs with
        | context[?x + s] ⇒
          abmonoid_not_word M x; rewrite (commax M x s) in H
        | context[?x + ?y + s] ⇒ abmonoid_not_word M y;
            rewrite (abmonoid_perm021 M x y s) in H
      end.

Ltac abmonoid_move_to_back_goal M s :=
  repeat
    let rhs := get_current_rhs in
    abmonoid_not_at_back M rhs s;
      match rhs with
        | context [s + ?x] ⇒ rewrite (commax M s x)
        | context[?x + s + ?y] ⇒ abmonoid_not_word M y;
            rewrite (abmonoid_perm021 M x s y)
        | context[s + ?x + ?y] ⇒
          abmonoid_not_word M x; abmonoid_not_word M y;
          rewrite (abmonoid_perm201 M s x y)
      end.

Ltac abmonoid_move_to_back_both_in M H s :=
  repeat
    let rhs := get_current_rhs_in H in
    abmonoid_not_at_back M rhs s;
      match rhs with
        | context [s + ?x] ⇒ rewrite (commax M s x)
        | context[?x + s + ?y] ⇒ abmonoid_not_word M y;
            rewrite (abmonoid_perm021 M x s y) in H
        | context[s + ?x + ?y] ⇒
          abmonoid_not_word M x; abmonoid_not_word M y;
          rewrite (abmonoid_perm201 M s x y) in H
      end.

Ltac abmonoid_group M s t :=
  abmonoid_move_to_front M t; abmonoid_move_to_front M s.

Ltac abmonoid_group_goal M s t :=
  abmonoid_move_to_front_goal M t; abmonoid_move_to_front_goal M s.

Ltac abmonoid_group_in M H s t :=
  abmonoid_move_to_front_in M H t; abmonoid_move_to_front_in M H s.

Ltac abmonoid_group_both_in M H s t :=
  abmonoid_move_to_front_both_in M H t; abmonoid_move_to_front_both_in M H s.

Ltac abmonoid_group_all M s t :=
  abmonoid_group_goal M s t;
  repeat
    match goal with
      | H : _ |- _ ⇒ abmonoid_group_both_in M H s t
    end.

t is a term of type M and abmonoid_group_as attempts to reorganize the lhs of the goal to include as a subterm t.
Ltac abmonoid_group_as M t :=
  match t with
    | ?x + ?y ⇒
      abmonoid_not_word M y; abmonoid_move_to_front M y;
      abmonoid_group_as M x
    | ?x ⇒ abmonoid_not_word M x; abmonoid_move_to_front M x
  end.

t is a term of type x = y for x, y : M and abmonoid_group_from attempts to reogranize the lhs of the goal to include as a subterm x.
Ltac abmonoid_group_from M t :=
  let T := type of t in
  match T with
    | ?lhs = ?rhs ⇒ abmonoid_group_as M lhs
  end.

Ltac abmonoid_op_strip M :=
  match goal with
    | |- ?lhs = ?rhs ⇒
      match lhs with
        | context [?x] ⇒
          match rhs with
            | context [x] ⇒ abmonoid_move_to_back_goal M x;
                apply (ap (λ v, v + x))
          end
      end
  end.

Ltac abmonoid_zap_body M f :=
  match goal with
    | |- ?lhs = ?rhs ⇒
      match lhs with
        | rhs ⇒ apply idpath
        | 0 ⇒ apply pathsinv0; abmonoid_zap_body M f
        | ?x + ?y ⇒
          match rhs with
            | y + x ⇒ apply (commax M x y)
          end
        | _ ⇒ (abmonoid_op_strip M; abmonoid_zap_body M f)
      end
    | E : ?l = ?r |- ?lhs = ?rhs ⇒ f E;
        let g := make_hyp_check E in
        let h := check_cons g f in
        abmonoid_group_from M E; matched_rewrite E; abmonoid_zap_body M h
  end.

Ltac abmonoid_zap M := monoid_clean_all M; abmonoid_zap_body M id_check.

TESTS