diff options
Diffstat (limited to 'src/hls/Predicate.v')
| -rw-r--r-- | src/hls/Predicate.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index 7a4ed60..b9333d9 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -697,3 +697,15 @@ Definition combine_pred (p1 p2: option pred_op): option pred_op := | Some p, _ | _, Some p => Some p | None, None => None end. + +Lemma predicate_lt : + forall p p0, + In p0 (predicate_use p) -> p0 <= max_predicate p. +Proof. + induction p; crush. + - destruct_match. inv H; try lia; contradiction. + - eapply Pos.max_le_iff. + eapply in_app_or in H. inv H; eauto. + - eapply Pos.max_le_iff. + eapply in_app_or in H. inv H; eauto. +Qed. |