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/Asmblock.v | 52 ++++++++++++++++++++++++++-------------------------- 1 file changed, 26 insertions(+), 26 deletions(-) (limited to 'kvx/Asmblock.v') 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. -- cgit