Skip to content

Instantly share code, notes, and snippets.

@greenrd greenrd/gist:334380
Created Mar 16, 2010

Embed
What would you like to do?
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)))) _).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.