mirror of
https://github.com/achlipala/frap.git
synced 2024-11-27 23:06:20 +00:00
Replace omega with lia
This commit is contained in:
Adam Chlipala
parent
d41373e0cb
commit
5a28d4fe6a
5 changed files with 40 additions and 41 deletions
1
.gitignore
vendored
1
.gitignore
vendored
|
|
@ -22,3 +22,4 @@ Deep.ml*
|
|||
Deeper.ml*
|
||||
DeeperWithFail.ml*
|
||||
*.dir-locals.el
|
||||
*.cache
|
||||
|
|
|
|||
|
|
@ -1538,7 +1538,7 @@ Proof.
|
|||
repeat erewrite interp_agree in * by eassumption; eauto 10.
|
||||
|
||||
assert (Hnu : noUnderscoreArith e = true) by assumption.
|
||||
eapply flatten_Assign with (tempCount := 0) (dst := x) in Hnu; eauto.
|
||||
eapply flatten_Assign with (tempCount := 0) (dst := x) in Hnu; try eassumption.
|
||||
first_order.
|
||||
do 3 eexists.
|
||||
split.
|
||||
|
|
@ -1659,8 +1659,8 @@ Proof.
|
|||
simplify; propositional; eauto.
|
||||
|
||||
invert H1; simplify; subst.
|
||||
assert (noUnderscore c2 = true) by eauto.
|
||||
eapply flatten_ok' in H5; eauto.
|
||||
assert (noUnderscore c2 = true) by eauto 4.
|
||||
eapply flatten_ok' in H5; eauto 4.
|
||||
first_order.
|
||||
cases vc2; simplify; subst.
|
||||
pose proof (plug_total x0 (flattenContext C)).
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
Require Import Eqdep String Arith Omega Program Sets Relations Map Var Invariant Bool ModelCheck.
|
||||
Require Import Eqdep String Arith Lia Program Sets Relations Map Var Invariant Bool ModelCheck.
|
||||
Export Ascii String Arith Sets Relations Map Var Invariant Bool ModelCheck.
|
||||
Require Import List.
|
||||
Export List ListNotations.
|
||||
|
|
@ -177,8 +177,8 @@ Ltac doSubtract :=
|
|||
Ltac simpl_maps :=
|
||||
repeat match goal with
|
||||
| [ |- context[add ?m ?k1 ?v $? ?k2] ] =>
|
||||
(rewrite (@lookup_add_ne _ _ m k1 k2 v) by (congruence || omega))
|
||||
|| (rewrite (@lookup_add_eq _ _ m k1 k2 v) by (congruence || omega))
|
||||
(rewrite (@lookup_add_ne _ _ m k1 k2 v) by (congruence || lia))
|
||||
|| (rewrite (@lookup_add_eq _ _ m k1 k2 v) by (congruence || lia))
|
||||
end.
|
||||
|
||||
Ltac simplify := repeat (unifyTails; pose proof I);
|
||||
|
|
@ -203,7 +203,7 @@ Ltac linear_arithmetic := intros;
|
|||
| [ _ : 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.
|
||||
end; lia.
|
||||
|
||||
Ltac equality := intuition congruence.
|
||||
|
||||
|
|
@ -333,8 +333,8 @@ Inductive ordering (n m : nat) :=
|
|||
| Gt (_ : n > m).
|
||||
|
||||
Local Hint Constructors ordering.
|
||||
Local Hint Extern 1 (_ < _) => omega.
|
||||
Local Hint Extern 1 (_ > _) => omega.
|
||||
Local Hint Extern 1 (_ < _) => lia.
|
||||
Local Hint Extern 1 (_ > _) => lia.
|
||||
|
||||
Theorem totally_ordered : forall n m, ordering n m.
|
||||
Proof.
|
||||
|
|
|
|||
15
HoareLogic.v
15
HoareLogic.v
|
|
@ -170,6 +170,7 @@ Qed.
|
|||
(* BEGIN syntax macros that won't be explained *)
|
||||
Coercion Const : nat >-> exp.
|
||||
Coercion Var : string >-> exp.
|
||||
Declare Scope cmd_scope.
|
||||
Notation "*[ e ]" := (Read e) : cmd_scope.
|
||||
Infix "+" := Plus : cmd_scope.
|
||||
Infix "-" := Minus : cmd_scope.
|
||||
|
|
@ -189,6 +190,7 @@ Notation "{{ I }} 'while' b 'loop' body 'done'" := (While_ I b body) (at level 7
|
|||
Notation "'assert' {{ I }}" := (Assert I) (at level 75).
|
||||
Delimit Scope cmd_scope with cmd.
|
||||
|
||||
Declare Scope reset_scope.
|
||||
Infix "+" := plus : reset_scope.
|
||||
Infix "-" := Init.Nat.sub : reset_scope.
|
||||
Infix "*" := mult : reset_scope.
|
||||
|
|
@ -351,8 +353,6 @@ Proof.
|
|||
apply HtAssign.
|
||||
simplify.
|
||||
t.
|
||||
ring [H0].
|
||||
(* This variant of [ring] suggests a hypothesis to use in the proof. *)
|
||||
simplify.
|
||||
t.
|
||||
Qed.
|
||||
|
|
@ -368,7 +368,6 @@ Theorem fact_ok_snazzy : forall n,
|
|||
{{_&v ~> v $! "acc" = fact n}}.
|
||||
Proof.
|
||||
ht.
|
||||
ring [H0].
|
||||
Qed.
|
||||
|
||||
(** ** Selection sort *)
|
||||
|
|
@ -384,10 +383,10 @@ Proof.
|
|||
ht.
|
||||
Qed.
|
||||
|
||||
Hint Resolve leq_f.
|
||||
Hint Extern 1 (@eq nat _ _) => linear_arithmetic.
|
||||
Hint Extern 1 (_ < _) => linear_arithmetic.
|
||||
Hint Extern 1 (_ <= _) => linear_arithmetic.
|
||||
Hint Resolve leq_f : core.
|
||||
Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
|
||||
Hint Extern 1 (_ < _) => linear_arithmetic : core.
|
||||
Hint Extern 1 (_ <= _) => linear_arithmetic : core.
|
||||
(* We also register [linear_arithmetic] as a step to try during proof search. *)
|
||||
|
||||
(* These invariants are fairly hairy, but probably the best way to understand
|
||||
|
|
@ -471,7 +470,7 @@ Inductive step : heap * valuation * cmd -> heap * valuation * cmd -> Prop :=
|
|||
a h v
|
||||
-> step (h, v, Assert a) (h, v, Skip).
|
||||
|
||||
Hint Constructors step.
|
||||
Hint Constructors step : core.
|
||||
|
||||
Definition trsys_of (st : heap * valuation * cmd) := {|
|
||||
Initial := {st};
|
||||
|
|
|
|||
|
|
@ -205,7 +205,7 @@ Module References.
|
|||
|
||||
-> heapty ht h.
|
||||
|
||||
Hint Constructors value plug step0 step hasty heapty.
|
||||
Hint Constructors value plug step0 step hasty heapty : core.
|
||||
|
||||
|
||||
(* Perhaps surprisingly, this language admits well-typed, nonterminating
|
||||
|
|
@ -222,7 +222,7 @@ Module References.
|
|||
repeat (econstructor; simplify).
|
||||
Qed.
|
||||
|
||||
Hint Resolve lookup_add_eq.
|
||||
Hint Resolve lookup_add_eq : core.
|
||||
|
||||
Ltac loopy := propositional; subst; simplify;
|
||||
repeat match goal with
|
||||
|
|
@ -293,7 +293,7 @@ Module References.
|
|||
|
||||
Ltac t := simplify; propositional; repeat (t0; simplify); try equality; eauto 7.
|
||||
|
||||
Hint Extern 2 (exists _ : _ * _, _) => eexists (_ $+ (_, _), _).
|
||||
Hint Extern 2 (exists _ : _ * _, _) => eexists (_ $+ (_, _), _) : core.
|
||||
|
||||
(* Progress is quite straightforward. *)
|
||||
Lemma progress : forall ht h, heapty ht h
|
||||
|
|
@ -323,7 +323,7 @@ Module References.
|
|||
cases (x ==v x'); simplify; eauto.
|
||||
Qed.
|
||||
|
||||
Hint Resolve weakening_override.
|
||||
Hint Resolve weakening_override : core.
|
||||
|
||||
Lemma weakening : forall H G e t,
|
||||
hasty H G e t
|
||||
|
|
@ -333,7 +333,7 @@ Module References.
|
|||
induct 1; t.
|
||||
Qed.
|
||||
|
||||
Hint Resolve weakening.
|
||||
Hint Resolve weakening : core.
|
||||
|
||||
Lemma hasty_change : forall H G e t,
|
||||
hasty H G e t
|
||||
|
|
@ -343,7 +343,7 @@ Module References.
|
|||
t.
|
||||
Qed.
|
||||
|
||||
Hint Resolve hasty_change.
|
||||
Hint Resolve hasty_change : core.
|
||||
|
||||
Lemma substitution : forall H G x t' e t e',
|
||||
hasty H (G $+ (x, t')) e t
|
||||
|
|
@ -353,7 +353,7 @@ Module References.
|
|||
induct 1; t.
|
||||
Qed.
|
||||
|
||||
Hint Resolve substitution.
|
||||
Hint Resolve substitution : core.
|
||||
|
||||
(* A new property: expanding the heap typing preserves typing. *)
|
||||
Lemma heap_weakening : forall H G e t,
|
||||
|
|
@ -364,7 +364,7 @@ Module References.
|
|||
induct 1; t.
|
||||
Qed.
|
||||
|
||||
Hint Resolve heap_weakening.
|
||||
Hint Resolve heap_weakening : core.
|
||||
|
||||
(* A property about extending heap typings *)
|
||||
Lemma heap_override : forall H h k t t0 l,
|
||||
|
|
@ -378,7 +378,7 @@ Module References.
|
|||
apply H2 in H0; t.
|
||||
Qed.
|
||||
|
||||
Hint Resolve heap_override.
|
||||
Hint Resolve heap_override : core.
|
||||
|
||||
(* A higher-level property, stated via [heapty] *)
|
||||
Lemma heapty_extend : forall H h l t v,
|
||||
|
|
@ -394,12 +394,11 @@ Module References.
|
|||
invert H0; eauto 6.
|
||||
apply H3 in H0; t.
|
||||
|
||||
rewrite lookup_add_ne by linear_arithmetic.
|
||||
apply H4.
|
||||
linear_arithmetic.
|
||||
Qed.
|
||||
|
||||
Hint Resolve heapty_extend.
|
||||
Hint Resolve heapty_extend : core.
|
||||
|
||||
(* The old cases of preservation proceed as before, and we need to fiddle with
|
||||
* the heap in the new cases. Note a crucial change to the theorem statement:
|
||||
|
|
@ -445,7 +444,7 @@ Module References.
|
|||
assumption.
|
||||
Qed.
|
||||
|
||||
Hint Resolve preservation0.
|
||||
Hint Resolve preservation0 : core.
|
||||
|
||||
(* This lemma gets more complicated, too, to accommodate heap typings. *)
|
||||
Lemma generalize_plug : forall H e1 C e1',
|
||||
|
|
@ -482,7 +481,7 @@ Module References.
|
|||
eauto.
|
||||
Qed.
|
||||
|
||||
Hint Resolve progress preservation.
|
||||
Hint Resolve progress preservation : core.
|
||||
|
||||
(* We'll need this fact for the base case of invariant induction. *)
|
||||
Lemma heapty_empty : heapty $0 $0.
|
||||
|
|
@ -490,7 +489,7 @@ Module References.
|
|||
exists 0; t.
|
||||
Qed.
|
||||
|
||||
Hint Resolve heapty_empty.
|
||||
Hint Resolve heapty_empty : core.
|
||||
|
||||
(* Now there isn't much more to the proof of type safety. The crucial overall
|
||||
* insight is a strengthened invariant that quantifies existentially over a
|
||||
|
|
@ -504,7 +503,7 @@ Module References.
|
|||
apply invariant_weaken with (invariant1 := fun he' => exists H,
|
||||
hasty H $0 (snd he') t
|
||||
/\ heapty H (fst he')); eauto.
|
||||
apply invariant_induction; simplify; eauto.
|
||||
apply invariant_induction; simplify.
|
||||
propositional.
|
||||
subst; simplify.
|
||||
eauto.
|
||||
|
|
@ -593,7 +592,7 @@ Module GarbageCollection.
|
|||
|
||||
-> step (h, e) (h', e).
|
||||
|
||||
Hint Constructors step.
|
||||
Hint Constructors step : core.
|
||||
|
||||
Definition trsys_of (e : exp) := {|
|
||||
Initial := {($0, e)};
|
||||
|
|
@ -632,10 +631,10 @@ Module GarbageCollection.
|
|||
assumption.
|
||||
Qed.
|
||||
|
||||
Hint Resolve reachableLocFromExp_trans.
|
||||
Hint Extern 1 (_ \in _) => simplify; solve [ sets ].
|
||||
Hint Extern 1 (_ \subseteq _) => simplify; solve [ sets ].
|
||||
Hint Constructors reachableLoc reachableLocFromExp.
|
||||
Hint Resolve reachableLocFromExp_trans : core.
|
||||
Hint Extern 1 (_ \in _) => simplify; solve [ sets ] : core.
|
||||
Hint Extern 1 (_ \subseteq _) => simplify; solve [ sets ] : core.
|
||||
Hint Constructors reachableLoc reachableLocFromExp : core.
|
||||
|
||||
(* Typing is preserved by moving to a heap typing that only needs to preserve
|
||||
* the mappings for *reachable* locations. *)
|
||||
|
|
@ -685,9 +684,9 @@ Module GarbageCollection.
|
|||
|
||||
(* The case for the original [step] rule proceeds exactly the same way as
|
||||
* before. *)
|
||||
eapply generalize_plug in H; eauto.
|
||||
eapply generalize_plug in H; eauto 3.
|
||||
invert H; propositional.
|
||||
eapply preservation0 in H6; eauto.
|
||||
eapply preservation0 in H6; eauto 3.
|
||||
invert H6; propositional.
|
||||
eauto.
|
||||
|
||||
|
|
@ -731,7 +730,7 @@ Module GarbageCollection.
|
|||
equality.
|
||||
Qed.
|
||||
|
||||
Hint Resolve progress preservation.
|
||||
Hint Resolve progress preservation : core.
|
||||
|
||||
(* The safety proof itself is anticlimactic, looking the same as before. *)
|
||||
Theorem safety : forall e t, hasty $0 $0 e t
|
||||
|
|
@ -743,7 +742,7 @@ Module GarbageCollection.
|
|||
apply invariant_weaken with (invariant1 := fun he' => exists H,
|
||||
hasty H $0 (snd he') t
|
||||
/\ heapty H (fst he')); eauto.
|
||||
apply invariant_induction; simplify; eauto.
|
||||
apply invariant_induction; simplify.
|
||||
propositional.
|
||||
subst; simplify.
|
||||
eauto.
|
||||
|
|
|
|||
Loading…
Reference in a new issue