diff options
Diffstat (limited to 'riscV/SelectLongproof.v')
| -rw-r--r-- | riscV/SelectLongproof.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/riscV/SelectLongproof.v b/riscV/SelectLongproof.v index f5e8edf8..0fc578bf 100644 --- a/riscV/SelectLongproof.v +++ b/riscV/SelectLongproof.v @@ -558,6 +558,7 @@ Proof. unfold longoffloat; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_longoffloat; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_longuoffloat: partial_unary_constructor_sound longuoffloat Val.longuoffloat. @@ -565,6 +566,7 @@ Proof. unfold longuoffloat; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_longuoffloat; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_floatoflong: partial_unary_constructor_sound floatoflong Val.floatoflong. @@ -572,6 +574,7 @@ Proof. unfold floatoflong; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_floatoflong; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_floatoflongu: partial_unary_constructor_sound floatoflongu Val.floatoflongu. @@ -579,6 +582,7 @@ Proof. unfold floatoflongu; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_floatoflongu; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle. @@ -586,6 +590,7 @@ Proof. unfold longofsingle; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_longofsingle; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_longuofsingle: partial_unary_constructor_sound longuofsingle Val.longuofsingle. @@ -593,6 +598,7 @@ Proof. unfold longuofsingle; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_longuofsingle; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong. @@ -600,6 +606,7 @@ Proof. unfold singleoflong; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_singleoflong; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. Theorem eval_singleoflongu: partial_unary_constructor_sound singleoflongu Val.singleoflongu. @@ -607,6 +614,7 @@ Proof. unfold singleoflongu; red; intros. destruct Archi.splitlong eqn:SL. eapply SplitLongproof.eval_singleoflongu; eauto. TrivialExists. + cbn; rewrite H0; reflexivity. Qed. End CMCONSTR. |