Library LambdaTamer.AutoSyntax
Require Import Eqdep List TheoryList.
Require Import LambdaTamer.Ext.
Require Import LambdaTamer.ListUtil.
Require Import LambdaTamer.ListT.
Require Import LambdaTamer.Binding.
Set Implicit Arguments.
Section AutoDep.
Variable dty rty : Set.
Variable term : list dty -> rty -> Set.
Record con : Type := {
quantifySets : listT Set;
varArgs : listT (listS quantifySets -> dty);
termArgs : listT (prodT
(listT (listS quantifySets -> dty))
(listS quantifySets -> rty));
result : listS quantifySets -> rty
}.
Fixpoint unT (ls : listT dty) : list dty :=
match ls with
| nilT => nil
| consT x ls' => cons x (unT ls')
end.
Fixpoint enT (ls : list dty) : listT dty :=
match ls with
| nil => nilT _
| x :: ls' => consT x (enT ls')
end.
Section con.
Variable G : list dty.
Definition makeTm (p : prodT (listT dty) rty) :=
term (unT (fstT p) ++ G) (sndT p).
Variable c : con.
Definition con_builder :=
forall (vals : listS (quantifySets c)),
listF (Var G)
(mapT (fun arg => arg vals) (varArgs c))
-> listF makeTm
(mapT (fun arg =>
pairT
(mapT (fun arg' => arg' vals) (fstT arg))
(sndT arg vals)) (termArgs c))
-> term G (result c vals).
Variable builder : con_builder.
Variable P : forall G t, term G t -> Type.
Definition con_ih :=
forall (vals : listS (quantifySets c))
(vars : listF (Var G)
(mapT (fun arg => arg vals) (varArgs c)))
(terms : listF makeTm
(mapT (fun arg =>
pairT
(mapT (fun arg' => arg' vals) (fstT arg))
(sndT arg vals)) (termArgs c))),
AllF (B:= makeTm) (fun p (e : makeTm p) => P e) terms
-> P (builder vals vars terms).
End con.
Definition conSig := fun c => forall G, con_builder G c.
Variable cons : listT (sigT (fun c => forall G, con_builder G c)).
Variable term_rect : forall (P : forall G t, term G t -> Type),
(forall (G : list dty),
listF (A:= sigT (fun c => forall G, con_builder G c))
(fun con => con_ih (projT2 con G) P) cons)
-> forall G t (e : term G t), P _ _ e.
Lemma appBinders_comm : forall ls1 ls2 ls3,
unT ls1 ++ (ls2 ++ ls3) = (unT ls1 ++ ls2) ++ ls3.
Definition lift'' : forall GpG' t, term GpG' t
-> forall G G', GpG' = G ++ G'
-> forall t', term (G ++ t' :: G') t.
Definition lift' : forall G G' t, term (G ++ G') t
-> forall t', term (G ++ t' :: G') t.
Definition lift : forall t' G t, term G t
-> term (t' :: G) t.
Definition permute' : forall G' t, term G' t
-> forall G1 t1 t2 G2, G' = G1 ++ t1 :: t2 :: G2
-> term (G1 ++ t2 :: t1 :: G2) t.
Definition permute : forall G1 t1 t2 G2 t, term (G1 ++ t1 :: t2 :: G2) t
-> term (G1 ++ t2 :: t1 :: G2) t.
Definition freeVars : forall G t, term G t
-> varInfo G.
Hypothesis term_rect_cons : forall (P : forall G t, term G t -> Type)
ccase c (elm : elemT cons c) G vals vars terms,
term_rect (P:= P) ccase (projT2 c G vals vars terms)
= get_elemT elm (ccase _) _ vars terms
(AllF_prover (fun p (e : makeTm G p) => P (unT (fstT p) ++ G) (sndT p) e)
(fun p (e : makeTm G p) => term_rect ccase e) _).
Lemma var_incl : forall (G0 : list dty)
(x : sigT (fun c : con => forall G : list dty, con_builder G c))
(X : elemT cons x)
(vals : listS (quantifySets (projT1 x)))
(vars : listF (Var G0)
(mapT
(fun arg : listS (quantifySets (projT1 x)) -> dty => arg vals)
(varArgs (projT1 x))))
(terms : listF (makeTm G0)
(mapT
(fun
arg : prodT
(listT (listS (quantifySets (projT1 x)) -> dty))
(listS (quantifySets (projT1 x)) -> rty) =>
pairT
(mapT
(fun arg' : listS (quantifySets (projT1 x)) -> dty =>
arg' vals) (fstT arg)) (sndT arg vals))
(termArgs (projT1 x))))
(vi : varInfo G0)
(H : varInfo_incl (G:=G0) (freeVars (projT2 x G0 vals vars terms)) vi)
(x0 : dty)
(X1 : elemT
(mapT (fun arg : listS (quantifySets (projT1 x)) -> dty => arg vals)
(varArgs (projT1 x))) x0),
varInfo_incl (G:=G0) (Var_freeVars (get_elemT X1 vars)) vi.
Lemma term_incl : forall (G0 : list dty)
(x : sigT (fun c : con => forall G : list dty, con_builder G c))
(X : elemT cons x)
(vals : listS (quantifySets (projT1 x)))
(vars : listF (Var G0)
(mapT
(fun arg : listS (quantifySets (projT1 x)) -> dty => arg vals)
(varArgs (projT1 x))))
(terms : listF (makeTm G0)
(mapT
(fun
arg : prodT
(listT (listS (quantifySets (projT1 x)) -> dty))
(listS (quantifySets (projT1 x)) -> rty) =>
pairT
(mapT
(fun arg' : listS (quantifySets (projT1 x)) -> dty =>
arg' vals) (fstT arg)) (sndT arg vals))
(termArgs (projT1 x))))
(vi : varInfo G0)
(H : varInfo_incl (G:=G0) (freeVars (projT2 x G0 vals vars terms)) vi)
(x0 : prodT (listT dty) rty)
(X1 : elemT
(mapT
(fun
arg : prodT (listT (listS (quantifySets (projT1 x)) -> dty))
(listS (quantifySets (projT1 x)) -> rty) =>
pairT
(mapT
(fun arg' : listS (quantifySets (projT1 x)) -> dty =>
arg' vals) (fstT arg)) (sndT arg vals))
(termArgs (projT1 x))) x0),
varInfo_incl (G:=unT (fstT x0) ++ G0) (freeVars (get_elemT X1 terms))
(varInfo_pad (unT (fstT x0)) (G2:=G0) vi).
Definition strengthen' : forall G t (e : term G t)
vi, varInfo_incl (freeVars e) vi
-> term (varInfo_apply G vi) t.
Definition strengthen G t (e : term G t)
: term (varInfo_apply G (freeVars e)) t :=
strengthen' e (freeVars e) (varInfo_incl_refl _ _).
Definition strengthen_app G1 G2 G3 t (e : term (G1 ++ G2 ++ G3) t)
: term (G1 ++ varInfo_apply _ (varInfo_take (varInfo_drop (freeVars e))) ++ G3) t.
Variable dtyDenote : dty -> Set.
Variable rtyDenote : rty -> Set.
Variable termDenote : forall G t,
term G t
-> Subst dtyDenote G
-> rtyDenote t.
Section meaning.
Variable ts : listT Set.
Variable vars : listT (listS ts -> dty).
Variable sigs : listT (prodT (listT (listS ts -> dty)) (listS ts -> rty)).
Inductive meaning : forall (fargs : listS ts -> listT Set),
(listS ts -> Set) -> Set :=
| Subvar : forall fargs t,
elemT vars t
-> meaning fargs (fun vs => dtyDenote (t vs))
| Subterm : forall fargs p1 p2,
elemT sigs (pairT p1 p2)
-> (forall T, elemT p1 T
-> forall (vs : listS ts), listS (fargs vs) -> dtyDenote (T vs))
-> meaning fargs (fun vs => rtyDenote (p2 vs))
| Construct : forall fargs
(formals : listT (listS ts -> Set))
(output : listS ts -> Set)
(interp : forall (vals : listS ts),
listS (fargs vals)
-> (forall T, elemT formals T -> T vals) -> output vals),
(forall T, elemT formals T -> meaning fargs T)
-> meaning fargs output
| Fun : forall fargs T T',
meaning (fun vs => consT (T vs) (fargs vs)) T'
-> meaning fargs (fun vs => T vs -> T' vs).
Hint Constructors elemT.
Section meaningDenote.
Variable G : list dty.
Variable vs : listS ts.
Definition extendSubst : forall (bound : listT (listS ts -> dty))
fargs (fvs : listS (fargs vs)),
(forall T, elemT bound T
-> forall vs, listS (fargs vs) -> dtyDenote (T vs))
-> Subst dtyDenote G
-> Subst dtyDenote
(unT (mapT (fun arg => arg vs) bound) ++ G).
Fixpoint meaningDenote fargs (T : listS ts -> Set)
(m : meaning fargs T) {struct m}
: (forall t, elemT vars t
-> Var G (t vs))
-> (forall p, elemT sigs p
-> term (unT (mapT (fun arg => arg vs) (fstT p)) ++ G)
(sndT p vs))
-> listS (fargs vs) -> Subst dtyDenote G -> T vs :=
match m in (meaning fargs T)
return ((forall t, elemT vars t
-> Var G (t vs))
-> (forall p, elemT sigs p
-> term (unT (mapT (fun arg => arg vs) (fstT p)) ++ G)
(sndT p vs))
-> listS (fargs vs) -> Subst dtyDenote G -> T vs) with
| Subvar _ _ elm => fun vbuild build actuals s =>
VarDenote (vbuild _ elm) s
| Subterm _ _ _ elm args => fun vbuild build actuals s =>
termDenote (build _ elm) (extendSubst _ actuals args s)
| Construct _ _ _ interp args => fun vbuild build actuals s =>
interp _ actuals (fun _ elm => meaningDenote (args _ elm) vbuild build actuals s)
| Fun _ _ T' m' => fun vbuild build actuals s =>
fun x => meaningDenote m' vbuild build (consF (B:= set) _ x actuals) s
end.
End meaningDenote.
End meaning.
Definition getTerm : forall c G vals,
listF (makeTm G)
(mapT (fun arg =>
pairT
(mapT (fun arg' => arg' vals) (fstT arg))
(sndT arg vals)) (termArgs c))
-> forall p, elemT (termArgs c) p
-> term
(unT
(mapT (fun arg : listS (quantifySets c) -> _ => arg vals)
(fstT p)) ++ G) (sndT p vals).
Definition getVar : forall c G vals,
listF (Var G)
(mapT (fun arg => arg vals) (varArgs c))
-> forall t, elemT (varArgs c) t
-> Var G (t vals).
Definition equations_type := forall c, elemT cons c
-> {m : meaning
(ts:= quantifySets (projT1 c))
(varArgs (projT1 c))
(termArgs (projT1 c))
(fun _ => nilT _)
(fun vs => rtyDenote (result (projT1 c) vs))
| forall G (vals : listS (quantifySets (projT1 c)))
(vars : listF (Var G)
(mapT (fun arg => arg vals) (varArgs (projT1 c))))
(terms : listF (makeTm G)
(mapT (fun arg =>
pairT
(mapT (fun arg' => arg' vals) (fstT arg))
(sndT arg vals)) (termArgs (projT1 c)))) s,
termDenote (projT2 c _ vals vars terms) s
= meaningDenote m (getVar _ _ vars) (getTerm _ _ terms) nilS s}.
Variable equations : equations_type.
Definition retype_Subst : forall G G', G = G'
-> Subst dtyDenote G
-> Subst dtyDenote G'.
Theorem retype_Subst_ident : forall G (H : G = G) (s : Subst dtyDenote G),
retype_Subst H s = s.
Definition retype_term : forall G G', G = G'
-> forall t, term G t
-> term G' t.
Theorem retype_term_ident : forall G (H : G = G) t (e : term G t),
retype_term H e = e.
Fixpoint appSubstF G1 (s1 : listF dtyDenote G1) {struct s1}
: forall G2 (s2 : Subst dtyDenote G2), Subst dtyDenote (unT G1 ++ G2) :=
match s1 in (listF _ G1)
return (forall G2 (s2 : Subst dtyDenote G2), Subst dtyDenote (unT G1 ++ G2)) with
| nilF => fun _ s2 => s2
| consF _ _ x s1' => fun _ s2 => SCons _ x (appSubstF s1' s2)
end.
Lemma extend_app : forall
(ts : listT Set)
(fargs : listS ts -> listT Set)
(vals : listS ts)
(fvals : listS (fargs vals))
(p1 : listT (listS ts -> dty))
(t : forall T : listS ts -> dty,
elemT p1 T -> forall vs : listS ts, listS (fargs vs) -> dtyDenote (T vs)),
exists s',
forall G (s : Subst dtyDenote G),
extendSubst vals fargs fvals t s = appSubstF s' s.
Lemma meaningDenote_change : forall ts
(vars : listT (listS ts -> dty))
(sigs : listT (prodT (listT (listS ts -> dty)) (listS ts -> rty)))
(fargs : listS ts -> listT Set) (T : listS ts -> Set)
(m : meaning vars sigs fargs T)
G1 G2 vals fvals
(vgetter1 : forall t : listS ts -> dty,
elemT vars t ->
Var G1 (t vals))
(vgetter2 : forall t : listS ts -> dty,
elemT vars t ->
Var G2 (t vals))
(getter1 : forall p : prodT (listT (listS ts -> dty)) (listS ts -> rty),
elemT sigs p ->
term
(unT
(mapT (fun arg : listS ts -> dty => arg vals) (fstT p)) ++ G1)
(sndT p vals))
(getter2 : forall p : prodT (listT (listS ts -> dty)) (listS ts -> rty),
elemT sigs p ->
term
(unT
(mapT (fun arg : listS ts -> dty => arg vals) (fstT p)) ++ G2)
(sndT p vals))
(s1 : Subst dtyDenote G1) (s2 : Subst dtyDenote G2),
(forall t (elm : elemT vars t),
VarDenote (vgetter1 _ elm) s1 = VarDenote (vgetter2 _ elm) s2)
-> (forall p (elm : elemT sigs p) s',
termDenote (getter1 _ elm) (appSubstF s' s1)
= termDenote (getter2 _ elm) (appSubstF s' s2))
-> meaningDenote m vgetter1 getter1 fvals s1 =
meaningDenote m vgetter2 getter2 fvals s2.
Section appT.
Variable A : Type.
Fixpoint appT (ls1 : listT A) : listT A -> listT A :=
match ls1 with
| nilT => fun ls2 => ls2
| consT x ls1' => fun ls2 => consT x (appT ls1' ls2)
end.
End appT.
Lemma subst_comm : forall ts vals fp G0 G',
unT
(mapT
(fun arg' : listS ts -> _ =>
arg' vals) fp) ++ unT G0 ++ G'
= unT
(appT
(mapT
(fun arg' : listS ts -> _ =>
arg' vals) fp) G0) ++ G'.
Theorem unT_appT : forall ls1 ls2,
unT ls1 ++ unT ls2 = unT (appT ls1 ls2).
Theorem retype_Subst_cons : forall t x G1 G2
(Heq1 : t :: G1 = t :: G2) (Heq2 : G1 = G2)
s,
retype_Subst Heq1 (SCons t x s) = SCons t x (retype_Subst Heq2 s).
Definition unT_cons : forall ls G0 G',
unT ls ++ unT G0 ++ G' = unT (appT ls G0) ++ G'.
Theorem appSubstF_liftSubst' : forall ts vals t' v G0 G' s fp
(s' : listF dtyDenote (mapT (fun arg' : listS ts -> _ => arg' vals) fp)) Heq1 Heq2,
retype_Subst Heq1 (appSubstF s' (liftSubst' (unT G0) G' s t' v))
= liftSubst'
(unT
(appT
(mapT
(fun arg' : listS ts -> _ => arg' vals)
fp) G0)) G'
(retype_Subst Heq2 (appSubstF s' s)) t' v.
Theorem mapT_appT : forall A (f : A -> _) ls1 ls2,
unT (mapT f ls1) ++ unT ls2
= unT (appT (mapT f ls1) ls2).
Theorem lift''_sound : forall GpG' t (e : term GpG' t)
G G' (Heq : GpG' = unT G ++ G') t' s v,
termDenote (lift'' e _ _ Heq t') (liftSubst' _ _ (retype_Subst Heq s) _ v)
= termDenote e s.
Theorem unT_enT : forall G,
unT (enT G) = G.
Theorem unT_enT_app : forall G G',
G ++ G' = unT (enT G) ++ G'.
Theorem lift'_sound : forall G G' t (e : term (G ++ G') t)
t' s v,
termDenote (lift' _ _ e t') (liftSubst' _ _ s _ v)
= termDenote e s.
Theorem lift_sound : forall G t (e : term G t)
t' v s,
termDenote (lift t' e) (SCons _ v s)
= termDenote e s.
Theorem appSubst_appSubstF : forall G1 (s' : listF dtyDenote G1)
G2 (s1 : Subst dtyDenote G2)
G3 (s2 : Subst dtyDenote G3)
Heq,
retype_Subst Heq (appSubst (appSubstF s' s1) s2)
= appSubstF s' (appSubst s1 s2).
Theorem permute'_sound : forall G' t (e : term G' t)
G1 t1 t2 G2 (Heq : G' = G1 ++ t1 :: t2 :: G2) s1 x1 x2 s2,
termDenote (permute' e _ _ _ _ Heq) (appSubst s1 (SCons _ x1 (SCons _ x2 s2)))
= termDenote e (retype_Subst (sym_eq Heq) (appSubst s1 (SCons _ x2 (SCons _ x1 s2)))).
Theorem permute_sound : forall G1 t1 t2 G2 t (e : term (G1 ++ t1 :: t2 :: G2) t)
s1 x1 x2 s2,
termDenote (permute _ _ _ _ e) (appSubst s1 (SCons _ x1 (SCons _ x2 s2)))
= termDenote e (appSubst s1 (SCons _ x2 (SCons _ x1 s2))).
Lemma appSubstF_strengthen : forall G1 G2
(s' : listF dtyDenote G1) (s : Subst dtyDenote G2) vi Heq,
eq_rect _ (Subst dtyDenote) (appSubstF s' (Subst_strengthen s vi)) _ Heq =
Subst_strengthen (appSubstF s' s) (varInfo_pad _ vi).
Theorem strengthen'_sound : forall G t (e : term G t)
vi (Hinc : varInfo_incl (freeVars e) vi) s,
termDenote (strengthen' e _ Hinc) (Subst_strengthen s vi)
= termDenote e s.
Theorem strengthen_sound : forall G t (e : term G t) s,
termDenote (strengthen e) (Subst_strengthen s (freeVars e))
= termDenote e s.
Theorem strengthen_app_sound : forall G1 G2 G3 t (e : term (G1 ++ G2 ++ G3) t) s1 s2 s3,
termDenote (strengthen_app _ _ _ e) (appSubst s1 (appSubst (Subst_strengthen s2 _) s3))
= termDenote e (appSubst s1 (appSubst s2 s3)).
End AutoDep.
Module Type PARAM.
Parameters dty rty : Set.
Parameter term : list dty -> rty -> Set.
Parameter cons : listT (sigT (fun c => forall G, con_builder term G c)).
Parameter term_rect : forall (P : forall G t, term G t -> Type),
(forall (G : list dty),
listF (A:= sigT (fun c => forall G, con_builder _ G c))
(fun con => con_ih (projT2 con G) P) cons)
-> forall G t (e : term G t), P _ _ e.
Parameter term_rect_cons : forall (P : forall G t, term G t -> Type)
ccase c (elm : elemT cons c) G vals vars terms,
term_rect (P:= P) ccase (projT2 c G vals vars terms)
= get_elemT elm (ccase _) _ vars terms
(AllF_prover (fun p (e : makeTm term G p) => P (unT (fstT p) ++ G) (sndT p) e)
(fun p (e : makeTm term G p) => term_rect ccase e) _).
End PARAM.
Module Type RESULT.
Parameters dty rty : Set.
Parameter term : list dty -> rty -> Set.
Parameter cons : listT (sigT (fun c => forall G, con_builder term G c)).
Parameter term_rect : forall (P : forall G t, term G t -> Type),
(forall (G : list dty),
listF (A:= sigT (fun c => forall G, con_builder _ G c))
(fun con => con_ih (projT2 con G) P) cons)
-> forall G t (e : term G t), P _ _ e.
Parameter term_rect_cons : forall (P : forall G t, term G t -> Type)
ccase c (elm : elemT cons c) G vals vars terms,
term_rect (P:= P) ccase (projT2 c G vals vars terms)
= get_elemT elm (ccase _) _ vars terms
(AllF_prover (fun p (e : makeTm term G p) => P (unT (fstT p) ++ G) (sndT p) e)
(fun p (e : makeTm term G p) => term_rect ccase e) _).
Definition lift'' : forall GpG' t, term GpG' t
-> forall G G', GpG' = G ++ G'
-> forall t', term (G ++ t' :: G') t
:= lift'' term_rect.
Definition lift' : forall G G' t, term (G ++ G') t
-> forall t', term (G ++ t' :: G') t
:= lift' term_rect.
Definition lift : forall t' G t, term G t
-> term (t' :: G) t
:= lift term_rect.
Definition permute : forall G1 t1 t2 G2 t, term (G1 ++ t1 :: t2 :: G2) t
-> term (G1 ++ t2 :: t1 :: G2) t
:= permute term_rect.
Definition freeVars : forall G t, term G t -> varInfo G
:= freeVars term_rect.
Definition strengthen : forall G t (e : term G t), term (varInfo_apply G (freeVars e)) t
:= strengthen term_rect term_rect_cons.
Definition strengthen_app : forall G1 G2 G3 t (e : term (G1 ++ G2 ++ G3) t),
term (G1 ++ varInfo_apply _ (varInfo_take (varInfo_drop (freeVars e))) ++ G3) t
:= strengthen_app term_rect term_rect_cons.
Module Type DENOTE_PARAM.
Parameter dtyDenote : dty -> Set.
Parameter rtyDenote : rty -> Set.
Parameter termDenote : forall G t,
term G t
-> Subst dtyDenote G
-> rtyDenote t.
Parameter equations : equations_type cons rtyDenote termDenote.
End DENOTE_PARAM.
Module Type DENOTE_RESULT.
Parameter dtyDenote : dty -> Set.
Parameter rtyDenote : rty -> Set.
Parameter termDenote : forall G t,
term G t
-> Subst dtyDenote G
-> rtyDenote t.
Axiom lift''_sound : forall GpG' t (e : term GpG' t)
G G' (Heq : GpG' = unT G ++ G') t' s v,
termDenote (lift'' e _ _ Heq t') (liftSubst' _ _ (retype_Subst Heq s) _ v)
= termDenote e s.
Axiom lift'_sound : forall G G' t (e : term (G ++ G') t)
t' s v,
termDenote (lift' _ _ e t') (liftSubst' _ _ s _ v)
= termDenote e s.
Axiom lift_sound : forall G t (e : term G t)
t' v s,
termDenote (lift t' e) (SCons _ v s)
= termDenote e s.
Axiom permute_sound : forall G1 t1 t2 G2 t (e : term (G1 ++ t1 :: t2 :: G2) t)
s1 x1 x2 s2,
termDenote (permute _ _ _ _ e) (appSubst s1 (SCons _ x1 (SCons _ x2 s2)))
= termDenote e (appSubst s1 (SCons _ x2 (SCons _ x1 s2))).
Axiom strengthen_sound : forall G t (e : term G t) s,
termDenote (strengthen e) (Subst_strengthen s (freeVars e))
= termDenote e s.
Axiom strengthen_app_sound : forall G1 G2 G3 t (e : term (G1 ++ G2 ++ G3) t) s1 s2 s3,
termDenote (strengthen_app _ _ _ e) (appSubst s1 (appSubst (Subst_strengthen s2 _) s3))
= termDenote e (appSubst s1 (appSubst s2 s3)).
End DENOTE_RESULT.
Declare Module Denote (Den : DENOTE_PARAM) : DENOTE_RESULT
with Definition dtyDenote := Den.dtyDenote
with Definition rtyDenote := Den.rtyDenote
with Definition termDenote := Den.termDenote.
End RESULT.
Module Make (Param : PARAM) : RESULT
with Definition dty := Param.dty
with Definition rty := Param.rty
with Definition term := Param.term
with Definition cons := Param.cons
with Definition term_rect := Param.term_rect.
Import Param.
Definition lift'' := lift'' term_rect.
Definition lift' := lift' term_rect.
Definition lift := lift term_rect.
Definition permute := permute term_rect.
Definition freeVars := freeVars term_rect.
Definition strengthen := strengthen term_rect term_rect_cons.
Definition strengthen_app := strengthen_app term_rect term_rect_cons.
Module Type DENOTE_PARAM.
Parameter dtyDenote : dty -> Set.
Parameter rtyDenote : rty -> Set.
Parameter termDenote : forall G t,
term G t
-> Subst dtyDenote G
-> rtyDenote t.
Parameter equations : equations_type cons rtyDenote termDenote.
End DENOTE_PARAM.
Module Type DENOTE_RESULT.
Parameter dtyDenote : dty -> Set.
Parameter rtyDenote : rty -> Set.
Parameter termDenote : forall G t,
term G t
-> Subst dtyDenote G
-> rtyDenote t.
Axiom lift''_sound : forall GpG' t (e : term GpG' t)
G G' (Heq : GpG' = unT G ++ G') t' s v,
termDenote (lift'' e _ _ Heq t') (liftSubst' _ _ (retype_Subst Heq s) _ v)
= termDenote e s.
Axiom lift'_sound : forall G G' t (e : term (G ++ G') t)
t' s v,
termDenote (lift' _ _ e t') (liftSubst' _ _ s _ v)
= termDenote e s.
Axiom lift_sound : forall G t (e : term G t)
t' v s,
termDenote (lift t' e) (SCons _ v s)
= termDenote e s.
Axiom permute_sound : forall G1 t1 t2 G2 t (e : term (G1 ++ t1 :: t2 :: G2) t)
s1 x1 x2 s2,
termDenote (permute _ _ _ _ e) (appSubst s1 (SCons _ x1 (SCons _ x2 s2)))
= termDenote e (appSubst s1 (SCons _ x2 (SCons _ x1 s2))).
Axiom strengthen_sound : forall G t (e : term G t) s,
termDenote (strengthen e) (Subst_strengthen s (freeVars e))
= termDenote e s.
Axiom strengthen_app_sound : forall G1 G2 G3 t (e : term (G1 ++ G2 ++ G3) t) s1 s2 s3,
termDenote (strengthen_app _ _ _ e) (appSubst s1 (appSubst (Subst_strengthen s2 _) s3))
= termDenote e (appSubst s1 (appSubst s2 s3)).
End DENOTE_RESULT.
Module Denote (Den : DENOTE_PARAM) : DENOTE_RESULT
with Definition dtyDenote := Den.dtyDenote
with Definition rtyDenote := Den.rtyDenote
with Definition termDenote := Den.termDenote.
Import Den.
Definition lift''_sound := lift''_sound term_rect
term_rect_cons equations.
Definition lift'_sound := lift'_sound term_rect
term_rect_cons equations.
Definition lift_sound := lift_sound term_rect
term_rect_cons equations.
Definition permute_sound := permute_sound term_rect
term_rect_cons equations.
Definition strengthen_sound := strengthen_sound term_rect
term_rect_cons equations.
Definition strengthen_app_sound := strengthen_app_sound term_rect
term_rect_cons equations.
Opaque lift''_sound.
Opaque lift'_sound.
Opaque lift_sound.
Opaque permute_sound.
Opaque strengthen_sound.
Opaque strengthen_app_sound.
Definition dtyDenote := dtyDenote.
Definition rtyDenote := rtyDenote.
Definition termDenote := termDenote.
End Denote.
Definition dty := dty.
Definition rty := rty.
Definition term := term.
Definition cons := cons.
Definition term_rect := term_rect.
Definition term_rect_cons := term_rect_cons.
End Make.
Ltac finish_term_rect := simpl; unfold eq_rect_r; simpl; auto.
Definition unvalify (T1 T2 T3 : Type) (p : prodT (listT (T1 -> T2)) (T1 -> T3))
(vals : T1) : prodT (listT T2) T3 :=
pairT (mapT (fun arg => arg vals) (fstT p)) (sndT p vals).
Section elemify.
Variable A : Type.
Variable B : A -> Type.
Definition elemify : forall (ts : listT A), listF B ts
-> (forall T, elemT ts T -> B T).
End elemify.
Ltac simpl_unvalify := unfold unvalify; simpl; unfold eq_rect_r; simpl.
Section etaF.
Variable A : Type.
Variable B : A -> Type.
Fixpoint etaF (ts : listT A) : listF B ts -> listF B ts :=
match ts return (listF B ts -> listF B ts) with
| nilT => fun _ => nilF _
| consT h t => fun ls => consF _ (headF ls) (etaF (tailF ls))
end.
Theorem etaF_eq : forall ts (ls : listF B ts),
ls = etaF ls.
End etaF.
Section etaT.
Variable A : Type.
Fixpoint all_elemT (ts : listT A) : listT (sigT (elemT ts)) :=
match ts return (listT (sigT (elemT ts))) with
| nilT => nilT _
| consT x ts' =>
consT (existT _ _ (firstT _ _))
(mapT
(fun package =>
match package with
| existT _ elm =>
existT _ _ (nextT _ elm)
end)
(all_elemT ts'))
end.
Theorem etaT : forall (ts : listT A) (package : sigT (elemT ts)),
InT package (all_elemT ts).
End etaT.
Ltac orer :=
match goal with
| [ H : False |- _ ] => tauto
| [ H : _ \/ _ |- _ ] => destruct H
end.
Ltac term_rect_cons_tac :=
intros P ccase c elm;
generalize (etaT (existT _ _ elm)); intro Helm; simpl in Helm;
repeat orer;
match goal with
| [ H : existT _ _ _ = existT _ _ _ |- _ ] =>
injection H; clear H; intros Heq1 Heq2; subst;
generalize (inj_pairT2 _ _ _ _ _ Heq1); clear Heq1; intro; subst;
simpl;
intros G vals;
rewrite (etaF_eq vals);
intros vars terms;
rewrite (etaF_eq vars);
rewrite (etaF_eq terms);
reflexivity
end.
Ltac equation_tac eqn :=
match goal with
| [ H : elemT _ _ |- _ ] =>
inversion H; subst; simpl;
[exists eqn; trivial
| clear H]
end.
Ltac equation_tac_finale :=
match goal with
| [ H : elemT _ _ |- _ ] =>
inversion H
end.
Index
This page has been generated by coqdoc