frap/Frap.v
2016-02-14 19:23:26 -05:00

85 lines
2.6 KiB
Coq

Require Import String Arith Omega Program Sets Relations Map Var Invariant Bool.
Export String Arith Sets Relations Map Var Invariant Bool.
Require Import List.
Export List ListNotations.
Open Scope string_scope.
Open Scope list_scope.
Ltac inductN n :=
match goal with
| [ |- forall x : ?E, _ ] =>
match type of E with
| Prop =>
let H := fresh in intro H;
match n with
| 1 => dependent induction H
| S ?n' => inductN n'
end
| _ => intro; inductN n
end
end.
Ltac induct e := inductN e || dependent induction e.
Ltac invert' H := inversion H; clear H; subst.
Ltac invertN n :=
match goal with
| [ |- forall x : ?E, _ ] =>
match type of E with
| Prop =>
let H := fresh in intro H;
match n with
| 1 => invert' H
| S ?n' => invertN n'
end
| _ => intro; invertN n
end
end.
Ltac invert e := invertN e || invert' e.
Ltac invert0 e := invert e; fail.
Ltac invert1 e := invert0 e || (invert e; []).
Ltac invert2 e := invert1 e || (invert e; [|]).
Ltac simplify := repeat progress (simpl in *; intros; try autorewrite with core in *; repeat unifyTails);
repeat (removeDups || doSubtract).
Ltac propositional := intuition idtac.
Ltac linear_arithmetic := intros;
repeat match goal with
| [ |- context[max ?a ?b] ] =>
let Heq := fresh "Heq" in destruct (Max.max_spec a b) as [[? Heq] | [? Heq]];
rewrite Heq in *; clear Heq
| [ _ : context[max ?a ?b] |- _ ] =>
let Heq := fresh "Heq" in destruct (Max.max_spec a b) as [[? Heq] | [? Heq]];
rewrite Heq in *; clear Heq
| [ |- context[min ?a ?b] ] =>
let Heq := fresh "Heq" in destruct (Min.min_spec a b) as [[? Heq] | [? Heq]];
rewrite Heq in *; clear Heq
| [ _ : context[min ?a ?b] |- _ ] =>
let Heq := fresh "Heq" in destruct (Min.min_spec a b) as [[? Heq] | [? Heq]];
rewrite Heq in *; clear Heq
end; omega.
Ltac equality := intuition congruence.
Ltac cases E :=
((is_var E; destruct E)
|| match type of E with
| {_} + {_} => destruct E
| _ => let Heq := fresh "Heq" in destruct E eqn:Heq
end);
repeat match goal with
| [ H : _ = left _ |- _ ] => clear H
| [ H : _ = right _ |- _ ] => clear H
end.
Global Opaque max min.
Infix "==n" := eq_nat_dec (no associativity, at level 50).
Export Frap.Map.
Ltac maps_equal := Frap.Map.M.maps_equal; simplify.