From 5b5682a4d4ebb102002616015adab46154597b10 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 16 Dec 2020 15:52:48 +0100 Subject: upgrade kvx backend to coq.8.12.2 --- kvx/Asmblockdeps.v | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) (limited to 'kvx/Asmblockdeps.v') 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. -- cgit