Instantly share code, notes, and snippets.

# greenrd/gist:334380 Created Mar 16, 2010

 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)))) _).