Move forall_ptree into common

2 files changed, 43 insertions, 42 deletions

diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index 389a74f..5540f34 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -28,6 +28,7 @@ Require Import Coq.micromega.Lia.
 
 Require Export compcert.lib.Coqlib.
 Require Import compcert.lib.Integers.
+Require Import compcert.lib.Maps.
 
 Require Import vericert.common.Show.
 
@@ -243,3 +244,45 @@ Definition debug_show {A B : Type} `{Show A} (a : A) (b : B) : B :=
 
 Definition debug_show_msg {A B : Type} `{Show A} (s : string) (a : A) (b : B) : B :=
   let unused := debug_print (s ++ show a) in b.
+
+Definition forall_ptree {A:Type} (f:positive->A->bool) (m:Maps.PTree.t A) : bool :=
+  Maps.PTree.fold (fun (res: bool) (i: positive) (x: A) => res && f i x) m true.
+
+Ltac boolInv :=
+  match goal with
+  | [ H: _ && _ = true |- _ ] =>
+      destruct (andb_prop _ _ H); clear H; boolInv
+  | [ H: proj_sumbool _ = true |- _ ] =>
+      generalize (proj_sumbool_true _ H); clear H;
+      let EQ := fresh in (intro EQ; try subst; boolInv)
+  | _ =>
+      idtac
+  end.
+
+Remark ptree_forall:
+  forall (A: Type) (f: positive -> A -> bool) (m: Maps.PTree.t A),
+  Maps.PTree.fold (fun (res: bool) (i: positive) (x: A) => res && f i x) m true = true ->
+  forall i x, Maps.PTree.get i m = Some x -> f i x = true.
+Proof.
+  intros.
+  set (f' := fun (res: bool) (i: positive) (x: A) => res && f i x).
+  set (P := fun (m: Maps.PTree.t A) (res: bool) =>
+              res = true -> Maps.PTree.get i m = Some x -> f i x = true).
+  assert (P m true).
+  rewrite <- H. fold f'. apply Maps.PTree_Properties.fold_rec.
+  unfold P; intros. rewrite <- H1 in H4. auto.
+  red; intros. now rewrite Maps.PTree.gempty in H2.
+  unfold P; intros. unfold f' in H4. boolInv.
+  rewrite Maps.PTree.gsspec in H5. destruct (peq i k).
+  subst. inv H5. auto.
+  apply H3; auto.
+  red in H1. auto.
+Qed.
+
+Lemma forall_ptree_true:
+  forall (A: Type) (f: positive -> A -> bool) (m: Maps.PTree.t A),
+    forall_ptree f m = true ->
+    forall i x, Maps.PTree.get i m = Some x -> f i x = true.
+Proof.
+  apply ptree_forall.
+Qed.
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index 8c77636..43d7783 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -692,48 +692,6 @@ Definition beq_pred_expr_once (pe1 pe2: pred_expr) : bool :=
     equiv_check p1 p2
   end.
 
-Definition forall_ptree {A:Type} (f:positive->A->bool) (m:Maps.PTree.t A) : bool :=
-  Maps.PTree.fold (fun (res: bool) (i: positive) (x: A) => res && f i x) m true.
-
-Ltac boolInv :=
-  match goal with
-  | [ H: _ && _ = true |- _ ] =>
-      destruct (andb_prop _ _ H); clear H; boolInv
-  | [ H: proj_sumbool _ = true |- _ ] =>
-      generalize (proj_sumbool_true _ H); clear H;
-      let EQ := fresh in (intro EQ; try subst; boolInv)
-  | _ =>
-      idtac
-  end.
-
-Remark ptree_forall:
-  forall (A: Type) (f: positive -> A -> bool) (m: Maps.PTree.t A),
-  Maps.PTree.fold (fun (res: bool) (i: positive) (x: A) => res && f i x) m true = true ->
-  forall i x, Maps.PTree.get i m = Some x -> f i x = true.
-Proof.
-  intros.
-  set (f' := fun (res: bool) (i: positive) (x: A) => res && f i x).
-  set (P := fun (m: Maps.PTree.t A) (res: bool) =>
-              res = true -> Maps.PTree.get i m = Some x -> f i x = true).
-  assert (P m true).
-  rewrite <- H. fold f'. apply Maps.PTree_Properties.fold_rec.
-  unfold P; intros. rewrite <- H1 in H4. auto.
-  red; intros. now rewrite Maps.PTree.gempty in H2.
-  unfold P; intros. unfold f' in H4. boolInv.
-  rewrite Maps.PTree.gsspec in H5. destruct (peq i k).
-  subst. inv H5. auto.
-  apply H3; auto.
-  red in H1. auto.
-Qed.
-
-Lemma forall_ptree_true:
-  forall (A: Type) (f: positive -> A -> bool) (m: Maps.PTree.t A),
-    forall_ptree f m = true ->
-    forall i x, Maps.PTree.get i m = Some x -> f i x = true.
-Proof.
-  apply ptree_forall.
-Qed.
-
 Definition tree_equiv_check_el (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool :=
   match np2 ! n with
   | Some p' => equiv_check p p'