diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-11-15 19:35:01 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-11-15 19:35:01 +0000 |
| commit | a8c196130327073d04efb04c1c23f3bc7ae5951b (patch) | |
| tree | 4fed9befd1ccbd5bb55fc6a5edd1bf2a95c40542 /src/hls/Abstr.v | |
| parent | 49828abd7c0b9bf2d7a859cce40a6ba59466f324 (diff) | |
| download | vericert-a8c196130327073d04efb04c1c23f3bc7ae5951b.tar.gz vericert-a8c196130327073d04efb04c1c23f3bc7ae5951b.zip | |
Prove top level theorems with evaluability
Diffstat (limited to 'src/hls/Abstr.v')
| -rw-r--r-- | src/hls/Abstr.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index 5ce7c0a..f67627d 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -1500,3 +1500,14 @@ Proof. unfold forest_preds, set_forest_p, get_forest_p'. rewrite PTree.gss; auto. Qed. + +Lemma forest_pred_gss2 : + forall (f : forest) r p, + (forest_preds (f #p r <- p)) ! r = Some p. +Proof. intros. unfold set_forest_p. simpl. now rewrite PTree.gss. Qed. + +Lemma forest_pred_gso2 : + forall (f : forest) r w p, + r <> w -> + (forest_preds (f #p w <- p)) ! r = (forest_preds f) ! r. +Proof. intros. unfold set_forest_p. simpl. now rewrite PTree.gso by auto. Qed. |