From c8cba24511fe5f0ffc16fd2f7d7e53c9a1a3a791 Mon Sep 17 00:00:00 2001
From: mohring
Date: Thu, 19 Apr 2001 14:33:41 +0000
Subject: Ajout de fonctions proposees par Cuiht Alvarado

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1630 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Lists/PolyList.v | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index 45ee894fa8..ed64bad707 100644
--- a/theories/Lists/PolyList.v
+++ b/theories/Lists/PolyList.v
@@ -407,6 +407,20 @@ Lemma nth_S_cons :
 Simpl; Auto.
 Save.
 
+Fixpoint nth_error [l:list;n:nat] : (Exc A) :=
+  Cases n l of
+  | O (cons x _) => (Value x)
+  | (S n) (cons _ l) => (nth_error l n)
+  | _ _ => Error 
+  end.
+
+Definition nth_default : A -> list -> nat -> A :=
+  [default,l,n]Cases (nth_error l n) of
+  | (value x) => x
+  | error => default
+  end.
+
+
 (*i
 Lemma nth_In :
   (n:nat)(l:list)(d:A)(lt n (length l))->(In (nth n l d) l).
@@ -423,6 +437,20 @@ Unfold lt; Induction l;
 ].
 i*)
 
+(* Decidable equality on lists *)
+
+
+Lemma list_eq_dec : ((x,y:A){x=y}+{~x=y})->(x,y:list){x=y}+{~x=y}.
+Proof.
+  Induction x; Destruct y; Intros; Auto.
+  Case (H a a0); Intro e.
+  Case (H0 l0); Intro e'.
+  Left; Rewrite e; Rewrite e'; Trivial.
+  Right; Red; Intro.
+  Apply e'; Injection H1; Trivial.
+  Right; Red; Intro.
+  Apply e; Injection H1; Trivial.
+Qed.
 
 (*********************************************)
 (*   Reverse Induction Principle on Lists    *)
-- 
cgit v1.2.3