From 51b3e27b67686927ba4f4d55b26b8d4a932b8dfd Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 30 Jun 2016 15:30:21 +0200
Subject: [PATCH] Some properties of imap

---
 theories/list.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index 0d7f6cea..59b7bda9 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1265,6 +1265,21 @@ Proof.
     take_app_alt by (rewrite ?app_length, ?take_length, ?Hk; lia).
 Qed.
 
+(** ** Properties of the [imap] function *)
+Lemma imap_cons {B} (f : nat → A → B) x l :
+  imap f (x :: l) = f 0 x :: imap (f ∘ S) l.
+Proof.
+  unfold imap. simpl. f_equal. generalize 0.
+  induction l; intros n; simpl; repeat (auto||f_equal).
+Qed.
+Lemma imap_ext {B} (f g : nat → A → B) l :
+  (∀ i x, f i x = g i x) →
+  imap f l = imap g l.
+Proof.
+  unfold imap. intro EQ. generalize 0.
+  induction l; simpl; intros n; f_equal; auto.
+Qed.
+
 (** ** Properties of the [mask] function *)
 Lemma mask_nil f βs : mask f βs (@nil A) = [].
 Proof. by destruct βs. Qed.
-- 
GitLab