From 76e7f701c10e517737ae095a0293b68f5205be90 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 12 Aug 2013 14:07:58 +0000 Subject: Simplify LPMap by smashing bottoms. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2306 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Constpropproof.v | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'backend/Constpropproof.v') diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index dcab6f62..328f724f 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -80,10 +80,10 @@ Lemma regs_match_approx_update: regs_match_approx ra rs -> regs_match_approx (D.set r a ra) (rs#r <- v). Proof. - intros; red; intros. rewrite Regmap.gsspec. - case (peq r0 r); intro. - subst r0. rewrite D.gss. auto. - rewrite D.gso; auto. + intros; red; intros. + rewrite D.gsspec. rewrite Regmap.gsspec. destruct (peq r0 r); auto. + red; intros; subst ra. specialize (H0 xH). rewrite D.get_bot in H0. inv H0. + unfold Approx.eq. red; intros; subst a. inv H. Qed. Lemma approx_regs_val_list: @@ -103,9 +103,10 @@ Lemma regs_match_approx_forget: Proof. induction rl; simpl; intros. auto. - apply IHrl. red; intros. destruct (peq r a). - subst a. rewrite D.gss. constructor. - rewrite D.gso; auto. + apply IHrl. + red; intros. rewrite D.gsspec. destruct (peq r a). constructor. auto. + red; intros; subst ra. specialize (H xH). inv H. + unfold Approx.eq, Approx.bot. congruence. Qed. (** The correctness of the static analysis follows from the results -- cgit