diff options
| -rw-r--r-- | kvx/Asm.v | 40 | ||||
| -rw-r--r-- | kvx/Asmblock.v | 52 | ||||
| -rw-r--r-- | kvx/Asmblockprops.v | 6 | ||||
| -rw-r--r-- | kvx/Asmgenproof.v | 4 | ||||
| -rw-r--r-- | kvx/Asmvliw.v | 16 | ||||
| -rw-r--r-- | kvx/CSE2depsproof.v | 6 | ||||
| -rw-r--r-- | kvx/CombineOpproof.v | 56 | ||||
| -rw-r--r-- | kvx/ConstpropOpproof.v | 196 | ||||
| -rw-r--r-- | kvx/Conventions1.v | 34 | ||||
| -rw-r--r-- | kvx/ExtValues.v | 72 | ||||
| -rw-r--r-- | kvx/NeedOp.v | 54 | ||||
| -rw-r--r-- | kvx/Op.v | 484 | ||||
| -rw-r--r-- | kvx/Peephole.v | 2 | ||||
| -rw-r--r-- | kvx/Stacklayout.v | 6 | ||||
| -rw-r--r-- | kvx/ValueAOp.v | 76 | ||||
| -rw-r--r-- | kvx/abstractbb/AbstractBasicBlocksDef.v | 50 | ||||
| -rw-r--r-- | kvx/abstractbb/ImpSimuTest.v | 52 | ||||
| -rw-r--r-- | kvx/abstractbb/Parallelizability.v | 124 | ||||
| -rw-r--r-- | kvx/abstractbb/SeqSimuTheory.v | 56 | ||||
| -rw-r--r-- | kvx/lib/ForwardSimulationBlock.v | 30 | ||||
| -rw-r--r-- | kvx/lib/Machblock.v | 14 | ||||
| -rw-r--r-- | kvx/lib/Machblockgen.v | 14 | ||||
| -rw-r--r-- | kvx/lib/Machblockgenproof.v | 138 |
23 files changed, 789 insertions, 793 deletions
@@ -611,15 +611,15 @@ Program Definition genv_trans (ge: genv) : Asmvliw.genv := Genv.genv_defs := PTree.map1 globdef_proj (Genv.genv_defs ge); Genv.genv_next := Genv.genv_next ge |}. Next Obligation. - destruct ge. simpl in *. eauto. + destruct ge. cbn in *. eauto. Qed. Next Obligation. - destruct ge; simpl in *. + destruct ge; cbn in *. rewrite PTree.gmap1 in H. destruct (genv_defs ! b) eqn:GEN. - eauto. - discriminate. Qed. Next Obligation. - destruct ge; simpl in *. + destruct ge; cbn in *. eauto. Qed. @@ -655,14 +655,14 @@ Program Definition transf_function (f: Asmvliw.function) : function := Lemma transf_function_proj: forall f, function_proj (transf_function f) = f. Proof. - intros f. destruct f as [sig blks]. unfold function_proj. simpl. auto. + intros f. destruct f as [sig blks]. unfold function_proj. cbn. auto. Qed. Definition transf_fundef : Asmvliw.fundef -> fundef := AST.transf_fundef transf_function. Lemma transf_fundef_proj: forall f, fundef_proj (transf_fundef f) = f. Proof. - intros f. destruct f as [f|e]; simpl; auto. + intros f. destruct f as [f|e]; cbn; auto. rewrite transf_function_proj. auto. Qed. @@ -674,18 +674,18 @@ Lemma program_equals {A B: Type} : forall (p1 p2: AST.program A B), prog_main p1 = prog_main p2 -> p1 = p2. Proof. - intros. destruct p1. destruct p2. simpl in *. subst. auto. + intros. destruct p1. destruct p2. cbn in *. subst. auto. Qed. Lemma transf_program_proj: forall p, program_proj (transf_program p) = p. Proof. - intros p. destruct p as [defs pub main]. unfold program_proj. simpl. - apply program_equals; simpl; auto. + intros p. destruct p as [defs pub main]. unfold program_proj. cbn. + apply program_equals; cbn; auto. induction defs. - - simpl; auto. - - simpl. rewrite IHdefs. - destruct a as [id gd]; simpl. - destruct gd as [f|v]; simpl; auto. + - cbn; auto. + - cbn. rewrite IHdefs. + destruct a as [id gd]; cbn. + destruct gd as [f|v]; cbn; auto. rewrite transf_fundef_proj. auto. Qed. @@ -707,16 +707,16 @@ Lemma match_program_transf: forall p tp, match_prog p tp -> transf_program p = tp. Proof. intros p tp H. inversion_clear H. inv H1. - destruct p as [defs pub main]. destruct tp as [tdefs tpub tmain]. simpl in *. - subst. unfold transf_program. unfold transform_program. simpl. - apply program_equals; simpl; auto. - induction H0; simpl; auto. + destruct p as [defs pub main]. destruct tp as [tdefs tpub tmain]. cbn in *. + subst. unfold transf_program. unfold transform_program. cbn. + apply program_equals; cbn; auto. + induction H0; cbn; auto. rewrite IHlist_forall2. apply cons_extract. destruct a1 as [ida gda]. destruct b1 as [idb gdb]. - simpl in *. + cbn in *. inv H. inv H2. - - simpl in *. subst. auto. - - simpl in *. subst. inv H. auto. + - cbn in *. subst. auto. + - cbn in *. subst. inv H. auto. Qed. Section PRESERVATION. @@ -744,7 +744,7 @@ Proof. pose proof (match_program_transf prog tprog TRANSF) as TR. subst. unfold semantics. rewrite transf_program_proj. - eapply forward_simulation_step with (match_states := match_states); simpl; auto. + eapply forward_simulation_step with (match_states := match_states); cbn; auto. - intros. exists s1. split; auto. congruence. - intros. inv H. auto. - intros. exists s1'. inv H0. split; auto. congruence. diff --git a/kvx/Asmblock.v b/kvx/Asmblock.v index 9c8e4cc3..64b2c535 100644 --- a/kvx/Asmblock.v +++ b/kvx/Asmblock.v @@ -78,7 +78,7 @@ Fixpoint code_to_basics (c: code) := Lemma code_to_basics_id: forall c, code_to_basics (basics_to_code c) = Some c. Proof. - intros. induction c as [|i c]; simpl; auto. + intros. induction c as [|i c]; cbn; auto. rewrite IHc. auto. Qed. @@ -88,8 +88,8 @@ Lemma code_to_basics_dist: code_to_basics c' = Some l' -> code_to_basics (c ++ c') = Some (l ++ l'). Proof. - induction c as [|i c]; simpl; auto. - - intros. inv H. simpl. auto. + induction c as [|i c]; cbn; auto. + - intros. inv H. cbn. auto. - intros. destruct i; try discriminate. destruct (code_to_basics c) eqn:CTB; try discriminate. inv H. erewrite IHc; eauto. auto. Qed. @@ -138,9 +138,9 @@ Lemma non_empty_bblock_refl: Proof. intros. split. - destruct body; destruct exit. - all: simpl; auto. intros. inversion H; contradiction. + all: cbn; auto. intros. inversion H; contradiction. - destruct body; destruct exit. - all: simpl; auto. + all: cbn; auto. all: intros; try (right; discriminate); try (left; discriminate). contradiction. Qed. @@ -155,14 +155,14 @@ Lemma builtin_alone_refl: Proof. intros. split. - destruct body; destruct exit. - all: simpl; auto. - all: exploreInst; simpl; auto. + all: cbn; auto. + all: exploreInst; cbn; auto. unfold builtin_alone. intros. assert (Some (Pbuiltin e l b0) = Some (Pbuiltin e l b0)); auto. assert (b :: body = nil). eapply H; eauto. discriminate. - destruct body; destruct exit. - all: simpl; auto; try constructor. + all: cbn; auto; try constructor. + exploreInst; try discriminate. - simpl. contradiction. + cbn. contradiction. + intros. discriminate. Qed. @@ -185,14 +185,14 @@ Ltac bblock_auto_correct := (apply non_empty_bblock_refl; try discriminate; try Lemma Istrue_proof_irrelevant (b: bool): forall (p1 p2:Is_true b), p1=p2. Proof. - destruct b; simpl; auto. + destruct b; cbn; auto. - destruct p1, p2; auto. - destruct p1. Qed. Lemma bblock_equality bb1 bb2: header bb1=header bb2 -> body bb1 = body bb2 -> exit bb1 = exit bb2 -> bb1 = bb2. Proof. - destruct bb1 as [h1 b1 e1 c1], bb2 as [h2 b2 e2 c2]; simpl. + destruct bb1 as [h1 b1 e1 c1], bb2 as [h2 b2 e2 c2]; cbn. intros; subst. rewrite (Istrue_proof_irrelevant _ c1 c2). auto. @@ -212,51 +212,51 @@ Qed. Lemma length_nonil {A: Type} : forall l:(list A), l <> nil -> (length l > 0)%nat. Proof. intros. destruct l; try (contradict H; auto; fail). - simpl. omega. + cbn. omega. Qed. Lemma to_nat_pos : forall z:Z, (Z.to_nat z > 0)%nat -> z > 0. Proof. intros. destruct z; auto. - - contradict H. simpl. apply gt_irrefl. + - contradict H. cbn. apply gt_irrefl. - apply Zgt_pos_0. - - contradict H. simpl. apply gt_irrefl. + - contradict H. cbn. apply gt_irrefl. Qed. Lemma size_positive (b:bblock): size b > 0. Proof. - unfold size. destruct b as [hd bdy ex cor]. simpl. - destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; simpl; omega). - inversion cor; contradict H; simpl; auto. + unfold size. destruct b as [hd bdy ex cor]. cbn. + destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; omega). + inversion cor; contradict H; cbn; auto. Qed. Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}. Next Obligation. - destruct bb; simpl. assumption. + destruct bb; cbn. assumption. Defined. Lemma no_header_size: forall bb, size (no_header bb) = size bb. Proof. - intros. destruct bb as [hd bdy ex COR]. unfold no_header. simpl. reflexivity. + intros. destruct bb as [hd bdy ex COR]. unfold no_header. cbn. reflexivity. Qed. Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}. Next Obligation. - destruct bb; simpl. assumption. + destruct bb; cbn. assumption. Defined. Lemma stick_header_size: forall h bb, size (stick_header h bb) = size bb. Proof. - intros. destruct bb. unfold stick_header. simpl. reflexivity. + intros. destruct bb. unfold stick_header. cbn. reflexivity. Qed. Lemma stick_header_no_header: forall bb, stick_header (header bb) (no_header bb) = bb. Proof. - intros. destruct bb as [hd bdy ex COR]. simpl. unfold no_header; unfold stick_header; simpl. reflexivity. + intros. destruct bb as [hd bdy ex COR]. cbn. unfold no_header; unfold stick_header; cbn. reflexivity. Qed. (** * Sequential Semantics of basic blocks *) @@ -308,7 +308,7 @@ Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome := Theorem builtin_body_nil: forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil. Proof. - intros. destruct bb as [hd bdy ex WF]. simpl in *. + intros. destruct bb as [hd bdy ex WF]. cbn in *. apply wf_bblock_refl in WF. inv WF. unfold builtin_alone in H1. eapply H1; eauto. Qed. @@ -321,11 +321,11 @@ Theorem exec_body_app: /\ exec_body l' rs' m' = Next rs'' m''. Proof. induction l. - - intros. simpl in H. repeat eexists. auto. - - intros. rewrite <- app_comm_cons in H. simpl in H. + - intros. cbn in H. repeat eexists. auto. + - intros. rewrite <- app_comm_cons in H. cbn in H. destruct (exec_basic_instr a rs m) eqn:EXEBI. + apply IHl in H. destruct H as (rs1 & m1 & EXEB1 & EXEB2). - repeat eexists. simpl. rewrite EXEBI. eauto. auto. + repeat eexists. cbn. rewrite EXEBI. eauto. auto. + discriminate. Qed. diff --git a/kvx/Asmblockprops.v b/kvx/Asmblockprops.v index bc14b231..c3929be5 100644 --- a/kvx/Asmblockprops.v +++ b/kvx/Asmblockprops.v @@ -53,7 +53,7 @@ Qed. Lemma preg_of_not_SP: forall r, preg_of r <> SP. Proof. - intros. unfold preg_of; destruct r; simpl; congruence. + intros. unfold preg_of; destruct r; cbn; congruence. Qed. Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen. @@ -233,7 +233,7 @@ Proof. destruct (ireg_eq rd2 ra); try discriminate. *) rewrite Pregmap.gso; try discriminate. - simpl in *. + cbn in *. destruct (Mem.loadv _ _ _); try discriminate. destruct (Mem.loadv _ _ _); try discriminate. destruct (Mem.loadv _ _ _); try discriminate. @@ -264,7 +264,7 @@ Lemma exec_store_q_offset_pc_var: exec_store_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. Proof. intros. unfold exec_store_q_offset in *. unfold parexec_store_q_offset in *. rewrite Pregmap.gso; try discriminate. - simpl in *. + cbn in *. destruct (gpreg_q_expand _) as [s0 s1]. destruct (Mem.storev _ _ _); try discriminate. destruct (Mem.storev _ _ _); try discriminate. diff --git a/kvx/Asmgenproof.v b/kvx/Asmgenproof.v index 9e35e268..636c105f 100644 --- a/kvx/Asmgenproof.v +++ b/kvx/Asmgenproof.v @@ -39,7 +39,7 @@ Proof. unfold Asmgen.transf_program in H. apply bind_inversion in H. destruct H. inversion_clear H. apply bind_inversion in H1. destruct H1. inversion_clear H. inversion H2. unfold time, Compopts.time in *. remember (Machblockgen.transf_program p) as mbp. - unfold match_prog; simpl. + unfold match_prog; cbn. exists mbp; split. apply Machblockgenproof.transf_program_match; auto. exists x; split. apply Asmblockgenproof.transf_program_match; auto. exists x0; split. apply PostpassSchedulingproof.transf_program_match; auto. @@ -72,7 +72,7 @@ Let tge := Genv.globalenv tprog. Theorem transf_program_correct: forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). Proof. - unfold match_prog in TRANSF. simpl in TRANSF. + unfold match_prog in TRANSF. cbn in TRANSF. inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H. eapply compose_forward_simulations. exploit Machblockgenproof.transf_program_correct; eauto. diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v index 296963a7..66b468d7 100644 --- a/kvx/Asmvliw.v +++ b/kvx/Asmvliw.v @@ -849,7 +849,7 @@ Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val): Proof. unfold Val.cmpu, Val_cmpu. remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob. - destruct ob; simpl. + destruct ob; cbn. - erewrite Val_cmpu_bool_correct; eauto. econstructor. - econstructor. @@ -873,9 +873,9 @@ Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val): Proof. unfold Val.cmplu, Val_cmplu. remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob. - destruct ob as [b|]; simpl. + destruct ob as [b|]; cbn. - erewrite Val_cmplu_bool_correct; eauto. - simpl. econstructor. + cbn. econstructor. - econstructor. Qed. @@ -1426,13 +1426,13 @@ Definition is_label (lbl: label) (bb: bblock) : bool := Lemma is_label_correct_true lbl bb: List.In lbl (header bb) <-> is_label lbl bb = true. Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. + unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition. Qed. Lemma is_label_correct_false lbl bb: ~(List.In lbl (header bb)) <-> is_label lbl bb = false. Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. + unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition. Qed. @@ -1667,7 +1667,7 @@ Proof. constructor 1. - rewrite app_nil_r; auto. - unfold parexec_wio_bblock. - destruct (parexec_wio f _ _ _); simpl; auto. + destruct (parexec_wio f _ _ _); cbn; auto. Qed. @@ -1739,7 +1739,7 @@ Ltac Det_WIO X := exploit det_parexec_write_in_order; [ eapply H | idtac]; clear H; intro X | _ => idtac end. - intros; constructor; simpl. + intros; constructor; cbn. - (* determ *) intros s t1 s1 t2 s2 H H0. inv H; Det_WIO X1; inv H0; Det_WIO X2; Equalities. + split. constructor. auto. @@ -1754,7 +1754,7 @@ Ltac Det_WIO X := exploit external_call_determ. eexact H3. eexact H8. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. - (* trace length *) - red; intros. inv H; simpl. + red; intros. inv H; cbn. omega. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. diff --git a/kvx/CSE2depsproof.v b/kvx/CSE2depsproof.v index f283c8ac..6c584450 100644 --- a/kvx/CSE2depsproof.v +++ b/kvx/CSE2depsproof.v @@ -71,7 +71,7 @@ Section MEMORY_WRITE. unfold largest_size_chunk in *. rewrite ptrofs_modulus in *. - simpl in *. + cbn in *. inv ADDRR. inv ADDRW. destruct base; try discriminate. @@ -126,12 +126,12 @@ Proof. { (* Aindexed / Aindexed *) destruct args as [ | base [ | ]]. 1,3: discriminate. destruct args' as [ | base' [ | ]]. 1,3: discriminate. - simpl in OVERLAP. + cbn in OVERLAP. destruct (peq base base'). 2: discriminate. subst base'. destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP. 2: discriminate. - simpl in *. + cbn in *. eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. } Qed. diff --git a/kvx/CombineOpproof.v b/kvx/CombineOpproof.v index dafc90df..5dffc565 100644 --- a/kvx/CombineOpproof.v +++ b/kvx/CombineOpproof.v @@ -46,7 +46,7 @@ Qed. Ltac UseGetSound := match goal with | [ H: get _ = Some _ |- _ ] => - let x := fresh "EQ" in (generalize (get_op_sound _ _ _ H); intros x; simpl in x; FuncInv) + let x := fresh "EQ" in (generalize (get_op_sound _ _ _ H); intros x; cbn in x; FuncInv) end. Lemma combine_compimm_ne_0_sound: @@ -58,7 +58,7 @@ Proof. intros until args. functional induction (combine_compimm_ne_0 get x); intros EQ; inv EQ. (* of cmp *) UseGetSound. rewrite <- H. - destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto. + destruct (eval_condition cond (map valu args) m); cbn; auto. destruct b; auto. Qed. Lemma combine_compimm_eq_0_sound: @@ -71,7 +71,7 @@ Proof. (* of cmp *) UseGetSound. rewrite <- H. rewrite eval_negate_condition. - destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto. + destruct (eval_condition c (map valu args) m); cbn; auto. destruct b; auto. Qed. Lemma combine_compimm_eq_1_sound: @@ -83,7 +83,7 @@ Proof. intros until args. functional induction (combine_compimm_eq_1 get x); intros EQ; inv EQ. (* of cmp *) UseGetSound. rewrite <- H. - destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto. + destruct (eval_condition cond (map valu args) m); cbn; auto. destruct b; auto. Qed. Lemma combine_compimm_ne_1_sound: @@ -96,7 +96,7 @@ Proof. (* of cmp *) UseGetSound. rewrite <- H. rewrite eval_negate_condition. - destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto. + destruct (eval_condition c (map valu args) m); cbn; auto. destruct b; auto. Qed. Theorem combine_cond_sound: @@ -106,21 +106,21 @@ Theorem combine_cond_sound: Proof. intros. functional inversion H; subst. (* compimm ne zero *) - - simpl; eapply combine_compimm_ne_0_sound; eauto. + - cbn; eapply combine_compimm_ne_0_sound; eauto. (* compimm ne one *) - - simpl; eapply combine_compimm_ne_1_sound; eauto. + - cbn; eapply combine_compimm_ne_1_sound; eauto. (* compimm eq zero *) - - simpl; eapply combine_compimm_eq_0_sound; eauto. + - cbn; eapply combine_compimm_eq_0_sound; eauto. (* compimm eq one *) - - simpl; eapply combine_compimm_eq_1_sound; eauto. + - cbn; eapply combine_compimm_eq_1_sound; eauto. (* compuimm ne zero *) - - simpl; eapply combine_compimm_ne_0_sound; eauto. + - cbn; eapply combine_compimm_ne_0_sound; eauto. (* compuimm ne one *) - - simpl; eapply combine_compimm_ne_1_sound; eauto. + - cbn; eapply combine_compimm_ne_1_sound; eauto. (* compuimm eq zero *) - - simpl; eapply combine_compimm_eq_0_sound; eauto. + - cbn; eapply combine_compimm_eq_0_sound; eauto. (* compuimm eq one *) - - simpl; eapply combine_compimm_eq_1_sound; eauto. + - cbn; eapply combine_compimm_eq_1_sound; eauto. Qed. Theorem combine_addr_sound: @@ -130,10 +130,10 @@ Theorem combine_addr_sound: Proof. intros. functional inversion H; subst. - (* indexed - addimm *) - UseGetSound. simpl. rewrite <- H0. destruct v; auto. simpl; rewrite H7; simpl. + UseGetSound. cbn. rewrite <- H0. destruct v; auto. cbn; rewrite H7; cbn. rewrite Ptrofs.add_assoc. auto. - (* indexed - addimml *) - UseGetSound. simpl. rewrite <- H0. destruct v; auto. simpl; rewrite H7; simpl. + UseGetSound. cbn. rewrite <- H0. destruct v; auto. cbn; rewrite H7; cbn. rewrite Ptrofs.add_assoc. auto. Qed. @@ -144,33 +144,33 @@ Theorem combine_op_sound: Proof. intros. functional inversion H; subst. (* addimm - addimm *) - - UseGetSound. FuncInv. simpl. + - UseGetSound. FuncInv. cbn. rewrite <- H0. rewrite Val.add_assoc. auto. (* andimm - andimm *) - - UseGetSound; simpl. + - UseGetSound; cbn. generalize (Int.eq_spec p m0); rewrite H7; intros. - rewrite <- H0. rewrite Val.and_assoc. simpl. fold p. rewrite H1. auto. - - UseGetSound; simpl. + rewrite <- H0. rewrite Val.and_assoc. cbn. fold p. rewrite H1. auto. + - UseGetSound; cbn. rewrite <- H0. rewrite Val.and_assoc. auto. (* orimm - orimm *) - - UseGetSound. simpl. rewrite <- H0. rewrite Val.or_assoc. auto. + - UseGetSound. cbn. rewrite <- H0. rewrite Val.or_assoc. auto. (* xorimm - xorimm *) - - UseGetSound. simpl. rewrite <- H0. rewrite Val.xor_assoc. auto. + - UseGetSound. cbn. rewrite <- H0. rewrite Val.xor_assoc. auto. (* addlimm - addlimm *) - - UseGetSound. FuncInv. simpl. + - UseGetSound. FuncInv. cbn. rewrite <- H0. rewrite Val.addl_assoc. auto. (* andlimm - andlimm *) - - UseGetSound; simpl. + - UseGetSound; cbn. generalize (Int64.eq_spec p m0); rewrite H7; intros. - rewrite <- H0. rewrite Val.andl_assoc. simpl. fold p. rewrite H1. auto. - - UseGetSound; simpl. + rewrite <- H0. rewrite Val.andl_assoc. cbn. fold p. rewrite H1. auto. + - UseGetSound; cbn. rewrite <- H0. rewrite Val.andl_assoc. auto. (* orlimm - orlimm *) - - UseGetSound. simpl. rewrite <- H0. rewrite Val.orl_assoc. auto. + - UseGetSound. cbn. rewrite <- H0. rewrite Val.orl_assoc. auto. (* xorlimm - xorlimm *) - - UseGetSound. simpl. rewrite <- H0. rewrite Val.xorl_assoc. auto. + - UseGetSound. cbn. rewrite <- H0. rewrite Val.xorl_assoc. auto. (* cmp *) - - simpl. decEq; decEq. eapply combine_cond_sound; eauto. + - cbn. decEq; decEq. eapply combine_cond_sound; eauto. Qed. End COMBINE. diff --git a/kvx/ConstpropOpproof.v b/kvx/ConstpropOpproof.v index 05bbdde1..ffd35bcc 100644 --- a/kvx/ConstpropOpproof.v +++ b/kvx/ConstpropOpproof.v @@ -105,7 +105,7 @@ Proof. + (* global *) inv H2. exists (Genv.symbol_address ge id ofs); auto. + (* stack *) - inv H2. exists (Vptr sp ofs); split; auto. simpl. rewrite Ptrofs.add_zero_l; auto. + inv H2. exists (Vptr sp ofs); split; auto. cbn. rewrite Ptrofs.add_zero_l; auto. Qed. Lemma cond_strength_reduction_correct: @@ -115,7 +115,7 @@ Lemma cond_strength_reduction_correct: eval_condition cond' e##args' m = eval_condition cond e##args m. Proof. intros until vl. unfold cond_strength_reduction. - case (cond_strength_reduction_match cond args vl); simpl; intros; InvApproxRegs; SimplVM. + case (cond_strength_reduction_match cond args vl); cbn; intros; InvApproxRegs; SimplVM. - apply Val.swap_cmp_bool. - auto. - apply Val.swap_cmpu_bool. @@ -137,7 +137,7 @@ Proof. intros. unfold make_cmp_base. generalize (cond_strength_reduction_correct c args vl H). destruct (cond_strength_reduction c args vl) as [c' args']. intros EQ. - econstructor; split. simpl; eauto. rewrite EQ. auto. + econstructor; split. cbn; eauto. rewrite EQ. auto. Qed. Lemma make_cmp_correct: @@ -154,43 +154,43 @@ Proof. unfold make_cmp. case (make_cmp_match c args vl); intros. - unfold make_cmp_imm_eq. destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. -+ simpl in H; inv H. InvBooleans. subst n. - exists (e#r1); split; auto. simpl. - exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. ++ cbn in H; inv H. InvBooleans. subst n. + exists (e#r1); split; auto. cbn. + exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto. + destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. -* simpl in H; inv H. InvBooleans. subst n. - exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl. - exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. +* cbn in H; inv H. InvBooleans. subst n. + exists (Val.xor e#r1 (Vint Int.one)); split; auto. cbn. + exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto. * apply make_cmp_base_correct; auto. - unfold make_cmp_imm_ne. destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. -+ simpl in H; inv H. InvBooleans. subst n. - exists (e#r1); split; auto. simpl. - exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. ++ cbn in H; inv H. InvBooleans. subst n. + exists (e#r1); split; auto. cbn. + exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto. + destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. -* simpl in H; inv H. InvBooleans. subst n. - exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl. - exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. +* cbn in H; inv H. InvBooleans. subst n. + exists (Val.xor e#r1 (Vint Int.one)); split; auto. cbn. + exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto. * apply make_cmp_base_correct; auto. - unfold make_cmp_imm_eq. destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. -+ simpl in H; inv H. InvBooleans. subst n. - exists (e#r1); split; auto. simpl. - exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. ++ cbn in H; inv H. InvBooleans. subst n. + exists (e#r1); split; auto. cbn. + exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto. + destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. -* simpl in H; inv H. InvBooleans. subst n. - exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl. - exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. +* cbn in H; inv H. InvBooleans. subst n. + exists (Val.xor e#r1 (Vint Int.one)); split; auto. cbn. + exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto. * apply make_cmp_base_correct; auto. - unfold make_cmp_imm_ne. destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. -+ simpl in H; inv H. InvBooleans. subst n. - exists (e#r1); split; auto. simpl. - exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. ++ cbn in H; inv H. InvBooleans. subst n. + exists (e#r1); split; auto. cbn. + exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto. + destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. -* simpl in H; inv H. InvBooleans. subst n. - exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl. - exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. +* cbn in H; inv H. InvBooleans. subst n. + exists (Val.xor e#r1 (Vint Int.one)); split; auto. cbn. + exploit Y; eauto. intros [A | [A | A]]; rewrite A; cbn; auto. * apply make_cmp_base_correct; auto. - apply make_cmp_base_correct; auto. Qed. @@ -203,7 +203,7 @@ Proof. intros. unfold make_addimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. exists (e#r); split; auto. - destruct (e#r); simpl; auto; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto. + destruct (e#r); cbn; auto; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto. exists (Val.add e#r (Vint n)); split; auto. Qed. @@ -215,10 +215,10 @@ Lemma make_shlimm_correct: Proof. intros; unfold make_shlimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. - exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shl_zero. auto. + exists (e#r1); split; auto. destruct (e#r1); cbn; auto. rewrite Int.shl_zero. auto. destruct (Int.ltu n Int.iwordsize). - econstructor; split. simpl. eauto. auto. - econstructor; split. simpl. eauto. rewrite H; auto. + econstructor; split. cbn. eauto. auto. + econstructor; split. cbn. eauto. rewrite H; auto. Qed. Lemma make_shrimm_correct: @@ -229,10 +229,10 @@ Lemma make_shrimm_correct: Proof. intros; unfold make_shrimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. - exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shr_zero. auto. + exists (e#r1); split; auto. destruct (e#r1); cbn; auto. rewrite Int.shr_zero. auto. destruct (Int.ltu n Int.iwordsize). - econstructor; split. simpl. eauto. auto. - econstructor; split. simpl. eauto. rewrite H; auto. + econstructor; split. cbn. eauto. auto. + econstructor; split. cbn. eauto. rewrite H; auto. Qed. Lemma make_shruimm_correct: @@ -243,10 +243,10 @@ Lemma make_shruimm_correct: Proof. intros; unfold make_shruimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. - exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.shru_zero. auto. + exists (e#r1); split; auto. destruct (e#r1); cbn; auto. rewrite Int.shru_zero. auto. destruct (Int.ltu n Int.iwordsize). - econstructor; split. simpl. eauto. auto. - econstructor; split. simpl. eauto. rewrite H; auto. + econstructor; split. cbn. eauto. auto. + econstructor; split. cbn. eauto. rewrite H; auto. Qed. Lemma make_mulimm_correct: @@ -257,12 +257,12 @@ Lemma make_mulimm_correct: Proof. intros; unfold make_mulimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. - exists (Vint Int.zero); split; auto. destruct (e#r1); simpl; auto. rewrite Int.mul_zero; auto. + exists (Vint Int.zero); split; auto. destruct (e#r1); cbn; auto. rewrite Int.mul_zero; auto. predSpec Int.eq Int.eq_spec n Int.one; intros. subst. - exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int.mul_one; auto. + exists (e#r1); split; auto. destruct (e#r1); cbn; auto. rewrite Int.mul_one; auto. destruct (Int.is_power2 n) eqn:?; intros. - rewrite (Val.mul_pow2 e#r1 _ _ Heqo). econstructor; split. simpl; eauto. auto. - econstructor; split; eauto. simpl. rewrite H; auto. + rewrite (Val.mul_pow2 e#r1 _ _ Heqo). econstructor; split. cbn; eauto. auto. + econstructor; split; eauto. cbn. rewrite H; auto. Qed. Lemma make_divimm_correct: @@ -275,11 +275,11 @@ Proof. intros; unfold make_divimm. predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H. destruct (e#r1) eqn:?; - try (rewrite Val.divs_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto); + try (rewrite Val.divs_one in H; exists (Vint i); split; cbn; try rewrite Heqv0; auto); inv H; auto. destruct (Int.is_power2 n) eqn:?. destruct (Int.ltu i (Int.repr 31)) eqn:?. - exists v; split; auto. simpl. + exists v; split; auto. cbn. erewrite Val.divs_pow2; eauto. reflexivity. congruence. exists v; auto. exists v; auto. @@ -295,10 +295,10 @@ Proof. intros; unfold make_divuimm. predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H. destruct (e#r1) eqn:?; - try (rewrite Val.divu_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto); + try (rewrite Val.divu_one in H; exists (Vint i); split; cbn; try rewrite Heqv0; auto); inv H; auto. destruct (Int.is_power2 n) eqn:?. - econstructor; split. simpl; eauto. + econstructor; split. cbn; eauto. rewrite H0 in H. erewrite Val.divu_pow2 by eauto. auto. exists v; auto. Qed. @@ -312,7 +312,7 @@ Lemma make_moduimm_correct: Proof. intros; unfold make_moduimm. destruct (Int.is_power2 n) eqn:?. - exists v; split; auto. simpl. decEq. eapply Val.modu_pow2; eauto. congruence. + exists v; split; auto. cbn. decEq. eapply Val.modu_pow2; eauto. congruence. exists v; auto. Qed. @@ -324,18 +324,18 @@ Lemma make_andimm_correct: Proof. intros; unfold make_andimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. - subst n. exists (Vint Int.zero); split; auto. destruct (e#r); simpl; auto. rewrite Int.and_zero; auto. + subst n. exists (Vint Int.zero); split; auto. destruct (e#r); cbn; auto. rewrite Int.and_zero; auto. predSpec Int.eq Int.eq_spec n Int.mone; intros. - subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.and_mone; auto. + subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int.and_mone; auto. destruct (match x with Uns _ k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero | _ => false end) eqn:UNS. destruct x; try congruence. exists (e#r); split; auto. - inv H; auto. simpl. replace (Int.and i n) with i; auto. + inv H; auto. cbn. replace (Int.and i n) with i; auto. generalize (Int.eq_spec (Int.zero_ext n0 (Int.not n)) Int.zero); rewrite UNS; intro EQ. Int.bit_solve. destruct (zlt i0 n0). replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)). - rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. + rewrite Int.bits_zero. cbn. rewrite andb_true_r. auto. rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. rewrite Int.bits_not by auto. apply negb_involutive. rewrite H6 by auto. auto. @@ -349,9 +349,9 @@ Lemma make_orimm_correct: Proof. intros; unfold make_orimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. - subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.or_zero; auto. + subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int.or_zero; auto. predSpec Int.eq Int.eq_spec n Int.mone; intros. - subst n. exists (Vint Int.mone); split; auto. destruct (e#r); simpl; auto. rewrite Int.or_mone; auto. + subst n. exists (Vint Int.mone); split; auto. destruct (e#r); cbn; auto. rewrite Int.or_mone; auto. econstructor; split; eauto. auto. Qed. @@ -362,7 +362,7 @@ Lemma make_xorimm_correct: Proof. intros; unfold make_xorimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. - subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.xor_zero; auto. + subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int.xor_zero; auto. predSpec Int.eq Int.eq_spec n Int.mone; intros. subst n. exists (Val.notint e#r); split; auto. econstructor; split; eauto. auto. @@ -376,7 +376,7 @@ Proof. intros. unfold make_addlimm. predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. subst. exists (e#r); split; auto. - destruct (e#r); simpl; auto; rewrite ? Int64.add_zero, ? Ptrofs.add_zero; auto. + destruct (e#r); cbn; auto; rewrite ? Int64.add_zero, ? Ptrofs.add_zero; auto. exists (Val.addl e#r (Vlong n)); split; auto. Qed. @@ -388,11 +388,11 @@ Lemma make_shllimm_correct: Proof. intros; unfold make_shllimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. - exists (e#r1); split; auto. destruct (e#r1); simpl; auto. + exists (e#r1); split; auto. destruct (e#r1); cbn; auto. unfold Int64.shl'. rewrite Z.shiftl_0_r, Int64.repr_unsigned. auto. destruct (Int.ltu n Int64.iwordsize'). - econstructor; split. simpl. eauto. auto. - econstructor; split. simpl. eauto. rewrite H; auto. + econstructor; split. cbn. eauto. auto. + econstructor; split. cbn. eauto. rewrite H; auto. Qed. Lemma make_shrlimm_correct: @@ -403,11 +403,11 @@ Lemma make_shrlimm_correct: Proof. intros; unfold make_shrlimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. - exists (e#r1); split; auto. destruct (e#r1); simpl; auto. + exists (e#r1); split; auto. destruct (e#r1); cbn; auto. unfold Int64.shr'. rewrite Z.shiftr_0_r, Int64.repr_signed. auto. destruct (Int.ltu n Int64.iwordsize'). - econstructor; split. simpl. eauto. auto. - econstructor; split. simpl. eauto. rewrite H; auto. + econstructor; split. cbn. eauto. auto. + econstructor; split. cbn. eauto. rewrite H; auto. Qed. Lemma make_shrluimm_correct: @@ -418,11 +418,11 @@ Lemma make_shrluimm_correct: Proof. intros; unfold make_shrluimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. - exists (e#r1); split; auto. destruct (e#r1); simpl; auto. + exists (e#r1); split; auto. destruct (e#r1); cbn; auto. unfold Int64.shru'. rewrite Z.shiftr_0_r, Int64.repr_unsigned. auto. destruct (Int.ltu n Int64.iwordsize'). - econstructor; split. simpl. eauto. auto. - econstructor; split. simpl. eauto. rewrite H; auto. + econstructor; split. cbn. eauto. auto. + econstructor; split. cbn. eauto. rewrite H; auto. Qed. Lemma make_mullimm_correct: @@ -433,15 +433,15 @@ Lemma make_mullimm_correct: Proof. intros; unfold make_mullimm. predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. subst. - exists (Vlong Int64.zero); split; auto. destruct (e#r1); simpl; auto. rewrite Int64.mul_zero; auto. + exists (Vlong Int64.zero); split; auto. destruct (e#r1); cbn; auto. rewrite Int64.mul_zero; auto. predSpec Int64.eq Int64.eq_spec n Int64.one; intros. subst. - exists (e#r1); split; auto. destruct (e#r1); simpl; auto. rewrite Int64.mul_one; auto. + exists (e#r1); split; auto. destruct (e#r1); cbn; auto. rewrite Int64.mul_one; auto. destruct (Int64.is_power2' n) eqn:?; intros. exists (Val.shll e#r1 (Vint i)); split; auto. - destruct (e#r1); simpl; auto. + destruct (e#r1); cbn; auto. erewrite Int64.is_power2'_range by eauto. erewrite Int64.mul_pow2' by eauto. auto. - econstructor; split; eauto. simpl; rewrite H; auto. + econstructor; split; eauto. cbn; rewrite H; auto. Qed. Lemma make_divlimm_correct: @@ -453,7 +453,7 @@ Lemma make_divlimm_correct: Proof. intros; unfold make_divlimm. destruct (Int64.is_power2' n) eqn:?. destruct (Int.ltu i (Int.repr 63)) eqn:?. - rewrite H0 in H. econstructor; split. simpl; eauto. + rewrite H0 in H. econstructor; split. cbn; eauto. erewrite Val.divls_pow2; eauto. auto. exists v; auto. exists v; auto. @@ -468,9 +468,9 @@ Lemma make_divluimm_correct: Proof. intros; unfold make_divluimm. destruct (Int64.is_power2' n) eqn:?. - econstructor; split. simpl; eauto. + econstructor; split. cbn; eauto. rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2. - simpl. + cbn. erewrite Int64.is_power2'_range by eauto. erewrite Int64.divu_pow2' by eauto. auto. exists v; auto. @@ -485,9 +485,9 @@ Lemma make_modluimm_correct: Proof. intros; unfold make_modluimm. destruct (Int64.is_power2 n) eqn:?. - exists v; split; auto. simpl. decEq. + exists v; split; auto. cbn. decEq. rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2. - simpl. erewrite Int64.modu_and by eauto. auto. + cbn. erewrite Int64.modu_and by eauto. auto. exists v; auto. Qed. @@ -498,9 +498,9 @@ Lemma make_andlimm_correct: Proof. intros; unfold make_andlimm. predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. - subst n. exists (Vlong Int64.zero); split; auto. destruct (e#r); simpl; auto. rewrite Int64.and_zero; auto. + subst n. exists (Vlong Int64.zero); split; auto. destruct (e#r); cbn; auto. rewrite Int64.and_zero; auto. predSpec Int64.eq Int64.eq_spec n Int64.mone; intros. - subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int64.and_mone; auto. + subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int64.and_mone; auto. econstructor; split; eauto. auto. Qed. @@ -511,9 +511,9 @@ Lemma make_orlimm_correct: Proof. intros; unfold make_orlimm. predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. - subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int64.or_zero; auto. + subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int64.or_zero; auto. predSpec Int64.eq Int64.eq_spec n Int64.mone; intros. - subst n. exists (Vlong Int64.mone); split; auto. destruct (e#r); simpl; auto. rewrite Int64.or_mone; auto. + subst n. exists (Vlong Int64.mone); split; auto. destruct (e#r); cbn; auto. rewrite Int64.or_mone; auto. econstructor; split; eauto. auto. Qed. @@ -524,7 +524,7 @@ Lemma make_xorlimm_correct: Proof. intros; unfold make_xorlimm. predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. - subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int64.xor_zero; auto. + subst n. exists (e#r); split; auto. destruct (e#r); cbn; auto. rewrite Int64.xor_zero; auto. predSpec Int64.eq Int64.eq_spec n Int64.mone; intros. subst n. exists (Val.notl e#r); split; auto. econstructor; split; eauto. auto. @@ -538,9 +538,9 @@ Lemma make_mulfimm_correct: Proof. intros; unfold make_mulfimm. destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. - simpl. econstructor; split. eauto. rewrite H; subst n. - destruct (e#r1); simpl; auto. rewrite Float.mul2_add; auto. - simpl. econstructor; split; eauto. + cbn. econstructor; split. eauto. rewrite H; subst n. + destruct (e#r1); cbn; auto. rewrite Float.mul2_add; auto. + cbn. econstructor; split; eauto. Qed. Lemma make_mulfimm_correct_2: @@ -551,10 +551,10 @@ Lemma make_mulfimm_correct_2: Proof. intros; unfold make_mulfimm. destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. - simpl. econstructor; split. eauto. rewrite H; subst n. - destruct (e#r2); simpl; auto. rewrite Float.mul2_add; auto. + cbn. econstructor; split. eauto. rewrite H; subst n. + destruct (e#r2); cbn; auto. rewrite Float.mul2_add; auto. rewrite Float.mul_commut; auto. - simpl. econstructor; split; eauto. + cbn. econstructor; split; eauto. Qed. Lemma make_mulfsimm_correct: @@ -565,9 +565,9 @@ Lemma make_mulfsimm_correct: Proof. intros; unfold make_mulfsimm. destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. - simpl. econstructor; split. eauto. rewrite H; subst n. - destruct (e#r1); simpl; auto. rewrite Float32.mul2_add; auto. - simpl. econstructor; split; eauto. + cbn. econstructor; split. eauto. rewrite H; subst n. + destruct (e#r1); cbn; auto. rewrite Float32.mul2_add; auto. + cbn. econstructor; split; eauto. Qed. Lemma make_mulfsimm_correct_2: @@ -578,10 +578,10 @@ Lemma make_mulfsimm_correct_2: Proof. intros; unfold make_mulfsimm. destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. - simpl. econstructor; split. eauto. rewrite H; subst n. - destruct (e#r2); simpl; auto. rewrite Float32.mul2_add; auto. + cbn. econstructor; split. eauto. rewrite H; subst n. + destruct (e#r2); cbn; auto. rewrite Float32.mul2_add; auto. rewrite Float32.mul_commut; auto. - simpl. econstructor; split; eauto. + cbn. econstructor; split; eauto. Qed. Lemma make_cast8signed_correct: @@ -594,8 +594,8 @@ Proof. exists e#r; split; auto. assert (V: vmatch bc e#r (Sgn Ptop 8)). { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. - econstructor; split; simpl; eauto. + inv V; cbn; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. + econstructor; split; cbn; eauto. Qed. Lemma make_cast16signed_correct: @@ -608,8 +608,8 @@ Proof. exists e#r; split; auto. assert (V: vmatch bc e#r (Sgn Ptop 16)). { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. - econstructor; split; simpl; eauto. + inv V; cbn; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. + econstructor; split; cbn; eauto. Qed. Lemma op_strength_reduction_correct: @@ -620,7 +620,7 @@ Lemma op_strength_reduction_correct: exists w, eval_operation ge (Vptr sp Ptrofs.zero) op' e##args' m = Some w /\ Val.lessdef v w. Proof. intros until v; unfold op_strength_reduction; - case (op_strength_reduction_match op args vl); simpl; intros. + case (op_strength_reduction_match op args vl); cbn; intros. - (* cast8signed *) InvApproxRegs; SimplVM; inv H0. apply make_cast8signed_correct; auto. - (* cast16signed *) @@ -733,15 +733,15 @@ Lemma addr_strength_reduction_correct: exists res', eval_addressing ge (Vptr sp Ptrofs.zero) addr' e##args' = Some res' /\ Val.lessdef res res'. Proof. intros until res. unfold addr_strength_reduction. - destruct (addr_strength_reduction_match addr args vl); simpl; + destruct (addr_strength_reduction_match addr args vl); cbn; intros VL EA; InvApproxRegs; SimplVM; try (inv EA). - destruct (orb _ _). + exists (Val.offset_ptr e#r1 n); auto. -+ simpl. rewrite Genv.shift_symbol_address. econstructor; split; eauto. - inv H0; simpl; auto. ++ cbn. rewrite Genv.shift_symbol_address. econstructor; split; eauto. + inv H0; cbn; auto. - rewrite Ptrofs.add_zero_l. econstructor; split; eauto. change (Vptr sp (Ptrofs.add n1 n)) with (Val.offset_ptr (Vptr sp n1) n). - inv H0; simpl; auto. + inv H0; cbn; auto. - exists res; auto. Qed. diff --git a/kvx/Conventions1.v b/kvx/Conventions1.v index ab30ded9..0b2cf406 100644 --- a/kvx/Conventions1.v +++ b/kvx/Conventions1.v @@ -108,7 +108,7 @@ Lemma loc_result_type: subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. intros. unfold proj_sig_res, loc_result, mreg_type. - destruct (sig_res sig); try destruct Archi.ptr64; simpl; trivial; destruct t; trivial. + destruct (sig_res sig); try destruct Archi.ptr64; cbn; trivial; destruct t; trivial. Qed. (** The result locations are caller-save registers *) @@ -118,7 +118,7 @@ Lemma loc_result_caller_save: forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. unfold loc_result, is_callee_save; - destruct (sig_res s); simpl; auto; try destruct Archi.ptr64; simpl; auto; try destruct t; simpl; auto. + destruct (sig_res s); cbn; auto; try destruct Archi.ptr64; cbn; auto; try destruct t; cbn; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -296,9 +296,9 @@ Proof. OKREGS regs -> OKF f -> ofs >= 0 -> OK (one_arg regs rn ofs ty f)). { intros until f; intros OR OF OO; red; unfold one_arg; intros. destruct (list_nth_z regs rn) as [r|] eqn:NTH; destruct H. - - subst p; simpl. apply OR. eapply list_nth_z_in; eauto. + - subst p; cbn. apply OR. eapply list_nth_z_in; eauto. - eapply OF; eauto. - - subst p; simpl. auto using align_divides, typealign_pos. + - subst p; cbn. auto using align_divides, typealign_pos. - eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega. } @@ -310,16 +310,16 @@ Proof. assert (OO': ofs' >= 0) by (apply (AL ofs Tlong); auto). assert (DFL: OK (Twolong (S Outgoing (ofs' + 1) Tint) (S Outgoing ofs' Tint) :: f rn' (ofs' + 2))). - { red; simpl; intros. destruct H. - - subst p; simpl. + { red; cbn; intros. destruct H. + - subst p; cbn. repeat split; auto using Z.divide_1_l. omega. - eapply OF; [idtac|eauto]. omega. } destruct (list_nth_z regs rn') as [r1|] eqn:NTH1; destruct (list_nth_z regs (rn' + 1)) as [r2|] eqn:NTH2; try apply DFL. - red; simpl; intros; destruct H. - - subst p; simpl. split; apply OR; eauto using list_nth_z_in. + red; cbn; intros; destruct H. + - subst p; cbn. split; apply OR; eauto using list_nth_z_in. - eapply OF; [idtac|eauto]. auto. } assert (C: forall regs rn ofs ty f, @@ -327,10 +327,10 @@ Proof. { intros until f; intros OR OF OO OTY; unfold hybrid_arg; red; intros. set (rn' := align rn 2) in *. destruct (list_nth_z regs rn') as [r|] eqn:NTH; destruct H. - - subst p; simpl. apply OR. eapply list_nth_z_in; eauto. + - subst p; cbn. apply OR. eapply list_nth_z_in; eauto. - eapply OF; eauto. - - subst p; simpl. rewrite OTY. split. apply (AL ofs Tlong OO). apply Z.divide_1_l. - - eapply OF; [idtac|eauto]. generalize (AL ofs Tlong OO); simpl; omega. + - subst p; cbn. rewrite OTY. split. apply (AL ofs Tlong OO). apply Z.divide_1_l. + - eapply OF; [idtac|eauto]. generalize (AL ofs Tlong OO); cbn; omega. } assert (D: OKREGS param_regs). { red. decide_goal. } @@ -339,8 +339,8 @@ Proof. cut (forall va tyl rn ofs, ofs >= 0 -> OK (loc_arguments_rec va tyl rn ofs)). unfold OK. eauto. - induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; simpl. - - red; simpl; tauto. + induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; cbn. + - red; cbn; tauto. - destruct ty1. + (* int *) apply A; auto. + (* float *) @@ -369,10 +369,10 @@ Remark fold_max_outgoing_above: Proof. assert (A: forall n l, max_outgoing_1 n l >= n). { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. } - induction l; simpl; intros. + induction l; cbn; intros. - omega. - eapply Zge_trans. eauto. - destruct a; simpl. apply A. eapply Zge_trans; eauto. + destruct a; cbn. apply A. eapply Zge_trans; eauto. Qed. Lemma size_arguments_above: @@ -392,14 +392,14 @@ Proof. assert (B: forall p n, In (S Outgoing ofs ty) (regs_of_rpair p) -> ofs + typesize ty <= max_outgoing_2 n p). - { intros. destruct p; simpl in H; intuition; subst; simpl. + { intros. destruct p; cbn in H; intuition; subst; cbn. - xomega. - eapply Z.le_trans. 2: apply A. xomega. - xomega. } assert (C: forall l n, In (S Outgoing ofs ty) (regs_of_rpairs l) -> ofs + typesize ty <= fold_left max_outgoing_2 l n). - { induction l; simpl; intros. + { induction l; cbn; intros. - contradiction. - rewrite in_app_iff in H. destruct H. + eapply Z.le_trans. eapply B; eauto. apply Z.ge_le. apply fold_max_outgoing_above. diff --git a/kvx/ExtValues.v b/kvx/ExtValues.v index 3664c00a..a0c10ddd 100644 --- a/kvx/ExtValues.v +++ b/kvx/ExtValues.v @@ -62,10 +62,10 @@ Lemma shift1_4_of_z_correct : end. Proof. intro. unfold shift1_4_of_z. - destruct (Z.eq_dec _ _); simpl; try congruence. - destruct (Z.eq_dec _ _); simpl; try congruence. - destruct (Z.eq_dec _ _); simpl; try congruence. - destruct (Z.eq_dec _ _); simpl; try congruence. + destruct (Z.eq_dec _ _); cbn; try congruence. + destruct (Z.eq_dec _ _); cbn; try congruence. + destruct (Z.eq_dec _ _); cbn; try congruence. + destruct (Z.eq_dec _ _); cbn; try congruence. trivial. Qed. @@ -215,19 +215,19 @@ Theorem divu_is_divlu: forall v1 v2 : val, end. Proof. intros. - destruct v1; simpl; trivial. - destruct v2; simpl; trivial. + destruct v1; cbn; trivial. + destruct v2; cbn; trivial. destruct i as [i_val i_range]. destruct i0 as [i0_val i0_range]. - simpl. + cbn. unfold Int.eq, Int64.eq, Int.zero, Int64.zero. - simpl. + cbn. rewrite Int.unsigned_repr by (compute; split; discriminate). rewrite (Int64.unsigned_repr 0) by (compute; split; discriminate). rewrite (unsigned64_repr i0_val) by assumption. - destruct (zeq i0_val 0) as [ | Hnot0]; simpl; trivial. + destruct (zeq i0_val 0) as [ | Hnot0]; cbn; trivial. f_equal. f_equal. - unfold Int.divu, Int64.divu. simpl. + unfold Int.divu, Int64.divu. cbn. rewrite (unsigned64_repr i_val) by assumption. rewrite (unsigned64_repr i0_val) by assumption. unfold Int64.loword. @@ -260,19 +260,19 @@ Theorem modu_is_modlu: forall v1 v2 : val, end. Proof. intros. - destruct v1; simpl; trivial. - destruct v2; simpl; trivial. + destruct v1; cbn; trivial. + destruct v2; cbn; trivial. destruct i as [i_val i_range]. destruct i0 as [i0_val i0_range]. - simpl. + cbn. unfold Int.eq, Int64.eq, Int.zero, Int64.zero. - simpl. + cbn. rewrite Int.unsigned_repr by (compute; split; discriminate). rewrite (Int64.unsigned_repr 0) by (compute; split; discriminate). rewrite (unsigned64_repr i0_val) by assumption. - destruct (zeq i0_val 0) as [ | Hnot0]; simpl; trivial. + destruct (zeq i0_val 0) as [ | Hnot0]; cbn; trivial. f_equal. f_equal. - unfold Int.modu, Int64.modu. simpl. + unfold Int.modu, Int64.modu. cbn. rewrite (unsigned64_repr i_val) by assumption. rewrite (unsigned64_repr i0_val) by assumption. unfold Int64.loword. @@ -347,19 +347,19 @@ Theorem divs_is_divls: forall v1 v2 : val, end. Proof. intros. - destruct v1; simpl; trivial. - destruct v2; simpl; trivial. + destruct v1; cbn; trivial. + destruct v2; cbn; trivial. destruct i as [i_val i_range]. destruct i0 as [i0_val i0_range]. - simpl. + cbn. unfold Int.eq, Int64.eq, Int.zero, Int64.zero. - simpl. + cbn. replace (Int.unsigned (Int.repr 0)) with 0 in * by reflexivity. - destruct (zeq _ _) as [H0' | Hnot0]; simpl; trivial. - destruct (zeq i_val (Int.unsigned (Int.repr Int.min_signed))) as [Hmin | Hnotmin]; simpl. + destruct (zeq _ _) as [H0' | Hnot0]; cbn; trivial. + destruct (zeq i_val (Int.unsigned (Int.repr Int.min_signed))) as [Hmin | Hnotmin]; cbn. { subst. destruct (zeq i0_val (Int.unsigned Int.mone)) as [Hmone | Hnotmone]; trivial. - unfold Int.signed. simpl. + unfold Int.signed. cbn. replace (Int64.unsigned (Int64.repr 0)) with 0 in * by reflexivity. rewrite if_zlt_min_signed_half_modulus. replace (if @@ -370,7 +370,7 @@ Proof. (Int64.unsigned (Int64.repr Int64.min_signed)) then true else false) with false by reflexivity. - simpl. + cbn. rewrite orb_false_r. destruct (zlt i0_val Int.half_modulus) as [Hlt_half | Hge_half]. { @@ -380,7 +380,7 @@ Proof. unfold Val.loword. f_equal. unfold Int64.divs, Int.divs, Int64.loword. - unfold Int.signed, Int64.signed. simpl. + unfold Int.signed, Int64.signed. cbn. rewrite if_zlt_min_signed_half_modulus. change Int.half_modulus with 2147483648 in *. destruct (zlt _ _) as [discard|]; try omega. clear discard. @@ -390,7 +390,7 @@ Proof. with 18446744071562067968. change Int64.half_modulus with 9223372036854775808. change Int64.modulus with 18446744073709551616. - simpl. + cbn. rewrite (Int64.unsigned_repr i0_val) by (change Int64.max_unsigned with 18446744073709551615; omega). destruct (zlt i0_val 9223372036854775808) as [discard |]; try omega. clear discard. @@ -449,7 +449,7 @@ Lemma big_unsigned_signed: Proof. destruct x as [xval xrange]. intro BIG. - unfold Int.signed, Int.unsigned in *. simpl in *. + unfold Int.signed, Int.unsigned in *. cbn in *. destruct (zlt _ _). omega. trivial. @@ -499,10 +499,10 @@ Lemma divs_is_quot: forall v1 v2 : val, end. Proof. - destruct v1; destruct v2; simpl; trivial. + destruct v1; destruct v2; cbn; trivial. unfold Int.divs. rewrite signed_0_eqb. - destruct (Int.eq i0 Int.zero) eqn:Eeq0; simpl; trivial. + destruct (Int.eq i0 Int.zero) eqn:Eeq0; cbn; trivial. destruct (Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone) eqn:EXCEPTION. { replace (Int.signed i0) with (-1). replace (Int.signed i) with Int.min_signed. @@ -523,7 +523,7 @@ Proof. unfold Int.eq in EXCEPTION. destruct (zeq _ _) in EXCEPTION; try discriminate. destruct (zeq _ _) as [Hmone | ] in EXCEPTION; try discriminate. - destruct i0 as [i0val i0range]; unfold Int.signed in *; simpl in *. + destruct i0 as [i0val i0range]; unfold Int.signed in *; cbn in *. rewrite Hmone. reflexivity. } @@ -651,7 +651,7 @@ Qed. Lemma sub_add_neg : forall x y, Val.sub x y = Val.add x (Val.neg y). Proof. - destruct x; destruct y; simpl; trivial. + destruct x; destruct y; cbn; trivial. f_equal. apply Int.sub_add_opp. Qed. @@ -659,7 +659,7 @@ Qed. Lemma neg_mul_distr_r : forall x y, Val.neg (Val.mul x y) = Val.mul x (Val.neg y). Proof. - destruct x; destruct y; simpl; trivial. + destruct x; destruct y; cbn; trivial. f_equal. apply Int.neg_mul_distr_r. Qed. @@ -668,7 +668,7 @@ Qed. Lemma sub_addl_negl : forall x y, Val.subl x y = Val.addl x (Val.negl y). Proof. - destruct x; destruct y; simpl; trivial. + destruct x; destruct y; cbn; trivial. + f_equal. apply Int64.sub_add_opp. + destruct (Archi.ptr64) eqn:ARCHI64; trivial. f_equal. rewrite Ptrofs.sub_add_opp. @@ -681,15 +681,15 @@ Proof. rewrite Hagree2. reflexivity. exact (Ptrofs.agree64_of_int ARCHI64 i0). - + destruct (Archi.ptr64) eqn:ARCHI64; simpl; trivial. - destruct (eq_block _ _); simpl; trivial. + + destruct (Archi.ptr64) eqn:ARCHI64; cbn; trivial. + destruct (eq_block _ _); cbn; trivial. Qed. *) Lemma negl_mull_distr_r : forall x y, Val.negl (Val.mull x y) = Val.mull x (Val.negl y). Proof. - destruct x; destruct y; simpl; trivial. + destruct x; destruct y; cbn; trivial. f_equal. apply Int64.neg_mul_distr_r. Qed. diff --git a/kvx/NeedOp.v b/kvx/NeedOp.v index 4c354d5a..f636336d 100644 --- a/kvx/NeedOp.v +++ b/kvx/NeedOp.v @@ -229,7 +229,7 @@ Lemma needs_of_condition0_sound: Proof. intros until arg2. intros Hcond Hagree. - apply eval_condition0_inj with (f := inject_id) (m1 := m1) (v1 := arg1); simpl; auto. + apply eval_condition0_inj with (f := inject_id) (m1 := m1) (v1 := arg1); cbn; auto. apply val_inject_lessdef. apply lessdef_vagree. assumption. Qed. @@ -239,7 +239,7 @@ Lemma addl_sound: vagree (Val.addl v1 v2) (Val.addl w1 w2) x. Proof. unfold default; intros. - destruct x; simpl in *; trivial. + destruct x; cbn in *; trivial. - unfold Val.addl. destruct v1; destruct v2; trivial; destruct Archi.ptr64; trivial. - apply Val.addl_lessdef; trivial. @@ -249,7 +249,7 @@ Lemma subl_lessdef: forall v1 v1' v2 v2', Val.lessdef v1 v1' -> Val.lessdef v2 v2' -> Val.lessdef (Val.subl v1 v2) (Val.subl v1' v2'). Proof. - intros. inv H. inv H0. auto. destruct v1'; simpl; auto. simpl; auto. + intros. inv H. inv H0. auto. destruct v1'; cbn; auto. cbn; auto. Qed. Lemma subl_sound: @@ -258,10 +258,10 @@ Lemma subl_sound: vagree (Val.subl v1 v2) (Val.subl w1 w2) x. Proof. unfold default; intros. - destruct x; simpl in *; trivial. + destruct x; cbn in *; trivial. - unfold Val.subl. - destruct v1; destruct v2; trivial; destruct Archi.ptr64; simpl; trivial. - destruct (eq_block _ _) ; simpl; trivial. + destruct v1; destruct v2; trivial; destruct Archi.ptr64; cbn; trivial. + destruct (eq_block _ _) ; cbn; trivial. - apply subl_lessdef; trivial. Qed. @@ -272,7 +272,7 @@ Lemma mull_sound: vagree (Val.mull v1 v2) (Val.mull w1 w2) x. Proof. unfold default; intros. - destruct x; simpl in *; trivial. + destruct x; cbn in *; trivial. - unfold Val.mull. destruct v1; destruct v2; trivial. - unfold Val.mull. @@ -284,7 +284,7 @@ Qed. Remark default_idem: forall nv, default (default nv) = default nv. Proof. - destruct nv; simpl; trivial. + destruct nv; cbn; trivial. Qed. Lemma vagree_triple_op_float : @@ -298,14 +298,14 @@ Proof. induction nv; intros Hax Hby Hcz. - trivial. - - simpl in *. destruct a; simpl; trivial. - destruct b; simpl; trivial. - destruct c; simpl; trivial. - - simpl in *. destruct a; simpl; trivial. - destruct b; simpl; trivial. - destruct c; simpl; trivial. + - cbn in *. destruct a; cbn; trivial. + destruct b; cbn; trivial. + destruct c; cbn; trivial. + - cbn in *. destruct a; cbn; trivial. + destruct b; cbn; trivial. + destruct c; cbn; trivial. inv Hax. inv Hby. inv Hcz. - simpl. + cbn. constructor. Qed. @@ -320,14 +320,14 @@ Proof. induction nv; intros Hax Hby Hcz. - trivial. - - simpl in *. destruct a; simpl; trivial. - destruct b; simpl; trivial. - destruct c; simpl; trivial. - - simpl in *. destruct a; simpl; trivial. - destruct b; simpl; trivial. - destruct c; simpl; trivial. + - cbn in *. destruct a; cbn; trivial. + destruct b; cbn; trivial. + destruct c; cbn; trivial. + - cbn in *. destruct a; cbn; trivial. + destruct b; cbn; trivial. + destruct c; cbn; trivial. inv Hax. inv Hby. inv Hcz. - simpl. + cbn. constructor. Qed. @@ -343,7 +343,7 @@ Lemma needs_of_operation_sound: /\ vagree v v' nv. Proof. unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail); - simpl in *; FuncInv; InvAgree; TrivialExists. + cbn in *; FuncInv; InvAgree; TrivialExists. - apply sign_ext_sound; auto. compute; auto. - apply sign_ext_sound; auto. compute; auto. - apply add_sound; auto. @@ -384,17 +384,17 @@ Proof. - destruct (eval_condition0 _ _ _) as [b|] eqn:EC. erewrite needs_of_condition0_sound by eauto. apply select_sound; auto. - simpl; auto with na. + cbn; auto with na. (* select imm *) - destruct (eval_condition0 _ _ _) as [b|] eqn:EC. { erewrite needs_of_condition0_sound by eauto. apply select_sound; auto with na. } - simpl; auto with na. + cbn; auto with na. (* select long imm *) - destruct (eval_condition0 _ _ _) as [b|] eqn:EC. { erewrite needs_of_condition0_sound by eauto. apply select_sound; auto with na. } - simpl; auto with na. + cbn; auto with na. Qed. Lemma operation_is_redundant_sound: @@ -404,7 +404,7 @@ Lemma operation_is_redundant_sound: vagree_list (arg1 :: args) (arg1' :: args') (needs_of_operation op nv) -> vagree v arg1' nv. Proof. - intros. destruct op; simpl in *; try discriminate; inv H1; FuncInv; subst. + intros. destruct op; cbn in *; try discriminate; inv H1; FuncInv; subst. - apply sign_ext_redundant_sound; auto. omega. - apply sign_ext_redundant_sound; auto. omega. - apply andimm_redundant_sound; auto. @@ -508,9 +508,9 @@ Qed. Ltac FuncInv := match goal with | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ => - destruct x; simpl in H; FuncInv + destruct x; cbn in H; FuncInv | H: (match ?v with Vundef => _ | Vint _ => _ | Vfloat _ => _ | Vptr _ _ => _ end = Some _) |- _ => - destruct v; simpl in H; FuncInv + destruct v; cbn in H; FuncInv | H: (if Archi.ptr64 then _ else _) = Some _ |- _ => destruct Archi.ptr64 eqn:?; FuncInv | H: (Some _ = Some _) |- _ => @@ -727,27 +727,27 @@ Qed. Remark type_sub: forall v1 v2, Val.has_type (Val.sub v1 v2) Tint. Proof. - intros. unfold Val.has_type, Val.sub. destruct Archi.ptr64, v1, v2; simpl; auto. + intros. unfold Val.has_type, Val.sub. destruct Archi.ptr64, v1, v2; cbn; auto. destruct (eq_block _ _); auto. Qed. Remark type_subl: forall v1 v2, Val.has_type (Val.subl v1 v2) Tlong. Proof. - intros. unfold Val.has_type, Val.subl. destruct Archi.ptr64, v1, v2; simpl; auto. + intros. unfold Val.has_type, Val.subl. destruct Archi.ptr64, v1, v2; cbn; auto. destruct (eq_block _ _); auto. Qed. Remark type_shl: forall v1 v2, Val.has_type (Val.shl v1 v2) Tint. Proof. - destruct v1, v2; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial. + destruct v1, v2; cbn; trivial; destruct (Int.ltu _ _); cbn; trivial. Qed. Remark type_shll: forall v1 v2, Val.has_type (Val.shll v1 v2) Tlong. Proof. - destruct v1, v2; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial. + destruct v1, v2; cbn; trivial; destruct (Int.ltu _ _); cbn; trivial. Qed. Lemma type_of_operation_sound: @@ -757,7 +757,7 @@ Lemma type_of_operation_sound: Val.has_type v (snd (type_of_operation op)). Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). intros. - destruct op; simpl; simpl in H0; FuncInv; subst; simpl. + destruct op; cbn; cbn in H0; FuncInv; subst; cbn. (* move *) - congruence. (* intconst, longconst, floatconst, singleconst *) @@ -777,30 +777,30 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - apply type_add. (* addx, addximm *) - apply type_add. - - destruct v0; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. + - destruct v0; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. (* neg, sub *) - destruct v0... - apply type_sub. (* revsubimm, revsubx, revsubximm *) - destruct v0... - apply type_sub. - - destruct v0; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. + - destruct v0; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. (* mul, mulimm, mulhs, mulhu *) - destruct v0; destruct v1... - destruct v0... - destruct v0; destruct v1... - destruct v0; destruct v1... (* div, divu *) - - destruct v0; destruct v1; simpl in *; inv H0. - destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2... - - destruct v0; destruct v1; simpl in *; inv H0. + - destruct v0; destruct v1; cbn in *; inv H0. + destruct (_ || _); inv H2... + - destruct v0; destruct v1; cbn in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2... (* mod, modu *) - - destruct v0; destruct v1; simpl in *; inv H0. - destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2... - - destruct v0; destruct v1; simpl in *; inv H0. + - destruct v0; destruct v1; cbn in *; inv H0. + destruct (_ || _); inv H2... + - destruct v0; destruct v1; cbn in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2... (* and, andimm *) - destruct v0; destruct v1... @@ -829,18 +829,18 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; destruct v1... - destruct v0... (* shl, shlimm *) - - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... - - destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)... + - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int.iwordsize)... + - destruct v0; cbn... destruct (Int.ltu n Int.iwordsize)... (* shr, shrimm *) - - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... - - destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)... + - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int.iwordsize)... + - destruct v0; cbn... destruct (Int.ltu n Int.iwordsize)... (* shru, shruimm *) - - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... - - destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)... + - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int.iwordsize)... + - destruct v0; cbn... destruct (Int.ltu n Int.iwordsize)... (* shrx *) - - destruct v0; simpl... destruct (Int.ltu n (Int.repr 31)); simpl; trivial. + - destruct v0; cbn... destruct (Int.ltu n (Int.repr 31)); cbn; trivial. (* shrimm *) - - destruct v0; simpl... + - destruct v0; cbn... (* madd *) - apply type_add. - apply type_add. @@ -858,13 +858,13 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - apply type_addl. (* addxl addxlimm *) - apply type_addl. - - destruct v0; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. + - destruct v0; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. (* negl, subl *) - destruct v0... - apply type_subl. - - destruct v0; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. + - destruct v0; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. - destruct v0... - apply type_subl. (* mull, mullhs, mullhu *) @@ -873,14 +873,14 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; destruct v1... - destruct v0; destruct v1... (* divl, divlu *) - - destruct v0; destruct v1; simpl in *; inv H0. - destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2... - - destruct v0; destruct v1; simpl in *; inv H0. + - destruct v0; destruct v1; cbn in *; inv H0. + destruct (_ || _); inv H2... + - destruct v0; destruct v1; cbn in *; inv H0. destruct (Int64.eq i0 Int64.zero); inv H2... (* modl, modlu *) - - destruct v0; destruct v1; simpl in *; inv H0. - destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2... - - destruct v0; destruct v1; simpl in *; inv H0. + - destruct v0; destruct v1; cbn in *; inv H0. + destruct (_ || _); inv H2... + - destruct v0; destruct v1; cbn in *; inv H0. destruct (Int64.eq i0 Int64.zero); inv H2... (* andl, andlimm *) - destruct v0; destruct v1... @@ -909,16 +909,16 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; destruct v1... - destruct v0... (* shll, shllimm *) - - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')... - - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... + - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int64.iwordsize')... + - destruct v0; cbn... destruct (Int.ltu n Int64.iwordsize')... (* shr, shrimm *) - - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')... - - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... + - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int64.iwordsize')... + - destruct v0; cbn... destruct (Int.ltu n Int64.iwordsize')... (* shru, shruimm *) - - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')... - - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... + - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int64.iwordsize')... + - destruct v0; cbn... destruct (Int.ltu n Int64.iwordsize')... (* shrxl *) - - destruct v0; simpl... destruct (Int.ltu n (Int.repr 63)); simpl; trivial. + - destruct v0; cbn... destruct (Int.ltu n (Int.repr 63)); cbn; trivial. (* maddl, maddlim *) - apply type_addl. - apply type_addl. @@ -960,59 +960,59 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0... - destruct v0... (* intoffloat, intuoffloat *) - - destruct v0; simpl... destruct (Float.to_int f); simpl; trivial. - - destruct v0; simpl... destruct (Float.to_intu f); simpl; trivial. + - destruct v0; cbn... destruct (Float.to_int f); cbn; trivial. + - destruct v0; cbn... destruct (Float.to_intu f); cbn; trivial. (* intofsingle, intuofsingle *) - - destruct v0; simpl... destruct (Float32.to_int f); simpl; trivial. - - destruct v0; simpl... destruct (Float32.to_intu f); simpl; trivial. + - destruct v0; cbn... destruct (Float32.to_int f); cbn; trivial. + - destruct v0; cbn... destruct (Float32.to_intu f); cbn; trivial. (* singleofint, singleofintu *) - - destruct v0; simpl... - - destruct v0; simpl... + - destruct v0; cbn... + - destruct v0; cbn... (* longoffloat, longuoffloat *) - - destruct v0; simpl... destruct (Float.to_long f); simpl; trivial. - - destruct v0; simpl... destruct (Float.to_longu f); simpl; trivial. + - destruct v0; cbn... destruct (Float.to_long f); cbn; trivial. + - destruct v0; cbn... destruct (Float.to_longu f); cbn; trivial. (* floatoflong, floatoflongu *) - - destruct v0; simpl... - - destruct v0; simpl... + - destruct v0; cbn... + - destruct v0; cbn... (* longofsingle, longuofsingle *) - - destruct v0; simpl... destruct (Float32.to_long f); simpl; trivial. - - destruct v0; simpl... destruct (Float32.to_longu f); simpl; trivial. + - destruct v0; cbn... destruct (Float32.to_long f); cbn; trivial. + - destruct v0; cbn... destruct (Float32.to_longu f); cbn; trivial. (* singleoflong, singleoflongu *) - - destruct v0; simpl... - - destruct v0; simpl... + - destruct v0; cbn... + - destruct v0; cbn... (* cmp *) - destruct (eval_condition cond vl m)... destruct b... (* extfz *) - unfold extfz. destruct (is_bitfield _ _). - + destruct v0; simpl; trivial. + + destruct v0; cbn; trivial. + constructor. (* extfs *) - unfold extfs. destruct (is_bitfield _ _). - + destruct v0; simpl; trivial. + + destruct v0; cbn; trivial. + constructor. (* extfzl *) - unfold extfzl. destruct (is_bitfieldl _ _). - + destruct v0; simpl; trivial. + + destruct v0; cbn; trivial. + constructor. (* extfsl *) - unfold extfsl. destruct (is_bitfieldl _ _). - + destruct v0; simpl; trivial. + + destruct v0; cbn; trivial. + constructor. (* insf *) - unfold insf, bitfield_mask. destruct (is_bitfield _ _). - + destruct v0; destruct v1; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. + + destruct v0; destruct v1; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. + constructor. (* insf *) - unfold insfl, bitfield_mask. destruct (is_bitfieldl _ _). - + destruct v0; destruct v1; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. + + destruct v0; destruct v1; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. + constructor. (* Osel *) - unfold Val.select. destruct (eval_condition0 _ _ m). @@ -1047,7 +1047,7 @@ Lemma is_trapping_op_sound: eval_operation genv sp op vl m <> None. Proof. unfold args_of_operation. - destruct op; destruct eq_operation; intros; simpl in *; try congruence. + destruct op; destruct eq_operation; intros; cbn in *; try congruence. all: try (destruct vl as [ | vh1 vl1]; try discriminate). all: try (destruct vl1 as [ | vh2 vl2]; try discriminate). all: try (destruct vl2 as [ | vh3 vl3]; try discriminate). @@ -1101,7 +1101,7 @@ Lemma eval_negate_condition: forall cond vl m, eval_condition (negate_condition cond) vl m = option_map negb (eval_condition cond vl m). Proof. - intros. destruct cond; simpl. + intros. destruct cond; cbn. repeat (destruct vl; auto). apply Val.negate_cmp_bool. repeat (destruct vl; auto). apply Val.negate_cmpu_bool. repeat (destruct vl; auto). apply Val.negate_cmp_bool. @@ -1147,7 +1147,7 @@ Lemma eval_shift_stack_addressing: eval_addressing ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl = eval_addressing ge (Vptr sp (Ptrofs.repr delta)) addr vl. Proof. - intros. destruct addr; simpl; auto. destruct vl; auto. + intros. destruct addr; cbn; auto. destruct vl; auto. rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto. Qed. @@ -1156,7 +1156,7 @@ Lemma eval_shift_stack_operation: eval_operation ge (Vptr sp Ptrofs.zero) (shift_stack_operation delta op) vl m = eval_operation ge (Vptr sp (Ptrofs.repr delta)) op vl m. Proof. - intros. destruct op; simpl; auto. destruct vl; auto. + intros. destruct op; cbn; auto. destruct vl; auto. rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto. Qed. @@ -1183,12 +1183,12 @@ Proof. assert (A: forall x n, Val.offset_ptr x (Ptrofs.add n (Ptrofs.repr delta)) = Val.add (Val.offset_ptr x n) (Vint (Int.repr delta))). - { intros; destruct x; simpl; auto. rewrite H1. + { intros; destruct x; cbn; auto. rewrite H1. rewrite Ptrofs.add_assoc. f_equal; f_equal; f_equal. symmetry; auto with ptrofs. } - destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst. + destruct addr; cbn in H; inv H; cbn in *; FuncInv; subst. - rewrite A; auto. - unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. - simpl. rewrite H1. f_equal; f_equal; f_equal. symmetry; auto with ptrofs. + cbn. rewrite H1. f_equal; f_equal; f_equal. symmetry; auto with ptrofs. - rewrite A; auto. Qed. @@ -1223,17 +1223,17 @@ Lemma op_depends_on_memory_correct: op_depends_on_memory op = false -> eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. - intros until m2. destruct op; simpl; try congruence. - - destruct cond; simpl; try congruence; + intros until m2. destruct op; cbn; try congruence. + - destruct cond; cbn; try congruence; intros SF; auto; rewrite ? negb_false_iff in SF; unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. - - destruct c0; simpl; try congruence; + - destruct c0; cbn; try congruence; intros SF; auto; rewrite ? negb_false_iff in SF; unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. - - destruct c0; simpl; try congruence; + - destruct c0; cbn; try congruence; intros SF; auto; rewrite ? negb_false_iff in SF; unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. - - destruct c0; simpl; try congruence; + - destruct c0; cbn; try congruence; intros SF; auto; rewrite ? negb_false_iff in SF; unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. Qed. @@ -1348,19 +1348,19 @@ Lemma eval_condition_inj: eval_condition cond vl1 m1 = Some b -> eval_condition cond vl2 m2 = Some b. Proof. - intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. + intros. destruct cond; cbn in H0; FuncInv; InvInject; cbn; auto. +- inv H3; inv H2; cbn in H0; inv H0; auto. - eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. -- inv H3; simpl in H0; inv H0; auto. +- inv H3; cbn in H0; inv H0; auto. - eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. -- inv H3; inv H2; simpl in H0; inv H0; auto. +- inv H3; inv H2; cbn in H0; inv H0; auto. - eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. -- inv H3; simpl in H0; inv H0; auto. +- inv H3; cbn in H0; inv H0; auto. - eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. +- inv H3; inv H2; cbn in H0; inv H0; auto. +- inv H3; inv H2; cbn in H0; inv H0; auto. +- inv H3; inv H2; cbn in H0; inv H0; auto. +- inv H3; inv H2; cbn in H0; inv H0; auto. Qed. Lemma eval_condition0_inj: @@ -1369,10 +1369,10 @@ Lemma eval_condition0_inj: eval_condition0 cond v1 m1 = Some b -> eval_condition0 cond v2 m2 = Some b. Proof. - intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto. - - inv H; simpl in *; congruence. + intros. destruct cond; cbn in H0; FuncInv; InvInject; cbn; auto. + - inv H; cbn in *; congruence. - eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. - - inv H; simpl in *; congruence. + - inv H; cbn in *; congruence. - eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. Qed. @@ -1393,248 +1393,244 @@ Lemma eval_operation_inj: eval_operation ge1 sp1 op vl1 m1 = Some v1 -> exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ Val.inject f v1 v2. Proof. - intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + intros until v1; intros GL; intros. destruct op; cbn in H1; cbn; FuncInv; InvInject; TrivialExists. (* addrsymbol *) - - apply GL; simpl; auto. + - apply GL; cbn; auto. (* addrstack *) - apply Val.offset_ptr_inject; auto. (* castsigned *) - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* add, addimm *) - apply Val.add_inject; auto. - apply Val.add_inject; auto. (* addx, addximm *) - apply Val.add_inject; trivial. - inv H4; inv H2; simpl; try destruct (Int.ltu _ _); simpl; auto. - - inv H4; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. + inv H4; inv H2; cbn; try destruct (Int.ltu _ _); cbn; auto. + - inv H4; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. (* neg, sub *) - - inv H4; simpl; auto. + - inv H4; cbn; auto. - apply Val.sub_inject; auto. (* revsubimm, revsubx, revsubximm *) - - inv H4; simpl; trivial. + - inv H4; cbn; trivial. - apply Val.sub_inject; trivial. - inv H4; inv H2; simpl; try destruct (Int.ltu _ _); simpl; auto. - - inv H4; simpl; try destruct (Int.ltu _ _); simpl; auto. + inv H4; inv H2; cbn; try destruct (Int.ltu _ _); cbn; auto. + - inv H4; cbn; try destruct (Int.ltu _ _); cbn; auto. (* mul, mulimm, mulhs, mulhu *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. - - inv H4; inv H2; simpl; auto. - - inv H4; inv H2; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; inv H2; cbn; auto. (* div, divu *) - - inv H4; inv H3; simpl in H1; inv H1. simpl. - destruct (Int.eq i0 Int.zero - || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. + - inv H4; inv H3; cbn in H1; inv H1. cbn. + destruct (_ || _); inv H2. TrivialExists. - - inv H4; inv H3; simpl in H1; inv H1. simpl. + - inv H4; inv H3; cbn in H1; inv H1. cbn. destruct (Int.eq i0 Int.zero); inv H2. TrivialExists. (* mod, modu *) - - inv H4; inv H3; simpl in H1; inv H1. simpl. - destruct (Int.eq i0 Int.zero - || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. + - inv H4; inv H3; cbn in H1; inv H1. cbn. + destruct (_ || _); inv H2. TrivialExists. - - inv H4; inv H3; simpl in H1; inv H1. simpl. + - inv H4; inv H3; cbn in H1; inv H1. cbn. destruct (Int.eq i0 Int.zero); inv H2. TrivialExists. (* and, andimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* nand, nandimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* or, orimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* nor, norimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* xor, xorimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* nxor, nxorimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* not *) - - inv H4; simpl; auto. + - inv H4; cbn; auto. (* andn, andnimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* orn, ornimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* shl, shlimm *) - - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. - - inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto. + - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int.iwordsize); auto. + - inv H4; cbn; auto. destruct (Int.ltu n Int.iwordsize); auto. (* shr, shrimm *) - - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. - - inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto. + - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int.iwordsize); auto. + - inv H4; cbn; auto. destruct (Int.ltu n Int.iwordsize); auto. (* shru, shruimm *) - - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. - - inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto. + - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int.iwordsize); auto. + - inv H4; cbn; auto. destruct (Int.ltu n Int.iwordsize); auto. (* shrx *) - - inv H4; simpl; auto. - destruct (Int.ltu n (Int.repr 31)); inv H; simpl; auto. + - inv H4; cbn; auto. + destruct (Int.ltu n (Int.repr 31)); inv H; cbn; auto. (* rorimm *) - - inv H4; simpl; auto. + - inv H4; cbn; auto. (* madd, maddim *) - - inv H2; inv H3; inv H4; simpl; auto. - - inv H2; inv H4; simpl; auto. + - inv H2; inv H3; inv H4; cbn; auto. + - inv H2; inv H4; cbn; auto. (* msub *) - apply Val.sub_inject; auto. - inv H3; inv H2; simpl; auto. + inv H3; inv H2; cbn; auto. (* makelong, highlong, lowlong *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* cast32 *) - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* addl, addlimm *) - apply Val.addl_inject; auto. - apply Val.addl_inject; auto. (* addxl, addxlimm *) - apply Val.addl_inject; auto. - inv H4; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. - - inv H4; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. + inv H4; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. + - inv H4; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. (* negl, subl *) - - inv H4; simpl; auto. + - inv H4; cbn; auto. - apply Val.subl_inject; auto. - inv H4; inv H2; simpl; trivial; - destruct (Int.ltu _ _); simpl; trivial. - - inv H4; simpl; trivial; - destruct (Int.ltu _ _); simpl; trivial. - - inv H4; simpl; auto. + inv H4; inv H2; cbn; trivial; + destruct (Int.ltu _ _); cbn; trivial. + - inv H4; cbn; trivial; + destruct (Int.ltu _ _); cbn; trivial. + - inv H4; cbn; auto. - apply Val.subl_inject; auto. (* mull, mullhs, mullhu *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. - - inv H4; inv H2; simpl; auto. - - inv H4; inv H2; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; inv H2; cbn; auto. (* divl, divlu *) - - inv H4; inv H3; simpl in H1; inv H1. simpl. - destruct (Int64.eq i0 Int64.zero - || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2. + - inv H4; inv H3; cbn in H1; inv H1. cbn. + destruct (_ || _); inv H2. TrivialExists. - - inv H4; inv H3; simpl in H1; inv H1. simpl. + - inv H4; inv H3; cbn in H1; inv H1. cbn. destruct (Int64.eq i0 Int64.zero); inv H2. TrivialExists. (* modl, modlu *) - - inv H4; inv H3; simpl in H1; inv H1. simpl. - destruct (Int64.eq i0 Int64.zero - || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2. + - inv H4; inv H3; cbn in H1; inv H1. cbn. + destruct (_ || _); inv H2. TrivialExists. - - inv H4; inv H3; simpl in H1; inv H1. simpl. + - inv H4; inv H3; cbn in H1; inv H1. cbn. destruct (Int64.eq i0 Int64.zero); inv H2. TrivialExists. (* andl, andlimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* nandl, nandlimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* orl, orlimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* norl, norlimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* xorl, xorlimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* nxorl, nxorlimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* notl *) - - inv H4; simpl; auto. + - inv H4; cbn; auto. (* andnl, andnlimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* ornl, ornlimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* shll, shllimm *) - - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. - - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. + - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. + - inv H4; cbn; auto. destruct (Int.ltu n Int64.iwordsize'); auto. (* shr, shrimm *) - - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. - - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. + - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. + - inv H4; cbn; auto. destruct (Int.ltu n Int64.iwordsize'); auto. (* shru, shruimm *) - - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. - - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. + - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. + - inv H4; cbn; auto. destruct (Int.ltu n Int64.iwordsize'); auto. (* shrx *) - - inv H4; simpl; auto. - destruct (Int.ltu n (Int.repr 63)); simpl; auto. + - inv H4; cbn; auto. + destruct (Int.ltu n (Int.repr 63)); cbn; auto. (* maddl, maddlimm *) - apply Val.addl_inject; auto. - inv H2; inv H3; inv H4; simpl; auto. + inv H2; inv H3; inv H4; cbn; auto. - apply Val.addl_inject; auto. - inv H4; inv H2; simpl; auto. + inv H4; inv H2; cbn; auto. (* msubl, msublimm *) - apply Val.subl_inject; auto. - inv H2; inv H3; inv H4; simpl; auto. + inv H2; inv H3; inv H4; cbn; auto. (* negf, absf *) - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* addf, subf *) - - inv H4; inv H2; simpl; auto. - - inv H4; inv H2; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; inv H2; cbn; auto. (* mulf, divf *) - - inv H4; inv H2; simpl; auto. - - inv H4; inv H2; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; inv H2; cbn; auto. (* minf, maxf *) - - inv H4; inv H2; simpl; auto. - - inv H4; inv H2; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; inv H2; cbn; auto. (* fmaddf, fmsubf *) - - inv H4; inv H3; inv H2; simpl; auto. - - inv H4; inv H3; inv H2; simpl; auto. + - inv H4; inv H3; inv H2; cbn; auto. + - inv H4; inv H3; inv H2; cbn; auto. (* negfs, absfs *) - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* addfs, subfs *) - - inv H4; inv H2; simpl; auto. - - inv H4; inv H2; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; inv H2; cbn; auto. (* mulfs, divfs *) - - inv H4; inv H2; simpl; auto. - - inv H4; inv H2; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; inv H2; cbn; auto. (* minfs, maxfs *) - - inv H4; inv H2; simpl; auto. - - inv H4; inv H2; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; inv H2; cbn; auto. (* invfs *) - - inv H4; simpl; auto. + - inv H4; cbn; auto. (* fmaddfs, fmsubfs *) - - inv H4; inv H3; inv H2; simpl; auto. - - inv H4; inv H3; inv H2; simpl; auto. + - inv H4; inv H3; inv H2; cbn; auto. + - inv H4; inv H3; inv H2; cbn; auto. (* singleoffloat, floatofsingle *) - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* intoffloat, intuoffloat *) - - inv H4; simpl; auto. destruct (Float.to_int f0); simpl; auto. - - inv H4; simpl; auto. destruct (Float.to_intu f0); simpl; auto. + - inv H4; cbn; auto. destruct (Float.to_int f0); cbn; auto. + - inv H4; cbn; auto. destruct (Float.to_intu f0); cbn; auto. (* intofsingle, intuofsingle *) - - inv H4; simpl; auto. destruct (Float32.to_int f0); simpl; auto. - - inv H4; simpl; auto. destruct (Float32.to_intu f0); simpl; auto. + - inv H4; cbn; auto. destruct (Float32.to_int f0); cbn; auto. + - inv H4; cbn; auto. destruct (Float32.to_intu f0); cbn; auto. (* singleofint, singleofintu *) - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* longoffloat, longuoffloat *) - - inv H4; simpl; auto. destruct (Float.to_long f0); simpl; auto. - - inv H4; simpl; auto. destruct (Float.to_longu f0); simpl; auto. + - inv H4; cbn; auto. destruct (Float.to_long f0); cbn; auto. + - inv H4; cbn; auto. destruct (Float.to_longu f0); cbn; auto. (* floatoflong, floatoflongu *) - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* longofsingle, longuofsingle *) - - inv H4; simpl; auto. destruct (Float32.to_long f0); simpl; auto. - - inv H4; simpl; auto. destruct (Float32.to_longu f0); simpl; auto. + - inv H4; cbn; auto. destruct (Float32.to_long f0); cbn; auto. + - inv H4; cbn; auto. destruct (Float32.to_longu f0); cbn; auto. (* singleoflong, singleoflongu *) - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* cmp *) - subst v1. destruct (eval_condition cond vl1 m1) eqn:?. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. - destruct b; simpl; constructor. - simpl; constructor. + destruct b; cbn; constructor. + cbn; constructor. (* extfz *) - unfold extfz. @@ -1664,16 +1660,16 @@ Proof. - unfold insf. destruct (is_bitfield _ _). + inv H4; inv H2; trivial. - simpl. destruct (Int.ltu _ _); trivial. - simpl. trivial. + cbn. destruct (Int.ltu _ _); trivial. + cbn. trivial. + trivial. (* insfl *) - unfold insfl. destruct (is_bitfieldl _ _). + inv H4; inv H2; trivial. - simpl. destruct (Int.ltu _ _); trivial. - simpl. trivial. + cbn. destruct (Int.ltu _ _); trivial. + cbn. trivial. + trivial. (* Osel *) @@ -1711,13 +1707,13 @@ Lemma eval_addressing_inj: eval_addressing ge1 sp1 addr vl1 = Some v1 -> exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2. Proof. - intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists. + intros. destruct addr; cbn in H2; cbn; FuncInv; InvInject; TrivialExists. - apply Val.addl_inject; trivial. - destruct v0; destruct v'0; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial; inv H3. + destruct v0; destruct v'0; cbn; trivial; destruct (Int.ltu _ _); cbn; trivial; inv H3. apply Val.inject_long. - apply Val.addl_inject; auto. - apply Val.offset_ptr_inject; auto. - - apply H; simpl; auto. + - apply H; cbn; auto. - apply Val.offset_ptr_inject; auto. Qed. @@ -1732,7 +1728,7 @@ Lemma eval_addressing_inj_none: eval_addressing ge2 sp2 addr vl2 = None. Proof. intros until vl2. intros Hglobal Hinjsp Hinjvl. - destruct addr; simpl in *. + destruct addr; cbn in *. 1,2: inv Hinjvl; trivial; inv H0; trivial; inv H2; trivial; @@ -1856,7 +1852,7 @@ Lemma eval_addressing_lessdef_none: eval_addressing genv sp addr vl2 = None. Proof. intros until vl2. intros Hlessdef Heval1. - destruct addr; simpl in *. + destruct addr; cbn in *. 1, 2, 4, 5: inv Hlessdef; trivial; inv H0; trivial; inv H2; trivial; @@ -1941,7 +1937,7 @@ Lemma eval_operation_inject: /\ Val.inject f v1 v2. Proof. intros. - rewrite eval_shift_stack_operation. simpl. + rewrite eval_shift_stack_operation. cbn. eapply eval_operation_inj with (sp1 := Vptr sp1 Ptrofs.zero) (m1 := m1); eauto. intros; eapply Mem.valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. diff --git a/kvx/Peephole.v b/kvx/Peephole.v index 35f4bbd9..5adb823b 100644 --- a/kvx/Peephole.v +++ b/kvx/Peephole.v @@ -153,6 +153,6 @@ Program Definition optimize_bblock (bb : bblock) := exit := exit bb |}. Next Obligation. destruct (wf_bblockb (optimize_body (body bb))) eqn:Rwf. - - rewrite Rwf. simpl. trivial. + - rewrite Rwf. cbn. trivial. - exact (correct bb). Qed. diff --git a/kvx/Stacklayout.v b/kvx/Stacklayout.v index 46202e03..81ffcebb 100644 --- a/kvx/Stacklayout.v +++ b/kvx/Stacklayout.v @@ -63,7 +63,7 @@ Lemma frame_env_separated: ** P. Proof. Local Opaque Z.add Z.mul sepconj range. - intros; simpl. + intros; cbn. set (w := if Archi.ptr64 then 8 else 4). set (olink := align (4 * b.(bound_outgoing)) w). set (oretaddr := olink + w). @@ -105,7 +105,7 @@ Lemma frame_env_range: let fe := make_env b in 0 <= fe_stack_data fe /\ fe_stack_data fe + bound_stack_data b <= fe_size fe. Proof. - intros; simpl. + intros; cbn. set (w := if Archi.ptr64 then 8 else 4). set (olink := align (4 * b.(bound_outgoing)) w). set (oretaddr := olink + w). @@ -133,7 +133,7 @@ Lemma frame_env_aligned: /\ (align_chunk Mptr | fe_ofs_link fe) /\ (align_chunk Mptr | fe_ofs_retaddr fe). Proof. - intros; simpl. + intros; cbn. set (w := if Archi.ptr64 then 8 else 4). set (olink := align (4 * b.(bound_outgoing)) w). set (oretaddr := olink + w). diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v index e634fdc0..122c9a60 100644 --- a/kvx/ValueAOp.v +++ b/kvx/ValueAOp.v @@ -406,8 +406,8 @@ Lemma intoffloat_total_sound: vmatch bc (Val.maketotal (Val.intoffloat v)) (intoffloat_total x). Proof. unfold Val.intoffloat, intoffloat_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor]. + inv MATCH; cbn in *; try constructor. + all: destruct (Float.to_int f) as [i|] eqn:E; cbn; [auto with va | constructor]. unfold ntop1, provenance. destruct (va_strict tt); constructor. Qed. @@ -420,8 +420,8 @@ Lemma intuoffloat_total_sound: vmatch bc (Val.maketotal (Val.intuoffloat v)) (intuoffloat_total x). Proof. unfold Val.intoffloat, intoffloat_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor]. + inv MATCH; cbn in *; try constructor. + all: destruct (Float.to_intu f) as [i|] eqn:E; cbn; [auto with va | constructor]. unfold ntop1, provenance. destruct (va_strict tt); constructor. Qed. @@ -434,8 +434,8 @@ Lemma intofsingle_total_sound: vmatch bc (Val.maketotal (Val.intofsingle v)) (intofsingle_total x). Proof. unfold Val.intofsingle, intofsingle_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float32.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor]. + inv MATCH; cbn in *; try constructor. + all: destruct (Float32.to_int f) as [i|] eqn:E; cbn; [auto with va | constructor]. unfold ntop1, provenance. destruct (va_strict tt); constructor. Qed. @@ -448,8 +448,8 @@ Lemma intuofsingle_total_sound: vmatch bc (Val.maketotal (Val.intuofsingle v)) (intuofsingle_total x). Proof. unfold Val.intofsingle, intofsingle_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float32.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor]. + inv MATCH; cbn in *; try constructor. + all: destruct (Float32.to_intu f) as [i|] eqn:E; cbn; [auto with va | constructor]. unfold ntop1, provenance. destruct (va_strict tt); constructor. Qed. @@ -461,7 +461,7 @@ Lemma singleofint_total_sound: vmatch bc (Val.maketotal (Val.singleofint v)) (singleofint x). Proof. unfold Val.singleofint, singleofint; intros. - inv H; simpl. + inv H; cbn. all: auto with va. all: unfold ntop1, provenance. all: try constructor. @@ -474,7 +474,7 @@ Lemma singleofintu_total_sound: vmatch bc (Val.maketotal (Val.singleofintu v)) (singleofintu x). Proof. unfold Val.singleofintu, singleofintu; intros. - inv H; simpl. + inv H; cbn. all: auto with va. all: unfold ntop1, provenance. all: try constructor. @@ -488,8 +488,8 @@ Lemma longoffloat_total_sound: vmatch bc (Val.maketotal (Val.longoffloat v)) (longoffloat_total x). Proof. unfold Val.longoffloat, longoffloat_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor]. + inv MATCH; cbn in *; try constructor. + all: destruct (Float.to_long f) as [i|] eqn:E; cbn; [auto with va | constructor]. unfold ntop1, provenance. destruct (va_strict tt); constructor. Qed. @@ -502,8 +502,8 @@ Lemma longuoffloat_total_sound: vmatch bc (Val.maketotal (Val.longuoffloat v)) (longuoffloat_total x). Proof. unfold Val.longoffloat, longoffloat_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor]. + inv MATCH; cbn in *; try constructor. + all: destruct (Float.to_longu f) as [i|] eqn:E; cbn; [auto with va | constructor]. unfold ntop1, provenance. destruct (va_strict tt); constructor. Qed. @@ -516,8 +516,8 @@ Lemma longofsingle_total_sound: vmatch bc (Val.maketotal (Val.longofsingle v)) (longofsingle_total x). Proof. unfold Val.longofsingle, longofsingle_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float32.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor]. + inv MATCH; cbn in *; try constructor. + all: destruct (Float32.to_long f) as [i|] eqn:E; cbn; [auto with va | constructor]. unfold ntop1, provenance. destruct (va_strict tt); constructor. Qed. @@ -530,8 +530,8 @@ Lemma longuofsingle_total_sound: vmatch bc (Val.maketotal (Val.longuofsingle v)) (longuofsingle_total x). Proof. unfold Val.longofsingle, longofsingle_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float32.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor]. + inv MATCH; cbn in *; try constructor. + all: destruct (Float32.to_longu f) as [i|] eqn:E; cbn; [auto with va | constructor]. unfold ntop1, provenance. destruct (va_strict tt); constructor. Qed. @@ -543,7 +543,7 @@ Lemma singleoflong_total_sound: vmatch bc (Val.maketotal (Val.singleoflong v)) (singleoflong x). Proof. unfold Val.singleoflong, singleoflong; intros. - inv H; simpl. + inv H; cbn. all: auto with va. all: unfold ntop1, provenance. all: try constructor. @@ -556,7 +556,7 @@ Lemma singleoflongu_total_sound: vmatch bc (Val.maketotal (Val.singleoflongu v)) (singleoflongu x). Proof. unfold Val.singleoflongu, singleoflongu; intros. - inv H; simpl. + inv H; cbn. all: auto with va. all: unfold ntop1, provenance. all: try constructor. @@ -569,7 +569,7 @@ Lemma floatoflong_total_sound: vmatch bc (Val.maketotal (Val.floatoflong v)) (floatoflong x). Proof. unfold Val.floatoflong, floatoflong; intros. - inv H; simpl. + inv H; cbn. all: auto with va. all: unfold ntop1, provenance. all: try constructor. @@ -582,7 +582,7 @@ Lemma floatoflongu_total_sound: vmatch bc (Val.maketotal (Val.floatoflongu v)) (floatoflongu x). Proof. unfold Val.floatoflongu, floatoflongu; intros. - inv H; simpl. + inv H; cbn. all: auto with va. all: unfold ntop1, provenance. all: try constructor. @@ -620,7 +620,7 @@ Proof. intros v x; intro MATCH; inversion MATCH; - simpl; + cbn; constructor. Qed. @@ -632,9 +632,9 @@ Lemma triple_op_float_sound: Proof. intros until z. intros Hax Hby Hcz. - inv Hax; simpl; try constructor; - inv Hby; simpl; try constructor; - inv Hcz; simpl; try constructor. + inv Hax; cbn; try constructor; + inv Hby; cbn; try constructor; + inv Hcz; cbn; try constructor. Qed. Lemma triple_op_single_sound: @@ -645,9 +645,9 @@ Lemma triple_op_single_sound: Proof. intros until z. intros Hax Hby Hcz. - inv Hax; simpl; try constructor; - inv Hby; simpl; try constructor; - inv Hcz; simpl; try constructor. + inv Hax; cbn; try constructor; + inv Hby; cbn; try constructor; + inv Hcz; cbn; try constructor. Qed. Lemma fmaddf_sound : @@ -691,9 +691,9 @@ Proof. intros until aargs; intros VM. inv VM. destruct cond; auto with va. inv H0. - destruct cond; simpl; eauto with va. + destruct cond; cbn; eauto with va. inv H2. - destruct cond; simpl; eauto with va. + destruct cond; cbn; eauto with va. destruct cond; auto with va. Qed. @@ -703,7 +703,7 @@ Theorem eval_static_condition0_sound: cmatch (eval_condition0 cond varg m) (eval_static_condition0 cond aarg). Proof. intros until aarg; intro VM. - destruct cond; simpl; eauto with va. + destruct cond; cbn; eauto with va. Qed. Lemma symbol_address_sound: @@ -812,8 +812,8 @@ Proof. + eauto with va. + destruct n; destruct shift; reflexivity. - (* shrx *) - inv H1; simpl; try constructor. - all: destruct Int.ltu; [simpl | constructor; fail]. + inv H1; cbn; try constructor. + all: destruct Int.ltu; [cbn | constructor; fail]. all: auto with va. - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with | Vlong n2 => Vlong (Int64.add n n2) @@ -833,8 +833,8 @@ Proof. + eauto with va. + destruct a1; destruct shift; reflexivity. - (* shrxl *) - inv H1; simpl; try constructor. - all: destruct Int.ltu; [simpl | constructor; fail]. + inv H1; cbn; try constructor. + all: destruct Int.ltu; [cbn | constructor; fail]. all: auto with va. - apply of_optbool_sound. eapply eval_static_condition_sound; eauto. @@ -865,12 +865,12 @@ Proof. (* insf *) - unfold insf, eval_static_insf. destruct (is_bitfield _ _). - + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor. + + inv H1; inv H0; cbn; try constructor; destruct (Int.ltu _ _); cbn; constructor. + constructor. (* insfl *) - unfold insfl, eval_static_insfl. destruct (is_bitfieldl _ _). - + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor. + + inv H1; inv H0; cbn; try constructor; destruct (Int.ltu _ _); cbn; constructor. + constructor. (* select *) - apply select_sound; auto. eapply eval_static_condition0_sound; eauto. diff --git a/kvx/abstractbb/AbstractBasicBlocksDef.v b/kvx/abstractbb/AbstractBasicBlocksDef.v index 948ed660..6960f363 100644 --- a/kvx/abstractbb/AbstractBasicBlocksDef.v +++ b/kvx/abstractbb/AbstractBasicBlocksDef.v @@ -170,7 +170,7 @@ Lemma exp_equiv e old1 old2: (exp_eval e m1 old1) = (exp_eval e m2 old2). Proof. intros H1. - induction e using exp_mut with (P0:=fun l => forall m1 m2, (forall x, m1 x = m2 x) -> list_exp_eval l m1 old1 = list_exp_eval l m2 old2); simpl; try congruence; auto. + induction e using exp_mut with (P0:=fun l => forall m1 m2, (forall x, m1 x = m2 x) -> list_exp_eval l m1 old1 = list_exp_eval l m2 old2); cbn; try congruence; auto. - intros; erewrite IHe; eauto. - intros; erewrite IHe, IHe0; auto. Qed. @@ -183,38 +183,38 @@ Lemma inst_equiv_refl i old1 old2: forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (inst_run i m1 old1) (inst_run i m2 old2). Proof. - intro H; induction i as [ | [x e]]; simpl; eauto. + intro H; induction i as [ | [x e]]; cbn; eauto. intros m1 m2 H1. erewrite exp_equiv; eauto. - destruct (exp_eval e m2 old2); simpl; auto. + destruct (exp_eval e m2 old2); cbn; auto. apply IHi. unfold assign; intro y. destruct (R.eq_dec x y); auto. Qed. Lemma bblock_equiv_refl p: forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (run p m1) (run p m2). Proof. - induction p as [ | i p']; simpl; eauto. + induction p as [ | i p']; cbn; eauto. intros m1 m2 H; lapply (inst_equiv_refl i m1 m2); auto. intros X; lapply (X m1 m2); auto; clear X. - destruct (inst_run i m1 m1); simpl. - - intros [m3 [H1 H2]]; rewrite H1; simpl; auto. - - intros H1; rewrite H1; simpl; auto. + destruct (inst_run i m1 m1); cbn. + - intros [m3 [H1 H2]]; rewrite H1; cbn; auto. + - intros H1; rewrite H1; cbn; auto. Qed. Lemma res_eq_sym om1 om2: res_eq om1 om2 -> res_eq om2 om1. Proof. - destruct om1; simpl. - - intros [m2 [H1 H2]]; subst; simpl. eauto. - - intros; subst; simpl; eauto. + destruct om1; cbn. + - intros [m2 [H1 H2]]; subst; cbn. eauto. + - intros; subst; cbn; eauto. Qed. Lemma res_eq_trans (om1 om2 om3: option mem): (res_eq om1 om2) -> (res_eq om2 om3) -> (res_eq om1 om3). Proof. - destruct om1; simpl. - - intros [m2 [H1 H2]]; subst; simpl. - intros [m3 [H3 H4]]; subst; simpl. + destruct om1; cbn. + - intros [m2 [H1 H2]]; subst; cbn. + intros [m3 [H3 H4]]; subst; cbn. eapply ex_intro; intuition eauto. rewrite H2; auto. - - intro; subst; simpl; auto. + - intro; subst; cbn; auto. Qed. Lemma bblock_simu_alt p1 p2: bblock_simu p1 p2 <-> (forall m1 m2, (forall x, m1 x = m2 x) -> (run p1 m1)<>None -> res_eq (run p1 m1) (run p2 m2)). @@ -232,8 +232,8 @@ Lemma run_app p1: forall m1 p2, | None => None end. Proof. - induction p1; simpl; try congruence. - intros; destruct (inst_run _ _ _); simpl; auto. + induction p1; cbn; try congruence. + intros; destruct (inst_run _ _ _); cbn; auto. Qed. Lemma run_app_None p1 m1 p2: @@ -334,7 +334,7 @@ Fixpoint allvalid ge (l: list term) m : Prop := Lemma allvalid_extensionality ge (l: list term) m: allvalid ge l m <-> (forall t, List.In t l -> term_eval ge t m <> None). Proof. - induction l as [|t l]; simpl; try (tauto). + induction l as [|t l]; cbn; try (tauto). destruct l. - intuition (congruence || eauto). - rewrite IHl; clear IHl. intuition (congruence || eauto). @@ -365,7 +365,7 @@ Qed. Lemma intro_fail_correct (l: list term) (t: term) : (forall ge m, term_eval ge t m <> None <-> allvalid ge l m) -> match_pt t (intro_fail l t). Proof. - unfold match_pt; simpl; intros; intuition congruence. + unfold match_pt; cbn; intros; intuition congruence. Qed. Hint Resolve intro_fail_correct: wlp. @@ -374,7 +374,7 @@ Definition identity_fail (t: term):= intro_fail [t] t. Lemma identity_fail_correct (t: term): match_pt t (identity_fail t). Proof. - eapply intro_fail_correct; simpl; tauto. + eapply intro_fail_correct; cbn; tauto. Qed. Global Opaque identity_fail. Hint Resolve identity_fail_correct: wlp. @@ -390,11 +390,11 @@ Definition nofail (is_constant: op -> bool) (t: term):= Lemma nofail_correct (is_constant: op -> bool) t: (forall ge o, is_constant o = true -> op_eval ge o nil <> None) -> match_pt t (nofail is_constant t). Proof. - destruct t; simpl. - + intros; eapply intro_fail_correct; simpl; intuition congruence. - + intros; destruct l; simpl; auto with wlp. - destruct (is_constant o) eqn:Heqo; simpl; intuition eauto with wlp. - eapply intro_fail_correct; simpl; intuition eauto with wlp. + destruct t; cbn. + + intros; eapply intro_fail_correct; cbn; intuition congruence. + + intros; destruct l; cbn; auto with wlp. + destruct (is_constant o) eqn:Heqo; cbn; intuition eauto with wlp. + eapply intro_fail_correct; cbn; intuition eauto with wlp. Qed. Global Opaque nofail. Hint Resolve nofail_correct: wlp. @@ -425,7 +425,7 @@ Lemma app_fail_allvalid_correct l pt t1 t2: forall (V2: forall (ge : genv) (m : mem), term_eval ge t2 m <> None <-> allvalid ge (mayfail {| mayfail := t1 :: l; effect := t1 |}) m) (ge : genv) (m : mem), term_eval ge t2 m <> None <-> allvalid ge (mayfail (app_fail l pt)) m. Proof. - intros; generalize (V1 ge m) (V2 ge m); rewrite !allvalid_extensionality; simpl. clear V1 V2. + intros; generalize (V1 ge m) (V2 ge m); rewrite !allvalid_extensionality; cbn. clear V1 V2. intuition subst. + rewrite rev_append_rev, in_app_iff, <- in_rev in H3. destruct H3; eauto. + eapply H3; eauto. diff --git a/kvx/abstractbb/ImpSimuTest.v b/kvx/abstractbb/ImpSimuTest.v index 89260ddb..b1a3b985 100644 --- a/kvx/abstractbb/ImpSimuTest.v +++ b/kvx/abstractbb/ImpSimuTest.v @@ -160,13 +160,13 @@ Definition list_term_set_hid (l: list_term) (hid: hashcode): list_term := Lemma term_eval_set_hid ge t hid m: term_eval ge (term_set_hid t hid) m = term_eval ge t m. Proof. - destruct t; simpl; auto. + destruct t; cbn; auto. Qed. Lemma list_term_eval_set_hid ge l hid m: list_term_eval ge (list_term_set_hid l hid) m = list_term_eval ge l m. Proof. - destruct l; simpl; auto. + destruct l; cbn; auto. Qed. (* Local nickname *) @@ -315,7 +315,7 @@ Proof. destruct (DM0 m) as (PRE & VALID0); clear DM0. assert (VALID1: allvalid ge hd.(hpre) m -> pre d ge m). { unfold smem_valid in PRE; tauto. } assert (VALID2: allvalid ge hd.(hpre) m -> forall x : Dict.R.t, ST.term_eval ge (d x) m <> None). { unfold smem_valid in PRE; tauto. } - rewrite !allvalid_extensionality in * |- *; simpl. + rewrite !allvalid_extensionality in * |- *; cbn. intuition (subst; eauto). + eapply smem_valid_set_proof; eauto. erewrite <- EQT; eauto. @@ -323,11 +323,11 @@ Proof. intros X1; exploit smem_valid_set_decompose_2; eauto. rewrite <- EQT; eauto. + exploit smem_valid_set_decompose_1; eauto. - - clear DM0. unfold hsmem_post_eval, hsmem_post_eval in * |- *; simpl. + - clear DM0. unfold hsmem_post_eval, hsmem_post_eval in * |- *; cbn. Local Hint Resolve smem_valid_set_decompose_1: core. intros; case (R.eq_dec x x0). - + intros; subst; rewrite !Dict.set_spec_eq; simpl; eauto. - + intros; rewrite !Dict.set_spec_diff; simpl; eauto. + + intros; subst; rewrite !Dict.set_spec_eq; cbn; eauto. + + intros; rewrite !Dict.set_spec_diff; cbn; eauto. Qed. Local Hint Resolve naive_set_correct: core. @@ -404,10 +404,10 @@ Lemma hterm_append_correct l: forall lh, WHEN hterm_append l lh ~> lh' THEN (forall ge m, allvalid ge lh' m <-> (allvalid ge l m /\ allvalid ge lh m)). Proof. Local Hint Resolve eq_trans: localhint. - induction l as [|t l']; simpl; wlp_xsimplify ltac:(eauto with wlp). + induction l as [|t l']; cbn; wlp_xsimplify ltac:(eauto with wlp). - intros; rewrite! allvalid_extensionality; intuition eauto. - intros REC ge m; rewrite REC; clear IHl' REC. rewrite !allvalid_extensionality. - simpl; intuition (subst; eauto with wlp localhint). + cbn; intuition (subst; eauto with wlp localhint). Qed. (*Local Hint Resolve hterm_append_correct: wlp.*) Global Opaque hterm_append. @@ -431,8 +431,8 @@ Lemma smart_set_correct hd x ht: forall ge m y, hsmem_post_eval ge d y m = hsmem_post_eval ge (Dict.set hd x ht) y m. Proof. destruct ht; wlp_simplify. - unfold hsmem_post_eval; simpl. case (R.eq_dec x0 y). - - intros; subst. rewrite Dict.set_spec_eq, Dict.rem_spec_eq. simpl; congruence. + unfold hsmem_post_eval; cbn. case (R.eq_dec x0 y). + - intros; subst. rewrite Dict.set_spec_eq, Dict.rem_spec_eq. cbn; congruence. - intros; rewrite Dict.set_spec_diff, Dict.rem_spec_diff; auto. Qed. (*Local Hint Resolve smart_set_correct: wlp.*) @@ -456,17 +456,17 @@ Proof. generalize (hterm_append_correct _ _ _ Hexta0); intro APPEND. generalize (hterm_lift_correct _ _ Hexta1); intro LIFT. generalize (smart_set_correct _ _ _ _ Hexta3); intro SMART. - eapply equiv_hsmem_models; eauto; unfold equiv_hsmem; simpl. + eapply equiv_hsmem_models; eauto; unfold equiv_hsmem; cbn. destruct H as (VALID & EFFECT); split. - intros; rewrite APPEND, <- VALID. - rewrite !allvalid_extensionality in * |- *; simpl; intuition (subst; eauto). + rewrite !allvalid_extensionality in * |- *; cbn; intuition (subst; eauto). - intros m x0 ALLVALID; rewrite SMART. destruct (term_eval ge ht m) eqn: Hht. * case (R.eq_dec x x0). - + intros; subst. unfold hsmem_post_eval; simpl. rewrite !Dict.set_spec_eq. + + intros; subst. unfold hsmem_post_eval; cbn. rewrite !Dict.set_spec_eq. erewrite LIFT, EFFECT; eauto. - + intros; unfold hsmem_post_eval; simpl. rewrite !Dict.set_spec_diff; auto. - * rewrite allvalid_extensionality in ALLVALID; destruct (ALLVALID ht); simpl; auto. + + intros; unfold hsmem_post_eval; cbn. rewrite !Dict.set_spec_diff; auto. + * rewrite allvalid_extensionality in ALLVALID; destruct (ALLVALID ht); cbn; auto. Qed. Local Hint Resolve hsmem_set_correct: wlp. Global Opaque hsmem_set. @@ -481,7 +481,7 @@ Proof. intro H. induction e using exp_mut with (P0:=fun le => forall d hd, smem_model ge d hd -> forall m, smem_valid ge d m -> smem_valid ge od m -> list_term_eval ge (list_exp_term le hd hod) m = list_term_eval ge (list_exp_term le d od) m); - unfold smem_model in * |- * ; simpl; intuition eauto. + unfold smem_model in * |- * ; cbn; intuition eauto. - erewrite IHe; eauto. - erewrite IHe0, IHe; eauto. Qed. @@ -516,10 +516,10 @@ Lemma exp_hterm_correct_x ge e hod od: induction e using exp_mut with (P0:=fun le => forall d hd, smem_model ge d hd -> WHEN list_exp_hterm le hd hod ~> lt THEN forall m, smem_valid ge d m -> smem_valid ge od m -> list_term_eval ge lt m = ST.list_term_eval ge (list_exp_term le d od) m); - unfold smem_model, hsmem_post_eval in * |- * ; simpl; wlp_simplify. + unfold smem_model, hsmem_post_eval in * |- * ; cbn; wlp_simplify. - rewrite H1, <- H4; auto. - - rewrite H4, <- H0; simpl; auto. - - rewrite H5, <- H0, <- H4; simpl; auto. + - rewrite H4, <- H0; cbn; auto. + - rewrite H5, <- H0, <- H4; cbn; auto. Qed. Global Opaque exp_hterm. @@ -544,7 +544,7 @@ Lemma hinst_smem_correct i: forall hd hod, forall ge od d, smem_model ge od hod -> smem_model ge d hd -> (forall m, smem_valid ge d m -> smem_valid ge od m) -> smem_model ge (inst_smem i d od) hd'. Proof. Local Hint Resolve smem_valid_set_proof: core. - induction i; simpl; wlp_simplify; eauto 15 with wlp. + induction i; cbn; wlp_simplify; eauto 15 with wlp. Qed. Global Opaque hinst_smem. Local Hint Resolve hinst_smem_correct: wlp. @@ -564,7 +564,7 @@ Fixpoint bblock_hsmem_rec (p: bblock) (d: hsmem): ?? hsmem := Lemma bblock_hsmem_rec_correct p: forall hd, WHEN bblock_hsmem_rec p hd ~> hd' THEN forall ge d, smem_model ge d hd -> smem_model ge (bblock_smem_rec p d) hd'. Proof. - induction p; simpl; wlp_simplify. + induction p; cbn; wlp_simplify. Qed. Global Opaque bblock_hsmem_rec. Local Hint Resolve bblock_hsmem_rec_correct: wlp. @@ -573,8 +573,8 @@ Definition hsmem_empty: hsmem := {| hpre:= nil ; hpost := Dict.empty |}. Lemma hsmem_empty_correct ge: smem_model ge smem_empty hsmem_empty. Proof. - unfold smem_model, smem_valid, hsmem_post_eval; simpl; intuition try congruence. - rewrite !Dict.empty_spec; simpl; auto. + unfold smem_model, smem_valid, hsmem_post_eval; cbn; intuition try congruence. + rewrite !Dict.empty_spec; cbn; auto. Qed. Definition bblock_hsmem: bblock -> ?? hsmem @@ -722,7 +722,7 @@ Theorem g_bblock_simu_test_correct p1 p2: WHEN g_bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2. Proof. wlp_simplify. - destruct exta0; simpl in * |- *; auto. + destruct exta0; cbn in * |- *; auto. Qed. Global Opaque g_bblock_simu_test. @@ -1209,8 +1209,8 @@ Lemma eq_test_correct A d1: forall (d2: t A), WHEN eq_test d1 d2 ~> b THEN b=true -> forall x, get d1 x = get d2 x. Proof. - unfold get; induction d1 as [|l1 Hl1 [x1|] r1 Hr1]; destruct d2 as [|l2 [x2|] r2]; simpl; - wlp_simplify; (discriminate || (subst; destruct x; simpl; auto)). + unfold get; induction d1 as [|l1 Hl1 [x1|] r1 Hr1]; destruct d2 as [|l2 [x2|] r2]; cbn; + wlp_simplify; (discriminate || (subst; destruct x; cbn; auto)). Qed. Global Opaque eq_test. diff --git a/kvx/abstractbb/Parallelizability.v b/kvx/abstractbb/Parallelizability.v index 79ec9038..e5d21434 100644 --- a/kvx/abstractbb/Parallelizability.v +++ b/kvx/abstractbb/Parallelizability.v @@ -50,8 +50,8 @@ Fixpoint inst_prun (i: inst) (m tmp old: mem): option mem := Lemma inst_run_prun i: forall m old, inst_run ge i m old = inst_prun i m m old. Proof. - induction i as [|[y e] i']; simpl; auto. - intros m old; destruct (exp_eval ge e m old); simpl; auto. + induction i as [|[y e] i']; cbn; auto. + intros m old; destruct (exp_eval ge e m old); cbn; auto. Qed. @@ -76,8 +76,8 @@ Lemma inst_prun_equiv i old: forall m1 m2 tmp, (forall x, m1 x = m2 x) -> res_eq (inst_prun i m1 tmp old) (inst_prun i m2 tmp old). Proof. - induction i as [|[x e] i']; simpl; eauto. - intros m1 m2 tmp H; destruct (exp_eval ge e tmp old); simpl; auto. + induction i as [|[x e] i']; cbn; eauto. + intros m1 m2 tmp H; destruct (exp_eval ge e tmp old); cbn; auto. eapply IHi'; unfold assign. intros; destruct (R.eq_dec x x0); auto. Qed. @@ -85,12 +85,12 @@ Lemma prun_iw_equiv p: forall m1 m2 old, (forall x, m1 x = m2 x) -> res_eq (prun_iw p m1 old) (prun_iw p m2 old). Proof. - induction p as [|i p']; simpl; eauto. + induction p as [|i p']; cbn; eauto. - intros m1 m2 old H. generalize (inst_prun_equiv i old m1 m2 old H); - destruct (inst_prun i m1 old old); simpl. - + intros (m3 & H3 & H4); rewrite H3; simpl; eauto. - + intros H1; rewrite H1; simpl; auto. + destruct (inst_prun i m1 old old); cbn. + + intros (m3 & H3 & H4); rewrite H3; cbn; eauto. + + intros H1; rewrite H1; cbn; auto. Qed. @@ -101,8 +101,8 @@ Lemma prun_iw_app p1: forall m1 old p2, | None => None end. Proof. - induction p1; simpl; try congruence. - intros; destruct (inst_prun _ _ _); simpl; auto. + induction p1; cbn; try congruence. + intros; destruct (inst_prun _ _ _); cbn; auto. Qed. Lemma prun_iw_app_None p1: forall m1 old p2, @@ -132,12 +132,12 @@ Fixpoint notIn {A} (x: A) (l:list A): Prop := Lemma notIn_iff A (x:A) l: (~List.In x l) <-> notIn x l. Proof. - induction l; simpl; intuition. + induction l; cbn; intuition. Qed. Lemma notIn_app A (x:A) l1: forall l2, notIn x (l1++l2) <-> (notIn x l1 /\ notIn x l2). Proof. - induction l1; simpl. + induction l1; cbn. - intuition. - intros; rewrite IHl1. intuition. Qed. @@ -145,7 +145,7 @@ Qed. Lemma In_Permutation A (l1 l2: list A): Permutation l1 l2 -> forall x, In x l1 -> In x l2. Proof. - induction 1; simpl; intuition. + induction 1; cbn; intuition. Qed. Lemma Permutation_incl A (l1 l2: list A): Permutation l1 l2 -> incl l1 l2. @@ -174,7 +174,7 @@ Qed. Lemma disjoint_cons_l A (x:A) (l1 l2: list A): disjoint (x::l1) l2 <-> (notIn x l2) /\ (disjoint l1 l2). Proof. - unfold disjoint. simpl; intuition subst; auto. + unfold disjoint. cbn; intuition subst; auto. Qed. Lemma disjoint_cons_r A (x:A) (l1 l2: list A): disjoint l1 (x::l2) <-> (notIn x l1) /\ (disjoint l1 l2). @@ -230,13 +230,13 @@ Fixpoint frame_assign m1 (f: list R.t) m2 := Lemma frame_assign_def f: forall m1 m2 x, frame_assign m1 f m2 x = if notIn_dec x f then m1 x else m2 x. Proof. - induction f as [|y f] ; simpl; auto. - - intros; destruct (notIn_dec x []); simpl in *; tauto. - - intros; rewrite IHf; destruct (notIn_dec x (y::f)); simpl in *. - + destruct (notIn_dec x f); simpl in *; intuition. + induction f as [|y f] ; cbn; auto. + - intros; destruct (notIn_dec x []); cbn in *; tauto. + - intros; rewrite IHf; destruct (notIn_dec x (y::f)); cbn in *. + + destruct (notIn_dec x f); cbn in *; intuition. rewrite assign_diff; auto. rewrite <- notIn_iff in *; intuition. - + destruct (notIn_dec x f); simpl in *; intuition subst. + + destruct (notIn_dec x f); cbn in *; intuition subst. rewrite assign_eq; auto. rewrite <- notIn_iff in *; intuition. Qed. @@ -266,7 +266,7 @@ Lemma frame_eq_list_split f1 (f2: R.t -> Prop) om1 om2: (forall m1 m2 x, om1 = Some m1 -> om2 = Some m2 -> f2 x -> notIn x f1 -> m1 x = m2 x) -> frame_eq f2 om1 om2. Proof. - unfold frame_eq; destruct om1 as [ m1 | ]; simpl; auto. + unfold frame_eq; destruct om1 as [ m1 | ]; cbn; auto. intros (m2 & H0 & H1); subst. intros H. eexists; intuition eauto. @@ -280,7 +280,7 @@ Lemma frame_eq_res_eq f om1 om2: res_eq om1 om2. Proof. intros H H0; lapply (frame_eq_list_split f (fun _ => True) om1 om2 H); eauto. - clear H H0; unfold frame_eq, res_eq. destruct om1; simpl; firstorder. + clear H H0; unfold frame_eq, res_eq. destruct om1; cbn; firstorder. Qed. *) @@ -296,9 +296,9 @@ Lemma inst_wframe_correct i m' old: forall m tmp, inst_prun ge i m tmp old = Some m' -> forall x, notIn x (inst_wframe i) -> m' x = m x. Proof. - induction i as [|[y e] i']; simpl. + induction i as [|[y e] i']; cbn. - intros m tmp H x H0; inversion_clear H; auto. - - intros m tmp H x (H1 & H2); destruct (exp_eval ge e tmp old); simpl; try congruence. + - intros m tmp H x (H1 & H2); destruct (exp_eval ge e tmp old); cbn; try congruence. cutrewrite (m x = assign m y v x); eauto. rewrite assign_diff; auto. Qed. @@ -306,9 +306,9 @@ Qed. Lemma inst_prun_fequiv i old: forall m1 m2 tmp, frame_eq (fun x => In x (inst_wframe i)) (inst_prun ge i m1 tmp old) (inst_prun ge i m2 tmp old). Proof. - induction i as [|[y e] i']; simpl. + induction i as [|[y e] i']; cbn. - intros m1 m2 tmp; eexists; intuition eauto. - - intros m1 m2 tmp. destruct (exp_eval ge e tmp old); simpl; auto. + - intros m1 m2 tmp. destruct (exp_eval ge e tmp old); cbn; auto. eapply frame_eq_list_split; eauto. clear IHi'. intros m1' m2' x H1 H2. lapply (inst_wframe_correct i' m1' old (assign m1 y v) (assign tmp y v)); eauto. @@ -323,7 +323,7 @@ Lemma inst_prun_None i m1 m2 tmp old: inst_prun ge i m2 tmp old = None. Proof. intros H; generalize (inst_prun_fequiv i old m1 m2 tmp). - rewrite H; simpl; auto. + rewrite H; cbn; auto. Qed. Lemma inst_prun_Some i m1 m2 tmp old m1': @@ -331,7 +331,7 @@ Lemma inst_prun_Some i m1 m2 tmp old m1': res_eq (Some (frame_assign m2 (inst_wframe i) m1')) (inst_prun ge i m2 tmp old). Proof. intros H; generalize (inst_prun_fequiv i old m1 m2 tmp). - rewrite H; simpl. + rewrite H; cbn. intros (m2' & H1 & H2). eexists; intuition eauto. rewrite frame_assign_def. @@ -351,7 +351,7 @@ Local Hint Resolve Permutation_app_head Permutation_app_tail Permutation_app_com Lemma bblock_wframe_Permutation p p': Permutation p p' -> Permutation (bblock_wframe p) (bblock_wframe p'). Proof. - induction 1 as [|i p p'|i1 i2 p|p1 p2 p3]; simpl; auto. + induction 1 as [|i p p'|i1 i2 p|p1 p2 p3]; cbn; auto. - rewrite! app_assoc; auto. - eapply Permutation_trans; eauto. Qed. @@ -361,11 +361,11 @@ Lemma bblock_wframe_correct p m' old: forall m, prun_iw p m old = Some m' -> forall x, notIn x (bblock_wframe p) -> m' x = m x. Proof. - induction p as [|i p']; simpl. + induction p as [|i p']; cbn. - intros m H; inversion_clear H; auto. - intros m H x; rewrite notIn_app; intros (H1 & H2). remember (inst_prun i m old old) as om. - destruct om as [m1|]; simpl. + destruct om as [m1|]; cbn. + eapply eq_trans. eapply IHp'; eauto. eapply inst_wframe_correct; eauto. @@ -375,12 +375,12 @@ Qed. Lemma prun_iw_fequiv p old: forall m1 m2, frame_eq (fun x => In x (bblock_wframe p)) (prun_iw p m1 old) (prun_iw p m2 old). Proof. - induction p as [|i p']; simpl. + induction p as [|i p']; cbn. - intros m1 m2; eexists; intuition eauto. - intros m1 m2; generalize (inst_prun_fequiv i old m1 m2 old). remember (inst_prun i m1 old old) as om. - destruct om as [m1'|]; simpl. - + intros (m2' & H1 & H2). rewrite H1; simpl. + destruct om as [m1'|]; cbn. + + intros (m2' & H1 & H2). rewrite H1; cbn. eapply frame_eq_list_split; eauto. clear IHp'. intros m1'' m2'' x H3 H4. rewrite in_app_iff. intros X X2. assert (X1: In x (inst_wframe i)). { destruct X; auto. rewrite <- notIn_iff in X2; tauto. } @@ -389,7 +389,7 @@ Proof. lapply (bblock_wframe_correct p' m2'' old m2'); eauto. intros Xm2' Xm1'. rewrite Xm1', Xm2'; auto. - + intro H; rewrite H; simpl; auto. + + intro H; rewrite H; cbn; auto. Qed. Lemma prun_iw_equiv p m1 m2 old: @@ -418,7 +418,7 @@ Fixpoint is_det (p: bblock): Prop := Lemma is_det_Permutation p p': Permutation p p' -> is_det p -> is_det p'. Proof. - induction 1; simpl; auto. + induction 1; cbn; auto. - intros; intuition. eapply disjoint_incl_r. 2: eauto. eapply Permutation_incl. eapply Permutation_sym. eapply bblock_wframe_Permutation; auto. @@ -431,20 +431,20 @@ Theorem is_det_correct p p': is_det p -> forall m old, res_eq (prun_iw ge p m old) (prun_iw ge p' m old). Proof. - induction 1 as [ | i p p' | i1 i2 p | p1 p2 p3 ]; simpl; eauto. + induction 1 as [ | i p p' | i1 i2 p | p1 p2 p3 ]; cbn; eauto. - intros [H0 H1] m old. remember (inst_prun ge i m old old) as om0. - destruct om0 as [ m0 | ]; simpl; auto. + destruct om0 as [ m0 | ]; cbn; auto. - rewrite disjoint_app_r. intros ([Z1 Z2] & Z3 & Z4) m old. remember (inst_prun ge i2 m old old) as om2. - destruct om2 as [ m2 | ]; simpl; auto. + destruct om2 as [ m2 | ]; cbn; auto. + remember (inst_prun ge i1 m old old) as om1. - destruct om1 as [ m1 | ]; simpl; auto. - * lapply (inst_prun_Some i2 m m1 old old m2); simpl; auto. - lapply (inst_prun_Some i1 m m2 old old m1); simpl; auto. + destruct om1 as [ m1 | ]; cbn; auto. + * lapply (inst_prun_Some i2 m m1 old old m2); cbn; auto. + lapply (inst_prun_Some i1 m m2 old old m1); cbn; auto. intros (m1' & Hm1' & Xm1') (m2' & Hm2' & Xm2'). - rewrite Hm1', Hm2'; simpl. + rewrite Hm1', Hm2'; cbn. eapply prun_iw_equiv. intros x; rewrite <- Xm1', <- Xm2'. clear Xm2' Xm1' Hm1' Hm2' m1' m2'. rewrite frame_assign_def. @@ -455,9 +455,9 @@ Proof. erewrite (inst_wframe_correct i1 m1 old m old); eauto. } rewrite frame_assign_notIn; auto. - * erewrite inst_prun_None; eauto. simpl; auto. + * erewrite inst_prun_None; eauto. cbn; auto. + remember (inst_prun ge i1 m old old) as om1. - destruct om1 as [ m1 | ]; simpl; auto. + destruct om1 as [ m1 | ]; cbn; auto. erewrite inst_prun_None; eauto. - intros; eapply res_eq_trans. eapply IHPermutation1; eauto. @@ -486,7 +486,7 @@ Lemma exp_frame_correct e old1 old2: (exp_eval ge e m1 old1)=(exp_eval ge e m2 old2). Proof. induction e using exp_mut with (P0:=fun l => (forall x, In x (list_exp_frame l) -> old1 x = old2 x) -> forall m1 m2, (forall x, In x (list_exp_frame l) -> m1 x = m2 x) -> - (list_exp_eval ge l m1 old1)=(list_exp_eval ge l m2 old2)); simpl; auto. + (list_exp_eval ge l m1 old1)=(list_exp_eval ge l m2 old2)); cbn; auto. - intros H1 m1 m2 H2; rewrite H2; auto. - intros H1 m1 m2 H2; erewrite IHe; eauto. - intros H1 m1 m2 H2; erewrite IHe, IHe0; eauto; @@ -501,7 +501,7 @@ Fixpoint inst_frame (i: inst): list R.t := Lemma inst_wframe_frame i x: In x (inst_wframe i) -> In x (inst_frame i). Proof. - induction i as [ | [y e] i']; simpl; intuition. + induction i as [ | [y e] i']; cbn; intuition. Qed. @@ -511,13 +511,13 @@ Lemma inst_frame_correct i wframe old1 old2: forall m tmp1 tmp2, (forall x, notIn x wframe -> tmp1 x = tmp2 x) -> inst_prun ge i m tmp1 old1 = inst_prun ge i m tmp2 old2. Proof. - induction i as [|[x e] i']; simpl; auto. + induction i as [|[x e] i']; cbn; auto. intros m tmp1 tmp2; rewrite disjoint_cons_l, disjoint_app_l. intros (H1 & H2 & H3) H6 H7. cutrewrite (exp_eval ge e tmp1 old1 = exp_eval ge e tmp2 old2). - destruct (exp_eval ge e tmp2 old2); auto. eapply IHi'; eauto. - simpl; intros x0 H0; unfold assign. destruct (R.eq_dec x x0); simpl; auto. + cbn; intros x0 H0; unfold assign. destruct (R.eq_dec x x0); cbn; auto. - unfold disjoint in H2; apply exp_frame_correct. intros;apply H6; auto. intros;apply H7; auto. @@ -535,8 +535,8 @@ Fixpoint pararec (p: bblock) (wframe: list R.t): Prop := Lemma pararec_disjoint (p: bblock): forall wframe, pararec p wframe -> disjoint (bblock_wframe p) wframe. Proof. - induction p as [|i p']; simpl. - - unfold disjoint; simpl; intuition. + induction p as [|i p']; cbn. + - unfold disjoint; cbn; intuition. - intros wframe [H0 H1]; rewrite disjoint_app_l. generalize (IHp' _ H1). rewrite disjoint_app_r. intuition. @@ -546,7 +546,7 @@ Qed. Lemma pararec_det p: forall wframe, pararec p wframe -> is_det p. Proof. - induction p as [|i p']; simpl; auto. + induction p as [|i p']; cbn; auto. intros wframe [H0 H1]. generalize (pararec_disjoint _ _ H1). rewrite disjoint_app_r. intuition. - apply disjoint_sym; auto. @@ -558,7 +558,7 @@ Lemma pararec_correct p old: forall wframe m, (forall x, notIn x wframe -> m x = old x) -> run ge p m = prun_iw ge p m old. Proof. - elim p; clear p; simpl; auto. + elim p; clear p; cbn; auto. intros i p' X wframe m [H H0] H1. erewrite inst_run_prun, inst_frame_correct; eauto. remember (inst_prun ge i m old old) as om0. @@ -646,7 +646,7 @@ Fixpoint inst_wsframe(i:inst): S.t := Lemma inst_wsframe_correct i: S.match_frame (inst_wsframe i) (inst_wframe i). Proof. - induction i; simpl; auto. + induction i; cbn; auto. Qed. Fixpoint exp_sframe (e: exp): S.t := @@ -664,7 +664,7 @@ with list_exp_sframe (le: list_exp): S.t := Lemma exp_sframe_correct e: S.match_frame (exp_sframe e) (exp_frame e). Proof. - induction e using exp_mut with (P0:=fun l => S.match_frame (list_exp_sframe l) (list_exp_frame l)); simpl; auto. + induction e using exp_mut with (P0:=fun l => S.match_frame (list_exp_sframe l) (list_exp_frame l)); cbn; auto. Qed. Fixpoint inst_sframe (i: inst): S.t := @@ -677,7 +677,7 @@ Local Hint Resolve exp_sframe_correct: core. Lemma inst_sframe_correct i: S.match_frame (inst_sframe i) (inst_frame i). Proof. - induction i as [|[y e] i']; simpl; auto. + induction i as [|[y e] i']; cbn; auto. Qed. Local Hint Resolve inst_wsframe_correct inst_sframe_correct: core. @@ -692,7 +692,7 @@ Fixpoint is_pararec (p: bblock) (wsframe: S.t): bool := Lemma is_pararec_correct (p: bblock): forall s l, S.match_frame s l -> (is_pararec p s)=true -> (pararec p l). Proof. - induction p; simpl; auto. + induction p; cbn; auto. intros s l H1 H2; rewrite lazy_andb_bool_true in H2. destruct H2 as [H2 H3]. constructor 1; eauto. Qed. @@ -739,14 +739,14 @@ Definition empty:=PositiveSet.empty. Lemma empty_match_frame: match_frame empty nil. Proof. - unfold match_frame, empty, PositiveSet.In; simpl; intuition. + unfold match_frame, empty, PositiveSet.In; cbn; intuition. Qed. Definition add: R.t -> t -> t := PositiveSet.add. Lemma add_match_frame: forall s x l, match_frame s l -> match_frame (add x s) (x::l). Proof. - unfold match_frame, add; simpl. + unfold match_frame, add; cbn. intros s x l H y. rewrite PositiveSet.add_spec, H. intuition. Qed. @@ -772,13 +772,13 @@ Fixpoint is_disjoint (s s': PositiveSet.t) : bool := Lemma is_disjoint_spec_true s: forall s', is_disjoint s s' = true -> forall x, PositiveSet.In x s -> PositiveSet.In x s' -> False. Proof. - unfold PositiveSet.In; induction s as [ |l IHl o r IHr]; simpl; try discriminate. - destruct s' as [|l' o' r']; simpl; try discriminate. + unfold PositiveSet.In; induction s as [ |l IHl o r IHr]; cbn; try discriminate. + destruct s' as [|l' o' r']; cbn; try discriminate. intros X. assert (H: ~(o = true /\ o'=true) /\ is_disjoint l l' = true /\ is_disjoint r r'=true). - { destruct o, o', (is_disjoint l l'), (is_disjoint r r'); simpl in X; intuition. } + { destruct o, o', (is_disjoint l l'), (is_disjoint r r'); cbn in X; intuition. } clear X; destruct H as (H & H1 & H2). - destruct x as [i|i|]; simpl; eauto. + destruct x as [i|i|]; cbn; eauto. Qed. Lemma is_disjoint_match_frame: forall s1 s2 l1 l2, match_frame s1 l1 -> match_frame s2 l2 -> (is_disjoint s1 s2)=true -> disjoint l1 l2. diff --git a/kvx/abstractbb/SeqSimuTheory.v b/kvx/abstractbb/SeqSimuTheory.v index a957c50a..df6b9963 100644 --- a/kvx/abstractbb/SeqSimuTheory.v +++ b/kvx/abstractbb/SeqSimuTheory.v @@ -92,13 +92,13 @@ Variable ge: genv. Lemma set_spec_eq d x t m: term_eval ge (smem_set d x t x) m = term_eval ge t m. Proof. - unfold smem_set; simpl; case (R.eq_dec x x); try congruence. + unfold smem_set; cbn; case (R.eq_dec x x); try congruence. Qed. Lemma set_spec_diff d x y t m: x <> y -> term_eval ge (smem_set d x t y) m = term_eval ge (d y) m. Proof. - unfold smem_set; simpl; case (R.eq_dec x y); try congruence. + unfold smem_set; cbn; case (R.eq_dec x y); try congruence. Qed. Fixpoint inst_smem (i: inst) (d old: smem): smem := @@ -123,15 +123,15 @@ Definition bblock_smem: bblock -> smem Lemma inst_smem_pre_monotonic i old: forall d m, (pre (inst_smem i d old) ge m) -> (pre d ge m). Proof. - induction i as [|[y e] i IHi]; simpl; auto. + induction i as [|[y e] i IHi]; cbn; auto. intros d a H; generalize (IHi _ _ H); clear H IHi. - unfold smem_set; simpl; intuition. + unfold smem_set; cbn; intuition. Qed. Lemma bblock_smem_pre_monotonic p: forall d m, (pre (bblock_smem_rec p d) ge m) -> (pre d ge m). Proof. - induction p as [|i p' IHp']; simpl; eauto. + induction p as [|i p' IHp']; cbn; eauto. intros d a H; eapply inst_smem_pre_monotonic; eauto. Qed. @@ -146,7 +146,7 @@ Proof. intro H. induction e using exp_mut with (P0:=fun l => forall (d:smem) m1, (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> list_term_eval ge (list_exp_term l d od) m0 = list_exp_eval ge l m1 old); - simpl; auto. + cbn; auto. - intros; erewrite IHe; eauto. - intros. erewrite IHe, IHe0; eauto. Qed. @@ -156,12 +156,12 @@ Lemma inst_smem_abort i m0 x old: forall (d:smem), term_eval ge (d x) m0 = None -> term_eval ge (inst_smem i d old x) m0 = None. Proof. - induction i as [|[y e] i IHi]; simpl; auto. + induction i as [|[y e] i IHi]; cbn; auto. intros d VALID H; erewrite IHi; eauto. clear IHi. - unfold smem_set; simpl; destruct (R.eq_dec y x); auto. + unfold smem_set; cbn; destruct (R.eq_dec y x); auto. subst; generalize (inst_smem_pre_monotonic _ _ _ _ VALID); clear VALID. - unfold smem_set; simpl. intuition congruence. + unfold smem_set; cbn. intuition congruence. Qed. Lemma block_smem_rec_abort p m0 x: forall d, @@ -169,7 +169,7 @@ Lemma block_smem_rec_abort p m0 x: forall d, term_eval ge (d x) m0 = None -> term_eval ge (bblock_smem_rec p d x) m0 = None. Proof. - induction p; simpl; auto. + induction p; cbn; auto. intros d VALID H; erewrite IHp; eauto. clear IHp. eapply inst_smem_abort; eauto. Qed. @@ -181,13 +181,13 @@ Lemma inst_smem_Some_correct1 i m0 old (od:smem): (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> forall x, term_eval ge (inst_smem i d od x) m0 = Some (m2 x). Proof. - intro X; induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H. + intro X; induction i as [|[x e] i IHi]; cbn; intros m1 m2 d H. - inversion_clear H; eauto. - intros H0 x0. destruct (exp_eval ge e m1 old) eqn:Heqov; try congruence. refine (IHi _ _ _ _ _ _); eauto. clear x0; intros x0. - unfold assign, smem_set; simpl. destruct (R.eq_dec x x0); auto. + unfold assign, smem_set; cbn. destruct (R.eq_dec x x0); auto. subst; erewrite term_eval_exp; eauto. Qed. @@ -197,7 +197,7 @@ Lemma bblocks_smem_rec_Some_correct1 p m0: forall (m1 m2: mem) (d: smem), forall x, term_eval ge (bblock_smem_rec p d x) m0 = Some (m2 x). Proof. Local Hint Resolve inst_smem_Some_correct1: core. - induction p as [ | i p]; simpl; intros m1 m2 d H. + induction p as [ | i p]; cbn; intros m1 m2 d H. - inversion_clear H; eauto. - intros H0 x0. destruct (inst_run ge i m1 m1) eqn: Heqov. @@ -218,15 +218,15 @@ Lemma inst_smem_None_correct i m0 old (od: smem): (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> inst_run ge i m1 old = None -> exists x, term_eval ge (inst_smem i d od x) m0 = None. Proof. - intro X; induction i as [|[x e] i IHi]; simpl; intros m1 d. + intro X; induction i as [|[x e] i IHi]; cbn; intros m1 d. - discriminate. - intros VALID H0. destruct (exp_eval ge e m1 old) eqn: Heqov. + refine (IHi _ _ _ _); eauto. - intros x0; unfold assign, smem_set; simpl. destruct (R.eq_dec x x0); auto. + intros x0; unfold assign, smem_set; cbn. destruct (R.eq_dec x x0); auto. subst; erewrite term_eval_exp; eauto. + intuition. - constructor 1 with (x:=x); simpl. + constructor 1 with (x:=x); cbn. apply inst_smem_abort; auto. rewrite set_spec_eq. erewrite term_eval_exp; eauto. @@ -241,14 +241,14 @@ Lemma inst_smem_Some_correct2 i m0 old (od: smem): res_eq (Some m2) (inst_run ge i m1 old). Proof. intro X. - induction i as [|[x e] i IHi]; simpl; intros m1 m2 d VALID H0. + induction i as [|[x e] i IHi]; cbn; intros m1 m2 d VALID H0. - intros H; eapply ex_intro; intuition eauto. generalize (H0 x); rewrite H. congruence. - intros H. destruct (exp_eval ge e m1 old) eqn: Heqov. + refine (IHi _ _ _ _ _ _); eauto. - intros x0; unfold assign, smem_set; simpl; destruct (R.eq_dec x x0); auto. + intros x0; unfold assign, smem_set; cbn; destruct (R.eq_dec x x0); auto. subst; erewrite term_eval_exp; eauto. + generalize (H x). rewrite inst_smem_abort; discriminate || auto. @@ -262,7 +262,7 @@ Lemma bblocks_smem_rec_Some_correct2 p m0: forall (m1 m2: mem) d, (forall x, term_eval ge (bblock_smem_rec p d x) m0 = Some (m2 x)) -> res_eq (Some m2) (run ge p m1). Proof. - induction p as [|i p]; simpl; intros m1 m2 d VALID H0. + induction p as [|i p]; cbn; intros m1 m2 d VALID H0. - intros H; eapply ex_intro; intuition eauto. generalize (H0 x); rewrite H. congruence. @@ -293,13 +293,13 @@ Lemma inst_valid i m0 old (od:smem): (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> pre (inst_smem i d od) ge m0. Proof. - induction i as [|[x e] i IHi]; simpl; auto. + induction i as [|[x e] i IHi]; cbn; auto. intros Hold m1 m2 d VALID0 H Hm1. - destruct (exp_eval ge e m1 old) eqn: Heq; simpl; try congruence. + destruct (exp_eval ge e m1 old) eqn: Heq; cbn; try congruence. eapply IHi; eauto. - + unfold smem_set in * |- *; simpl. + + unfold smem_set in * |- *; cbn. rewrite Hm1; intuition congruence. - + intros x0. unfold assign, smem_set; simpl; destruct (R.eq_dec x x0); auto. + + intros x0. unfold assign, smem_set; cbn; destruct (R.eq_dec x x0); auto. subst; erewrite term_eval_exp; eauto. Qed. @@ -311,7 +311,7 @@ Lemma block_smem_rec_valid p m0: forall (m1 m2: mem) (d:smem), pre (bblock_smem_rec p d) ge m0. Proof. Local Hint Resolve inst_valid: core. - induction p as [ | i p]; simpl; intros m1 d H; auto. + induction p as [ | i p]; cbn; intros m1 d H; auto. intros H0 H1. destruct (inst_run ge i m1 m1) eqn: Heqov; eauto. congruence. @@ -322,7 +322,7 @@ Lemma bblock_smem_valid p m0 m1: pre (bblock_smem p) ge m0. Proof. intros; eapply block_smem_rec_valid; eauto. - unfold smem_empty; simpl. auto. + unfold smem_empty; cbn. auto. Qed. Definition smem_valid ge d m := pre d ge m /\ forall x, term_eval ge (d x) m <> None. @@ -339,7 +339,7 @@ Theorem bblock_smem_simu p1 p2: Proof. Local Hint Resolve bblock_smem_valid bblock_smem_Some_correct1: core. intros (INCL & EQUIV) m DONTFAIL; unfold smem_valid in * |-. - destruct (run ge p1 m) as [m1|] eqn: RUN1; simpl; try congruence. + destruct (run ge p1 m) as [m1|] eqn: RUN1; cbn; try congruence. assert (X: forall x, term_eval ge (bblock_smem p1 x) m = Some (m1 x)); eauto. eapply bblock_smem_Some_correct2; eauto. + destruct (INCL m); intuition eauto. @@ -371,7 +371,7 @@ Lemma smem_valid_set_proof d x t m: Proof. unfold smem_valid; intros (PRE & VALID) PREt. split. + split; auto. - + intros x0; unfold smem_set; simpl; case (R.eq_dec x x0); intros; subst; auto. + + intros x0; unfold smem_set; cbn; case (R.eq_dec x x0); intros; subst; auto. Qed. @@ -384,7 +384,7 @@ Definition smem_correct ge (d: smem) (m: mem) (om: option mem): Prop:= Lemma bblock_smem_correct ge p m: smem_correct ge (bblock_smem p) m (run ge p m). Proof. - unfold smem_correct; simpl; intros m'; split. + unfold smem_correct; cbn; intros m'; split. + intros; split. * eapply bblock_smem_valid; eauto. * eapply bblock_smem_Some_correct1; eauto. diff --git a/kvx/lib/ForwardSimulationBlock.v b/kvx/lib/ForwardSimulationBlock.v index f79814f2..61466dad 100644 --- a/kvx/lib/ForwardSimulationBlock.v +++ b/kvx/lib/ForwardSimulationBlock.v @@ -42,11 +42,11 @@ Lemma starN_split n s t s': forall m k, n=m+k -> exists (t1 t2:trace) s0, starN (step L) (globalenv L) m s t1 s0 /\ starN (step L) (globalenv L) k s0 t2 s' /\ t=t1**t2. Proof. - induction 1; simpl. + induction 1; cbn. + intros m k H; assert (X: m=0); try omega. assert (X0: k=0); try omega. subst; repeat (eapply ex_intro); intuition eauto. - + intros m; destruct m as [| m']; simpl. + + intros m; destruct m as [| m']; cbn. - intros k H2; subst; repeat (eapply ex_intro); intuition eauto. - intros k H2. inversion H2. exploit (IHstarN m' k); eauto. intro. @@ -61,7 +61,7 @@ Lemma starN_tailstep n s t1 s': forall (t t2:trace) s'', Step L s' t2 s'' -> t = t1 ** t2 -> starN (step L) (globalenv L) (S n) s t s''. Proof. - induction 1; simpl. + induction 1; cbn. + intros t t1 s0; autorewrite with trace_rewrite. intros; subst; eapply starN_step; eauto. autorewrite with trace_rewrite; auto. @@ -153,8 +153,8 @@ Definition head (s: memostate): state L1 := Lemma head_followed (s: memostate): follows_in_block (head s) (real s). Proof. - destruct s as [rs ms Hs]. simpl. - destruct ms as [ms|]; unfold head; simpl; auto. + destruct s as [rs ms Hs]. cbn. + destruct ms as [ms|]; unfold head; cbn; auto. constructor 1. omega. cutrewrite ((dist_end_block rs - dist_end_block rs)%nat=O). @@ -198,21 +198,21 @@ Definition memoL1 := {| Lemma discr_dist_end s: {dist_end_block s = O} + {dist_end_block s <> O}. Proof. - destruct (dist_end_block s); simpl; intuition. + destruct (dist_end_block s); cbn; intuition. Qed. Lemma memo_simulation_step: forall s1 t s1', Step L1 s1 t s1' -> forall s2, s1 = (real s2) -> exists s2', Step memoL1 s2 t s2' /\ s1' = (real s2'). Proof. - intros s1 t s1' H1 [rs2 ms2 Hmoi] H2. simpl in H2; subst. + intros s1 t s1' H1 [rs2 ms2 Hmoi] H2. cbn in H2; subst. destruct (discr_dist_end rs2) as [H3 | H3]. - + refine (ex_intro _ {|real:=s1'; memorized:=None |} _); simpl. + + refine (ex_intro _ {|real:=s1'; memorized:=None |} _); cbn. intuition. + destruct ms2 as [s|]. - - refine (ex_intro _ {|real:=s1'; memorized:=Some s |} _); simpl. + - refine (ex_intro _ {|real:=s1'; memorized:=Some s |} _); cbn. intuition. - - refine (ex_intro _ {|real:=s1'; memorized:=Some rs2 |} _); simpl. + - refine (ex_intro _ {|real:=s1'; memorized:=Some rs2 |} _); cbn. intuition. Unshelve. * intros; discriminate. @@ -228,7 +228,7 @@ Qed. Lemma forward_memo_simulation_1: forward_simulation L1 memoL1. Proof. apply forward_simulation_step with (match_states:=fun s1 s2 => s1 = (real s2)); auto. - + intros s1 H; eapply ex_intro with (x:={|real:=s1; memorized:=None |}); simpl. + + intros s1 H; eapply ex_intro with (x:={|real:=s1; memorized:=None |}); cbn. intuition. + intros; subst; auto. + intros; exploit memo_simulation_step; eauto. @@ -239,8 +239,8 @@ Qed. Lemma forward_memo_simulation_2: forward_simulation memoL1 L2. Proof. - unfold memoL1; simpl. - apply forward_simulation_opt with (measure:=fun s => dist_end_block (real s)) (match_states:=fun s1 s2 => match_states (head s1) s2); simpl; auto. + unfold memoL1; cbn. + apply forward_simulation_opt with (measure:=fun s => dist_end_block (real s)) (match_states:=fun s1 s2 => match_states (head s1) s2); cbn; auto. + intros s1 [H0 H1]; destruct (match_initial_states (real s1) H0). unfold head; rewrite H1. intuition eauto. @@ -254,14 +254,14 @@ Proof. - (* MidBloc *) constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H5 H4]; auto. unfold head in * |- *. rewrite H3. rewrite H4. intuition. - destruct (memorized s1); simpl; auto. tauto. + destruct (memorized s1); cbn; auto. tauto. - (* EndBloc *) constructor 1. destruct (simu_end_block (head s1) t (real s1') s2) as (s2' & H3 & H4); auto. * destruct (head_followed s1) as [H4 H3]. cutrewrite (dist_end_block (head s1) - dist_end_block (real s1) = dist_end_block (head s1)) in H3; try omega. eapply starN_tailstep; eauto. - * unfold head; rewrite H2; simpl. intuition eauto. + * unfold head; rewrite H2; cbn. intuition eauto. Qed. Lemma forward_simulation_block_rel: forward_simulation L1 L2. diff --git a/kvx/lib/Machblock.v b/kvx/lib/Machblock.v index edae0ed4..404c2a96 100644 --- a/kvx/lib/Machblock.v +++ b/kvx/lib/Machblock.v @@ -70,7 +70,7 @@ Lemma bblock_eq: b1 = b2. Proof. intros. destruct b1. destruct b2. - simpl in *. subst. auto. + cbn in *. subst. auto. Qed. Definition length_opt {A} (o: option A) : nat := @@ -85,15 +85,15 @@ Lemma size_null b: size b = 0%nat -> header b = nil /\ body b = nil /\ exit b = None. Proof. - destruct b as [h b e]. simpl. unfold size. simpl. + destruct b as [h b e]. cbn. unfold size. cbn. intros H. assert (length h = 0%nat) as Hh; [ omega |]. assert (length b = 0%nat) as Hb; [ omega |]. assert (length_opt e = 0%nat) as He; [ omega|]. repeat split. - destruct h; try (simpl in Hh; discriminate); auto. - destruct b; try (simpl in Hb; discriminate); auto. - destruct e; try (simpl in He; discriminate); auto. + destruct h; try (cbn in Hh; discriminate); auto. + destruct b; try (cbn in Hb; discriminate); auto. + destruct e; try (cbn in He; discriminate); auto. Qed. (** ** programs *) @@ -127,13 +127,13 @@ Definition is_label (lbl: label) (bb: bblock) : bool := Lemma is_label_correct_true lbl bb: List.In lbl (header bb) <-> is_label lbl bb = true. Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. + unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition. Qed. Lemma is_label_correct_false lbl bb: ~(List.In lbl (header bb)) <-> is_label lbl bb = false. Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. + unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition. Qed. diff --git a/kvx/lib/Machblockgen.v b/kvx/lib/Machblockgen.v index ab186083..3d5d7b2c 100644 --- a/kvx/lib/Machblockgen.v +++ b/kvx/lib/Machblockgen.v @@ -148,11 +148,11 @@ Lemma add_to_code_is_trans_code i c bl: is_trans_code c bl -> is_trans_code (i::c) (add_to_code (trans_inst i) bl). Proof. - destruct bl as [|bh0 bl]; simpl. + destruct bl as [|bh0 bl]; cbn. - intro H. inversion H. subst. eauto. - remember (trans_inst i) as ti. destruct ti as [l|bi|cfi]. - + intros; eapply Tr_add_label; eauto. destruct i; simpl in * |- *; congruence. + + intros; eapply Tr_add_label; eauto. destruct i; cbn in * |- *; congruence. + intros. remember (header bh0) as hbh0. destruct hbh0 as [|b]. * eapply Tr_add_basic; eauto. * cutrewrite (add_basic bi empty_bblock = add_to_new_bblock (MB_basic bi)); auto. @@ -170,7 +170,7 @@ Lemma trans_code_is_trans_code_rev c1: forall c2 mbi, is_trans_code c2 mbi -> is_trans_code (rev_append c1 c2) (trans_code_rev c1 mbi). Proof. - induction c1 as [| i c1]; simpl; auto. + induction c1 as [| i c1]; cbn; auto. Qed. Lemma trans_code_is_trans_code c: is_trans_code c (trans_code c). @@ -186,17 +186,17 @@ Lemma add_to_code_is_trans_code_inv i c bl: is_trans_code (i::c) bl -> exists bl0, is_trans_code c bl0 /\ bl = add_to_code (trans_inst i) bl0. Proof. intro H; inversion H as [|H0 H1 bl0| | H0 bi bh H1 bl0]; clear H; subst; (repeat econstructor); eauto. - + (* case Tr_end_block *) inversion H3; subst; simpl; auto. + + (* case Tr_end_block *) inversion H3; subst; cbn; auto. * destruct (header bh); congruence. - * destruct bl0; simpl; congruence. - + (* case Tr_add_basic *) rewrite H3. simpl. destruct (header bh); congruence. + * destruct bl0; cbn; congruence. + + (* case Tr_add_basic *) rewrite H3. cbn. destruct (header bh); congruence. Qed. Lemma trans_code_is_trans_code_rev_inv c1: forall c2 mbi, is_trans_code (rev_append c1 c2) mbi -> exists mbi0, is_trans_code c2 mbi0 /\ mbi=trans_code_rev c1 mbi0. Proof. - induction c1 as [| i c1]; simpl; eauto. + induction c1 as [| i c1]; cbn; eauto. intros; exploit IHc1; eauto. intros (mbi0 & H1 & H2); subst. exploit add_to_code_is_trans_code_inv; eauto. diff --git a/kvx/lib/Machblockgenproof.v b/kvx/lib/Machblockgenproof.v index dfb97bfe..fc722887 100644 --- a/kvx/lib/Machblockgenproof.v +++ b/kvx/lib/Machblockgenproof.v @@ -146,16 +146,16 @@ Lemma parent_sp_preserved: forall s, Mach.parent_sp s = parent_sp (trans_stack s). Proof. - unfold parent_sp. unfold Mach.parent_sp. destruct s; simpl; auto. - unfold trans_stackframe. destruct s; simpl; auto. + unfold parent_sp. unfold Mach.parent_sp. destruct s; cbn; auto. + unfold trans_stackframe. destruct s; cbn; auto. Qed. Lemma parent_ra_preserved: forall s, Mach.parent_ra s = parent_ra (trans_stack s). Proof. - unfold parent_ra. unfold Mach.parent_ra. destruct s; simpl; auto. - unfold trans_stackframe. destruct s; simpl; auto. + unfold parent_ra. unfold Mach.parent_ra. destruct s; cbn; auto. + unfold trans_stackframe. destruct s; cbn; auto. Qed. Lemma external_call_preserved: @@ -175,11 +175,11 @@ Proof. destruct i; try (constructor 2; split; auto; discriminate ). destruct (peq l0 l) as [P|P]. - constructor. subst l0; split; auto. - revert H. unfold Mach.find_label. simpl. rewrite peq_true. + revert H. unfold Mach.find_label. cbn. rewrite peq_true. intros H; injection H; auto. - constructor 2. split. + intro F. injection F. intros. contradict P; auto. - + revert H. unfold Mach.find_label. simpl. rewrite peq_false; auto. + + revert H. unfold Mach.find_label. cbn. rewrite peq_false; auto. Qed. Lemma find_label_is_end_block_not_label i l c bl: @@ -192,24 +192,24 @@ Proof. remember (is_label l _) as b. cutrewrite (b = false); auto. subst; unfold is_label. - destruct i; simpl in * |- *; try (destruct (in_dec l nil); intuition). + destruct i; cbn in * |- *; try (destruct (in_dec l nil); intuition). inversion H. destruct (in_dec l (l0::nil)) as [H6|H6]; auto. - simpl in H6; intuition try congruence. + cbn in H6; intuition try congruence. Qed. Lemma find_label_at_begin l bh bl: In l (header bh) -> find_label l (bh :: bl) = Some (bh::bl). Proof. - unfold find_label; rewrite is_label_correct_true; intro H; rewrite H; simpl; auto. + unfold find_label; rewrite is_label_correct_true; intro H; rewrite H; cbn; auto. Qed. Lemma find_label_add_label_diff l bh bl: ~(In l (header bh)) -> find_label l (bh::bl) = find_label l bl. Proof. - unfold find_label; rewrite is_label_correct_false; intro H; rewrite H; simpl; auto. + unfold find_label; rewrite is_label_correct_false; intro H; rewrite H; cbn; auto. Qed. Definition concat (h: list label) (c: code): code := @@ -227,18 +227,18 @@ Proof. rewrite <- is_trans_code_inv in * |-. induction Heqbl. + (* Tr_nil *) - intros; exists (l::nil); simpl in * |- *; intuition. + intros; exists (l::nil); cbn in * |- *; intuition. discriminate. + (* Tr_end_block *) intros. exploit Mach_find_label_split; eauto. clear H0; destruct 1 as [(H0&H2)|(H0&H2)]. - - subst. rewrite find_label_at_begin; simpl; auto. + - subst. rewrite find_label_at_begin; cbn; auto. inversion H as [mbi H1 H2| | ]. subst. inversion Heqbl. subst. - exists (l :: nil); simpl; eauto. + exists (l :: nil); cbn; eauto. - exploit IHHeqbl; eauto. destruct 1 as (h & H3 & H4). exists h. @@ -251,21 +251,21 @@ Proof. - subst. inversion H0 as [H1]. clear H0. - erewrite find_label_at_begin; simpl; eauto. + erewrite find_label_at_begin; cbn; eauto. subst_is_trans_code Heqbl. - exists (l :: nil); simpl; eauto. + exists (l :: nil); cbn; eauto. - subst; assert (H: l0 <> l); try congruence; clear H0. exploit IHHeqbl; eauto. clear IHHeqbl Heqbl. intros (h & H3 & H4). - simpl; unfold is_label, add_label; simpl. - destruct (in_dec l (l0::header bh)) as [H5|H5]; simpl in H5. + cbn; unfold is_label, add_label; cbn. + destruct (in_dec l (l0::header bh)) as [H5|H5]; cbn in H5. * destruct H5; try congruence. - exists (l0::h); simpl; intuition. + exists (l0::h); cbn; intuition. rewrite find_label_at_begin in H4; auto. apply f_equal. inversion H4 as [H5]. clear H4. - destruct (trans_code c'); simpl in * |- *; - inversion H5; subst; simpl; auto. + destruct (trans_code c'); cbn in * |- *; + inversion H5; subst; cbn; auto. * exists h. intuition. erewrite <- find_label_add_label_diff; eauto. + (* Tr_add_basic *) @@ -318,12 +318,12 @@ Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exe Lemma size_add_label l bh: size (add_label l bh) = size bh + 1. Proof. - unfold add_label, size; simpl; omega. + unfold add_label, size; cbn; omega. Qed. Lemma size_add_basic bi bh: header bh = nil -> size (add_basic bi bh) = size bh + 1. Proof. - intro H. unfold add_basic, size; rewrite H; simpl. omega. + intro H. unfold add_basic, size; rewrite H; cbn. omega. Qed. @@ -418,8 +418,8 @@ Proof. + exists lbl. unfold trans_inst in H1. destruct i; congruence. - + unfold add_basic in H; simpl in H; congruence. - + unfold cfi_bblock in H; simpl in H; congruence. + + unfold add_basic in H; cbn in H; congruence. + + unfold cfi_bblock in H; cbn in H; congruence. Qed. Local Hint Resolve Mlabel_is_not_basic: core. @@ -433,11 +433,11 @@ Proof. intros b bl H; remember (trans_inst i) as ti. destruct ti as [lbl|bi|cfi]; inversion H as [|d0 d1 d2 H0 H1| |]; subst; - try (rewrite <- Heqti in * |- *); simpl in * |- *; + try (rewrite <- Heqti in * |- *); cbn in * |- *; try congruence. + (* label at end block *) inversion H1; subst. inversion H0; subst. - assert (X:i=Mlabel lbl). { destruct i; simpl in Heqti; congruence. } + assert (X:i=Mlabel lbl). { destruct i; cbn in Heqti; congruence. } subst. repeat econstructor; eauto. + (* label at mid block *) exploit IHc; eauto. @@ -451,12 +451,12 @@ Proof. assert (X:(trans_inst i) = MB_basic bi ). { repeat econstructor; congruence. } repeat econstructor; congruence. - exists (i::c), c, c. - repeat econstructor; eauto; inversion H0; subst; repeat econstructor; simpl; try congruence. + repeat econstructor; eauto; inversion H0; subst; repeat econstructor; cbn; try congruence. * exploit (add_to_new_block_is_label i0); eauto. - intros (l & H8); subst; simpl; congruence. + intros (l & H8); subst; cbn; congruence. * exploit H3; eauto. * exploit (add_to_new_block_is_label i0); eauto. - intros (l & H8); subst; simpl; congruence. + intros (l & H8); subst; cbn; congruence. + (* basic at mid block *) inversion H1; subst. exploit IHc; eauto. @@ -476,7 +476,7 @@ Lemma step_simu_header st f sp rs m s c h c' t: starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length h) (Mach.State st f sp c rs m) t s -> s = Mach.State st f sp c' rs m /\ t = E0. Proof. - induction 1; simpl; intros hs; try (inversion hs; tauto). + induction 1; cbn; intros hs; try (inversion hs; tauto). inversion hs as [|n1 s1 t1 t2 s2 t3 s3 H1]. inversion H1. subst. auto. Qed. @@ -487,21 +487,21 @@ Lemma step_simu_basic_step (i: Mach.instruction) (bi: basic_inst) (c: Mach.code) Mach.step (inv_trans_rao rao) ge (Mach.State s f sp (i::c) rs m) t s' -> exists rs' m', s'=Mach.State s f sp c rs' m' /\ t=E0 /\ basic_step tge (trans_stack s) f sp rs m bi rs' m'. Proof. - destruct i; simpl in * |-; + destruct i; cbn in * |-; (discriminate || (intro H; inversion_clear H; intro X; inversion_clear X; eapply ex_intro; eapply ex_intro; intuition eauto)). - eapply exec_MBgetparam; eauto. exploit (functions_translated); eauto. intro. destruct H3 as (tf & A & B). subst. eapply A. - all: simpl; rewrite <- parent_sp_preserved; auto. - - eapply exec_MBop; eauto. rewrite <- H. destruct o; simpl; auto. destruct (rs ## l); simpl; auto. + all: cbn; rewrite <- parent_sp_preserved; auto. + - eapply exec_MBop; eauto. rewrite <- H. destruct o; cbn; auto. destruct (rs ## l); cbn; auto. unfold Genv.symbol_address; rewrite symbols_preserved; auto. - - eapply exec_MBload; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + - eapply exec_MBload; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto; unfold Genv.symbol_address; rewrite symbols_preserved; auto. - - eapply exec_MBload_notrap1; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + - eapply exec_MBload_notrap1; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto; unfold Genv.symbol_address; rewrite symbols_preserved; auto. - - eapply exec_MBload_notrap2; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + - eapply exec_MBload_notrap2; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto; unfold Genv.symbol_address; rewrite symbols_preserved; auto. - - eapply exec_MBstore; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + - eapply exec_MBstore; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto; unfold Genv.symbol_address; rewrite symbols_preserved; auto. Qed. @@ -511,7 +511,7 @@ Lemma star_step_simu_body_step s f sp c bdy c': starN (Mach.step (inv_trans_rao rao)) ge (length bdy) (Mach.State s f sp c rs m) t s' -> exists rs' m', s'=Mach.State s f sp c' rs' m' /\ t=E0 /\ body_step tge (trans_stack s) f sp bdy rs m rs' m'. Proof. - induction 1; simpl. + induction 1; cbn. + intros. inversion H. exists rs. exists m. auto. + intros. inversion H0. exists rs. exists m. auto. + intros. inversion H1; subst. @@ -531,15 +531,15 @@ Local Hint Resolve eval_builtin_args_preserved external_call_symbols_preserved f Lemma match_states_concat_trans_code st f sp c rs m h: match_states (Mach.State st f sp c rs m) (State (trans_stack st) f sp (concat h (trans_code c)) rs m). Proof. - intros; constructor 1; simpl. + intros; constructor 1; cbn. + intros (t0 & s1' & H0) t s'. remember (trans_code _) as bl. destruct bl as [|bh bl]. { rewrite <- is_trans_code_inv in Heqbl; inversion Heqbl; inversion H0; congruence. } clear H0. - simpl; constructor 1; - intros X; inversion X as [d1 d2 d3 d4 d5 d6 d7 rs' m' d10 d11 X1 X2| | | ]; subst; simpl in * |- *; - eapply exec_bblock; eauto; simpl; + cbn; constructor 1; + intros X; inversion X as [d1 d2 d3 d4 d5 d6 d7 rs' m' d10 d11 X1 X2| | | ]; subst; cbn in * |- *; + eapply exec_bblock; eauto; cbn; inversion X2 as [cfi d1 d2 d3 H1|]; subst; eauto; inversion H1; subst; eauto. + intros H r; constructor 1; intro X; inversion X. @@ -551,7 +551,7 @@ Lemma step_simu_cfi_step (i: Mach.instruction) (cfi: control_flow_inst) (c: Mach Mach.step (inv_trans_rao rao) ge (Mach.State stk f sp (i::c) rs m) t s' -> exists s2, cfi_step rao tge cfi (State (trans_stack stk) f sp (b::blc) rs m) t s2 /\ match_states s' s2. Proof. - destruct i; simpl in * |-; + destruct i; cbn in * |-; (intro H; intro Htc;apply is_trans_code_inv in Htc;rewrite Htc;inversion_clear H;intro X; inversion_clear X). * eapply ex_intro. intuition auto. @@ -561,8 +561,8 @@ Proof. intuition auto. eapply exec_MBtailcall;eauto. - rewrite <-H; exploit (find_function_ptr_same); eauto. - - simpl; rewrite <- parent_sp_preserved; auto. - - simpl; rewrite <- parent_ra_preserved; auto. + - cbn; rewrite <- parent_sp_preserved; auto. + - cbn; rewrite <- parent_ra_preserved; auto. * eapply ex_intro. intuition auto. eapply exec_MBbuiltin ;eauto. @@ -605,7 +605,7 @@ Proof. inversion H1; subst. exploit (step_simu_cfi_step); eauto. intros [s2 [Hcfi1 Hcfi3]]. - inversion H4. subst; simpl. + inversion H4. subst; cbn. autorewrite with trace_rewrite. exists s2. split;eauto. @@ -616,7 +616,7 @@ Lemma simu_end_block: starN (Mach.step (inv_trans_rao rao)) ge (Datatypes.S (dist_end_block s1)) s1 t s1' -> exists s2', step rao tge (trans_state s1) t s2' /\ match_states s1' s2'. Proof. - destruct s1; simpl. + destruct s1; cbn. + (* State *) remember (trans_code _) as tc. rewrite <- is_trans_code_inv in Heqtc. @@ -624,7 +624,7 @@ Proof. destruct tc as [|b bl]. { (* nil => absurd *) inversion Heqtc. subst. - unfold dist_end_block_code; simpl. + unfold dist_end_block_code; cbn. inversion_clear H; inversion_clear H0. } @@ -659,7 +659,7 @@ Proof. intros t s1' H; inversion_clear H. eapply ex_intro; constructor 1; eauto. inversion H1; subst; clear H1. - inversion_clear H0; simpl. + inversion_clear H0; cbn. - (* function_internal*) cutrewrite (trans_code (Mach.fn_code f0) = fn_code (transf_function f0)); eauto. eapply exec_function_internal; eauto. @@ -674,7 +674,7 @@ Proof. intros t s1' H; inversion_clear H. eapply ex_intro; constructor 1; eauto. inversion H1; subst; clear H1. - inversion_clear H0; simpl. + inversion_clear H0; cbn. eapply exec_return. Qed. @@ -685,10 +685,10 @@ dist_end_block_code (i :: c) = 0. Proof. unfold dist_end_block_code. intro H. destruct H as [cfi H]. - destruct i;simpl in H;try(congruence); ( + destruct i;cbn in H;try(congruence); ( remember (trans_code _) as bl; rewrite <- is_trans_code_inv in Heqbl; - inversion Heqbl; subst; simpl in * |- *; try (congruence)). + inversion Heqbl; subst; cbn in * |- *; try (congruence)). Qed. Theorem transf_program_correct: @@ -697,23 +697,23 @@ Proof. apply forward_simulation_block_trans with (dist_end_block := dist_end_block) (trans_state := trans_state). (* simu_mid_block *) - intros s1 t s1' H1 H2. - destruct H1; simpl in * |- *; omega || (intuition auto); - destruct H2; eapply cfi_dist_end_block; simpl; eauto. + destruct H1; cbn in * |- *; omega || (intuition auto); + destruct H2; eapply cfi_dist_end_block; cbn; eauto. (* public_preserved *) - apply senv_preserved. (* match_initial_states *) - - intros. simpl. + - intros. cbn. eapply ex_intro; constructor 1. eapply match_states_trans_state. destruct H. split. apply init_mem_preserved; auto. rewrite prog_main_preserved. rewrite <- H0. apply symbols_preserved. (* match_final_states *) - - intros. simpl. destruct H. split with (r := r); auto. + - intros. cbn. destruct H. split with (r := r); auto. (* final_states_end_block *) - - intros. simpl in H0. + - intros. cbn in H0. inversion H0. - inversion H; simpl; auto. + inversion H; cbn; auto. all: try (subst; discriminate). apply cfi_dist_end_block; exists MBreturn; eauto. (* simu_end_block *) @@ -733,8 +733,8 @@ Proof. intro H; destruct c as [|i' c]. { inversion H. } remember (trans_inst i) as ti. destruct ti as [lbl|bi|cfi]. - - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2: ( destruct i; simpl in * |- *; try congruence ). - exists nil; simpl; eexists. eapply Tr_add_label; eauto. + - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2: ( destruct i; cbn in * |- *; try congruence ). + exists nil; cbn; eexists. eapply Tr_add_label; eauto. - (*i=basic*) destruct i'. 10: { exists (add_to_new_bblock (MB_basic bi)::nil). exists b. @@ -742,11 +742,11 @@ Proof. rewrite Heqti. eapply Tr_end_block; eauto. rewrite <-Heqti. - eapply End_basic. inversion H; try(simpl; congruence). - simpl in H5; congruence. } - all: try(exists nil; simpl; eexists; eapply Tr_add_basic; eauto; inversion H; try(eauto || congruence)). + eapply End_basic. inversion H; try(cbn; congruence). + cbn in H5; congruence. } + all: try(exists nil; cbn; eexists; eapply Tr_add_basic; eauto; inversion H; try(eauto || congruence)). - (*i=cfi*) - destruct i; try(simpl in Heqti; congruence). + destruct i; try(cbn in Heqti; congruence). all: exists (add_to_new_bblock (MB_cfi cfi)::nil); exists b; cutrewrite ((add_to_new_bblock (MB_cfi cfi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_cfi cfi) :: (b::l)));eauto; rewrite Heqti; @@ -768,13 +768,13 @@ Qed. (* FIXME: these two lemma should go into [Coqlib.v] *) Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2). Proof. - induction l1; simpl; auto with coqlib. + induction l1; cbn; auto with coqlib. Qed. Hint Resolve is_tail_app: coqlib. Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3. Proof. - induction l1; simpl; auto with coqlib. + induction l1; cbn; auto with coqlib. intros l2 l3 H; inversion H; eauto with coqlib. Qed. Hint Resolve is_tail_app_inv: coqlib. @@ -787,17 +787,17 @@ Proof. - intros; subst. remember (trans_code (Mcall _ _::c)) as tc2. rewrite <- is_trans_code_inv in Heqtc2. - inversion Heqtc2; simpl in * |- *; subst; try congruence. + inversion Heqtc2; cbn in * |- *; subst; try congruence. subst_is_trans_code H1. eapply ex_intro; eauto with coqlib. - intros; exploit IHis_tail; eauto. clear IHis_tail. intros (b & Hb). inversion Hb; clear Hb. * exploit (trans_code_monotonic i c2); eauto. intros (l' & b' & Hl'); rewrite Hl'. - exists b'; simpl; eauto with coqlib. + exists b'; cbn; eauto with coqlib. * exploit (trans_code_monotonic i c2); eauto. intros (l' & b' & Hl'); rewrite Hl'. - simpl; eapply ex_intro. + cbn; eapply ex_intro. eapply is_tail_trans; eauto with coqlib. Qed. |