From 68a6d0dd0ea5774529d823fb9a9ca981c1ecebb0 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 4 Jun 2019 22:58:34 +0200 Subject: osel imm --- mppa_k1c/SelectOpproof.v | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) (limited to 'mppa_k1c/SelectOpproof.v') diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 4047048c..39ad763e 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -1451,12 +1451,10 @@ Lemma eval_select0: /\ Val.lessdef (Val.select (eval_condition0 cond0 vc m) v1 v2 ty) v. Proof. intros. - econstructor; split. - { - unfold select0. - repeat (try econstructor; try eassumption). - } - constructor. + unfold select0. + destruct (select0_match ty cond0 a1 a2 ac). + all: InvEval; econstructor; split; + repeat (try econstructor; try eassumption). Qed. Lemma bool_cond0_ne: @@ -1578,12 +1576,11 @@ Proof. erewrite <- (bool_cond0_ne (Val.cmplu_bool (Mem.valid_pointer m) c v0 (Vlong x))). eapply eval_select0; repeat (try econstructor; try eassumption). } - TrivialExists. - repeat (try econstructor; try eassumption). + erewrite <- (bool_cond0_ne (Some b)). + eapply eval_select0; repeat (try econstructor; try eassumption). + rewrite <- HeC. simpl. - f_equal. - rewrite HeC. - destruct b; simpl; reflexivity. + reflexivity. Qed. (* floating-point division *) -- cgit