From b2fc9b55d9c59a9c507786a650377e2f0a1ddad8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 29 Sep 2020 16:22:18 +0200 Subject: simpl -> cbn --- kvx/Asm.v | 40 ++++++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 20 deletions(-) (limited to 'kvx/Asm.v') diff --git a/kvx/Asm.v b/kvx/Asm.v index 30aafc55..515e13e0 100644 --- a/kvx/Asm.v +++ b/kvx/Asm.v @@ -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. -- cgit