Require Export List.
Require Export Setoid.
Require Import Omega.
Set Implicit Arguments.

Definition Feq A B (F G : A -> B) := forall x, F x = G x.
Hint Unfold Feq.

Lemma Feq_refl A B : Reflexive (@Feq A B).
red; unfold Feq; trivial.
Qed.

Lemma Feq_sym A B : Symmetric (@Feq A B).
red; unfold Feq; auto.
Qed.

Lemma Feq_trans A B : Transitive (@Feq A B).
red; unfold Feq; intros.
transitivity (y x0); auto.
Qed.

Add Parametric Relation {A B} : (A -> B) (@Feq A B)
reflexivity proved by (@Feq_refl A B)
symmetry proved by (@Feq_sym A B)
transitivity proved by (@Feq_trans A B)
as Feq_setoid.

Definition arity := list Type.

Fixpoint fam (T:arity) : Type :=
    match T with nil => unit | (T::nil) => T | T::lT => (T * fam lT)%type end.

Definition fzero : fam nil := tt.

Definition fsingl (A:Type) : arity := A :: nil.
Definition fcouple (A B:Type) : arity := A :: B:: nil.

Definition fhd {A} {T} : fam (A::T) -> A :=
    match T with nil => fun a => a
               | _ => fun x => fst x
    end.

Definition ftl {A} {T} : fam (A::T) -> fam T :=
    match T with nil => fun a => tt
               | _ => fun x => snd x
    end.

Definition fcons {A} {T} : A -> fam T -> fam (A::T) :=
    fun a => match T with nil => fun x => a | _ => fun x => (a,x) end.

Lemma fhd_simpl : forall {A} {T} (a:A) (p:fam T), fhd (fcons a p) = a.
destruct T; trivial.
Save.

Lemma ftl_simpl : forall {A} {T} (a:A) (p:fam T), ftl (fcons a p) = p.
destruct T; simpl; trivial.
destruct p; trivial.
Save.

Lemma fcons_simpl : forall {A} {T} (p:fam (A::T)),
      fcons (fhd p) (ftl p) = p.
destruct T; simpl; trivial.
destruct p; trivial.
Save.

Hint Resolve @fhd_simpl @ftl_simpl @fcons_simpl.

Lemma fcons_inj : forall A T (p q:A) (l m:fam T),
      fcons p l = fcons q m -> (p=q) /\ (l=m).
split.
transitivity (fhd (fcons p l)); auto.
rewrite H; auto.
transitivity (ftl (fcons p l)); auto.
rewrite H; auto.
Save.
Hint Resolve fcons_inj.

Fixpoint fprodn X (n:nat) : arity :=
    match n with O => nil | S p => X::fprodn X p end.

Fixpoint fcte {X} n x : fam (fprodn X n) :=
    match n with O => tt | S p => fcons x (fcte p x) end.

Fixpoint fproj {X} {n} i : fam (fprodn X n) -> option X :=
  match n return fam (fprodn X n) -> option X
  with O => fun x => None
             | S p => match i with O => fun x => Some (fhd x)
                                  | S j => fun x => fproj j (ftl x)
                       end
  end.

Definition fprod (TI TJ:arity) : arity := TI++TJ.

Fixpoint fpair {TI} {TJ} {struct TI} : fam TI -> fam TJ -> fam (fprod TI TJ) :=
    match TI with nil => fun x y => y
             | (A::T) => fun x y => (fcons (fhd x) (fpair (ftl x) y))
    end.

Fixpoint ffst {TI} {TJ} : fam (fprod TI TJ) -> fam TI :=
    match TI with nil => fun p => tt
             | (A::T) => fun p => fcons (fhd p) (ffst (ftl p))
    end.

Fixpoint fsnd {TI} {TJ} : fam (fprod TI TJ) -> fam TJ :=
    match TI with nil => fun p => p
             | (A::T) => fun p => fsnd (ftl p)
    end.

Lemma ffst_simpl {TI} {TJ} : forall (X:fam TI) (Y:fam TJ), ffst (fpair X Y) = X.
induction TI.
simpl.
destruct X; trivial.
simpl.
intros; repeat rewrite fhd_simpl; repeat rewrite ftl_simpl.
rewrite IHTI; auto.
apply fcons_simpl.
Save.

Lemma fsnd_simpl {TI} {TJ} : forall (X:fam TI) (Y:fam TJ), fsnd (fpair X Y) = Y.
induction TI; auto.
simpl.
intros; repeat rewrite ftl_simpl; auto.
Save.

Lemma fpair_simpl {TI} {TJ} : forall (P:fam (fprod TI TJ)), fpair (ffst P) (fsnd P) = P.
induction TI; auto.
simpl.
intros; repeat rewrite fhd_simpl; repeat rewrite ftl_simpl; auto.
rewrite IHTI.
apply fcons_simpl.
Save.
Hint Resolve @ffst_simpl @fsnd_simpl @fpair_simpl.

Fixpoint fdupn X (n:nat) : arity :=
    match n with O => nil | S p => fprod (fdupn X p) X end.

Fixpoint fdupcte {X} n x : fam (fdupn X n) :=
    match n with O => tt | S p => fpair (fdupcte p x) x end.

Fixpoint fdupproj {X} {n} i : fam (fdupn X n) -> option (fam X) :=
  match n return fam (fdupn X n) -> option (fam X)
  with O => fun x => None
       | S p => match i with O => fun x => Some (fsnd x)
                                  | S j => fun x => fdupproj j (ffst x)
                       end
  end.

Definition Fnth (n:nat) (TI:arity) : Type := nth n TI unit.

Fixpoint Fproj (n:nat) {TI} : fam TI -> Fnth n TI :=
   match n return fam TI -> Fnth n TI
   with O => match TI return fam TI -> Fnth O TI
             with nil => fun p => tt | _ => fun p => fhd p
             end
     | S m => match TI return fam TI -> Fnth (S m) TI
              with nil => fun p => tt | _::T => fun p => @Fproj m T (ftl p)
              end
   end.

Fixpoint fmap (l:list nat) (TI:arity) : arity :=
    match l with nil => nil
               | n::l => Fnth n TI::(fmap l TI)
    end.

Fixpoint fmap_intro (l:list nat) {TI} (X:fam TI) : fam (fmap l TI) :=
   match l return fam (fmap l TI)
   with nil => tt
              | n::l => fcons (Fproj n X) (fmap_intro l X)
   end.

Fixpoint FL (TI : arity) : arity :=
    match TI with nil => nil | A::T => list A :: FL T end.

Fixpoint Fopt (TI : arity) : arity :=
    match TI with nil => nil | A::T => option A :: Fopt T end.

Fixpoint Fnil {TI} : fam (FL TI) :=
    match TI with nil => tt | A::T => fcons nil (@Fnil T) end.

Fixpoint Fcons {TI} : fam TI -> fam (FL TI) -> fam (FL TI) :=
    match TI return fam TI -> fam (FL TI) -> fam (FL TI)
    with nil => fun X P => tt
       | A::T => fun X P => fcons (fhd X::fhd P) (Fcons (ftl X) (ftl P))
    end.

Lemma Fcons_nil TI (p:fam TI) l : Fcons p l = Fnil -> TI=nil.
destruct TI; simpl; auto.
intros H.
assert (fhd (fcons (fhd p :: fhd l) (Fcons (ftl p) (ftl l))) = fhd (fcons nil (@Fnil TI))).
f_equal; trivial.
repeat rewrite fhd_simpl in H0; discriminate.
Save.

Lemma Fcons_inj TI (p q:fam TI) l m :
      Fcons p l = Fcons q m -> p = q /\ l = m.
induction TI; simpl; auto.
destruct p; destruct q; destruct l; destruct m; auto.
intro H.
destruct (fcons_inj _ _ _ _ _ H) as (H1,H2).
injection H1; intros.
destruct (IHTI _ _ _ _ H2) as (Hp,Hl).
split.
transitivity (fcons (fhd p) (ftl p)).
rewrite fcons_simpl; auto.
rewrite H3; rewrite Hp; auto.
rewrite fcons_simpl; auto.
transitivity (fcons (fhd l) (ftl l)).
rewrite fcons_simpl; auto.
rewrite H0; rewrite Hl; auto.
rewrite fcons_simpl; auto.
Save.

Fixpoint Ftl {TI} : fam (FL TI) -> fam (FL TI) :=
    match TI return fam (FL TI) -> fam (FL TI)
    with nil => fun P => tt
      | A::T => fun P => fcons (tl (fhd P)) (Ftl (ftl P))
    end.

Lemma Ftl_simpl {TI} (p:fam TI) l : Ftl (Fcons p l) = l.
induction TI; simpl; auto.
destruct l; trivial.
repeat rewrite fhd_simpl, ftl_simpl.
rewrite IHTI.
apply fcons_simpl.
Save.

Fixpoint Fcons_opt {TI} : fam (Fopt TI) -> fam (FL TI) -> fam (FL TI) :=
   match TI return fam (Fopt TI) -> fam (FL TI) -> fam (FL TI)
    with nil => fun X P => tt
      | A::T => fun X P => fcons (match fhd X with None => fhd P | Some a => a::fhd P end)
                                 (Fcons_opt (ftl X) (ftl P))
    end.

Fixpoint Fhd_opt {TI} : fam (FL TI) -> fam (Fopt TI) :=
   match TI return fam (FL TI) -> fam (Fopt TI)
    with nil => fun P => tt
      | A::T => fun P => fcons (match fhd P with nil => None | a::_ => Some a end)
                               (Fhd_opt (ftl P))
    end.

Fixpoint FL_fst {TI} {TJ} : fam (FL (fprod TI TJ)) -> fam (FL TI) :=
    match TI return fam (FL (fprod TI TJ)) -> fam (FL TI)
    with nil => fun p => tt
             | (A::T) => fun p => fcons (fhd p) (FL_fst (ftl p))
    end.

Fixpoint FL_snd {TI} {TJ} : fam (FL (fprod TI TJ)) -> fam (FL TJ) :=
    match TI return fam (FL (fprod TI TJ)) -> fam (FL TJ)
    with nil => fun p => p
             | (A::T) => fun p => FL_snd (ftl p)
    end.

Definition FL1 A B : fam (FL (fcouple A B)) -> fam (FL (fsingl A)) :=
        @FL_fst (fsingl A) (fsingl B).

Definition FL2 A B : fam (FL (fcouple A B)) -> fam (FL (fsingl B)) :=
        @FL_snd (fsingl A) (fsingl B).

Fixpoint FL_pair {TI TJ} : fam (FL TI) -> fam (FL TJ) -> fam (FL (fprod TI TJ)) :=
    match TI return fam (FL TI) -> fam (FL TJ) -> fam (FL (fprod TI TJ))
    with nil => fun X Y => Y
             | (A::T) => fun X Y => fcons (fhd X) (FL_pair (ftl X) Y)
    end.

Lemma FL_pair_simpl {TI TJ} : forall (P:fam (FL (fprod TI TJ))),
      FL_pair (FL_fst P) (FL_snd P) = P.
induction TI; auto.
simpl.
intro; rewrite fhd_simpl, ftl_simpl.
rewrite IHTI; auto.
apply fcons_simpl.
Save.

Fixpoint FL_cte {X} n (x:list X) : fam (FL (fprodn X n)) :=
    match n return fam (FL (fprodn X n)) with O => tt | S p => fcons x (FL_cte p x) end.

Fixpoint FL_proj {X} {n} i : fam (FL (fprodn X n)) -> list X :=
  match n return fam (FL (fprodn X n)) -> list X
  with O => fun x => nil
       | S p => match i with O => fun x => fhd x
                                | S j => fun x => FL_proj j (ftl x) end
  end.