diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-03-22 16:42:55 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-22 16:42:55 +0000 |
commit | 2926dabad750aa862c7108f53a195c7973f5d619 (patch) | |
tree | fc248494060381fbe8d283887617313f11031346 /src/hls/Abstr.v | |
parent | 5bb3e077854e33a7bd51d38f97970b08da171130 (diff) | |
download | vericert-2926dabad750aa862c7108f53a195c7973f5d619.tar.gz vericert-2926dabad750aa862c7108f53a195c7973f5d619.zip |
Move forall_ptree into common
Diffstat (limited to 'src/hls/Abstr.v')
-rw-r--r-- | src/hls/Abstr.v | 42 |
1 files changed, 0 insertions, 42 deletions
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' |