diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-12-16 15:52:48 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-12-16 15:52:48 +0100 |
| commit | 5b5682a4d4ebb102002616015adab46154597b10 (patch) | |
| tree | b9f8833c35558ae7c636d46c548b4bc01adda194 /kvx/Asmblockdeps.v | |
| parent | dc413cc8b95c4205af4de247de69a166284ecf99 (diff) | |
| download | compcert-kvx-5b5682a4d4ebb102002616015adab46154597b10.tar.gz compcert-kvx-5b5682a4d4ebb102002616015adab46154597b10.zip | |
upgrade kvx backend to coq.8.12.2
Diffstat (limited to 'kvx/Asmblockdeps.v')
| -rw-r--r-- | kvx/Asmblockdeps.v | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/kvx/Asmblockdeps.v b/kvx/Asmblockdeps.v index 3d981100..67430b54 100644 --- a/kvx/Asmblockdeps.v +++ b/kvx/Asmblockdeps.v @@ -40,6 +40,10 @@ Require Import Chunks. Require Import Lia. + +Import ListNotations. +Local Open Scope list_scope. + Open Scope impure. (** Definition of [L] *) @@ -706,19 +710,20 @@ Proof. destruct r; destruct r'. all: try discriminate; try contradiction. - intros. apply not_eq_add. apply ireg_to_pos_discr. congruence. - - intros. unfold ppos. cutrewrite (3 + ireg_to_pos g = (1 + ireg_to_pos g) + 2). apply Pos.add_no_neutral. - apply eq_sym. rewrite Pos.add_comm. rewrite Pos.add_assoc. reflexivity. + - intros. unfold ppos. replace (3 + ireg_to_pos g) with ((1 + ireg_to_pos g) + 2). + apply Pos.add_no_neutral. + rewrite Pos.add_comm, Pos.add_assoc. reflexivity. - intros. unfold ppos. rewrite Pos.add_comm. apply Pos.add_no_neutral. - intros. unfold ppos. apply not_eq_sym. - cutrewrite (3 + ireg_to_pos g = (1 + ireg_to_pos g) + 2). apply Pos.add_no_neutral. - apply eq_sym. rewrite Pos.add_comm. rewrite Pos.add_assoc. reflexivity. + replace (3 + ireg_to_pos g) with ((1 + ireg_to_pos g) + 2). apply Pos.add_no_neutral. + rewrite Pos.add_comm, Pos.add_assoc. reflexivity. - intros. unfold ppos. apply not_eq_sym. rewrite Pos.add_comm. apply Pos.add_no_neutral. Qed. Lemma ppos_pmem_discr: forall r, pmem <> ppos r. Proof. intros. destruct r. - - unfold ppos. unfold pmem. apply not_eq_sym. rewrite Pos.add_comm. cutrewrite (3 = 2 + 1). rewrite Pos.add_assoc. apply Pos.add_no_neutral. + - unfold ppos. unfold pmem. apply not_eq_sym. rewrite Pos.add_comm. replace 3 with (2 + 1). rewrite Pos.add_assoc. apply Pos.add_no_neutral. reflexivity. - unfold ppos. unfold pmem. discriminate. - unfold ppos. unfold pmem. discriminate. @@ -1250,7 +1255,7 @@ Theorem bisimu_par_exit ex sz ge fn rsr rsw mr mw sr sw: Proof. intros; unfold estep. exploit (bisimu_par_control ex sz rsw#PC ge fn rsr rsw mr mw sr sw); eauto. - cutrewrite (rsw # PC <- (rsw PC) = rsw); auto. + replace (rsw # PC <- (rsw PC)) with rsw; auto. apply extensionality. intros; destruct x; simpl; auto. Qed. @@ -1461,8 +1466,8 @@ Proof. destruct H2 as (m2' & H2 & H4). discriminate. rewrite H2 in H3. destruct (exec_bblock ge fn p2 rs m); simpl in H3. * destruct H3 as (s' & H3 & H5 & H6). inv H3. inv MS'. - cutrewrite (rs0=rs1). - - cutrewrite (m0=m1); auto. congruence. + replace rs0 with rs1. + - replace m0 with m1; auto. congruence. - apply functional_extensionality. intros r. generalize (H0 r). intros Hr. congruence. * discriminate. |