Library HoTT.Tactics.RewriteModuloAssociativity

Tactics for rewriting modulo assciativity

Require Import Overture PathGroupoids.
Require Import Tactics.BinderApply.

Local Open Scope path_scope.

Throughout this file, we prefix with idtac; all imperative tactics (those not returning constrs) which would otherwise start with let or match. This prevents them from being evaluated at the call site. See https://coq.inria.fr/bugs/show_bug.cgi?id=3498 for more details on this difference between tactics and tactic expressions.
rewrite lem modulo associativity using:
  • assoc_tac : unit to associate the goal (in place)
  • assoc_in_tac : hyp unit to associate the hypothesis (in place)
  • prepostcompose_any_tac : constr constr to pre/post compose an arbitrary morphism onto the lemma
  • rew_tac : hyp unit to do the actual rewriting (in place). This tactic is called first with the non-associated version of the lemma, then with the associated version.
Ltac rewriteA_using_helper rew_tac lem prepostcompose_any_tac assoc_tac assoc_in_tac :=
  idtac;
  let lem' := prepostcompose_any_tac lem in
  let H := fresh in
  pose proof lem' as H;
    assoc_tac;
    match goal with
      | _rew_tac H
      | _assoc_in_tac H;
            rew_tac H
    end;
    clear H.

This tactic is similar to the above, except that it passes both the unassociated lemma and the associated lemma to repeat_rew_tac, which may then contain optimizations over a manual repeat such as being rewrite ?lem, ?lem'.
Ltac repeat_rewriteA_using_helper repeat_rew_tac lem prepostcompose_any_tac assoc_tac assoc_in_tac :=
  idtac;
  let lem' := prepostcompose_any_tac lem in
  let H := fresh in
  pose proof lem' as H;
    assoc_in_tac H;
    assoc_tac;
    repeat_rew_tac lem' H;
    clear H.

Module Export Compose.

Rewriting modulo associativity of composition (o)

Since f o g is just a notation, we need to define a constant that isn't reduced by cbv beta.
  Local Definition compose {A B C} (g : B C) (f : A B) (x : A) : C := g (f x).

  Ltac to_compose T :=
    match T with
      | context G[?g o ?f] ⇒ let T' := context G[compose g f] in
                              to_compose T'
      | ?T'constr:(T')
    end.

Turns a lemma of type f = g into h, h o f = h o g
  Ltac precompose_any H :=
    let ret := make_tac_under_binders_using_in ltac:(fun H ⇒ (let H' := fresh in
                                                               rename H into H';
                                                               let T := type of H' in
                                                               let T' := to_compose T in
                                                               pose proof (fun src (g : _ src) ⇒ @ap _ _ (fun fcompose g f) _ _ (H' : T')) as H))
                                                      ltac:(idtac) H in
    let T := type of ret in
    let T' := (eval cbv beta in T) in
    constr:(ret : T').

Associates a type fully to the left
  Ltac left_associate_compose_type T :=
    let rec_tac := left_associate_compose_type in
    match to_compose T with
      | a : ?A, @?P alet ret := constr:( a : A, let T' := P a in
                                                                 ltac:(
                                                                   let T'' := (eval unfold T' in T') in
                                                                   let ret := rec_tac T'' in
                                                                   exact ret)) in
                                eval cbv beta zeta in ret
      | context T'[compose ?a (compose ?b ?c)]
        ⇒ let T'' := context T'[compose (compose a b) c] in
           rec_tac T''
      | ?T'constr:(T')
    end.

  Ltac left_associate_compose_in_type_of H :=
    let T := type of H in
    let T' := left_associate_compose_type T in
    constr:(H : T').

  Ltac left_associate_compose :=
    idtac;
    (lazymatch goal with
    | [ |- ?G ] ⇒ let G' := left_associate_compose_type G in change G'
     end).

  Ltac left_associate_compose_in H :=
    idtac;
    (lazymatch type of H with
    | ?Tlet T' := left_associate_compose_type T in change T' in H
     end).

  Ltac after_rewrite :=
    repeat match goal with
             | [ |- context G[compose ?g ?f] ] ⇒ let G' := context G[g o f] in change G'
             | _
               match goal with
                 | [ |- context G[@compose ?A ?B ?C ?g] ] ⇒ let G' := context G[fun f : A Bg o f] in change G'
                 | [ |- context G[@compose ?A ?B ?C] ] ⇒ let G' := context G[fun (g : B C) (f : A B) ⇒ g o f] in change G'
                 | _progress cbv delta [compose]
               end;
                 idtac "Warning: could not fully restore pre-rewrite state."
                       "Try introducing more things or removing binders."
           end.

  Tactic Notation "rewriteoA" constr(lem) :=
    rewriteA_using_helper ltac:(fun lem'rewrite lem') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.
  Tactic Notation "rewriteoA" "->" constr(lem) :=
    rewriteA_using_helper ltac:(fun lem'rewritelem') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.
  Tactic Notation "rewriteoA" "<-" constr(lem) :=
    rewriteA_using_helper ltac:(fun lem'rewrite <- lem') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.
  Tactic Notation "rewriteoA" "!" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''progress rewrite ?lem', ?lem'') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.
  Tactic Notation "rewriteoA" "?" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''rewrite ?lem', ?lem'') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.
  Tactic Notation "rewriteoA" "->" "!" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''progress rewrite → ?lem', → ?lem'') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.
  Tactic Notation "rewriteoA" "<-" "!" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''progress rewrite <- ?lem', <- ?lem'') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.
  Tactic Notation "rewriteoA" "->" "?" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''rewrite → ?lem', → ?lem'') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.
  Tactic Notation "rewriteoA" "<-" "?" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''rewrite <- ?lem', <- ?lem'') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.

  Tactic Notation "erewriteoA" constr(lem) :=
    rewriteA_using_helper ltac:(fun lem'erewrite lem') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.
  Tactic Notation "erewriteoA" "->" constr(lem) :=
    rewriteA_using_helper ltac:(fun lem'erewritelem') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.
  Tactic Notation "erewriteoA" "<-" constr(lem) :=
    rewriteA_using_helper ltac:(fun lem'erewrite <- lem') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.
  Tactic Notation "erewriteoA" "!" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''progress erewrite ?lem', ?lem'') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.
  Tactic Notation "erewriteoA" "?" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''erewrite ?lem', ?lem'') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.
  Tactic Notation "erewriteoA" "->" "!" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''progress erewrite → ?lem', → ?lem'') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.
  Tactic Notation "erewriteoA" "<-" "!" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''progress erewrite <- ?lem', <- ?lem'') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.
  Tactic Notation "erewriteoA" "->" "?" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''erewrite → ?lem', → ?lem'') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.
  Tactic Notation "erewriteoA" "<-" "?" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''erewrite <- ?lem', <- ?lem'') lem ltac:(precompose_any) ltac:(left_associate_compose) ltac:(left_associate_compose_in); after_rewrite.

  Tactic Notation "rewrite∘A" constr(lem) := rewriteoA lem.
  Tactic Notation "rewrite∘A" "->" constr(lem) := rewriteoAlem.
  Tactic Notation "rewrite∘A" "<-" constr(lem) := rewriteoA <- lem.
  Tactic Notation "rewrite∘A" "!" constr(lem) := rewriteoA !lem.
  Tactic Notation "rewrite∘A" "?" constr(lem) := rewriteoA ? lem.
  Tactic Notation "rewrite∘A" "->" "!" constr(lem) := rewriteoA → !lem.
  Tactic Notation "rewrite∘A" "<-" "!" constr(lem) := rewriteoA <- !lem.
  Tactic Notation "rewrite∘A" "->" "?" constr(lem) := rewriteoA → ? lem.
  Tactic Notation "rewrite∘A" "<-" "?" constr(lem) := rewriteoA <- ? lem.

  Tactic Notation "erewrite∘A" open_constr(lem) := erewriteoA lem.
  Tactic Notation "erewrite∘A" "->" open_constr(lem) := erewriteoAlem.
  Tactic Notation "erewrite∘A" "<-" open_constr(lem) := erewriteoA <- lem.
  Tactic Notation "erewrite∘A" "!" open_constr(lem) := erewriteoA !lem.
  Tactic Notation "erewrite∘A" "?" open_constr(lem) := erewriteoA ? lem.
  Tactic Notation "erewrite∘A" "->" "!" open_constr(lem) := erewriteoA → !lem.
  Tactic Notation "erewrite∘A" "<-" "!" open_constr(lem) := erewriteoA <- !lem.
  Tactic Notation "erewrite∘A" "->" "?" open_constr(lem) := erewriteoA → ? lem.
  Tactic Notation "erewrite∘A" "<-" "?" open_constr(lem) := erewriteoA <- ? lem.
End Compose.

Module Export Concat.

Rewriting modulo associativity of concatenation (@)

Turns a lemma of type f = g into h, h @ f = h @ g
  Ltac preconcat_any H :=
    let ret := make_tac_under_binders_using_in ltac:(fun H ⇒ (let H' := fresh in
                                                               rename H into H';
                                                               pose proof (fun dst (g : dst = _) ⇒ @ap _ _ (fun fg @ f) _ _ H') as H))
                                                      ltac:(idtac) H in
    let T := type of ret in
    let T' := (eval cbv beta in T) in
    constr:(ret : T').

Associates a path fully to the left
  Ltac left_associate_concat_in H :=
    let rec_tac := left_associate_concat_in in
    let T := type of H in
    let T' := (eval cbv beta in T) in
    match T' with
      | a : ?A, @?P alet ret := constr:(fun a : Alet H' := H a in
                                                                ltac:(
                                                                  let H'' := (eval unfold H' in H') in
                                                                  let ret := rec_tac H'' in
                                                                  exact ret)) in
                                let T := type of ret in
                                let T' := (eval cbv beta zeta in T) in
                                let ret' := (eval cbv beta zeta in ret) in
                                constr:(ret' : T')
      | context[@concat ?A1 ?x1 ?y1 ?z1 ?a (@concat ?A2 ?x2 ?y2 ?z2 ?b ?c)] ⇒
        (lazymatch eval pattern (@concat A1 x1 y1 z1 a (@concat A2 x2 y2 z2 b c)) in T' with
        | ?P _let H' := constr:(transport P (concat_p_pp a b c) H) in
                  rec_tac H'
         end)
      | ?T'constr:(H : T')
    end.

We really should just use setoid_rewrite !concat_p_pp here, to take care of binders, but we threw away Setoids.
  Ltac left_associate_concat :=
    repeat match goal with
             | _rewrite → !concat_p_pp
             | [ |- a : ?A, _ ] ⇒ let H := fresh in
                                          intro H;
                                            left_associate_concat;
                                            revert H
           end.

  Ltac left_associate_concat_in_hyp H :=
    let H' := fresh in
    rename H into H';
      let H_rep := left_associate_concat_in H' in
      pose proof H_rep as H;
        clear H'.

  Tactic Notation "rewrite@A" constr(lem) :=
    rewriteA_using_helper ltac:(fun lem'rewrite lem') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).
  Tactic Notation "rewrite@A" "->" constr(lem) :=
    rewriteA_using_helper ltac:(fun lem'rewritelem') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).
  Tactic Notation "rewrite@A" "<-" constr(lem) :=
    rewriteA_using_helper ltac:(fun lem'rewrite <- lem') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).
  Tactic Notation "rewrite@A" "!" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''progress rewrite ?lem', ?lem'') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).
  Tactic Notation "rewrite@A" "?" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''rewrite ?lem', ?lem'') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).
  Tactic Notation "rewrite@A" "->" "!" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''progress rewrite → ?lem', → ?lem'') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).
  Tactic Notation "rewrite@A" "<-" "!" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''progress rewrite <- ?lem', <- ?lem'') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).
  Tactic Notation "rewrite@A" "->" "?" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''rewrite → ?lem', → ?lem'') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).
  Tactic Notation "rewrite@A" "<-" "?" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''rewrite <- ?lem', <- ?lem'') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).

  Tactic Notation "erewrite@A" constr(lem) :=
    rewriteA_using_helper ltac:(fun lem'erewrite lem') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).
  Tactic Notation "erewrite@A" "->" constr(lem) :=
    rewriteA_using_helper ltac:(fun lem'erewritelem') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).
  Tactic Notation "erewrite@A" "<-" constr(lem) :=
    rewriteA_using_helper ltac:(fun lem'erewrite <- lem') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).
  Tactic Notation "erewrite@A" "!" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''progress erewrite ?lem', ?lem'') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).
  Tactic Notation "erewrite@A" "?" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''erewrite ?lem', ?lem'') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).
  Tactic Notation "erewrite@A" "->" "!" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''progress erewrite → ?lem', → ?lem'') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).
  Tactic Notation "erewrite@A" "<-" "!" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''progress erewrite <- ?lem', <- ?lem'') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).
  Tactic Notation "erewrite@A" "->" "?" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''erewrite → ?lem', → ?lem'') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).
  Tactic Notation "erewrite@A" "<-" "?" constr(lem) :=
    repeat_rewriteA_using_helper ltac:(fun lem' lem''erewrite <- ?lem', <- ?lem'') lem ltac:(preconcat_any) ltac:(left_associate_concat) ltac:(left_associate_concat_in_hyp).

  Tactic Notation "rewrite•A" constr(lem) := rewrite@A lem.
  Tactic Notation "rewrite•A" "->" constr(lem) := rewrite@Alem.
  Tactic Notation "rewrite•A" "<-" constr(lem) := rewrite@A <- lem.
  Tactic Notation "rewrite•A" "!" constr(lem) := rewrite@A !lem.
  Tactic Notation "rewrite•A" "?" constr(lem) := rewrite@A ? lem.
  Tactic Notation "rewrite•A" "->" "!" constr(lem) := rewrite@A → !lem.
  Tactic Notation "rewrite•A" "<-" "!" constr(lem) := rewrite@A <- !lem.
  Tactic Notation "rewrite•A" "->" "?" constr(lem) := rewrite@A → ? lem.
  Tactic Notation "rewrite•A" "<-" "?" constr(lem) := rewrite@A <- ? lem.

  Tactic Notation "erewrite•A" open_constr(lem) := erewrite@A lem.
  Tactic Notation "erewrite•A" "->" open_constr(lem) := erewrite@Alem.
  Tactic Notation "erewrite•A" "<-" open_constr(lem) := erewrite@A <- lem.
  Tactic Notation "erewrite•A" "!" open_constr(lem) := erewrite@A !lem.
  Tactic Notation "erewrite•A" "?" open_constr(lem) := erewrite@A ? lem.
  Tactic Notation "erewrite•A" "->" "!" open_constr(lem) := erewrite@A → !lem.
  Tactic Notation "erewrite•A" "<-" "!" open_constr(lem) := erewrite@A <- !lem.
  Tactic Notation "erewrite•A" "->" "?" open_constr(lem) := erewrite@A → ? lem.
  Tactic Notation "erewrite•A" "<-" "?" open_constr(lem) := erewrite@A <- ? lem.
End Concat.

Section examples.
  Section compose.
    Example simple_01 {A} (f g h i j : A A) : f o g = h (i o f) o (g o j) = i o h o j.
    Proof.
      intro H.
      rewriteA H.
      reflexivity.
    Abort.

    Example simple_02 {A} (f g h i j : A A) : f o g = h (i o f) o (g o f o g o j) = i o h o h o j.
    Proof.
      intro H.
      rewriteA !H.
      reflexivity.
    Abort.
  End compose.

  Section concat.
    Example simple_01 {A} {a : A} (f g h i j : a = a) : f @ g = h (i @ f) @ (g @ j) = i @ h @ j.
    Proof.
      intro H.
      rewrite@A H.
      reflexivity.
    Abort.

    Example simple_02 {A} {a : A} (f g h i j : A = A) : f @ g = h (i @ f) @ (g @ f @ g @ j) = i @ h @ h @ j.
    Proof.
      intro H.
      rewrite@A !H.
      reflexivity.
    Abort.
  End concat.
End examples.