Commit 0fcba367 authored by Joachim Bard's avatar Joachim Bard

sort preconds before checking

parent 565e31c3
......@@ -4,8 +4,7 @@ From Flover
Environments TypeValidator FPRangeValidator ExpressionAbbrevs ResultChecker
Require Import List.
Require Import FunInd.
Require Import List FunInd Sorting.Permutation Sorting.Mergesort Orders.
Fixpoint resultLeq e (A1 A2: analysisResult) :=
match e with
......@@ -341,11 +340,39 @@ Proof.
eapply IHP; eauto.
Module PrecondOrder <: TotalLeBool.
Definition t := list (expr Q * intv).
Fixpoint leb (P1 P2: list (expr Q * intv)) :=
match P1, P2 with
| nil, _ => true
| _, nil => false
| (_, iv1) :: P1, (_, iv2) :: P2 =>
match (fst iv1) ?= (fst iv2) with
| Lt => true
| Eq => leb P1 P2
| Gt => false
Theorem leb_total P1 P2 : leb P1 P2 = true \/ leb P2 P1 = true.
induction P1 in P2 |- *; destruct P2 as [|[e2 iv2] P2]; auto.
destruct a as [e1 iv1]; cbn.
rewrite <- (Qcompare_antisym (fst iv1)).
destruct (fst iv1 ?= fst iv2); cbn; auto.
End PrecondOrder.
Module Import PrecondSort := Sort PrecondOrder.
Definition checkPreconds (subdivs: list precond) (P: precond) :=
let Piv := FloverMap.elements (fst P) in
let Ps := map (fun P => FloverMap.elements (fst P)) subdivs in
let S_qs := map snd subdivs in
covers Piv Ps && forallb (fun q => SMTLogic_eqb q (snd P)) S_qs.
covers Piv (sort Ps) && forallb (fun q => SMTLogic_eqb q (snd P)) S_qs.
Lemma checkPreconds_sound (subdivs: list precond) E P :
checkPreconds subdivs P = true ->
......@@ -356,6 +383,8 @@ Proof.
apply andb_true_iff in H as [cov Hqs].
eapply covers_sound in cov; eauto.
destruct cov as [Pl1 [Hin H]].
eapply Permutation_in in Hin.
2: eapply Permutation_sym, Permuted_sort.
apply in_map_iff in Hin as [P1 [Heq1 Hin]].
exists P1. split; auto.
rewrite <- Heq1 in H.
......@@ -376,10 +405,10 @@ Proof.
erewrite SMTLogic_eqb_varsLogic; eauto.
apply NatSetProps.union_equal_1.
eapply covers_preVars; eauto.
eapply Permutation_in; eauto using Permuted_sort.
apply in_map_iff; eauto.
(* TODO: merge hd and tl again *)
(** Interval subdivisions checking function **)
Definition SubdivsChecker (e: expr Q) (absenv: analysisResult)
(P: precond) subdivs (defVars: FloverMap.t mType) Gamma :=
......@@ -443,4 +472,4 @@ Proof.
intros vF0 m Heval.
specialize (err_bounded vF0 m Heval).
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment