Library Coq.Vectors.Fin
fin n is a convenient way to represent \
1 .. n\
fin n can be seen as a n-uplet of unit.
F1 is the first element of
the n-uplet. If
f is the k-th element of the (n-1)-uplet,
FS f is the
(k+1)-th element of the n-uplet.
Author: Pierre Boutillier
Institution: PPS, INRIA 12/2010-01/2012-07/2012
Inductive t :
nat -> Set :=
|
F1 :
forall {
n},
t (
S n)
|
FS :
forall {
n},
t n -> t (
S n).
Section SCHEMES.
Definition case0 P (
p:
t 0):
P p :=
match p with |
F1 |
FS _ =>
fun devil =>
False_rect (@
IDProp)
devil end.
Definition caseS' {
n :
nat} (
p :
t (
S n)) :
forall (
P :
t (
S n)
-> Type)
(
P1 :
P F1) (
PS :
forall (
p :
t n),
P (
FS p)),
P p :=
match p with
| @
F1 k =>
fun P P1 PS =>
P1
|
FS pp =>
fun P P1 PS =>
PS pp
end.
Definition caseS (
P:
forall {
n},
t (
S n)
-> Type)
(
P1:
forall n, @
P n F1) (
PS :
forall {
n} (
p:
t n),
P (
FS p))
{
n} (
p:
t (
S n)) :
P p :=
caseS' p P (
P1 n)
PS.
Definition rectS (
P:
forall {
n},
t (
S n)
-> Type)
(
P1:
forall n, @
P n F1) (
PS :
forall {
n} (
p:
t (
S n)),
P p -> P (
FS p)):
forall {
n} (
p:
t (
S n)),
P p :=
fix rectS_fix {
n} (
p:
t (
S n)):
P p:=
match p with
| @
F1 k =>
P1 k
| @
FS 0
pp =>
case0 (
fun f =>
P (
FS f))
pp
| @
FS (
S k)
pp =>
PS pp (
rectS_fix pp)
end.
Definition rect2 (
P :
forall {
n} (
a b :
t n),
Type)
(
H0 :
forall n, @
P (
S n)
F1 F1)
(
H1 :
forall {
n} (
f :
t n),
P F1 (
FS f))
(
H2 :
forall {
n} (
f :
t n),
P (
FS f)
F1)
(
HS :
forall {
n} (
f g :
t n),
P f g -> P (
FS f) (
FS g)) :
forall {
n} (
a b :
t n),
P a b :=
fix rect2_fix {
n} (
a :
t n) {
struct a} :
forall (
b :
t n),
P a b :=
match a with
| @
F1 m =>
fun (
b :
t (
S m)) =>
caseS' b (
P F1) (
H0 _)
H1
| @
FS m a' =>
fun (
b :
t (
S m)) =>
caseS' b (
fun b =>
P (@
FS m a')
b) (
H2 a') (
fun b' =>
HS _ _ (
rect2_fix a' b'))
end.
End SCHEMES.
Definition FS_inj {
n} (
x y:
t n) (
eq:
FS x = FS y):
x = y :=
match eq in _ = a return
match a as a' in t m return match m with |0 =>
Prop |
S n' =>
t n' -> Prop end
with F1 =>
fun _ =>
True |
FS y =>
fun x' =>
x' = y end x with
eq_refl =>
eq_refl
end.
to_nat f = p iff f is the p{^ th} element of fin m.
of_nat p n answers the p{^ th} element of fin n if p < n or a proof of
p >= n else
of_nat_lt p n H answers the p{^ th} element of fin n
it behaves much better than of_nat p n on open term
weak p f answers a function witch is the identity for the p{^ th} first
element of fin (p + m) and FS (FS .. (FS (f k))) for FS (FS .. (FS k))
with p FSs
The p{^ th} element of fin m viewed as the p{^ th} element of
fin (m + n)
The p{^ th} element of fin m viewed as the p{^ th} element of
fin (n + m)
Really really ineficient !!!
The p{^ th} element of fin m viewed as the (n + p){^ th} element of
fin (n + m)