mirror of
https://github.com/achlipala/frap.git
synced 2024-09-20 04:07:13 +00:00
128 lines
4 KiB
Coq
128 lines
4 KiB
Coq
Require Import String Arith Omega Program Sets Relations Map Var Invariant Bool ModelCheck.
|
|
Export String Arith Sets Relations Map Var Invariant Bool ModelCheck.
|
|
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 (unifyTails; pose proof I);
|
|
repeat match goal with
|
|
| [ H : True |- _ ] => clear H
|
|
end;
|
|
repeat progress (simpl in *; intros; try autorewrite with core in *);
|
|
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.
|
|
|
|
Ltac first_order := firstorder idtac.
|
|
|
|
|
|
(** * Model checking *)
|
|
|
|
Ltac model_check_done :=
|
|
apply MscDone; apply prove_oneStepClosure; simplify; propositional; subst;
|
|
repeat match goal with
|
|
| [ H : _ |- _ ] => invert H
|
|
end; simplify; equality.
|
|
|
|
Ltac singletoner :=
|
|
repeat match goal with
|
|
| _ => apply singleton_in
|
|
| [ |- (_ \cup _) _ ] => apply singleton_in_other
|
|
end.
|
|
|
|
Ltac model_check_step :=
|
|
eapply MscStep; [
|
|
repeat (apply oneStepClosure_empty
|
|
|| (apply oneStepClosure_split; [ simplify;
|
|
repeat match goal with
|
|
| [ H : _ |- _ ] => invert H; simplify; try congruence
|
|
end; solve [ singletoner ] | ]))
|
|
| simplify ].
|
|
|
|
Ltac model_check_steps1 := model_check_done || model_check_step.
|
|
Ltac model_check_steps := repeat model_check_steps1.
|
|
|
|
Ltac model_check_finish := simplify; propositional; subst; simplify; equality.
|
|
|
|
Ltac model_check_infer :=
|
|
apply multiStepClosure_ok; simplify; model_check_steps.
|
|
|
|
Ltac model_check_find_invariant :=
|
|
simplify; eapply invariant_weaken; [ model_check_infer | ]; cbv beta in *.
|
|
|
|
Ltac model_check := model_check_find_invariant; model_check_finish.
|