From 6ae7da3db058fb6a9d6856519856ecbaf28d3a9d Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Tue, 26 Jul 2022 15:43:31 +0200
Subject: [PATCH] utils: simplification of proofs
Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
src/utils.v | 15 +++------------
1 file changed, 3 insertions(+), 12 deletions(-)
diff --git a/src/utils.v b/src/utils.v
index 32e4c82..f8244f1 100644
--- a/src/utils.v
+++ b/src/utils.v
@@ -9,9 +9,7 @@ Proof.
induction l.
- reflexivity.
- simpl.
- destruct f.
- + discriminate.
- + exact IHl.
+ now destruct f.
Qed.
Lemma nth_error_on_composed_list :
@@ -26,8 +24,7 @@ Proof.
simpl.
lia.
- - rewrite (nth_error_nth' _ d Hlength), Hl, Hi, nth_middle.
- reflexivity.
+ - now rewrite (nth_error_nth' _ d Hlength), Hl, Hi, nth_middle.
Qed.
Lemma map_in_the_middle :
@@ -36,13 +33,7 @@ Lemma map_in_the_middle :
List.nth_error (List.map f l) i = Some (f a).
Proof.
intros A B a d f l lpre lpost i Hl Hi.
-
- assert (List.nth_error l i = Some a) as Hnth.
- apply (nth_error_on_composed_list _ _ d _ lpre lpost);
- assumption.
-
- rewrite (map_nth_error _ i l Hnth).
- reflexivity.
+ now apply map_nth_error, (nth_error_on_composed_list _ _ d _ lpre lpost).
Qed.
Section ListCustomBool.
--
GitLab