From ea6b2801cebe4f2a02cb1b07fc7caed0c5c24288 Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@gmail.com>
Date: Thu, 11 Feb 2016 09:48:21 -0800
Subject: [PATCH] a few more functions.

---
 theories/Data/List.v  | 12 ++++++++++++
 theories/Data/Nat.v   |  6 ++++++
 theories/Data/PList.v | 13 +++++++++++--
 3 files changed, 29 insertions(+), 2 deletions(-)

diff --git a/theories/Data/List.v b/theories/Data/List.v
index e6f84e7c..3de8220c 100644
--- a/theories/Data/List.v
+++ b/theories/Data/List.v
@@ -58,6 +58,7 @@ Section EqDec.
   Qed.
 End EqDec.
 
+(* Specialized induction rules *)
 Lemma list_ind_singleton
 : forall {T : Type} (P : list T -> Prop)
          (Hnil : P nil)
@@ -69,6 +70,17 @@ Proof.
   destruct ls. eauto. eauto.
 Qed.
 
+Lemma list_rev_ind
+  : forall T (P : list T -> Prop),
+    P nil ->
+    (forall l ls, P ls -> P (ls ++ l :: nil)) ->
+    forall ls, P ls.
+Proof.
+  clear. intros. rewrite <- rev_involutive.
+  induction (rev ls).
+  apply H.
+  simpl. auto.
+Qed.
 
 Section AllB.
   Variable T : Type.
diff --git a/theories/Data/Nat.v b/theories/Data/Nat.v
index c25c0af9..1a40c0f5 100644
--- a/theories/Data/Nat.v
+++ b/theories/Data/Nat.v
@@ -107,3 +107,9 @@ Global Instance Injective_S (a b : nat) : Injective (S a = S b) :=
 }.
 abstract (inversion 1; auto).
 Defined.
+
+Definition nat_get_eq (n m : nat) (pf : unit -> n = m) : n = m :=
+  match PeanoNat.Nat.eq_dec n m with
+  | left pf => pf
+  | right bad => match bad (pf tt) with end
+  end.
\ No newline at end of file
diff --git a/theories/Data/PList.v b/theories/Data/PList.v
index 01b187b1..1e984864 100644
--- a/theories/Data/PList.v
+++ b/theories/Data/PList.v
@@ -2,7 +2,7 @@ Require Import ExtLib.Structures.Functor.
 Require Import ExtLib.Structures.Applicative.
 Require Import ExtLib.Data.POption.
 
-Set Printing Universes.
+Set Universe Polymorphism.
 
 Section plist.
   Polymorphic Universe i.
@@ -24,7 +24,6 @@ Section plist.
     | pcons l ls => pcons l (app ls ls')
     end.
 
-
   Polymorphic Definition hd (ls : plist) : poption T :=
     match ls with
     | pnil => pNone
@@ -55,6 +54,13 @@ Section plist.
     | pcons l ls0 => if p l then anyb p ls0 else false
     end.
 
+  Polymorphic Fixpoint nth_error (ls : plist) (n : nat) : poption T :=
+    match n , ls with
+    | 0 , pcons l _ => pSome l
+    | S n , pcons _ ls => nth_error ls n
+    | _ , _ => pNone
+    end.
+
   Section folds.
     Polymorphic Universe j.
     Context {U : Type@{j}}.
@@ -80,6 +86,9 @@ Arguments pcons {_} _ _.
 Arguments pIn {_} _ _.
 Arguments anyb {_} _ _.
 Arguments allb {_} _ _.
+Arguments fold_left {_ _} _ _ _.
+Arguments fold_right {_ _} _ _ _.
+Arguments nth_error {_} _ _.
 
 Section pmap.
   Polymorphic Universe i j.