From 3523794498e9ac8b86eeec8e1a2147e9abe997b6 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@inria.fr>
Date: Tue, 30 Jun 2020 13:33:39 +0200
Subject: Remove two axioms

---
 src/Misc.v                | 34 ++++++++++++++++++++++++++++++++++
 src/array/Array_checker.v |  4 ----
 src/bva/Bva_checker.v     |  7 -------
 src/cnf/Cnf.v             |  8 --------
 4 files changed, 34 insertions(+), 19 deletions(-)

(limited to 'src')

diff --git a/src/Misc.v b/src/Misc.v
index b675599..24e27c0 100644
--- a/src/Misc.v
+++ b/src/Misc.v
@@ -495,6 +495,23 @@ Proof.
 Qed.
 
 
+Lemma afold_left_and p a :
+  afold_left bool int true andb p a =
+  List.forallb p (to_list a).
+Proof.
+  rewrite afold_left_spec; auto.
+  rewrite fold_left_to_list.
+  assert (H:forall l acc, List.fold_left (fun (a0 : bool) (v : int) => a0 && p v) l acc =
+  acc && List.forallb p l).
+  {
+    clear a. induction l; simpl.
+    - intros; now rewrite andb_true_r.
+    - intro acc. rewrite IHl. now rewrite andb_assoc.
+  }
+  now apply H.
+Qed.
+
+
 (* Case orb *)
 
 Lemma afold_left_orb_true : forall A i a f,
@@ -541,6 +558,23 @@ Proof.
 Qed.
 
 
+Lemma afold_left_or p a :
+  afold_left bool int false orb p a =
+  List.existsb p (to_list a).
+Proof.
+  rewrite afold_left_spec; auto.
+  rewrite fold_left_to_list.
+  assert (H:forall l acc, List.fold_left (fun (a0 : bool) (v : int) => a0 || p v) l acc =
+  acc || List.existsb p l).
+  {
+    clear a. induction l; simpl.
+    - intros; now rewrite orb_false_r.
+    - intro acc. rewrite IHl. now rewrite orb_assoc.
+  }
+  now apply H.
+Qed.
+
+
 (* Case implb *)
 
 Lemma afold_right_implb_false : forall A a f,
diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v
index 3a982b2..0540855 100644
--- a/src/array/Array_checker.v
+++ b/src/array/Array_checker.v
@@ -893,10 +893,6 @@ Section certif.
             apply read_over_other_write; now auto.
     Qed.
 
-  Axiom afold_left_or : forall a,
-    afold_left bool int false orb (Lit.interp rho) a =
-    C.interp rho (to_list a).
-
   Lemma valid_check_ext lres : C.valid rho (check_ext lres).
     unfold check_ext, eq_sel_sym.
     case_eq (Lit.is_pos lres); intro Heq; simpl; try now apply C.interp_true.
diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v
index 84df9bd..180fbcf 100644
--- a/src/bva/Bva_checker.v
+++ b/src/bva/Bva_checker.v
@@ -1926,13 +1926,6 @@ Qed.
 Lemma eq_head: forall {A: Type} a b (l: list A), (a :: l) = (b :: l) <-> a = b.
 Proof. intros A a b l; split; [intros H; inversion H|intros ->]; auto. Qed.
 
-Axiom afold_left_and : forall a, 
-      afold_left bool int true andb (Lit.interp rho) a = List.forallb (Lit.interp rho) (to_list a).
-
-  Axiom afold_left_or : forall a,
-    afold_left bool int false orb (Lit.interp rho) a =
-    C.interp rho (to_list a).
-
   Axiom afold_left_xor : forall a,
     afold_left bool int false xorb (Lit.interp rho) a =
     C.interp rho (to_list a).
diff --git a/src/cnf/Cnf.v b/src/cnf/Cnf.v
index ec18c15..d6a6640 100644
--- a/src/cnf/Cnf.v
+++ b/src/cnf/Cnf.v
@@ -287,14 +287,6 @@ Section CHECKER.
      match goal with |- context [Lit.interp rho ?x] => 
      destruct (Lit.interp rho x);trivial end.
 
-  Axiom afold_left_and : forall a,
-    afold_left bool int true andb (Lit.interp rho) a =
-    List.forallb (Lit.interp rho) (to_list a).
-
-  Axiom afold_left_or : forall a,
-    afold_left bool int false orb (Lit.interp rho) a =
-    C.interp rho (to_list a).
-
   Axiom afold_right_impb : forall a,
     (afold_right bool int true implb (Lit.interp rho) a) =
     C.interp rho (to_list (or_of_imp a)).
-- 
cgit