# Finite lists as functions with finite ordinal domain

Require Import prelim.

Definition scons {T n} (x : T) (xr : 'I_n -> T) (i : 'I_n.+1) : T :=
match @split 1 n i with
| inl _ => x
| inr j => xr j
end.

Notation "0" := ord0.
Definition S {n} (i : 'I_n) : 'I_n.+1 := rshift 1 i.
Notation "x .: xr" := (scons x xr)
(at level 55, xr at level 56, right associativity).

Lemma scons0 T n (x : T) (xr : 'I_n -> T) :
(x .: xr) 0 = x.
Proof. rewrite/scons. by case: splitP. Qed.

Lemma sconsS T n (x : T) (xr : 'I_n -> T) (i : 'I_n) :
(x .: xr) (S i) = xr i.
Proof.
rewrite/scons. by case: splitP => [[[|]]//=|k]/=[/ord_inj->].
Qed.

Lemma ord_inv n (P : 'I_n.+1 -> Prop) :
P 0 -> (forall x, P (S x)) -> forall x, P x.
Proof.
move=> p0 ps [[|x] h].
- have->: Ordinal h = 0 by exact: ord_inj. exact: p0.
- have->: Ordinal h = S (@Ordinal n x h) by exact: ord_inj. exact: ps.
Qed.

Lemma scons_eta T n (f : 'I_n.+1 -> T) :
f 0 .: f \o S = f.
Proof.
apply: fext => i. rewrite/scons. case: splitP.
- move: i => [[|a] b] [[]//=] _ _. congr f. exact: ord_inj.
- move=> k eqn /=. congr f. exact: ord_inj.
Qed.

Lemma scons_eq T n (f g : 'I_n.+1 -> T) :
f 0 = g 0 -> (forall i : 'I_n, f (S i) = g (S i)) -> f = g.
Proof.
move=> h1 h2. rewrite -[f]scons_eta -[g]scons_eta h1.
congr scons. apply: fext => i /=. exact: h2.
Qed.

Definition scons_simpl := (scons0, sconsS, scons_eta).