From 0fcba3672e7b64de86173b259a87f3deb33b35f6 Mon Sep 17 00:00:00 2001
From: Joachim Bard <jbard@mpi-sws.org>
Date: Fri, 15 Mar 2019 15:31:02 +0100
Subject: [PATCH] sort preconds before checking

---
 coq/SubdivsChecker.v | 41 +++++++++++++++++++++++++++++++++++------
 1 file changed, 35 insertions(+), 6 deletions(-)

diff --git a/coq/SubdivsChecker.v b/coq/SubdivsChecker.v
index 31425a0..68fa9b6 100644
--- a/coq/SubdivsChecker.v
+++ b/coq/SubdivsChecker.v
@@ -4,8 +4,7 @@ From Flover
      Environments TypeValidator FPRangeValidator ExpressionAbbrevs ResultChecker
      IntervalArithQ.
 
-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.
 Qed.
 
+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
+      end
+    end.
+
+  Theorem leb_total P1 P2 : leb P1 P2 = true \/ leb P2 P1 = true.
+  Proof.
+    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.
+  Qed.
+
+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.
 Qed.
-  
-(* 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).
   lra.
-Qed.
\ No newline at end of file
+Qed.
-- 
GitLab