diff options
| author | Jérémie Koenig <jeremie.koenig@gmail.com> | 2018-01-03 04:15:57 -0500 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-01-03 10:15:57 +0100 |
| commit | 87558f62b29ee94392c3955434aa2680aaaeffa5 (patch) | |
| tree | 7c67724e85e406f161e0d1fcf2bf85752fc0ddf0 /backend/ValueAnalysis.v | |
| parent | 488e6dd710cc799e7adcc124d161f29285185c27 (diff) | |
| download | compcert-kvx-87558f62b29ee94392c3955434aa2680aaaeffa5.tar.gz compcert-kvx-87558f62b29ee94392c3955434aa2680aaaeffa5.zip | |
ValueAnalysis: remove duplicate list_forall2_in_left (#212)
The lemma is now in lib/Coqlib.v.
Diffstat (limited to 'backend/ValueAnalysis.v')
| -rw-r--r-- | backend/ValueAnalysis.v | 15 |
1 files changed, 2 insertions, 13 deletions
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 3c3aecfd..1f80c293 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -1022,17 +1022,6 @@ Proof. apply UNCH1; auto. intros; red. unfold inj_of_bc; rewrite H0; auto. Qed. -Remark list_forall2_in_l: - forall (A B: Type) (P: A -> B -> Prop) x1 l1 l2, - list_forall2 P l1 l2 -> In x1 l1 -> exists x2, In x2 l2 /\ P x1 x2. -Proof. - induction 1; simpl; intros. -- contradiction. -- destruct H1. - + subst. exists b1; auto. - + exploit IHlist_forall2; eauto. intros (x2 & U & V). exists x2; auto. -Qed. - (** ** Semantic invariant *) Section SOUNDNESS. @@ -1314,7 +1303,7 @@ Proof. exploit hide_stack; eauto. apply pincl_ge; auto. intros (bc1 & A & B & C & D & E & F & G). exploit external_call_match; eauto. - intros. exploit list_forall2_in_l; eauto. intros (av & U & V). + intros. exploit list_forall2_in_left; eauto. intros (av & U & V). eapply D; eauto with va. apply vpincl_ge. apply H3; auto. intros (bc2 & J & K & L & M & N & O & P & Q). exploit (return_from_private_call bc bc2); eauto. @@ -1336,7 +1325,7 @@ Proof. exploit anonymize_stack; eauto. intros (bc1 & A & B & C & D & E & F & G). exploit external_call_match; eauto. - intros. exploit list_forall2_in_l; eauto. intros (av & U & V). eapply D; eauto with va. + intros. exploit list_forall2_in_left; eauto. intros (av & U & V). eapply D; eauto with va. intros (bc2 & J & K & L & M & N & O & P & Q). exploit (return_from_public_call bc bc2); eauto. eapply mmatch_below; eauto. |