blob: 2e5523b207262c0538defeb545f27d5448a79b35 (
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
|
Require Export Coq.Bool.Bool.
Require Export Coq.Lists.List.
Require Export Coq.Strings.String.
Require Export Coq.ZArith.ZArith.
Require Export Coq.ZArith.Znumtheory.
Require Import Coq.micromega.Lia.
Require Export TVSMT.Coqlib.
(* Require Import compcert.lib.Integers. *)
Require Export TVSMT.Errors.
(* This tactic due to Clement Pit-Claudel with some minor additions by JDP to
allow the result to be named: https://pit-claudel.fr/clement/MSc/#org96a1b5f *)
Inductive Learnt {A: Type} (a: A) :=
| AlreadyKnown : Learnt a.
Ltac learn_tac fact name :=
lazymatch goal with
| [ H: Learnt fact |- _ ] =>
fail 0 "fact" fact "has already been learnt"
| _ => let type := type of fact in
lazymatch goal with
| [ H: @Learnt type _ |- _ ] =>
fail 0 "fact" fact "of type" type "was already learnt through" H
| _ => let learnt := fresh "Learn" in
pose proof (AlreadyKnown fact) as learnt; pose proof fact as name
end
end.
Tactic Notation "learn" constr(fact) := let name := fresh "H" in learn_tac fact name.
Tactic Notation "learn" constr(fact) "as" simple_intropattern(name) := learn_tac fact name.
Ltac unfold_rec c := unfold c; fold c.
Ltac solve_by_inverts n :=
match goal with | H : ?T |- _ =>
match type of T with Prop =>
inversion H;
match n with S (S (?n')) => subst; try constructor; solve_by_inverts (S n') end
end
end.
Ltac solve_by_invert := solve_by_inverts 1.
Ltac invert x := inversion x; subst; clear x.
Ltac destruct_match :=
match goal with
| [ |- context[match ?x with | _ => _ end ] ] => destruct x eqn:?
| [ H: context[match ?x with | _ => _ end] |- _ ] => destruct x eqn:?
end.
Ltac auto_destruct x := destruct x eqn:?; simpl in *; try discriminate; try congruence.
Ltac nicify_hypotheses :=
repeat match goal with
| [ H : ex _ |- _ ] => invert H
| [ H : Some _ = Some _ |- _ ] => invert H
| [ H : OK _ = OK _ |- _ ] => invert H
| [ H : ?x = ?x |- _ ] => clear H
| [ H : _ /\ _ |- _ ] => invert H
| [ H : (_, _) = (_, _) |- _ ] => invert H
end.
Ltac nicify_goals :=
repeat match goal with
| [ |- _ /\ _ ] => split
| [ |- Some _ = Some _ ] => f_equal
| [ |- OK _ = OK _ ] => f_equal
| [ |- S _ = S _ ] => f_equal
end.
Ltac kill_bools :=
repeat match goal with
| [ H : _ && _ = true |- _ ] => apply andb_prop in H
| [ H : _ || _ = false |- _ ] => apply orb_false_elim in H
| [ H : negb _ = true |- _ ] => apply negb_true_iff in H
| [ H : negb _ = false |- _ ] => apply negb_false_iff in H
| [ H : _ <=? _ = true |- _ ] => apply Z.leb_le in H
| [ H : _ <=? _ = false |- _ ] => apply Z.leb_gt in H
| [ H : _ <? _ = true |- _ ] => apply Z.ltb_lt in H
| [ H : _ <? _ = false |- _ ] => apply Z.ltb_ge in H
| [ H : _ >=? _ = _ |- _ ] => rewrite Z.geb_leb in H
| [ H : _ >? _ = _ |- _ ] => rewrite Z.gtb_ltb in H
| [ H : _ =? _ = true |- _ ] => apply Z.eqb_eq in H
| [ H : _ =? _ = false |- _ ] => apply Z.eqb_neq in H
| [ H : (_ <=? _)%positive = true |- _ ] => apply Pos.leb_le in H
| [ H : (_ <=? _)%positive = false |- _ ] => apply Pos.leb_gt in H
| [ H : (_ <? _)%positive = true |- _ ] => apply Pos.ltb_lt in H
| [ H : (_ <? _)%positive = false |- _ ] => apply Pos.ltb_ge in H
| [ H : (_ =? _)%positive = true |- _ ] => apply Pos.eqb_eq in H
| [ H : (_ =? _)%positive = false |- _ ] => apply Pos.eqb_neq in H
end.
Ltac substpp :=
repeat match goal with
| [ H1 : ?x = Some _, H2 : ?x = Some _ |- _ ] =>
let EQ := fresh "EQ" in
learn H1 as EQ; rewrite H2 in EQ; invert EQ
| _ => idtac
end.
Ltac simplify := intros; simpl in *;
repeat progress (try nicify_hypotheses; try nicify_goals; try kill_bools; substpp);
simpl in *.
Ltac crush := simplify; try discriminate; try congruence; try (zify; lia);
try assumption; try (solve [auto]).
Ltac ecrush m := simplify; try discriminate; try congruence; try (zify; lia);
try assumption; try (solve [eauto with m]).
|
