diff options
Diffstat (limited to 'plugins/setoid_ring/BinList.v')
-rw-r--r-- | plugins/setoid_ring/BinList.v | 93 |
1 files changed, 93 insertions, 0 deletions
diff --git a/plugins/setoid_ring/BinList.v b/plugins/setoid_ring/BinList.v new file mode 100644 index 00000000..d403c9ef --- /dev/null +++ b/plugins/setoid_ring/BinList.v @@ -0,0 +1,93 @@ +(************************************************************************) +(* 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 Local Scope positive_scope. + +Section MakeBinList. + Variable A : Type. + Variable default : A. + + Fixpoint jump (p:positive) (l:list A) {struct p} : list A := + match p with + | xH => tail l + | xO p => jump p (jump p l) + | xI p => jump p (jump p (tail l)) + end. + + Fixpoint nth (p:positive) (l:list A) {struct p} : A:= + match p with + | xH => hd default l + | xO p => nth p (jump p l) + | xI p => nth p (jump p (tail l)) + end. + + Lemma jump_tl : forall j l, tail (jump j l) = jump j (tail l). + Proof. + induction j;simpl;intros. + repeat rewrite IHj;trivial. + repeat rewrite IHj;trivial. + trivial. + Qed. + + Lemma jump_Psucc : forall j l, + (jump (Psucc j) l) = (jump 1 (jump j l)). + Proof. + induction j;simpl;intros. + repeat rewrite IHj;simpl;repeat rewrite jump_tl;trivial. + repeat rewrite jump_tl;trivial. + trivial. + Qed. + + Lemma jump_Pplus : forall i j l, + (jump (i + j) l) = (jump i (jump j l)). + Proof. + induction i;intros. + rewrite xI_succ_xO;rewrite Pplus_one_succ_r. + rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. + repeat rewrite IHi. + rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite jump_Psucc;trivial. + rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. + repeat rewrite IHi;trivial. + rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite jump_Psucc;trivial. + Qed. + + Lemma jump_Pdouble_minus_one : forall i l, + (jump (Pdouble_minus_one i) (tail l)) = (jump i (jump i l)). + Proof. + induction i;intros;simpl. + repeat rewrite jump_tl;trivial. + rewrite IHi. do 2 rewrite <- jump_tl;rewrite IHi;trivial. + trivial. + Qed. + + + 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. + rewrite <-jump_tl;rewrite IHp;trivial. + trivial. + Qed. + + Lemma nth_Pdouble_minus_one : + 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. + rewrite jump_Pdouble_minus_one. + repeat rewrite <- jump_tl;rewrite IHp;trivial. + trivial. + Qed. + +End MakeBinList. + + |