diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-27 17:45:08 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-27 17:45:08 +0100 |
| commit | 0b1ffa332effdc452b1c76dcbcc738908360f5a8 (patch) | |
| tree | c974542ccfa18914fa702cbb64851ca240d9fa89 /mppa_k1c/abstractbb | |
| parent | 25f47289ff5d9b497d45d3f4efbf4c5df56829a9 (diff) | |
| download | compcert-kvx-0b1ffa332effdc452b1c76dcbcc738908360f5a8.tar.gz compcert-kvx-0b1ffa332effdc452b1c76dcbcc738908360f5a8.zip | |
dealing with permutations
Diffstat (limited to 'mppa_k1c/abstractbb')
| -rw-r--r-- | mppa_k1c/abstractbb/Parallelizability.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/mppa_k1c/abstractbb/Parallelizability.v b/mppa_k1c/abstractbb/Parallelizability.v index b6d1f142..065c0922 100644 --- a/mppa_k1c/abstractbb/Parallelizability.v +++ b/mppa_k1c/abstractbb/Parallelizability.v @@ -79,6 +79,24 @@ Proof. + intros H1; rewrite H1; simpl; auto. Qed. +Lemma prun_iw_app_None p1: forall m1 old p2, + prun_iw p1 m1 old = None -> + prun_iw (p1++p2) m1 old = None. +Proof. + induction p1; simpl; try congruence. + intros; destruct (macro_prun _ _ _); simpl; auto. +Qed. + +Lemma prun_iw_app_Some p1: forall m1 old m2 p2, + prun_iw p1 m1 old = Some m2 -> + prun_iw (p1++p2) m1 old = prun_iw p2 m2 old. +Proof. + induction p1; simpl; try congruence. + intros; destruct (macro_prun _ _ _); simpl; auto. + congruence. +Qed. + + End PARALLEL. End ParallelSemantics. |