diff options
Diffstat (limited to 'kvx/SelectOpproof.v')
-rw-r--r-- | kvx/SelectOpproof.v | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v index e6cce0fa..cffa2583 100644 --- a/kvx/SelectOpproof.v +++ b/kvx/SelectOpproof.v @@ -1951,6 +1951,50 @@ Proof. } inv EVAL. constructor. + - cbn in *. + intro EVAL. + inv EVAL. discriminate. + inv H0. discriminate. + inv H2. 2: discriminate. + inv Heval. + intro EVAL. + destruct v1; try discriminate. + destruct v0; try discriminate. + unfold Int.eq in EVAL. + change (Int.unsigned Int.zero) with 0 in EVAL. + unfold zeq in EVAL. + destruct (Z.eq_dec (Int.unsigned i0) 0) as [EQ | NEQ]. + { discriminate. } + exists (Vint (Int.modu i i0)). split. + { + apply FPDivision32.fp_modu32_correct; auto. + pose proof (Int.unsigned_range i0). + lia. + } + inv EVAL. + constructor. + - cbn in *. + intro EVAL. + inv EVAL. discriminate. + inv H0. discriminate. + inv H2. 2: discriminate. + inv Heval. + intro EVAL. + destruct v1; try discriminate. + destruct v0; try discriminate. + unfold Int64.eq in EVAL. + change (Int64.unsigned Int64.zero) with 0 in EVAL. + unfold zeq in EVAL. + destruct (Z.eq_dec (Int64.unsigned i0) 0) as [EQ | NEQ]. + { discriminate. } + exists (Vlong (Int64.modu i i0)). split. + { + apply FPDivision64.fp_modu64_correct; auto. + pose proof (Int64.unsigned_range i0). + lia. + } + inv EVAL. + constructor. Qed. End CMCONSTR. |