From 76263149abe2ceb826691f742e9d92ca03b9dcc0 Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Thu, 3 Nov 2016 16:02:07 +0100
Subject: [PATCH] Add more lemmas about zip
---
util/list.v | 54 +++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 54 insertions(+)
diff --git a/util/list.v b/util/list.v
index 17a22147a..8e441bb82 100644
--- a/util/list.v
+++ b/util/list.v
@@ -228,6 +228,60 @@ Section Zip.
}
Qed.
+ Lemma unzip1_pair:
+ forall {T1 T2: eqType} (l: seq T1) (f: T1 -> T2),
+ unzip1 [seq (x, f x) | x <- l] = l.
+ Proof.
+ intros T1 T2.
+ induction l; first by done.
+ by intros f; simpl; f_equal.
+ Qed.
+
+ Lemma unzip2_pair:
+ forall {T1 T2: eqType} (l: seq T1) (f: T1 -> T2),
+ unzip2 [seq (f x, x) | x <- l] = l.
+ Proof.
+ intros T1 T2.
+ induction l; first by done.
+ by intros f; simpl; f_equal.
+ Qed.
+
+ Lemma eq_unzip1:
+ forall {T1 T2: eqType} (l1 l2: seq (T1 * T2)) x0,
+ size l1 = size l2 ->
+ (forall i, i < size l1 -> (fst (nth x0 l1 i)) = (fst (nth x0 l2 i))) ->
+ unzip1 l1 = unzip1 l2.
+ Proof.
+ intros T1 T2.
+ induction l1; simpl; first by destruct l2.
+ intros l2 x0 SIZE ALL.
+ destruct l2; first by done.
+ simpl; f_equal; first by feed (ALL 0).
+ case: SIZE => SIZE.
+ apply IHl1 with (x0 := x0); first by done.
+ intros i LTi.
+ by feed (ALL i.+1);
+ first by rewrite -[X in X < _]addn1 -[X in _ < X]addn1 ltn_add2r.
+ Qed.
+
+ Lemma eq_unzip2:
+ forall {T1 T2: eqType} (l1 l2: seq (T1 * T2)) x0,
+ size l1 = size l2 ->
+ (forall i, i < size l1 -> (snd (nth x0 l1 i)) = (snd (nth x0 l2 i))) ->
+ unzip2 l1 = unzip2 l2.
+ Proof.
+ intros T1 T2.
+ induction l1; simpl; first by destruct l2.
+ intros l2 x0 SIZE ALL.
+ destruct l2; first by done.
+ simpl; f_equal; first by feed (ALL 0).
+ case: SIZE => SIZE.
+ apply IHl1 with (x0 := x0); first by done.
+ intros i LTi.
+ by feed (ALL i.+1);
+ first by rewrite -[X in X < _]addn1 -[X in _ < X]addn1 ltn_add2r.
+ Qed.
+
End Zip.
(* Restate nth_error function from Coq library. *)
--
GitLab