Automation.v 2.58 KB
Newer Older
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
1
2
(* This file implements various helper tactics *)

3
4
5
6
7
8
9
10
From Coq Require Import Eqdep List Omega Permutation.
Import ListNotations.

Lemma Permutation_app_middle {A : Type} (xs l1 l2 l3 l4 : list A) :
  Permutation (l1 ++ l2) (l3 ++ l4) ->
  Permutation (l1 ++ xs ++ l2) (l3 ++ xs ++ l4).
Proof.
  intros perm.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
11
12
13
14
  rewrite 2!(Permutation_app_comm xs).
  rewrite 2!app_assoc.
  apply Permutation_app_tail.
  auto.
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
Qed.

(* Change all x :: l into [x] ++ l *)
Ltac appify :=
  match goal with
  | [|- context[?e :: ?l]] =>
    match l with
    | nil => fail 1
    | _ => change (e :: l) with ([e] ++ l)
    end
  end.

Local Ltac reassoc_right :=
  match goal with
  | [|- Permutation _ (?l1 ++ ?l2 ++ ?l3)] => rewrite (app_assoc l1 l2 l3)
  end.

Local Ltac reassoc_left :=
  match goal with
  | [|- Permutation (?l1 ++ ?l2 ++ ?l3) _] => rewrite (app_assoc l1 l2 l3)
  end.

Local Ltac unassoc_right :=
  repeat
    match goal with
    | [|- Permutation _ ((?l1 ++ ?l2) ++ ?l3)] => rewrite <- (app_assoc l1 l2 l3)
    end.

43
Local Ltac perm_simplify_once :=
44
45
46
47
48
49
50
51
  let rec aux :=
      apply Permutation_app_middle ||
      tryif reassoc_right
        then aux
        else (unassoc_right; reassoc_left; aux) in
  repeat rewrite <- app_assoc;
  aux.

52
Local Ltac perm_simplify_round :=
53
  cbn;
54
55
56
57
58
59
60
  repeat appify;
  (* Change into [] ++ l ++ [] *)
  match goal with
  | [|- Permutation ?l1 ?l2] => change l1 with ([] ++ l1);
                                change l2 with ([] ++ l2);
                                rewrite <- (app_nil_r l1), <- (app_nil_r l2)
  end;
61
  repeat perm_simplify_once;
62
  cbn;
63
64
65
66
67
68
69
  repeat rewrite <- app_assoc;
  repeat rewrite app_nil_r;
  repeat
    match goal with
    | [H: Permutation ?l1 ?l2|-_] => rewrite H
    end.

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
70
(* Automatically tries to solve obvious "Permutation x y" goals. *)
71
72
Ltac perm_simplify :=
  repeat perm_simplify_round;
73
  cbn;
74
75
  try apply Permutation_refl.

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
76
Ltac destruct_match :=
77
78
  match goal with
  | [|- context [ match ?x with _ => _ end ]] => destruct x eqn:?
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
79
  | [H: context [ match ?x with _ => _ end ] |- _] => destruct x eqn:?
80
81
  end.

82
83
84
85
86
87
Ltac destruct_if :=
  match goal with
  | [|- context [ if ?x then _ else _ ]] => destruct x eqn:?
  | [H: context [ if ?x then _ else _ ] |- _] => destruct x eqn:?
  end.

88
89
90
91
92
Ltac destruct_units :=
  repeat
    match goal with
    | [u: unit |- _] => destruct u
    end.
93
94
95
96
97

Ltac solve_by_rewrite :=
  match goal with
  | [H: _ |- _] => now rewrite H
  end.
98
99
100
101
102
103
104
105
106
107
108

Ltac solve_by_inversion :=
  match goal with
  | [H: _ |- _] => solve [inversion H]
  end.

Ltac specialize_hypotheses :=
  repeat
    match goal with
    | [H: _ -> _ |- _] => specialize (H ltac:(auto))
    end.