From 18a60d7a8ae87aa64c73f9ac03c785b12f8bd25a Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 10 Jul 2011 22:04:16 -0700 Subject: [PATCH] General: add ilist_ins --- src/General.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/General.v b/src/General.v index 53e3753..541dc6f 100644 --- a/src/General.v +++ b/src/General.v @@ -912,6 +912,19 @@ Lemma ilist_app {T}{F}{l1:list T}(v1:IList T F l1) : forall {l2:list T}(v2:IList apply IHl1; auto. Defined. +Definition ilist_ins {T}{F}{l:list T} z (fz:F z) : forall n (il:IList T F l), IList T F (list_ins n z l). + induction l; simpl. + intros. + destruct n; simpl. + apply ICons; [ apply fz | apply INil ]. + apply ICons; [ apply fz | apply INil ]. + intros. + destruct n; simpl. + apply ICons; auto. + inversion il; subst. + apply ICons; auto. + Defined. + Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z := match il with | INil => nil -- 1.7.10.4