diff options
Diffstat (limited to 'plugins/setoid_ring/BinList.v')
| -rw-r--r-- | plugins/setoid_ring/BinList.v | 77 |
1 files changed, 32 insertions, 45 deletions
diff --git a/plugins/setoid_ring/BinList.v b/plugins/setoid_ring/BinList.v index 7128280a..b3c59457 100644 --- a/plugins/setoid_ring/BinList.v +++ b/plugins/setoid_ring/BinList.v @@ -1,16 +1,15 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \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. +Set Implicit Arguments. +Local Open Scope positive_scope. Section MakeBinList. Variable A : Type. @@ -18,76 +17,64 @@ Section MakeBinList. Fixpoint jump (p:positive) (l:list A) {struct p} : list A := match p with - | xH => tail l + | xH => tl l | xO p => jump p (jump p l) - | xI p => jump p (jump p (tail l)) + | xI p => jump p (jump p (tl 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)) + | xI p => nth p (jump p (tl l)) end. - Lemma jump_tl : forall j l, tail (jump j l) = jump j (tail l). + Lemma jump_tl : forall j l, tl (jump j l) = jump j (tl l). Proof. - induction j;simpl;intros. - repeat rewrite IHj;trivial. - repeat rewrite IHj;trivial. - trivial. + induction j;simpl;intros; now rewrite ?IHj. Qed. - Lemma jump_Psucc : forall j l, - (jump (Psucc j) l) = (jump 1 (jump j l)). + Lemma jump_succ : forall j l, + jump (Pos.succ 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. + - rewrite !IHj; simpl; now rewrite !jump_tl. + - now rewrite !jump_tl. + - trivial. Qed. - Lemma jump_Pplus : forall i j l, - (jump (i + j) l) = (jump i (jump j l)). + Lemma jump_add : 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. + induction i using Pos.peano_ind; intros. + - now rewrite Pos.add_1_l, jump_succ. + - now rewrite Pos.add_succ_l, !jump_succ, IHi. Qed. - Lemma jump_Pdouble_minus_one : forall i l, - (jump (Pdouble_minus_one i) (tail l)) = (jump i (jump i l)). + Lemma jump_pred_double : forall i l, + jump (Pos.pred_double i) (tl 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. + - now rewrite !jump_tl. + - now rewrite IHi, <- 2 jump_tl, IHi. + - trivial. Qed. - - Lemma nth_jump : forall p l, nth p (tail l) = hd default (jump p l). + Lemma nth_jump : forall p l, nth p (tl l) = hd default (jump p l). Proof. induction p;simpl;intros. - rewrite <-jump_tl;rewrite IHp;trivial. - rewrite <-jump_tl;rewrite IHp;trivial. - trivial. + - now rewrite <-jump_tl, IHp. + - now rewrite <-jump_tl, IHp. + - trivial. Qed. - Lemma nth_Pdouble_minus_one : - forall p l, nth (Pdouble_minus_one p) (tail l) = nth p (jump p l). + Lemma nth_pred_double : + forall p l, nth (Pos.pred_double p) (tl 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. + - now rewrite !jump_tl. + - now rewrite jump_pred_double, <- !jump_tl, IHp. + - trivial. Qed. End MakeBinList. - - |