blob: eac46751ea86ac003d3a4634b4229701aca4369d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
|
Ltac induction_with_subterm c H :=
let x := fresh "x" in
let y := fresh "y" in
(set(x := c) ; assert(y:x = c) by reflexivity ;
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).
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 t := fresh "t" in
set (t := p); simpl in t ;
try ((case t ; clear t) || (clearbody t; rewrite (UIP_refl _ _ t); clear t))
end
end.
|
