Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.11

1 files changed, 34 insertions, 0 deletions

diff --git a/src/Misc.v b/src/Misc.v
index 952985f..8553172 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,