1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
Set Implicit Arguments.
10
Require Import BinPos.
12
Require Export ListTactics.
13
Open Local Scope positive_scope.
19
Fixpoint jump (p:positive) (l:list A) {struct p} : list A :=
22
| xO p => jump p (jump p l)
23
| xI p => jump p (jump p (tail l))
26
Fixpoint nth (p:positive) (l:list A) {struct p} : A:=
29
| xO p => nth p (jump p l)
30
| xI p => nth p (jump p (tail l))
33
Lemma jump_tl : forall j l, tail (jump j l) = jump j (tail l).
35
induction j;simpl;intros.
36
repeat rewrite IHj;trivial.
37
repeat rewrite IHj;trivial.
41
Lemma jump_Psucc : forall j l,
42
(jump (Psucc j) l) = (jump 1 (jump j l)).
44
induction j;simpl;intros.
45
repeat rewrite IHj;simpl;repeat rewrite jump_tl;trivial.
46
repeat rewrite jump_tl;trivial.
50
Lemma jump_Pplus : forall i j l,
51
(jump (i + j) l) = (jump i (jump j l)).
54
rewrite xI_succ_xO;rewrite Pplus_one_succ_r.
55
rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
57
rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite jump_Psucc;trivial.
58
rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
59
repeat rewrite IHi;trivial.
60
rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite jump_Psucc;trivial.
63
Lemma jump_Pdouble_minus_one : forall i l,
64
(jump (Pdouble_minus_one i) (tail l)) = (jump i (jump i l)).
66
induction i;intros;simpl.
67
repeat rewrite jump_tl;trivial.
68
rewrite IHi. do 2 rewrite <- jump_tl;rewrite IHi;trivial.
73
Lemma nth_jump : forall p l, nth p (tail l) = hd default (jump p l).
75
induction p;simpl;intros.
76
rewrite <-jump_tl;rewrite IHp;trivial.
77
rewrite <-jump_tl;rewrite IHp;trivial.
81
Lemma nth_Pdouble_minus_one :
82
forall p l, nth (Pdouble_minus_one p) (tail l) = nth p (jump p l).
84
induction p;simpl;intros.
85
repeat rewrite jump_tl;trivial.
86
rewrite jump_Pdouble_minus_one.
87
repeat rewrite <- jump_tl;rewrite IHp;trivial.