diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-01-23 17:30:29 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-01-23 17:30:29 +0100 |
| commit | ee8a92ea19469db7f1747849e2dfb18b1e70538d (patch) | |
| tree | 9c5f311800880e34c53be8a45a2b56440030b8c2 | |
| parent | 897d83b892df7f2e7a0a633ab7c22313c91c1bb9 (diff) | |
| download | compcert-kvx-ee8a92ea19469db7f1747849e2dfb18b1e70538d.tar.gz compcert-kvx-ee8a92ea19469db7f1747849e2dfb18b1e70538d.zip | |
Preuve de app_nonil2 dans PostpassSchedulingproof
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 4205398a..ddc09569 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -41,11 +41,12 @@ Proof. - discriminate.
Qed.
-Lemma app_nonil2 {A: Type} : forall (l': list A) l, l' <> nil -> l ++ l' <> nil.
+Lemma app_nonil2 {A: Type} : forall (l: list A) l', l' <> nil -> l ++ l' <> nil.
Proof.
- induction l'; try contradiction.
- intros. cutrewrite (l ++ a :: l' = (l ++ a :: nil) ++ l'). apply app_nonil.
-Admitted.
+ destruct l.
+ - intros. simpl. auto.
+ - intros. rewrite <- app_comm_cons. discriminate.
+Qed.
Program Definition concat2 (bb bb': bblock) : res bblock :=
match (exit bb) with
|