diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-18 06:19:46 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-18 06:19:46 +0000 |
| commit | 24a8dbb62e8171f3f3ad87e8d3f697e726df0e6a (patch) | |
| tree | cea508ab113778dd3918e98f49d371359dbbbc34 | |
| parent | f43399e0eb0704e270e25fdada770725f58635ed (diff) | |
| download | compcert-24a8dbb62e8171f3f3ad87e8d3f697e726df0e6a.tar.gz compcert-24a8dbb62e8171f3f3ad87e8d3f697e726df0e6a.zip | |
"val_match_approx_increasing" moved from mach-dep part to mach-indep part.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1128 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
| -rw-r--r-- | arm/ConstpropOpproof.v | 11 | ||||
| -rw-r--r-- | backend/Constpropproof.v | 11 | ||||
| -rw-r--r-- | powerpc/ConstpropOpproof.v | 11 |
3 files changed, 11 insertions, 22 deletions
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 70fc606c..bb9caffb 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -47,17 +47,6 @@ Definition val_match_approx (a: approx) (v: val) : Prop := | _ => False end. -Lemma val_match_approx_increasing: - forall a1 a2 v, - Approx.ge a1 a2 -> val_match_approx a2 v -> val_match_approx a1 v. -Proof. - intros until v. - intros [A|[B|C]]. - subst a1. simpl. auto. - subst a2. simpl. tauto. - subst a2. auto. -Qed. - Inductive val_list_match_approx: list approx -> list val -> Prop := | vlma_nil: val_list_match_approx nil nil diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index e628d426..dadb192f 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -47,6 +47,17 @@ Proof. unfold Approx.top, val_match_approx. auto. Qed. +Lemma val_match_approx_increasing: + forall a1 a2 v, + Approx.ge a1 a2 -> val_match_approx ge a2 v -> val_match_approx ge a1 v. +Proof. + intros until v. + intros [A|[B|C]]. + subst a1. simpl. auto. + subst a2. simpl. tauto. + subst a2. auto. +Qed. + Lemma regs_match_approx_increasing: forall a1 a2 rs, D.ge a1 a2 -> regs_match_approx a2 rs -> regs_match_approx a1 rs. diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index c9d77143..0c7be7bd 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -47,17 +47,6 @@ Definition val_match_approx (a: approx) (v: val) : Prop := | _ => False end. -Lemma val_match_approx_increasing: - forall a1 a2 v, - Approx.ge a1 a2 -> val_match_approx a2 v -> val_match_approx a1 v. -Proof. - intros until v. - intros [A|[B|C]]. - subst a1. simpl. auto. - subst a2. simpl. tauto. - subst a2. auto. -Qed. - Inductive val_list_match_approx: list approx -> list val -> Prop := | vlma_nil: val_list_match_approx nil nil |