SmallStepNI/UtilTactics.v at master · aslanix/SmallStepNI · GitHub

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
From Stdlib Require Import Bool Arith List.
Require Import CpdtTactics SfLib LibTactics.
From Stdlib Require Import Program.Equality.


Set Implicit Arguments.


Ltac remove_duplicate_hypothesis := repeat
  match goal with
    | [ H : ?orig, H' : ?orig |- _ ] => clear H'
  end.

Ltac destruct_split :=
  match goal with
    | [ H : _ /\ _  |- _ ] => destruct H
    | [ H : _ \/ _  |- _ ] => destruct H
    | [ H : exists _,_ |- _ ] => destruct H
    | [ |- _ /\ _ ] => split
    | [ |- _ \/ _ ] => split
    | [ |- _ -> _ ] => intros

  end.


Ltac super_destruct_split :=
  repeat (destruct_split; subst; auto).


Ltac clear_nq_facts:=

  match goal with
    |   [  H  : ?X <> ?Y -> _ ,
           H' : ?X = ?Y |- _] =>
        clear H
    |   [  H  :  ?X = ?Y -> _ ,
           H' : ?X <> ?Y |- _] =>
        clear H
  end.


Ltac super_destruct :=
      repeat
        match goal with  [ H : context [ _ /\ _ ] |- _ ] =>
                         destruct H
        end.


Ltac subst_trivial:=
  repeat match goal
         with [ H : ?a = ?a -> _ |- _] =>
              let H' := fresh in
              assert (a = a) as H' by auto;
                specialize (H H'); clear H'
         end; subst.


Ltac clear_impossible:=
  repeat match goal with
             [ H : ?X <> ?X -> _ |- _ ] => clear H
               end.


Ltac specialize_gen:=
  match goal with
    | [  H  : ?F -> _ ,
              H' : ?F |- _] =>
      specialize (H H')
    | [ H : ?X = ?X -> _ |- _ ] =>
      let h := fresh "H"
      in
      assert (X = X) by auto;
        specialize (H h);
        clear h


  end.

Ltac specialize_gens := specialize_gen; subst~ .


Ltac cleanup := subst; subst_trivial; clear_impossible.
Ltac duplicate H :=
  let H' := fresh in assert (H' := H).


Ltac destruct_exists_conj:=
  repeat
    match goal with
      | [ H: context [exists _,_ ] |- _] => destruct H
      | [ H: context [ _ /\ _ ] |- _] => destruct H
    end.


Ltac destruct_conj :=
            repeat match goal with
                     | [ H: _ /\ _ |- _ ] => destruct H
              end.


Ltac destruct_exists :=
            repeat match goal with
                       | [ H : exists _, _ |- _ ] => destruct H
                   end.

Ltac clear_trivial:=
          match goal with
            | [ H: ?X = ?X |- _ ] => clear H
          end.