HyPre.util.Tac

From Coq Require Import Lia.

Ltac exploit' H :=
  let p := fresh "Q" in
  lazymatch type of H with
  | ?P -> ?Q => assert P as p; [eauto|specialize (H p); clear p]
  | forall (x : ?P), ?Q => lazymatch goal with
                     | [ p : P |- _ ] => specialize (H p)
                     end
  end.

Ltac exploit_lia' H :=
  let p := fresh "Q" in
  lazymatch type of H with
  | ?P -> ?Q => assert P as p; [eauto; try lia|specialize (H p); clear p]
  | forall (x : ?P), ?Q => lazymatch goal with
                     | [ p : P |- _ ] => specialize (H p)
                     end
  end.

Ltac exploit_lia H :=
  let p := fresh "Q" in
  lazymatch type of H with
  | ?P -> ?Q => assert P as p; [eauto;try lia|specialize (H p); clear p;try exploit_lia H]
  | forall (x : ?P), ?Q => lazymatch goal with
                     | [ p : P |- _ ] => specialize (H p);try exploit_lia H
                     end
  end.

Ltac exploit H :=
  let p := fresh "Q" in
  lazymatch type of H with
  | ?P -> ?Q => assert P as p; [eauto|specialize (H p); clear p;try exploit H]
  | forall (x : ?P), ?Q => lazymatch goal with
                     | [ p : P |- _ ] => specialize (H p);try exploit H
                     end
  end.

Ltac split_conj :=
  lazymatch goal with
  | [ |- _ /\ _ ] => split; split_conj
  | [ |- _ <-> _ ] => split; split_conj
  | _ => idtac
  end.

Ltac destructH' H :=
  lazymatch type of H with
  | ?P /\ ?Q => let H1 := fresh H in
              let H2 := fresh H in
              destruct H as [H1 H2]; destructH' H1; destructH' H2
  | exists x, ?P => let x0 := fresh x in
              destruct H as [x0 H]; destructH' H
  | _ => idtac
  end.

Ltac destructH :=
  match goal with
  | [H : ?P /\ ?Q |- _ ] => let H1 := fresh H in
                         let H2 := fresh H in
                         destruct H as [H1 H2]; destructH' H1; destructH' H2
  | [H : exists x, ?P |- _ ] => let x0 := fresh x in
                         destruct H as [x0 H]; destructH' H
  end.

Ltac split1 := match goal with
                 |- ?x /\ ?y => let Q := fresh "Q" in enough (x /\ (x -> y)) as Q; [clear - Q; firstorder|split]
               end.

Ltac split2 := match goal with
                 |- ?x /\ ?y => let Q := fresh "Q" in enough ((y -> x) /\ x) as Q; [split|clear - Q; firstorder]
               end.

Ltac destr_let_pair
  := match goal with [|- context c [let (_,_) := ?x in _]] => destruct x end.

Ltac destr_let_pair_eqn
  := match goal with [|- context c [let (_,_) := ?x in _]] => destruct x eqn:E end.

Ltac destr_m1 := match goal with [|- match ?x with _ => _ end] => destruct x end.
Ltac destr_m2 := match goal with [|- match match ?x with _ => _ end with _ => _ end] => destruct x end.
Ltac destr_m3 := match goal with [|- match match match ?x with _=>_ end with _=>_ end with _=>_ end] => destruct x end.
Ltac destr_m4 := match goal with [|- match match match match ?x with _=>_ end with _=>_ end with _=>_ end with _=>_ end] => destruct x end.
Ltac destr_m5 := match goal with [|- match match match match match ?x with _=>_ end with _=>_ end with _=>_ end with _=>_ end with _=>_ end] => destruct x end.
Ltac destr_m1_eqn E := match goal with [|- match ?x with _ => _ end] => destruct x eqn:E end.
Ltac destr_m2_eqn E := match goal with [|- match match ?x with _ => _ end with _ => _ end] => destruct x eqn:E end.
Ltac destr_m3_eqn E := match goal with [|- match match match ?x with _=>_ end with _=>_ end with _=>_ end] => destruct x eqn:E end.
Ltac destr_m4_eqn := match goal with [|- match match match match ?x with _=>_ end with _=>_ end with _=>_ end with _=>_ end] => destruct x eqn:E end.
Ltac destr_m5_eqn := match goal with [|- match match match match match ?x with _=>_ end with _=>_ end with _=>_ end with _=>_ end with _=>_ end] => destruct x eqn:E end.

From Coq Require Import Lists.List.
Import ListNotations.

Lemma rcons_destructT {A : Type} (l : list A) : {a & { l' | l = l' ++ [a] } } + {l = nil}.
Proof.
  rewrite <-(rev_involutive l).
  remember (rev l) as rl. clear Heqrl l.
  eapply list_rect with (l:=rl).
  - right. reflexivity.
  - intros.
    left.
    exists a, (rev l). cbn.
    reflexivity.
Qed.

Lemma rcons_destruct {A : Type} (l : list A) : l = [] \/ exists a l', l = l' ++ [a].
Proof.
  specialize (rcons_destructT l) as Q.
  destruct Q.
  - right. destruct s,s. eexists;eauto.
  - left. assumption.
Qed.

Ltac list_destr_r l :=
  let H := fresh "Hl" in
  let x := fresh "x" in
  let l' := fresh "l" in
  let Hlx := fresh "Hx" in
  specialize (rcons_destruct l) as H;
  destruct H as [H|[x [l' Hlx]]];
  subst l.

Ltac cbn_this x
  := let Qy := fresh "Qx" in
     let y := fresh "y" in
     remember x as y eqn:Qy;
     cbn in Qy;
     subst y.