Library LambdaTamer.Binding
Require Import Bool List TheoryList Eqdep Omega.
Require Import LambdaTamer.ListUtil.
Require Import LambdaTamer.ListT.
Set Implicit Arguments.
Section Subst.
Variable dom : Set.
Inductive Var : list dom -> dom -> Set :=
| First : forall G t, Var (t :: G) t
| Next : forall G t t', Var G t -> Var (t' :: G) t.
Definition VarNil : forall ls (t : dom), Var ls t -> Var (ls ++ nil) t.
Definition liftVar' : forall (G : list dom) t G', Var (G ++ G') t
-> forall t', Var (G ++ t' :: G') t.
Definition liftVar (G : list dom) (t : dom) (v : Var G t) (t' : dom) : Var (t' :: G) t :=
liftVar' nil G v t'.
Fixpoint liftVarEnd (G : list dom) (t : dom) (G' : list dom) (v : Var G t) {struct G'}
: Var (G ++ G') t :=
match G' return (Var (G ++ G') t) with
| nil => VarNil v
| _ :: _ => liftVar' _ _ (liftVarEnd _ v) _
end.
Fixpoint grabVar (G : list dom) (t : dom) (G' : list dom) {struct G} : Var (G ++ t :: G') t :=
match G return (Var (G ++ t :: G') t) with
| nil => First _ _
| _ :: _ => Next _ (grabVar _ _ _)
end.
Definition lastVar G t : Var (G ++ t :: nil) t :=
grabVar _ _ _.
Definition lastVar' G1 G2 t : Var (G1 ++ (G2 ++ t :: nil)) t.
Variable denote : dom -> Type.
Inductive Subst : list dom -> Type :=
| SNil : Subst nil
| SCons : forall t G, denote t -> Subst G -> Subst (t :: G).
Fixpoint appSubst (ts1 : list dom) (s1 : Subst ts1) (ts2 : list dom) (s2 : Subst ts2) {struct s1}
: Subst (ts1 ++ ts2) :=
match s1 in (Subst ts1) return (Subst (ts1 ++ ts2)) with
| SNil => s2
| SCons _ _ x s1' => SCons x (appSubst s1' s2)
end.
Definition head : forall t G, Subst (t :: G) -> denote t.
Definition tail : forall t G, Subst (t :: G) -> Subst G.
Fixpoint revAppN_Subst G1 (s1 : Subst G1) (pos : nat) G2 (s2 : Subst G2) {struct s1}
: Subst (revAppN G1 pos G2) :=
match s1 in (Subst G1) return (Subst (revAppN G1 pos G2)) with
| SNil => s2
| SCons t G v s1' =>
match pos return (Subst (revAppN (t :: G) pos G2)) with
| O => s2
| S pos' => revAppN_Subst s1' pos' (SCons v s2)
end
end.
Fixpoint Subst_drop (G : list dom) (s : Subst G) (n : nat) {struct s}
: Subst (drop G n) :=
match s in (Subst G) return (Subst (drop G n)) with
| SNil => SNil
| SCons t G' v s' =>
match n return (Subst (drop (t :: G') n)) with
| O => SCons v s'
| S n' => Subst_drop s' n'
end
end.
Lemma Subst_revAppN_split' : forall ts1 (s1 : Subst ts1)
pos1 pos2 ts2 (s2 : Subst ts2)
(Heq : revAppN ts1 (pos1 + pos2) ts2
= revAppN (drop ts1 pos1) pos2 (revAppN ts1 pos1 ts2)),
revAppN_Subst s1 (pos1 + pos2) s2
= eq_rect _ Subst
(revAppN_Subst (Subst_drop s1 pos1) pos2 (revAppN_Subst s1 pos1 s2))
_ (sym_eq Heq).
Lemma Subst_revAppN_split : forall ts1 (s1 : Subst ts1)
pos1 pos2 ts2 (s2 : Subst ts2),
revAppN_Subst s1 (pos1 + pos2) s2
= eq_rect _ Subst
(revAppN_Subst (Subst_drop s1 pos1) pos2 (revAppN_Subst s1 pos1 s2))
_ (sym_eq (revAppN_split _ _ _ _)).
Fixpoint VarDenote (G : list dom) (t : dom) (v : Var G t) {struct v}
: Subst G -> denote t :=
match v in (Var G t) return (Subst G -> denote t) with
| First _ _ => fun s => head s
| Next _ _ _ v => fun s => VarDenote v (tail s)
end.
Lemma Subst_invert_nil'
: forall P : Subst nil -> Type,
P SNil ->
forall G s, match G return (Subst G -> _) with
| nil => P
| _ => fun _ => True
end s.
Theorem Subst_invert_nil
: forall P : Subst nil -> Type,
P SNil ->
forall s, P s.
Lemma Subst_invert_cons'
: forall P : forall t G, Subst (t :: G) -> Type,
(forall (t : dom) (G : list dom) (d : denote t) (s : Subst G),
P t G (SCons d s))
-> forall G s, match G return (Subst G -> Type) with
| nil => fun _ => True
| _ => P _ _
end s.
Theorem Subst_invert_cons
: forall P : forall t G, Subst (t :: G) -> Type,
(forall (t : dom) (G : list dom) (d : denote t) (s : Subst G),
P t G (SCons d s))
-> forall t G (s : Subst (t :: G)), P _ _ s.
Theorem inversion_Subst_nil : forall (s : Subst nil),
s = SNil.
Theorem inversion_Subst_cons : forall t G (s : Subst (t :: G)),
exists v, exists s', s = SCons v s'.
End Subst.
Ltac inversion_Subst_nil ls :=
let His := fresh "His" in
(generalize (inversion_Subst_nil ls); intro His;
subst; simpl in *; unfold eq_rect_r in *; simpl in *).
Ltac inversion_Subst_cons ls :=
let His := fresh "His"
with h := fresh "h"
with t := fresh "t" in
(destruct (inversion_Subst_cons ls) as [h [t His]];
subst; simpl in *;
repeat rewrite eq_rect_r_ident; repeat rewrite eq_rect_ident).
Ltac inversion_Subst s := inversion_Subst_nil s || inversion_Subst_cons s.
Ltac inversion_Subst_any :=
match goal with
| [ ls : Subst _ nil |- _ ] => inversion_Subst_nil ls
| [ ls : Subst _ (_ :: _) |- _ ] => inversion_Subst_cons ls
end.
Section Var_invert.
Variable dom : Set.
Lemma Var_invert'
: forall P : forall (t' : dom) l t, Var (t' :: l) t -> Prop,
(forall G t, P t G t (First G t)) ->
(forall G t t' v,
P t' G t (Next t' v)) ->
forall l t v,
match l return (Var l t -> Prop) with
| nil => fun _ => True
| _ => fun v => P _ _ _ v
end v.
Theorem Var_invert
: forall P : forall (t' : dom) l t, Var (t' :: l) t -> Prop,
(forall G t, P t G t (First G t)) ->
(forall G t t' v,
P t' G t (Next t' v)) ->
forall t' l t v, P t' l t v.
Definition permuteVar : forall (G1 : list dom) t1 t2 G2 t, Var (G1 ++ t1 :: t2 :: G2) t
-> Var (G1 ++ t2 :: t1 :: G2) t.
Definition frontVar' : forall G1 (t : dom) G2 t',
Var (G1 +++ t :: G2) t'
-> Var (t :: G1 +++ G2) t'.
Definition frontVar : forall G1 (t : dom) G2 t',
Var (G1 ++ t :: G2) t'
-> Var (t :: G1 ++ G2) t'.
Section substVar.
Variable dom2 : Set.
Variable term : list dom -> dom2 -> Set.
Variable inj : dom -> dom2.
Variable var : forall G t, Var G t -> term G (inj t).
Variable lift : forall a G t, term G t -> term (a :: G) t.
Definition substVar' : forall (G : list dom) t' G' t, Var (G ++ t' :: G') t
-> term G' (inj t') -> term (G ++ G') (inj t).
Definition substVar : forall t' (G : list dom) t, Var (t' :: G) t
-> term G (inj t') -> term G (inj t).
End substVar.
Definition retype_Var : forall t t', t = t'
-> forall G, Var (dom:= dom) G t
-> Var G t'.
Theorem retype_Var_ident : forall G t (H : t = t) (k : Var G t),
retype_Var H k = k.
Lemma Var_split : forall t G t' (v : Var (t :: G) t'),
(t = t' /\ forall Heq : t = t', v = retype_Var Heq (First _ _))
\/ exists v', v = Next _ v'.
End Var_invert.
Ltac inversion_Var elm :=
let Heq := fresh "Heq"
with His := fresh "His"
with v' := fresh "v'" in
(destruct (Var_split elm) as [[Heq His] | [v' His]];
[subst; generalize (His (refl_equal _)); clear His; intro His;
repeat rewrite retype_Var_ident in His
| idtac];
subst; simpl in *;
repeat rewrite eq_rect_r_ident; repeat rewrite eq_rect_ident);
repeat rewrite eq_rect_ident.
Ltac inversion_Var_any :=
match goal with
| [ v : Var _ _ |- _ ] => inversion v; fail
| [ v : Var _ _ |- _ ] => inversion_Var v
end.
Ltac simpl_Binding := repeat progress
(repeat inversion_Subst_any;
repeat inversion_Var_any;
simpl in *; intuition).
Section VarConvert.
Variables dom1 dom2 : Set.
Variable convert : dom1 -> dom2.
Fixpoint VarConvert (G : list dom1) (t : dom1) (v : Var G t) {struct v}
: Var (map convert G) (convert t) :=
match v in (Var G t) return (Var (map convert G) (convert t)) with
| First _ _ => First _ _
| Next _ _ _ v' => Next _ (VarConvert v')
end.
End VarConvert.
Section Subst_lr.
Variables dom1 dom2 : Set.
Variable denote1 : dom1 -> Type.
Variable denote2 : dom2 -> Type.
Variable compile : dom1 -> dom2.
Variable val_lr : forall (t : dom1), denote1 t -> denote2 (compile t) -> Prop.
Inductive Subst_lr : forall G, Subst denote1 G -> Subst denote2 (map compile G) -> Prop :=
| Slr_Nil : Subst_lr (SNil _) (SNil _)
| Slr_Cons : forall t G (v : denote1 t) (s : Subst _ G) cv cs,
val_lr v cv
-> Subst_lr s cs
-> Subst_lr (SCons _ v s) (SCons _ cv cs).
Lemma Subst_lr_Var : forall G t (v : Var G t) s s',
Subst_lr s s'
-> val_lr (VarDenote v s) (VarDenote (VarConvert compile v) s').
Definition liftSubst' : forall G G', Subst denote1 (G ++ G')
-> forall t, denote1 t -> Subst denote1 (G ++ t :: G').
Theorem liftSubst'_sound : forall G G' (s : Subst denote1 (G ++ G'))
t' (v0 : denote1 t')
t (v : Var (G ++ G') t),
VarDenote (liftVar' G G' v t') (liftSubst' _ _ s v0) =
VarDenote v s.
Lemma VarNil_sound : forall G t (v : Var G t) (s' : Subst denote1 _),
VarDenote (VarNil v)
(appSubst s' (SNil _))
= VarDenote v s'.
Theorem grabVar_sound : forall G t G' s x s',
VarDenote (grabVar G t G') (appSubst (denote:= denote1) s (SCons _ x s')) = x.
Theorem lastVar_sound : forall G1 G2 t s1 s2 x,
VarDenote (lastVar (G1 ++ G2) t)
(appSubst (appSubst s1 s2) (SCons t x (SNil denote1))) = x.
Lemma appSubst_liftSubst' : forall G (s : Subst denote1 G)
a h G' (s' : Subst denote1 G'),
appSubst s (SCons a h s')
= liftSubst' _ _ (appSubst s s') h.
Theorem permuteVar_sound : forall (G1 : list dom1) t1 t2 G2 t
(v : Var (G1 ++ t1 :: t2 :: G2) t) (s1 : Subst denote1 _) x1 x2 s2,
VarDenote (permuteVar _ _ _ _ v) (appSubst s1 (SCons _ x1 (SCons _ x2 s2)))
= VarDenote v (appSubst s1 (SCons _ x2 (SCons _ x1 s2))).
End Subst_lr.
Section SubstU_lr.
Variables dom : Set.
Variables denote1 denote2 : dom -> Type.
Variable val_lr : forall (t : dom), denote1 t -> denote2 t -> Prop.
Inductive SubstU_lr : forall G, Subst denote1 G -> Subst denote2 G -> Prop :=
| SlrU_Nil : SubstU_lr (SNil _) (SNil _)
| SlrU_Cons : forall t G (v : denote1 t) (s : Subst _ G) cv cs,
val_lr v cv
-> SubstU_lr s cs
-> SubstU_lr (SCons _ v s) (SCons _ cv cs).
Lemma SubstU_lr_Var : forall G t (v : Var G t) s s',
SubstU_lr s s'
-> val_lr (VarDenote v s) (VarDenote v s').
End SubstU_lr.
Section multiOp.
Variables dty rty : Set.
Variable term : list dty -> rty -> Set.
Variable dtyDenote : dty -> Type.
Variable rtyDenote : rty -> Type.
Variable termDenote : forall G t, term G t -> Subst dtyDenote G -> rtyDenote t.
Lemma Subst_decomp : forall t G (s1 s2 : Subst dtyDenote (t :: G)),
head s1 = head s2
-> tail s1 = tail s2
-> s1 = s2.
Lemma cast_SCons_head : forall t x G (s : Subst dtyDenote G)
G' (Heq : t :: G = t :: G'),
head (t:= t) (G:= G') (eq_rect _ (Subst dtyDenote) (SCons t x s) _ Heq)
= x.
Lemma cast_SCons_tail : forall t x G (s : Subst dtyDenote G)
G' (Heq : t :: G = t :: G') Heq',
tail (t:= t) (G:= G') (eq_rect _ (Subst dtyDenote) (SCons t x s) _ Heq)
= eq_rect _ (Subst dtyDenote) s _ Heq'.
Lemma appSubst_decomp : forall G1 G2 (s1 : Subst dtyDenote G1) (s2 : Subst dtyDenote G2)
G2' (Heq : G1 ++ G2 = G1 ++ G2') Heq',
eq_rect _ (Subst dtyDenote) (appSubst s1 s2) _ Heq
= appSubst s1 (eq_rect _ (Subst dtyDenote) s2 _ Heq').
Lemma appSubst_nil : forall G (s : Subst dtyDenote G) Heq,
s = eq_rect _ (Subst _) (appSubst s (SNil _)) _ Heq.
Lemma appSubst_nil' : forall G (s : Subst dtyDenote G) Heq,
appSubst s (SNil _) = eq_rect _ (Subst dtyDenote) s _ Heq.
Theorem appSubst_assoc : forall G1 (s1 : Subst dtyDenote G1)
G2 (s2 : Subst dtyDenote G2)
G3 (s3 : Subst dtyDenote G3)
Heq,
appSubst s1 (appSubst s2 s3)
= eq_rect _ (Subst dtyDenote) (appSubst (appSubst s1 s2) s3) _ Heq.
Theorem appSubst_assoc' : forall G1 (s1 : Subst dtyDenote G1)
G2 (s2 : Subst dtyDenote G2)
G3 (s3 : Subst dtyDenote G3)
Heq,
appSubst (appSubst s1 s2) s3
= eq_rect _ (Subst dtyDenote) (appSubst s1 (appSubst s2 s3)) _ Heq.
Lemma revAppN_Subst_app : forall G1 (s1 : Subst dtyDenote G1) pos,
exists G1', exists s1', forall G2,
exists Heq : revAppN G1 pos G2 = G1' ++ G2,
forall (s2 : Subst dtyDenote G2),
revAppN_Subst s1 pos s2
= eq_rect _ (Subst dtyDenote)
(appSubst s1' s2)
_ (sym_eq Heq).
Lemma termDenote_ass : forall G1 G2 G3 t (op : term ((G1 ++ G2) ++ G3) t) s1 s2 s3 Heq,
termDenote op (appSubst (appSubst s1 s2) s3)
= termDenote (eq_rect _ (fun G => term G _) op _ Heq) (appSubst s1 (appSubst s2 s3)).
Hint Resolve app_middle.
Lemma termDenote_cons_ass : forall t' G1 G2 G3 t (op : term (G1 ++ t' :: G2 ++ G3) t) s1 x s2 s3 Heq,
termDenote op (appSubst s1 (SCons _ x (appSubst s2 s3)))
= termDenote (eq_rect _ (fun G => term G _) op _ Heq) (appSubst (appSubst s1 (SCons _ x (SNil _))) (appSubst s2 s3)).
Definition termNil : forall G t,
term (G ++ nil) t
-> term G t.
Implicit Arguments termNil [G t].
Theorem lastVar'_sound : forall G1 G2 t (s1 : Subst dtyDenote G1) s2 x,
VarDenote
(lastVar' G1 G2 t)
(appSubst s1 (appSubst s2 (SCons _ x (SNil _))))
= x.
Section lift.
Variable lift' : forall G G' t, term (G ++ G') t
-> forall t', term (G ++ t' :: G') t.
Definition liftEnd G' G t (op : term G t) : term (G ++ G') t.
Definition liftEnd' G'' G G' t (op : term (G ++ G') t) : term (G ++ G' ++ G'') t.
Definition liftMiddle G'' G G' t (op : term (G ++ G') t) : term (G ++ G'' ++ G') t.
Hypothesis 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 liftEnd_sound : forall G' G t
(op : term G t) s1 s2,
termDenote (liftEnd G' op) (appSubst s1 s2)
= termDenote op s1.
Implicit Arguments liftEnd' [G G' t].
Theorem liftEnd'_sound : forall G'' G G' t (op : term (G ++ G') t) s1 s2 s3,
termDenote (liftEnd' G'' op) (appSubst s1 (appSubst s2 s3))
= termDenote op (appSubst s1 s2).
Implicit Arguments liftMiddle [G G' t].
Theorem liftMiddle_sound : forall G'' G G' t (op : term (G ++ G') t)
s1 s2 s3,
termDenote (liftMiddle G'' op) (appSubst s1 (appSubst s2 s3))
= termDenote op (appSubst s1 s3).
Theorem liftMiddle_cons_sound : forall G'' t' G G' t (op : term (t' :: G ++ G') t)
x1 s1 s2 s3,
termDenote (liftMiddle (G:= t' :: G) G'' op) (SCons _ x1 (appSubst s1 (appSubst s2 s3)))
= termDenote op (SCons _ x1 (appSubst s1 s3)).
End lift.
Section permute.
Variable permute : forall G1 t1 t2 G2 t, term (G1 ++ t1 :: t2 :: G2) t
-> term (G1 ++ t2 :: t1 :: G2) t.
Definition front' : forall t' t G2 G1 G3 (lin : term (G1 ++ G2 ++ t' :: G3) t),
term (G1 ++ t' :: G2 ++ G3) t.
Definition front t' t G1 G2 (lin : term (G1 ++ t' :: G2) t)
: term (t' :: G1 ++ G2) t :=
front' t' G1 nil G2 lin.
Definition embed' : forall t' t G2 G1 G3 (lin : term (G1 ++ t' :: G2 ++ G3) t),
term (G1 ++ G2 ++ t' :: G3) t.
Definition embed t' t G1 G2 (lin : term (t' :: G1 ++ G2) t)
: term (G1 ++ t' :: G2) t :=
embed' t' G1 nil G2 lin.
Implicit Arguments embed [t' t G1 G2].
Definition multiSwap G2 G1 G3 t (lin : term (G1 ++ G2 ++ G3) t)
: term (G2 ++ G1 ++ G3) t.
Implicit Arguments multiSwap [G2 G1 G3 t].
Hypothesis 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))).
Theorem front'_sound : forall t' t G2 G1 G3 (lin : term (G1 ++ G2 ++ t' :: G3) t)
s1 x s2 s3,
termDenote (front' _ _ _ _ lin) (appSubst s1 (SCons _ x (appSubst s2 s3)))
= termDenote lin (appSubst s1 (appSubst s2 (SCons _ x s3))).
Implicit Arguments front [t' t G1 G2].
Theorem front_sound : forall t' t G1 G2 (lin : term (G1 ++ t' :: G2) t)
x s1 s2,
termDenote (front lin) (SCons _ x (appSubst s1 s2))
= termDenote lin (appSubst s1 (SCons _ x s2)).
Theorem embed'_sound : forall t' t G2 G1 G3 (lin : term (G1 ++ t' :: G2 ++ G3) t)
s1 x s2 s3,
termDenote (embed' _ _ _ _ lin) (appSubst s1 (appSubst s2 (SCons _ x s3)))
= termDenote lin (appSubst s1 (SCons _ x (appSubst s2 s3))).
Theorem embed_sound : forall t' t G1 G2 (lin : term (t' :: G1 ++ G2) t)
x s1 s2,
termDenote (embed lin) (appSubst s1 (SCons _ x s2))
= termDenote lin (SCons _ x (appSubst s1 s2)).
Definition eq_cons : forall ls1 ls2 (a : dty), ls1 = ls2 -> a :: ls1 = a :: ls2.
Theorem cast_cons : forall (P : list dty -> Type) (a : dty) ls1 ls2 (v : P (a :: ls1)) (Heq : ls1 = ls2),
eq_rect _ (fun ls => P (a :: ls)) v _ Heq
= eq_rect _ P v _ (eq_cons _ Heq).
Theorem multiSwap_sound : forall G2 G1 G3 t (lin : term (G1 ++ G2 ++ G3) t)
s1 s2 s3,
termDenote (multiSwap lin) (appSubst s2 (appSubst s1 s3))
= termDenote lin (appSubst s1 (appSubst s2 s3)).
Definition eq_app : forall ls1 ls2 (G : list dty), ls1 = ls2 -> G ++ ls1 = G ++ ls2.
Theorem cast_app : forall (P : list dty -> Type) (G : list dty) ls1 ls2 (v : P (G ++ ls1)) (Heq : ls1 = ls2),
eq_rect _ (fun ls => P (G ++ ls)) v _ Heq
= eq_rect _ P v _ (eq_app _ Heq).
End permute.
End multiOp.
Implicit Arguments termNil [dty rty G t].
Implicit Arguments front [dty rty term t' t G1 G2].
Implicit Arguments embed [dty rty term t' t G1 G2].
Implicit Arguments multiSwap [dty rty term G2 G1 G3 t].
Implicit Arguments liftEnd [dty rty term G t].
Implicit Arguments liftEnd' [dty rty term G t].
Implicit Arguments liftMiddle [dty rty term G G' t].
Implicit Arguments front_sound [dty rty term dtyDenote rtyDenote termDenote permute t' t G1 G2].
Implicit Arguments embed_sound [dty rty term dtyDenote rtyDenote termDenote permute t' t G1 G2].
Implicit Arguments liftEnd_sound [dty rty term dtyDenote rtyDenote termDenote lift'].
Implicit Arguments liftEnd'_sound [dty rty term dtyDenote rtyDenote termDenote lift'].
Implicit Arguments liftMiddle_sound [dty rty term dtyDenote rtyDenote termDenote lift'].
Implicit Arguments liftMiddle_cons_sound [dty rty term dtyDenote rtyDenote termDenote lift'].
Implicit Arguments multiSwap_sound [dty rty term dtyDenote rtyDenote termDenote permute].
Section strengthen.
Variable dom : Set.
Fixpoint varInfo (G : list dom) : Set :=
match G with
| nil => unit
| _ :: G' => (bool * varInfo G')%type
end.
Fixpoint varInfo_incl (G : list dom) : varInfo G -> varInfo G -> Prop :=
match G return (varInfo G -> varInfo G -> Prop) with
| nil => fun _ _ => True
| _ :: _ => fun vi1 vi2 => implb (fst vi1) (fst vi2) = true /\ varInfo_incl _ (snd vi1) (snd vi2)
end.
Implicit Arguments varInfo_incl [G].
Fixpoint varInfo_none (G : list dom) : varInfo G :=
match G return (varInfo G) with
| nil => tt
| _ :: G' => (false, varInfo_none G')
end.
Fixpoint varInfo_all (G : list dom) : varInfo G :=
match G return (varInfo G) with
| nil => tt
| _ :: G' => (true, varInfo_all G')
end.
Fixpoint varInfo_pad (G1 : list dom) : forall G2, varInfo G2 -> varInfo (G1 ++ G2) :=
match G1 return (forall G2, varInfo G2 -> varInfo (G1 ++ G2)) with
| nil => fun _ vi => vi
| _ :: G1' => fun _ vi => (true, varInfo_pad G1' _ vi)
end.
Fixpoint varInfo_drop (G2 G1 : list dom) {struct G1} : varInfo (G1 ++ G2) -> varInfo G2 :=
match G1 return (varInfo (G1 ++ G2) -> varInfo G2) with
| nil => fun vi => vi
| _ :: _ => fun vi => varInfo_drop _ _ (snd vi)
end.
Fixpoint varInfo_keep (G2 G1 : list dom) {struct G1} : varInfo (G1 ++ G2) -> varInfo (G1 ++ G2) :=
match G1 return (varInfo (G1 ++ G2) -> varInfo (G1 ++ G2)) with
| nil => fun _ => varInfo_all _
| _ :: _ => fun vi => (fst vi, varInfo_keep _ _ (snd vi))
end.
Fixpoint varInfo_take (G1 G2 : list dom) {struct G1} : varInfo (G1 ++ G2) -> varInfo G1 :=
match G1 return (varInfo (G1 ++ G2) -> varInfo G1) with
| nil => fun _ => tt
| _ :: _ => fun vi => (fst vi, varInfo_take _ _ (snd vi))
end.
Fixpoint varInfo_app (G1 G2 : list dom) {struct G1} : varInfo G1 -> varInfo G2 -> varInfo (G1 ++ G2) :=
match G1 return (varInfo G1 -> varInfo G2 -> varInfo (G1 ++ G2)) with
| nil => fun _ vi2 => vi2
| _ :: _ => fun vi1 vi2 => (fst vi1, varInfo_app _ _ (snd vi1) vi2)
end.
Fixpoint Var_freeVars (G : list dom) (t : dom) (v : Var G t) {struct v}
: varInfo G :=
match v in (Var G t) return (varInfo G) with
| First _ _ => (true, varInfo_none _)
| Next _ _ _ v' => (false, Var_freeVars v')
end.
Fixpoint varInfo_apply (G : list dom) : varInfo G -> list dom :=
match G return (varInfo G -> list dom) with
| nil => fun _ => nil
| t :: G' => fun vi =>
if fst vi
then t :: varInfo_apply G' (snd vi)
else varInfo_apply G' (snd vi)
end.
Theorem varInfo_apply_pad : forall G1 G2 (vi : varInfo G2),
varInfo_apply _ (varInfo_pad G1 _ vi)
= G1 ++ varInfo_apply _ vi.
Theorem varInfo_all_incl : forall G (vi : varInfo G),
varInfo_incl vi (varInfo_all _).
Hint Resolve varInfo_all_incl.
Theorem varInfo_keep_incl : forall G1 G2 (vi : varInfo (G1 ++ G2)),
varInfo_incl vi (varInfo_keep _ _ vi).
Theorem varInfo_incl_take G1 G2 (vi : varInfo (G1 ++ G2))
: varInfo_incl vi (varInfo_app _ _ (varInfo_take _ _ vi) (varInfo_all G2)).
Theorem varInfo_incl_split : forall G1 G2 (vi1 vi2 : varInfo (G1 ++ G2)),
varInfo_incl (varInfo_take _ _ vi1) (varInfo_take _ _ vi2)
-> varInfo_incl (varInfo_drop _ _ vi1) (varInfo_drop _ _ vi2)
-> varInfo_incl vi1 vi2.
Theorem varInfo_take_app : forall G1 G2 (vi1 : varInfo G1) (vi2 : varInfo G2),
varInfo_take _ _ (varInfo_app _ _ vi1 vi2) = vi1.
Theorem varInfo_drop_app : forall G1 G2 (vi1 : varInfo G1) (vi2 : varInfo G2),
varInfo_drop _ _ (varInfo_app _ _ vi1 vi2) = vi2.
Theorem varInfo_incl_take_drop G1 G2 G3 (vi : varInfo (G1 ++ G2 ++ G3))
: varInfo_incl vi
(varInfo_app _ _
(varInfo_all G1)
(varInfo_app _ _
(varInfo_take _ _ (varInfo_drop _ _ vi))
(varInfo_all G3))).
Theorem varInfo_apply_all : forall G (vi : varInfo G),
G = varInfo_apply _ (varInfo_all G).
Hint Resolve varInfo_apply_all.
Theorem varInfo_apply_take G1 G2 (vi : varInfo (G1 ++ G2))
: varInfo_apply G1 (varInfo_take _ _ vi) ++ G2
= varInfo_apply (G1 ++ G2)
(varInfo_app _ _
(varInfo_take _ _ vi)
(varInfo_all G2)).
Theorem varInfo_apply_drop G1 G2 (vi : varInfo G2)
: varInfo_apply (G1 ++ G2)
(varInfo_app _ _
(varInfo_all G1) vi)
= G1 ++ varInfo_apply G2 vi.
Theorem varInfo_apply_take_drop G1 G2 G3 (vi : varInfo (G1 ++ G2 ++ G3))
: G1 ++ varInfo_apply G2 (varInfo_take _ _ (varInfo_drop _ _ vi)) ++ G3
= varInfo_apply (G1 ++ G2 ++ G3)
(varInfo_app _ _
(varInfo_all G1)
(varInfo_app _ _
(varInfo_take _ _ (varInfo_drop _ _ vi))
(varInfo_all G3))).
Lemma strengthen_First : forall G t vi,
varInfo_incl (Var_freeVars (First G t)) vi
-> Var (t :: varInfo_apply G (snd vi)) t
-> Var (varInfo_apply (t :: G) vi) t.
Lemma strengthen_Next_true : forall G t t' vi,
fst vi = true
-> Var (t' :: varInfo_apply G (snd vi)) t
-> Var (varInfo_apply (t' :: G) vi) t.
Implicit Arguments strengthen_Next_true [G t t' vi].
Lemma strengthen_Next_false : forall G t t' vi,
fst vi = false
-> Var (varInfo_apply G (snd vi)) t
-> Var (varInfo_apply (t' :: G) vi) t.
Implicit Arguments strengthen_Next_false [G t t' vi].
Fixpoint Var_strengthen (G : list dom) (t : dom) (v : Var G t) {struct v}
: forall (vi : varInfo G), varInfo_incl (Var_freeVars v) vi -> Var (varInfo_apply G vi) t :=
match v in (Var G t) return (forall (vi : varInfo G), varInfo_incl (Var_freeVars v) vi -> Var (varInfo_apply G vi) t) with
| First _ _ => fun vi Hscoped => strengthen_First Hscoped (First _ _)
| Next _ _ _ v' => fun vi Hscoped =>
match fst vi as b return (fst vi = b -> _) with
| true => fun Heq => strengthen_Next_true Heq (Next _ (Var_strengthen v' _ (proj2 Hscoped)))
| false => fun Heq => strengthen_Next_false Heq (Var_strengthen v' _ (proj2 Hscoped))
end (refl_equal _)
end.
Fixpoint varInfo_join (G : list dom) : varInfo G -> varInfo G -> varInfo G :=
match G return (varInfo G -> varInfo G -> varInfo G) with
| nil => fun _ _ => tt
| _ :: G' => fun vi1 vi2 => (orb (fst vi1) (fst vi2), varInfo_join _ (snd vi1) (snd vi2))
end.
Implicit Arguments varInfo_join [G].
Theorem varInfo_join_incl : forall G (vi : varInfo G)
vi1, varInfo_incl vi vi1
-> forall vi2, varInfo_incl vi vi2
-> varInfo_incl vi (varInfo_join vi1 vi2).
Hint Resolve varInfo_join_incl.
Theorem varInfo_join_incl1 : forall G (vi1 vi2 : varInfo G),
varInfo_incl vi1 (varInfo_join vi1 vi2).
Hint Resolve varInfo_join_incl1.
Theorem varInfo_join_incl2 : forall G (vi1 vi2 : varInfo G),
varInfo_incl vi1 (varInfo_join vi2 vi1).
Hint Resolve varInfo_join_incl2.
Theorem varInfo_double_join_incl : forall G (vi1 vi2 vi : varInfo G),
varInfo_incl vi1 vi2
-> varInfo_incl (varInfo_join vi1 vi) (varInfo_join vi2 vi).
Hint Resolve varInfo_double_join_incl.
Theorem varInfo_fold_incl_acc' : forall G (ls : list (varInfo G)) (vi1 vi2 : varInfo G),
varInfo_incl vi1 vi2
-> varInfo_incl
(fold_left (varInfo_join (G:= _)) ls vi1)
(fold_left (varInfo_join (G:= _)) ls vi2).
Hint Resolve varInfo_fold_incl_acc'.
Theorem varInfo_incl_trans : forall G (v1 v2 v3 : varInfo G),
varInfo_incl v1 v2
-> varInfo_incl v2 v3
-> varInfo_incl v1 v3.
Hint Resolve varInfo_incl_trans.
Theorem varInfo_fold_incl_acc : forall G (vi2 : varInfo G) (ls : list (varInfo G)) (vi1 : varInfo G),
varInfo_incl (fold_left (varInfo_join (G:= _)) ls vi1) vi2
-> varInfo_incl vi1 vi2.
Hint Resolve varInfo_fold_incl_acc.
Theorem varInfo_incl_refl : forall G (vi : varInfo G),
varInfo_incl vi vi.
Hint Resolve varInfo_incl_refl.
Theorem varInfo_fold_incl_acc'' : forall G (vi2 : varInfo G) (ls : list (varInfo G)) (vi : varInfo G),
varInfo_incl vi (fold_left (varInfo_join (G:= _)) ls vi).
Hint Resolve varInfo_fold_incl_acc''.
Theorem varInfo_fold_incl_ls : forall G (vi2 : varInfo G) (ls : list (varInfo G)) (vi1 : varInfo G),
varInfo_incl (fold_left (varInfo_join (G:= _)) ls vi1) vi2
-> forall vi, In vi ls
-> varInfo_incl vi vi2.
Theorem varInfo_incl_drop : forall G1 G2 (vi1 : varInfo (G1 ++ G2)) vi2,
varInfo_incl (varInfo_drop _ _ vi1) vi2
-> varInfo_incl vi1 (varInfo_pad _ _ vi2).
Variable denote : dom -> Type.
Lemma strengthen_SCons_true : forall G t' vi,
fst vi = true
-> Subst denote (t' :: varInfo_apply G (snd vi))
-> Subst denote (varInfo_apply (t' :: G) vi).
Implicit Arguments strengthen_SCons_true [G t' vi].
Lemma strengthen_SCons_false : forall G t' vi,
fst vi = false
-> Subst denote (varInfo_apply G (snd vi))
-> Subst denote (varInfo_apply (t' :: G) vi).
Implicit Arguments strengthen_SCons_false [G t' vi].
Fixpoint Subst_strengthen (G : list dom) (s : Subst denote G) {struct s}
: forall (vi : varInfo G), Subst denote (varInfo_apply G vi) :=
match s in (Subst _ G) return (forall (vi : varInfo G), Subst denote (varInfo_apply G vi)) with
| SNil => fun _ => SNil _
| SCons _ _ x s' => fun vi =>
match fst vi as b return (fst vi = b -> _) with
| true => fun Heq => strengthen_SCons_true Heq (SCons _ x (Subst_strengthen s' (snd vi)))
| false => fun Heq => strengthen_SCons_false Heq (Subst_strengthen s' (snd vi))
end (refl_equal _)
end.
Theorem Subst_strengthen_all : forall (G : list dom) s Heq,
eq_rect _ (Subst denote) (Subst_strengthen s (varInfo_all G)) _ Heq = s.
Theorem Var_strengthen_sound : forall G t (v : Var G t) vi
(Hscoped : varInfo_incl (Var_freeVars v) vi) s,
VarDenote (Var_strengthen v vi Hscoped) (Subst_strengthen s vi)
= VarDenote v s.
End strengthen.
Implicit Arguments frontVar [dom G1 t G2 t'].
Implicit Arguments varInfo_join [dom G].
Implicit Arguments varInfo_pad [dom G2].
Implicit Arguments varInfo_drop [dom G1 G2].
Implicit Arguments varInfo_keep [dom G1 G2].
Implicit Arguments varInfo_take [dom G1 G2].
Implicit Arguments varInfo_incl [dom G].
Implicit Arguments varInfo_app [dom G1 G2].
Index
This page has been generated by coqdoc