Library Binding
Require Import List TheoryList Eqdep Omega.
Set Implicit Arguments.
Theorem eq_rec_r_ident : forall (A : Type) (x : A) (P : A -> Set)
(H : P x) (H0 : x = x), eq_rec_r P H H0 = H.
intros.
rewrite (UIP_refl _ _ H0).
trivial.
Qed.
Theorem eq_rect_r_ident : forall (A : Type) (x : A) (P : A -> Type)
(H : P x) (H0 : x = x), eq_rect_r P H H0 = H.
intros.
rewrite (UIP_refl _ _ H0).
trivial.
Qed.
Theorem eq_rect_ident : forall (A : Type) (x : A) (P : A -> Type)
(H : P x) (H0 : x = x), eq_rect _ P H _ H0 = H.
intros.
rewrite (UIP_refl _ _ H0).
trivial.
Qed.
Section Subst.
Variable dom : Set.
Variable denote : dom -> Type.
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.
Inductive Subst : list dom -> Type :=
| SNil : Subst nil
| SCons : forall t G, denote t -> Subst G -> Subst (t :: G).
Definition head : forall t G, Subst (t :: G) -> denote t.
inversion 1; subst; trivial.
Defined.
Definition tail : forall t G, Subst (t :: G) -> Subst G.
inversion 1; subst; trivial.
Defined.
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.
intros.
destruct s; trivial.
Qed.
Theorem Subst_invert_nil
: forall P : Subst nil -> Type,
P SNil ->
forall s, P s.
intros.
generalize (Subst_invert_nil' P); intuition.
generalize (X1 nil); auto.
Qed.
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.
intros.
destruct s; trivial.
Qed.
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.
intros.
generalize (Subst_invert_cons' P); intuition.
generalize (X1 (t :: G)); auto.
Qed.
Theorem inversion_Subst_nil : forall (s : Subst nil),
s = SNil.
intros.
pattern s.
apply Subst_invert_nil.
trivial.
Qed.
Theorem inversion_Subst_cons : forall t G (s : Subst (t :: G)),
exists v, exists s', s = SCons v s'.
intros.
pattern t, G, s.
apply Subst_invert_cons.
eauto.
Qed.
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.
intros.
destruct v; auto.
Qed.
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.
intros.
generalize (Var_invert' P).
intuition.
generalize (H1 (t' :: l)).
trivial.
Qed.
Definition liftVar' : forall (G : list dom) t G', Var (G ++ G') t
-> forall t', Var (G ++ t' :: G') t.
induction G; simpl; intuition.
apply Next; trivial.
inversion H; subst.
apply First.
apply Next.
auto.
Defined.
Definition liftVar (G : list dom) (t : dom) (v : Var G t) (t' : dom) : Var (t' :: G) t :=
liftVar' nil G v 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).
induction G; simpl; intuition.
inversion H; subst.
exact H0.
apply var; exact H4.
inversion H; subst.
apply var.
apply First.
apply lift.
apply IHG with t'.
exact H4.
exact H0.
Defined.
Definition substVar : forall t' (G : list dom) t, Var (t' :: G) t
-> term G (inj t') -> term G (inj t).
intros t' G t v e.
exact (substVar' nil v e).
Defined.
End substVar.
Definition retype_Var : forall t t', t = t'
-> forall G, Var (dom:= dom) G t
-> Var G t'.
intros; subst; trivial.
Defined.
Theorem retype_Var_ident : forall G t (H : t = t) (k : Var G t),
retype_Var H k = k.
intros.
unfold retype_Var.
rewrite eq_rec_r_ident.
trivial.
Qed.
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'.
intros.
pattern t, G, t', v.
apply Var_invert; simpl; intuition.
left; intuition.
rewrite retype_Var_ident; trivial.
eauto.
Qed.
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').
induction 1; simpl; intuition;
inversion_Var_any; simpl; intuition.
Qed.
Definition liftSubst' : forall G G', Subst denote1 (G ++ G')
-> forall t, denote1 t -> Subst denote1 (G ++ t :: G').
induction G; simpl; intuition.
constructor.
exact X0.
exact X.
inversion X; subst.
constructor.
exact X1.
eauto.
Defined.
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.
induction G; simpl_Binding.
Qed.
End Subst_lr.
Ltac rewriteEverywhere H :=
try rewrite H;
repeat match goal with
| [ H' : _ |- _ ] => rewrite H in H'
end;
clear H.
Ltac rewriteNat :=
match goal with
| [ H : _ = O |- _ ] => rewriteEverywhere H
| [ H : _ = S _ |- _ ] => rewriteEverywhere H
end.
Ltac simplify' := repeat progress (simpl in *;
repeat rewrite eq_rect_r_ident; intuition).
Ltac rewriteOnce tac :=
match goal with
| [ H : _ |- _ ] =>
(rewrite H; tac; fail)
|| (rewrite <- H; tac; fail)
end.
Ltac simplify := simplify'; try rewriteOnce ltac:(auto; try omega; rewriteOnce ltac:(auto; omega));
intuition eauto.
Ltac forward' self search_context search_goal is_relevant H :=
match type of H with
| ?T =>
match goal with
| [ H : ?T1 -> _ |- _ ] =>
match type of H with
| T => idtac
end;
match type of T1 with
| Prop => idtac
end;
let pf := fresh "pf" in
(assert (pf : T1);
[eauto; fail
| generalize (H pf); clear H; intro H; self H])
| [ H : forall (s : ?T1), _ |- _ ] =>
match type of H with
| T => idtac
end;
search_context T1;
match goal with
| [ x : _ |- _ ] =>
generalize (H x); clear H; intro H; self H
end
| [ H : forall (s : ?T1), _ |- _ ] =>
match type of H with
| T => idtac
end;
search_goal T1;
match goal with
| [ |- context[?E] ] =>
generalize (H E); clear H; intro H; self H
end
| _ => is_relevant T
end
end.
Ltac forward search_context search_goal is_relevant H :=
forward' ltac:(forward ltac:search_context ltac:search_goal ltac:is_relevant)
ltac:search_context ltac:search_goal ltac:is_relevant H.
Ltac check_eq E1 E2 :=
let dummy := fresh "dummy" in
(assert (dummy : E1 = E2);
[reflexivity
| clear dummy]).
Ltac crush search_context search_goal is_relevant simplifier solver :=
repeat (simplifier;
match goal with
| [ H : forall x, _ |- _ ] =>
forward ltac:search_context ltac:search_goal ltac:is_relevant H
end;
solver).
Index
This page has been generated by coqdoc