Library Paco.hpattern

Set Implicit Arguments.

Definition hresolve_arg (A:Type) (a:A) := True.

Ltac hresolve_pre C T tac_resolve :=
 (let hT := fresh "_temp_" in
    assert (hT : hresolve_arg T) by (exact I);
  let hx := fresh "hx" in
    set (hx := C) in hT;
    lazymatch goal with [ _ : @hresolve_arg _ ?T' |- _ ] => tac_resolve hx T' end;
    clear hT ;
  let hf := fresh "hf" in
    intro hf).

Ltac hresolve_post tac :=
 (lazymatch goal with [ hf := ?T' |- _ ] => clear hf;
    lazymatch goal with [ hx := _ |- _ ] => tac T' hx; try (clear hx) end
  end).

Tactic Notation "hresolve_constr" constr(C) "at" int_or_var(occ) "in" constr(T) :=
  hresolve_pre C T ltac:(fun hx T' => hresolve_core (hx := C) at occ in T').

Tactic Notation "hresolve_constr" constr(C) "in" constr(T) :=
  hresolve_pre C T ltac:(fun hx T' => hresolve_core (hx := C) in T').

Ltac get_concl := lazymatch goal with [ |- ?G ] => G end.

Ltac get_hyp H := match goal with [ Hcrr : ?G |- _ ] => match Hcrr with H => G end end.

Tactic Notation "hresolve" constr(C) "at" int_or_var(occ) :=
 (let G := get_concl in hresolve_constr C at occ in G; hresolve_post ltac:(fun G' hx => change G')).

Tactic Notation "hresolve" constr(C) :=
 (let G := get_concl in hresolve_constr C in G; hresolve_post ltac:(fun G' hx => change G')).

Tactic Notation "hresolve" constr(C) "at" int_or_var(occ) "in" hyp(H) :=
 (let G := get_hyp H in hresolve_constr C at occ in G; hresolve_post ltac:(fun G' hx => change G' in H)).

Tactic Notation "hresolve" constr(C) "in" hyp(H) :=
 (let G := get_hyp H in hresolve_constr C in G; hresolve_post ltac:(fun G' hx => change G' in H)).

Tactic Notation "hpattern" constr(C) "at" int_or_var(occ) :=
 (let G := get_concl in hresolve_constr C at occ in G; hresolve_post ltac:(fun G' hx => change G'; pattern hx; change hx with C)).

Tactic Notation "hpattern" constr(C) :=
 (let G := get_concl in hresolve_constr C in G; hresolve_post ltac:(fun G' hx => change G'; pattern hx; change hx with C)).

Tactic Notation "hpattern" constr(C) "at" int_or_var(occ) "in" hyp(H) :=
 (let G := get_hyp H in hresolve_constr C at occ in G; hresolve_post ltac:(fun G' hx => change G' in H; pattern hx in H; change hx with C in H)).

Tactic Notation "hpattern" constr(C) "in" hyp(H) :=
 (let G := get_hyp H in hresolve_constr C in G; hresolve_post ltac:(fun G' hx => change G' in H; pattern hx in H; change hx with C in H)).

Tactic Notation "hgeneralize" constr(C) "at" int_or_var(occ) "as" ident(id) :=
 (let G := get_concl in hresolve_constr C at occ in G; hresolve_post ltac:(fun G' hx => change G'; generalize hx as id)).

Tactic Notation "hgeneralize" constr(C) "as" ident(id) :=
 (let G := get_concl in hresolve_constr C in G; hresolve_post ltac:(fun G' hx => change G'; generalize hx as id)).

Tactic Notation "hgeneralize_simpl" constr(C) "at" int_or_var(occ) "as" ident(id) :=
 (hgeneralize C at occ as id; intro; lazymatch goal with [ H : _ |- _ ] => simpl in H; revert H end).

Tactic Notation "hgeneralize_simpl" constr(C) "as" ident(id) :=
 (hgeneralize C as id; intro; lazymatch goal with [ H : _ |- _ ] => simpl in H; revert H end).

Ltac hrewrite_with eqn tac_res :=
 (lazymatch (type of eqn) with @eq _ ?X ?Y =>
    let G := get_concl in
      tac_res X G;
      hresolve_post ltac:(fun G' hx =>
        change G'; let Heqn := fresh "_temp_" in assert (Heqn : hx = Y) by (apply eqn); rewrite Heqn; clear Heqn)
  end).

Tactic Notation "hrewrite" constr(eqn) "at" int_or_var(occ) :=
  hrewrite_with eqn ltac:(fun X G => hresolve_constr X at occ in G).

Tactic Notation "hrewrite" "<-" constr(eqn) "at" int_or_var(occ) := (hrewrite (sym_eq eqn) at occ).

Tactic Notation "hrewrite" constr(eqn) :=
  hrewrite_with eqn ltac:(fun X G => hresolve_constr X in G).

Tactic Notation "hrewrite" "<-" constr(eqn) := (hrewrite (sym_eq eqn)).