diff options
Diffstat (limited to 'contrib/setoid_ring/BinList.v')
-rw-r--r-- | contrib/setoid_ring/BinList.v | 58 |
1 files changed, 24 insertions, 34 deletions
diff --git a/contrib/setoid_ring/BinList.v b/contrib/setoid_ring/BinList.v index 0def087f..0d0fe5a4 100644 --- a/contrib/setoid_ring/BinList.v +++ b/contrib/setoid_ring/BinList.v @@ -1,46 +1,36 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + Set Implicit Arguments. Require Import BinPos. +Require Export List. +Require Export ListTactics. Open Scope positive_scope. +Section MakeBinList. + Variable A : Type. + Variable default : A. -Section LIST. - - Variable A:Type. - Variable default:A. - - Inductive list : Type := - | nil : list - | cons : A -> list -> list. - - Infix "::" := cons (at level 60, right associativity). - - Definition hd l := match l with hd :: _ => hd | _ => default end. - - Definition tl l := match l with _ :: tl => tl | _ => nil end. - - Fixpoint jump (p:positive) (l:list) {struct p} : list := + Fixpoint jump (p:positive) (l:list A) {struct p} : list A := match p with - | xH => tl l + | xH => tail l | xO p => jump p (jump p l) - | xI p => jump p (jump p (tl l)) + | xI p => jump p (jump p (tail l)) end. - Fixpoint nth (p:positive) (l:list) {struct p} : A:= + Fixpoint nth (p:positive) (l:list A) {struct p} : A:= match p with - | xH => hd l + | xH => hd default l | xO p => nth p (jump p l) - | xI p => nth p (jump p (tl l)) + | xI p => nth p (jump p (tail l)) end. - Fixpoint rev_append (rev l : list) {struct l} : list := - match l with - | nil => rev - | (cons h t) => rev_append (cons h rev) t - end. - - Definition rev l : list := rev_append nil l. - - Lemma jump_tl : forall j l, tl (jump j l) = jump j (tl l). + Lemma jump_tl : forall j l, tail (jump j l) = jump j (tail l). Proof. induction j;simpl;intros. repeat rewrite IHj;trivial. @@ -71,7 +61,7 @@ Section LIST. Qed. Lemma jump_Pdouble_minus_one : forall i l, - (jump (Pdouble_minus_one i) (tl l)) = (jump i (jump i l)). + (jump (Pdouble_minus_one i) (tail l)) = (jump i (jump i l)). Proof. induction i;intros;simpl. repeat rewrite jump_tl;trivial. @@ -80,7 +70,7 @@ Section LIST. Qed. - Lemma nth_jump : forall p l, nth p (tl l) = hd (jump p l). + Lemma nth_jump : forall p l, nth p (tail l) = hd default (jump p l). Proof. induction p;simpl;intros. rewrite <-jump_tl;rewrite IHp;trivial. @@ -89,7 +79,7 @@ Section LIST. Qed. Lemma nth_Pdouble_minus_one : - forall p l, nth (Pdouble_minus_one p) (tl l) = nth p (jump p l). + forall p l, nth (Pdouble_minus_one p) (tail l) = nth p (jump p l). Proof. induction p;simpl;intros. repeat rewrite jump_tl;trivial. @@ -98,4 +88,4 @@ Section LIST. trivial. Qed. -End LIST. +End MakeBinList. |