semantics.data.fintype

Require Import base.

Fixpoint fin (n : nat) : Type :=
  match n with
  | 0 => False
  | S m => option (fin m)
  end.

Definition scons {X : Type} {n : nat} (x : X) (f : fin n -> X) (m : fin (S n)) : X :=
  match m with
  | None => x
  | Some i => f i
  end.

Notation "f >> g" := (funcomp tt g f) (at level 50) : subst_scope.
Notation "x .: f" := (@scons _ _ x f) (at level 55) : subst_scope.
Open Scope subst_scope.

Definition ren (m n : nat) : Type := fin m -> fin n.

Definition bound {n : nat} : fin n.+1 := None.
Definition null {T} (i : fin 0) : T := match i with end.

Definition shift {n : nat} : ren n n.+1 := Some.

Definition up {m n : nat} (f : ren m n) : ren m.+1 n.+1 :=
  bound .: f >> shift.

Lemma shift_up {m n} (f : ren m n) :
  shift >> up f = f >> shift.
Proof. by []. Qed.

Lemma scons_eta {T} {n : nat} (f : fin n.+1 -> T) :
  f bound .: shift >> f = f.
Proof. by fext=>/=;case. Qed.

Lemma scons_eta_id {n : nat} : bound .: shift = id :> (fin n.+1 -> fin n.+1).
Proof. by fext=>/=;case. Qed.

Lemma scons_comp {T1 T2} {n : nat} (x : T1) (f : fin n -> T1) (g : T1 -> T2) :
  (x .: f) >> g = (g x) .: f >> g.
Proof. by fext=>/=;case. Qed.

Ltac fsimpl :=
  repeat match goal with
    | [|- context[id >> ?f]] => change (id >> f) with f
    | [|- context[?f >> id]] => change (f >> id) with f
    | [|- context[(?f >> ?g) >> ?h]] =>
        change ((f >> g) >> h) with (f >> (g >> h))
    | [|- context[?f >> (?x .: ?g)]] =>
        change (f >> (x .: g)) with g
    | [|- context[?x2 .: shift >> ?f]] =>
        change x2 with (f bound); rewrite (@scons_eta _ _ f)
    | [|- context[?f bound .: ?g]] =>
        change g with (shift >> f); rewrite scons_eta
    | _ => progress (rewrite ?scons_comp ?scons_eta_id)
  end.