diff options
Diffstat (limited to 'contrib/subtac/SubtacTactics.v')
| -rw-r--r-- | contrib/subtac/SubtacTactics.v | 158 |
1 files changed, 0 insertions, 158 deletions
diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v deleted file mode 100644 index a00234dd..00000000 --- a/contrib/subtac/SubtacTactics.v +++ /dev/null @@ -1,158 +0,0 @@ -Ltac induction_with_subterm c H := - let x := fresh "x" in - let y := fresh "y" in - (remember c as x ; rewrite <- y in H ; induction H ; subst). - -Ltac induction_on_subterm c := - let x := fresh "x" in - let y := fresh "y" in - (set(x := c) ; assert(y:x = c) by reflexivity ; clearbody x ; induction x ; inversion y ; try subst ; - clear y). - -Ltac induction_with_subterms c c' H := - let x := fresh "x" in - let y := fresh "y" in - let z := fresh "z" in - let w := fresh "w" in - (set(x := c) ; assert(y:x = c) by reflexivity ; - set(z := c') ; assert(w:z = c') by reflexivity ; - rewrite <- y in H ; rewrite <- w in H ; - induction H ; subst). - - -Ltac destruct_one_pair := - match goal with - | [H : (_ /\ _) |- _] => destruct H - | [H : prod _ _ |- _] => destruct H - end. - -Ltac destruct_pairs := repeat (destruct_one_pair). - -Ltac destruct_one_ex := - let tac H := let ph := fresh "H" in destruct H as [H ph] in - match goal with - | [H : (ex _) |- _] => tac H - | [H : (sig ?P) |- _ ] => tac H - | [H : (ex2 _) |- _] => tac H - end. - -Ltac destruct_exists := repeat (destruct_one_ex). - -Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht]. - -Tactic Notation "destruct" "or" ident(H) := destruct H as [H|H]. - -Tactic Notation "contradiction" "by" constr(t) := - let H := fresh in assert t as H by auto with * ; contradiction. - -Ltac discriminates := - match goal with - | [ H : ?x <> ?x |- _ ] => elim H ; reflexivity - | _ => discriminate - end. - -Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex). - -Ltac on_last_hyp tac := - match goal with - [ H : _ |- _ ] => tac H - end. - -Tactic Notation "on_last_hyp" tactic(t) := on_last_hyp t. - -Ltac revert_last := - match goal with - [ H : _ |- _ ] => revert H - end. - -Ltac reverse := repeat revert_last. - -Ltac on_call f tac := - match goal with - | H : ?T |- _ => - match T with - | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u) - | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v) - | context [f ?x ?y ?z ?w] => tac (f x y z w) - | context [f ?x ?y ?z] => tac (f x y z) - | context [f ?x ?y] => tac (f x y) - | context [f ?x] => tac (f x) - end - | |- ?T => - match T with - | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u) - | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v) - | context [f ?x ?y ?z ?w] => tac (f x y z w) - | context [f ?x ?y ?z] => tac (f x y z) - | context [f ?x ?y] => tac (f x y) - | context [f ?x] => tac (f x) - end - end. - -(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *) -Ltac destruct_call f := - let tac t := destruct t in on_call f tac. - -Ltac destruct_call_as f l := - let tac t := destruct t as l in on_call f tac. - -Tactic Notation "destruct_call" constr(f) := destruct_call f. -Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := destruct_call_as f l. - -Ltac myinjection := - let tac H := inversion H ; subst ; clear H in - match goal with - | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H - | [ H : ?f ?a ?b = ?f' ?a' ?b' |- _ ] => tac H - | [ H : ?f ?a ?b ?c = ?f' ?a' ?b' ?c' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d ?e ?g= ?f' ?a' ?b' ?c' ?d' ?e' ?g' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d ?e ?g ?h= ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i ?j = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' ?j' |- _ ] => tac H - | _ => idtac - end. - -Ltac destruct_nondep H := let H0 := fresh "H" in assert(H0 := H); destruct H0. - -Ltac bang := - match goal with - | |- ?x => - match x with - | context [False_rect _ ?p] => elim p - end - end. - -Require Import Eqdep. - -Ltac elim_eq_rect := - match goal with - | [ |- ?t ] => - match t with - | context [ @eq_rect _ _ _ _ _ ?p ] => - let P := fresh "P" in - set (P := p); simpl in P ; - try ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) - | context [ @eq_rect _ _ _ _ _ ?p _ ] => - let P := fresh "P" in - set (P := p); simpl in P ; - try ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) - end - end. - -Ltac real_elim_eq_rect := - match goal with - | [ |- ?t ] => - match t with - | context [ @eq_rect _ _ _ _ _ ?p ] => - let P := fresh "P" in - set (P := p); simpl in P ; - ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) - | context [ @eq_rect _ _ _ _ _ ?p _ ] => - let P := fresh "P" in - set (P := p); simpl in P ; - ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P)) - end - end. -
\ No newline at end of file |