Fin.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Arith_base.

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 (* subterm !!! *) 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.

Fixpoint to_nat {m} (n : t m) : {i | i < m} :=
  match n with
    |@F1 j => exist _ 0 (Lt.lt_0_Sn j)
    |FS p => match to_nat p with |exist _ i P => exist _ (S i) (Lt.lt_n_S _ _ P) end
  end.

of_nat p n answers the p{^ th} element of fin n if p < n or a proof of p >= n else

Fixpoint of_nat (p n : nat) : (t n) + { exists m, p = n + m } :=
  match n with
   |0 => inright _ (ex_intro _ p eq_refl)
   |S n' => match p with
      |0 => inleft _ (F1)
      |S p' => match of_nat p' n' with
        |inleft f => inleft _ (FS f)
        |inright arg => inright _ (match arg with |ex_intro _ m e =>
          ex_intro (fun x => S p' = S n' + x) m (f_equal S e) end)
      end
    end
  end.

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

Fixpoint of_nat_lt {p n : nat} : p < n -> t n :=
  match n with
    |0 => fun H : p < 0 => False_rect _ (Lt.lt_n_O p H)
    |S n' => match p with
      |0 => fun _ => @F1 n'
      |S p' => fun H => FS (of_nat_lt (Lt.lt_S_n _ _ H))
    end
  end.

Lemma of_nat_ext {p}{n} (h h' : p < n) : of_nat_lt h = of_nat_lt h'.p, n:nat
h, h':p < n
of_nat_lt h = of_nat_lt h'
Proof.p, n:nat
h, h':p < n
of_nat_lt h = of_nat_lt h'
 now rewrite (Peano_dec.le_unique _ _ h h').
Qed.

Lemma of_nat_to_nat_inv {m} (p : t m) : of_nat_lt (proj2_sig (to_nat p)) = p.m:nat
p:t m
of_nat_lt (proj2_sig (to_nat p)) = p
Proof.m:nat
p:t m
of_nat_lt (proj2_sig (to_nat p)) = p
induction p; simpl.n:nat
F1 = F1
n:nat
p:t n
IHp:of_nat_lt (proj2_sig (to_nat p)) = p
of_nat_lt
  (proj2_sig
     (let (i, P) := to_nat p in
      exist (fun i0 : nat => i0 < S n) (S i)
        (Lt.lt_n_S i n P))) = FS p
-n:nat
F1 = F1 reflexivity.
-n:nat
p:t n
IHp:of_nat_lt (proj2_sig (to_nat p)) = p
of_nat_lt
  (proj2_sig
     (let (i, P) := to_nat p in
      exist (fun i0 : nat => i0 < S n) (S i)
        (Lt.lt_n_S i n P))) = FS p destruct (to_nat p); simpl in *.n:nat
p:t n
x:nat
l:x < n
IHp:of_nat_lt l = p
FS (of_nat_lt (Lt.lt_S_n x n (Lt.lt_n_S x n l))) =
FS p f_equal.n:nat
p:t n
x:nat
l:x < n
IHp:of_nat_lt l = p
of_nat_lt (Lt.lt_S_n x n (Lt.lt_n_S x n l)) = p subst p.n, x:nat
l:x < n
of_nat_lt (Lt.lt_S_n x n (Lt.lt_n_S x n l)) =
of_nat_lt l apply of_nat_ext.
Qed.

Lemma to_nat_of_nat {p}{n} (h : p < n) : to_nat (of_nat_lt h) = exist _ p h.p, n:nat
h:p < n
to_nat (of_nat_lt h) =
exist (fun i : nat => i < n) p h
Proof.p, n:nat
h:p < n
to_nat (of_nat_lt h) =
exist (fun i : nat => i < n) p h
 revert n h.p:nat
forall (n : nat) (h : p < n),
to_nat (of_nat_lt h) =
exist (fun i : nat => i < n) p h
 induction p; (destruct n ; intros h; [ destruct (Lt.lt_n_O _ h) | cbn]);
 [ | rewrite (IHp _ (Lt.lt_S_n p n h))];  f_equal; apply Peano_dec.le_unique.
Qed.

Lemma to_nat_inj {n} (p q : t n) :
 proj1_sig (to_nat p) = proj1_sig (to_nat q) -> p = q.n:nat
p, q:t n
proj1_sig (to_nat p) = proj1_sig (to_nat q) -> p = q
Proof.n:nat
p, q:t n
proj1_sig (to_nat p) = proj1_sig (to_nat q) -> p = q
 intro H.n:nat
p, q:t n
H:proj1_sig (to_nat p) = proj1_sig (to_nat q)
p = q
 rewrite <- (of_nat_to_nat_inv p), <- (of_nat_to_nat_inv q).n:nat
p, q:t n
H:proj1_sig (to_nat p) = proj1_sig (to_nat q)
of_nat_lt (proj2_sig (to_nat p)) =
of_nat_lt (proj2_sig (to_nat q))
 destruct (to_nat p) as (np,hp), (to_nat q) as (nq,hq); simpl in *.n:nat
p, q:t n
np:nat
hp:np < n
nq:nat
hq:nq < n
H:np = nq
of_nat_lt hp = of_nat_lt hq
 revert hp hq.n:nat
p, q:t n
np, nq:nat
H:np = nq
forall (hp : np < n) (hq : nq < n),
of_nat_lt hp = of_nat_lt hq rewrite H.n:nat
p, q:t n
np, nq:nat
H:np = nq
forall hp hq : nq < n, of_nat_lt hp = of_nat_lt hq apply of_nat_ext.
Qed.

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

Fixpoint weak {m}{n} p (f : t m -> t n) :
  t (p + m) -> t (p + n) :=
match p as p' return t (p' + m) -> t (p' + n) with
  |0 => f
  |S p' => fun x => match x with
     |@F1 n' => fun eq : n' = p' + m => F1
     |@FS n' y => fun eq : n' = p' + m => FS (weak p' f (eq_rect _ t y _ eq))
  end (eq_refl _)
end.

The p{^ th} element of fin m viewed as the p{^ th} element of fin (m + n)

Fixpoint L {m} n (p : t m) : t (m + n) :=
  match p with |F1 => F1 |FS p' => FS (L n p') end.

Lemma L_sanity {m} n (p : t m) : proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p).m, n:nat
p:t m
proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p)
Proof.m, n:nat
p:t m
proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p)
induction p.n, n0:nat
proj1_sig (to_nat (L n F1)) = proj1_sig (to_nat F1)
n, n0:nat
p:t n0
IHp:proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p)
proj1_sig (to_nat (L n (FS p))) =
proj1_sig (to_nat (FS p))
-n, n0:nat
proj1_sig (to_nat (L n F1)) = proj1_sig (to_nat F1) reflexivity.
-n, n0:nat
p:t n0
IHp:proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p)
proj1_sig (to_nat (L n (FS p))) =
proj1_sig (to_nat (FS p)) simpl; destruct (to_nat (L n p)); simpl in *; rewrite IHp.n, n0:nat
p:t n0
x:nat
l:x < n0 + n
IHp:x = proj1_sig (to_nat p)
S (proj1_sig (to_nat p)) =
proj1_sig
  (let (i, P) := to_nat p in
   exist (fun i0 : nat => i0 < S n0) (S i)
     (Lt.lt_n_S i n0 P)) now destruct (to_nat p).
Qed.

The p{^ th} element of fin m viewed as the p{^ th} element of fin (n + m) Really really inefficient !!!

Definition L_R {m} n (p : t m) : t (n + m).m, n:nat
p:t m
t (n + m)
Proof.m, n:nat
p:t m
t (n + m)
induction n.m:nat
p:t m
t (0 + m)
m, n:nat
p:t m
IHn:t (n + m)
t (S n + m)
-m:nat
p:t m
t (0 + m) exact p.
-m, n:nat
p:t m
IHn:t (n + m)
t (S n + m) exact ((fix LS k (p: t k) :=
    match p with
      |@F1 k' => @F1 (S k')
      |FS p' => FS (LS _ p')
    end) _ IHn).
Defined.

The p{^ th} element of fin m viewed as the (n + p){^ th} element of fin (n + m)

Fixpoint R {m} n (p : t m) : t (n + m) :=
  match n with |0 => p |S n' => FS (R n' p) end.

Lemma R_sanity {m} n (p : t m) : proj1_sig (to_nat (R n p)) = n + proj1_sig (to_nat p).m, n:nat
p:t m
proj1_sig (to_nat (R n p)) = n + proj1_sig (to_nat p)
Proof.m, n:nat
p:t m
proj1_sig (to_nat (R n p)) = n + proj1_sig (to_nat p)
induction n.m:nat
p:t m
proj1_sig (to_nat (R 0 p)) = 0 + proj1_sig (to_nat p)
m, n:nat
p:t m
IHn:proj1_sig (to_nat (R n p)) = n + proj1_sig (to_nat p)
proj1_sig (to_nat (R (S n) p)) =
S n + proj1_sig (to_nat p)
-m:nat
p:t m
proj1_sig (to_nat (R 0 p)) = 0 + proj1_sig (to_nat p) reflexivity.
-m, n:nat
p:t m
IHn:proj1_sig (to_nat (R n p)) = n + proj1_sig (to_nat p)
proj1_sig (to_nat (R (S n) p)) =
S n + proj1_sig (to_nat p) simpl; destruct (to_nat (R n p)); simpl in *; rewrite IHn.m, n:nat
p:t m
x:nat
l:x < n + m
IHn:x = n + proj1_sig (to_nat p)
S (n + proj1_sig (to_nat p)) =
S (n + proj1_sig (to_nat p)) now destruct (to_nat p).
Qed.

Fixpoint depair {m n} (o : t m) (p : t n) : t (m * n) :=
match o with
  |@F1 m' => L (m' * n) p
  |FS o' => R n (depair o' p)
end.

Lemma depair_sanity {m n} (o : t m) (p : t n) :
  proj1_sig (to_nat (depair o p)) = n * (proj1_sig (to_nat o)) + (proj1_sig (to_nat p)).m, n:nat
o:t m
p:t n
proj1_sig (to_nat (depair o p)) =
n * proj1_sig (to_nat o) + proj1_sig (to_nat p)
Proof.m, n:nat
o:t m
p:t n
proj1_sig (to_nat (depair o p)) =
n * proj1_sig (to_nat o) + proj1_sig (to_nat p)
induction o ; simpl.n, n0:nat
p:t n
proj1_sig (to_nat (L (n0 * n) p)) =
n * 0 + proj1_sig (to_nat p)
n, n0:nat
o:t n0
p:t n
IHo:proj1_sig (to_nat (depair o p)) =
n * proj1_sig (to_nat o) + proj1_sig (to_nat p)
proj1_sig (to_nat (R n (depair o p))) =
n *
proj1_sig
  (let (i, P) := to_nat o in
   exist (fun i0 : nat => i0 < S n0) (S i)
     (Lt.lt_n_S i n0 P)) + proj1_sig (to_nat p)
-n, n0:nat
p:t n
proj1_sig (to_nat (L (n0 * n) p)) =
n * 0 + proj1_sig (to_nat p) rewrite L_sanity.n, n0:nat
p:t n
proj1_sig (to_nat p) = n * 0 + proj1_sig (to_nat p) now rewrite Mult.mult_0_r.

-n, n0:nat
o:t n0
p:t n
IHo:proj1_sig (to_nat (depair o p)) =
n * proj1_sig (to_nat o) + proj1_sig (to_nat p)
proj1_sig (to_nat (R n (depair o p))) =
n *
proj1_sig
  (let (i, P) := to_nat o in
   exist (fun i0 : nat => i0 < S n0) (S i)
     (Lt.lt_n_S i n0 P)) + proj1_sig (to_nat p) rewrite R_sanity.n, n0:nat
o:t n0
p:t n
IHo:proj1_sig (to_nat (depair o p)) =
n * proj1_sig (to_nat o) + proj1_sig (to_nat p)
n + proj1_sig (to_nat (depair o p)) =
n *
proj1_sig
  (let (i, P) := to_nat o in
   exist (fun i0 : nat => i0 < S n0) (S i)
     (Lt.lt_n_S i n0 P)) + proj1_sig (to_nat p) rewrite IHo.n, n0:nat
o:t n0
p:t n
IHo:proj1_sig (to_nat (depair o p)) =
n * proj1_sig (to_nat o) + proj1_sig (to_nat p)
n + (n * proj1_sig (to_nat o) + proj1_sig (to_nat p)) =
n *
proj1_sig
  (let (i, P) := to_nat o in
   exist (fun i0 : nat => i0 < S n0) (S i)
     (Lt.lt_n_S i n0 P)) + proj1_sig (to_nat p)
  rewrite Plus.plus_assoc.n, n0:nat
o:t n0
p:t n
IHo:proj1_sig (to_nat (depair o p)) =
n * proj1_sig (to_nat o) + proj1_sig (to_nat p)
n + n * proj1_sig (to_nat o) + proj1_sig (to_nat p) =
n *
proj1_sig
  (let (i, P) := to_nat o in
   exist (fun i0 : nat => i0 < S n0) (S i)
     (Lt.lt_n_S i n0 P)) + proj1_sig (to_nat p) destruct (to_nat o); simpl; rewrite Mult.mult_succ_r.n, n0:nat
o:t n0
p:t n
x:nat
l:x < n0
IHo:proj1_sig (to_nat (depair o p)) =
n * proj1_sig (exist (fun i : nat => i < n0) x l) + proj1_sig (to_nat p)
n + n * x + proj1_sig (to_nat p) =
n * x + n + proj1_sig (to_nat p)
    now rewrite (Plus.plus_comm n).
Qed.

Fixpoint eqb {m n} (p : t m) (q : t n) :=
match p, q with
| @F1 m', @F1 n' => EqNat.beq_nat m' n'
| FS _, F1 => false
| F1, FS _ => false
| FS p', FS q' => eqb p' q'
end.

Lemma eqb_nat_eq : forall m n (p : t m) (q : t n), eqb p q = true -> m = n.forall (m n : nat) (p : t m) (q : t n),
eqb p q = true -> m = n
Proof.forall (m n : nat) (p : t m) (q : t n),
eqb p q = true -> m = n
intros m n p; revert n; induction p; destruct q; simpl; intros; f_equal.n, n0:nat
H:PeanoNat.Nat.eqb n n0 = true
n = n0
n, n0:nat
q:t n0
H:false = true
n = n0
n:nat
p:t n
IHp:forall (n1 : nat) (q : t n1), eqb p q = true -> n = n1
n0:nat
H:false = true
n = n0
n:nat
p:t n
IHp:forall (n1 : nat) (q0 : t n1), eqb p q0 = true -> n = n1
n0:nat
q:t n0
H:eqb p q = true
n = n0
-n, n0:nat
H:PeanoNat.Nat.eqb n n0 = true
n = n0 now apply EqNat.beq_nat_true.
-n, n0:nat
q:t n0
H:false = true
n = n0 easy.
-n:nat
p:t n
IHp:forall (n1 : nat) (q : t n1), eqb p q = true -> n = n1
n0:nat
H:false = true
n = n0 easy.
-n:nat
p:t n
IHp:forall (n1 : nat) (q0 : t n1), eqb p q0 = true -> n = n1
n0:nat
q:t n0
H:eqb p q = true
n = n0 eapply IHp.n:nat
p:t n
IHp:forall (n1 : nat) (q0 : t n1), eqb p q0 = true -> n = n1
n0:nat
q:t n0
H:eqb p q = true
eqb p ?q = true eassumption.
Qed.

Lemma eqb_eq : forall n (p q : t n), eqb p q = true <-> p = q.forall (n : nat) (p q : t n), eqb p q = true <-> p = q
Proof.forall (n : nat) (p q : t n), eqb p q = true <-> p = q
apply rect2; simpl; intros.n:nat
PeanoNat.Nat.eqb n n = true <-> F1 = F1
n:nat
f:t n
false = true <-> F1 = FS f
n:nat
f:t n
false = true <-> FS f = F1
n:nat
f, g:t n
H:eqb f g = true <-> f = g
eqb f g = true <-> FS f = FS g
-n:nat
PeanoNat.Nat.eqb n n = true <-> F1 = F1 split; intros ; [ reflexivity | now apply EqNat.beq_nat_true_iff ].
-n:nat
f:t n
false = true <-> F1 = FS f now split.
-n:nat
f:t n
false = true <-> FS f = F1 now split.
-n:nat
f, g:t n
H:eqb f g = true <-> f = g
eqb f g = true <-> FS f = FS g eapply iff_trans.n:nat
f, g:t n
H:eqb f g = true <-> f = g
eqb f g = true <-> ?B
n:nat
f, g:t n
H:eqb f g = true <-> f = g
?B <-> FS f = FS g
 +n:nat
f, g:t n
H:eqb f g = true <-> f = g
eqb f g = true <-> ?B eassumption.
 +n:nat
f, g:t n
H:eqb f g = true <-> f = g
f = g <-> FS f = FS g split.n:nat
f, g:t n
H:eqb f g = true <-> f = g
f = g -> FS f = FS g
n:nat
f, g:t n
H:eqb f g = true <-> f = g
FS f = FS g -> f = g
  *n:nat
f, g:t n
H:eqb f g = true <-> f = g
f = g -> FS f = FS g intros; now f_equal.
  *n:nat
f, g:t n
H:eqb f g = true <-> f = g
FS f = FS g -> f = g apply FS_inj.
Qed.

Lemma eq_dec {n} (x y : t n): {x = y} + {x <> y}.n:nat
x, y:t n
{x = y} + {x <> y}
Proof.n:nat
x, y:t n
{x = y} + {x <> y}
case_eq (eqb x y); intros.n:nat
x, y:t n
H:eqb x y = true
{x = y} + {x <> y}
n:nat
x, y:t n
H:eqb x y = false
{x = y} + {x <> y}
-n:nat
x, y:t n
H:eqb x y = true
{x = y} + {x <> y} left; now apply eqb_eq.
-n:nat
x, y:t n
H:eqb x y = false
{x = y} + {x <> y} right.n:nat
x, y:t n
H:eqb x y = false
x <> y intros Heq.n:nat
x, y:t n
H:eqb x y = false
Heq:x = y
False apply <- eqb_eq in Heq.n:nat
x, y:t n
H:eqb x y = false
Heq:eqb x y = true
False congruence.
Defined.

Definition cast: forall {m} (v: t m) {n}, m = n -> t n.forall m : nat, t m -> forall n : nat, m = n -> t n
Proof.forall m : nat, t m -> forall n : nat, m = n -> t n
refine (fix cast {m} (v: t m) {struct v} :=
 match v in t m' return forall n, m' = n -> t n with
 |F1 => fun n => match n with
   | 0 => fun H => False_rect _ _
   | S n' => fun H => F1
 end
 |FS f => fun n => match n with
   | 0 => fun H => False_rect _ _
   | S n' => fun H => FS (cast f n' (f_equal pred H))
 end
end); discriminate.
Defined.