diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-06-06 15:44:43 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-06-06 15:44:43 +0100 |
| commit | 703b43cb326feb971966edaa0b19c1548920f7ac (patch) | |
| tree | d8b3d8f96503aa479fb177f3334aa9e2b43574f3 /src/hls/Predicate.v | |
| parent | baa7185e411df24c307691bd77fb91e908a257c6 (diff) | |
| download | vericert-703b43cb326feb971966edaa0b19c1548920f7ac.tar.gz vericert-703b43cb326feb971966edaa0b19c1548920f7ac.zip | |
Rearrange definitions and create IfConversion template
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. |