gistfile1.txt

Inductive TupleT : nat -> Type :=
nilT : TupleT 0
| consT {n} A : (A -> TupleT n) -> TupleT (S n).

Require Import Relations.

Inductive TupleT_direct_subterm : relation (sigT TupleT) :=
  TupleT_sub n A (x : A) F : TupleT_direct_subterm (existT _ n (F x)) (existT _ _ (consT A F)).

Require Import Subterm.

Program Instance wf_TupleT_subterm : WellFounded (clos_trans _ TupleT_direct_subterm).
Next Obligation.
  solve_subterm.
Qed.

Require Import Equations.

Equations constTupleT (A : Set) n : TupleT n :=
constTupleT A (S _) := consT A (const (constTupleT A _));
constTupleT _ _     := nilT.

Inductive Tuple : forall n, TupleT n -> Type :=
  nil : Tuple _ nilT
| cons {n A} (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F).

Derive Subterm for Tuple.

Inductive TupleMap : forall n, TupleT n -> TupleT n -> Type :=
  tmNil : TupleMap _ nilT nilT
| tmCons {n} {A B} (F : A -> TupleT n) (G : B -> TupleT n)
  : (forall x, sigT (TupleMap _ (F x) ∘ G)) -> TupleMap _ (consT A F) (consT B G).

Equations myId {n} {T : TupleT n} : TupleMap _ T T :=
myId ?(S _) (consT _ _) := tmCons _ _ (fun x => existT (TupleMap _ _ ∘ _) _ myId);
myId _      _           := tmNil.

Inductive TupleMap_direct_subterm
  : forall n (T U : TupleT n) m (V W : TupleT m), TupleMap _ T U -> TupleMap _ V W -> Prop
    := TupleMap_direct_subterm_0_1 n {A B} (F : A -> TupleT n) (G : B -> TupleT n)
    (H : forall x, sigT (TupleMap _ (F x) ∘ G)) (x : A)
    : TupleMap_direct_subterm _ _ (G (projT1 (H _))) _ _ _ (projT2 (H x)) (tmCons _ _ H).

Open Scope type_scope.

Definition TupleMap_subterm
  := clos_trans _
  (fun i j : {index : {n : nat & TupleT n * TupleT n} & TupleMap _ (fst (projT2 index)) (snd (projT2 index))} 
    => TupleMap_direct_subterm _ _ _ _ _ _ (projT2 i) (projT2 j)).

Definition TupleMap_superrect (P : forall n t t0, TupleMap n t t0 -> Type)
  : P _ _ _ tmNil ->
  (forall n A B (F : A -> TupleT n) (G : B -> TupleT n)
    (s : forall x, sigT (TupleMap _ (F x) ∘ G))
    (r : forall x, P _ _ _ (projT2 (s x))),
    P _ _ _ (tmCons F G s))
  -> forall n t t0 (tm : TupleMap n t t0), P _ _ _ tm.
Proof.
  intros P f f0.
  fix IH 4.
  intros.
  destruct tm; [ | apply f0 ]; auto.
Defined.

Instance TupleMap_rect_pack n t t0 : DependentEliminationPackage (TupleMap n t t0) :=
  { elim_type := _ ; elim := TupleMap_superrect }.

Ltac deSig H := generalize H;
  repeat apply simplification_existT2;
  let H1 := fresh in
    intro H1; rewrite H1; auto.

Ltac subst_trans_sym H H1 V := injection (eq_trans H (eq_sym H1)); intros; subst V.

Program Instance well_founded_TupleMap_subterm : WellFounded TupleMap_subterm.
Next Obligation.
  Require Import Wellfounded.
  intros ; apply wf_clos_trans;
  red ; intros; simp_exists.
  dependent induction X.
    split.
    simpl.
    intros.
    inversion H2.

    split.
    simpl.
    intros.
    simp_exists.
    dependent destruction H2.
    subst_trans_sym H5 H A.
    subst_trans_sym H6 H0 B.
    assert (F0 = F) by deSig H9.
    generalize dependent s.
    generalize dependent H2.
    replace G0 with G by deSig H10.
    rewrite H11.
    intros.
    injection (JMeq_eq (JMeq_trans H1 (JMeq_sym H8))).
    intro H12.
    apply (r x).
      congruence.

      transitivity (G (projT1 (H2 x))).
        deSig H12.

        auto.

      deSig H12.
Qed.

Derive Signature for TupleMap. (* What is this for? *)

Instance TupleMap_Recursor {n} {T U : TupleT n} : Recursor (TupleMap _ T U) :=
  { rec_type := λ tm, Π (P : Π n T U (tm : TupleMap n T U), Type) z s, P _ _ _ tm ;
    rec := λ tm P z s, TupleMap_superrect P z s _ _ _ tm }.

Equations(nocomp noind) myComp {n} {A B C : TupleT n} (tm1 : TupleMap _ B C) (tm2 : TupleMap _ A B)
: TupleMap _ A C :=
myComp n A B C tm1 tm2 by rec tm2 :=
myComp ?(0) ?(nilT) ?(nilT) ?(nilT) tmNil tmNil := tmNil;
myComp ?(S _) ?(consT _ _) ?(consT _ _) ?(consT _ _) (tmCons ?(G) H g) (tmCons F G f)
:= tmCons _ _ (fun x => existT (fun y => TupleMap _ (_ y)) (projT1 (g (projT1 (f x)))) _).