Library nijn.Syntax.Signature.RewriteLemmas
Require Import Prelude.Funext.
Require Import Prelude.Basics.
Require Import Syntax.Signature.
Require Import Syntax.Signature.SubstitutionLemmas.
Require Import Coq.Program.Equality.
Require Import Prelude.Basics.
Require Import Syntax.Signature.
Require Import Syntax.Signature.SubstitutionLemmas.
Require Import Coq.Program.Equality.
Lemma is_BaseTm_wkTm
{B : Type}
{F : Type}
{ar : F → ty B}
{C1 C2 : con B}
(w : wk C1 C2)
{A : ty B}
{t : tm ar C2 A}
(Ht : is_BaseTm t)
: is_BaseTm (wkTm t w).
Proof.
induction t ; try contradiction.
apply I.
Qed.
Definition wWeakened
{B : Type}
{F : Type}
{ar : F → ty B}
{C1 C2 : con B}
(w : wk C1 C2)
{A : ty B}
(t : tm ar C1 A)
: Type
:= { t' : tm ar C2 A | wkTm t' w = t }.
Definition term_of
{B : Type}
{F : Type}
{ar : F → ty B}
{C1 C2 : con B}
{w : wk C1 C2}
{A : ty B}
{t : tm ar C1 A}
(p : wWeakened w t)
: tm ar C2 A.
Proof.
destruct p as [x e].
exact x.
Defined.
Definition term_of_eq
{B : Type}
{F : Type}
{ar : F → ty B}
{C1 C2 : con B}
{w : wk C1 C2}
{A : ty B}
{t : tm ar C1 A}
(p : wWeakened w t)
: wkTm (term_of p) w = t.
Proof.
destruct p as [x e].
exact e.
Defined.
Definition wkTm_red_lam_help
{B : Type}
{F : Type}
{ar : F → ty B}
{C1 C2 : con B}
(w : wk C1 C2)
{A1 A2 A' : ty B}
(t : tm ar C2 A')
(f : tm ar (A1 ,, C1) A2)
(p : A' = (A1 ⟶ A2))
(q : wkTm (transport _ p t) w = λ f)
: { t' : tm ar (A1 ,, C2) A2 | transport _ p t = λ t' }.
Proof.
destruct t ; try (subst ; simpl in × ; discriminate).
- enough (is_BaseTm (λ f)) by contradiction.
rewrite <- q.
apply is_BaseTm_wkTm.
apply transport_BaseTm.
apply I.
- dependent destruction p ; simpl.
∃ t.
reflexivity.
Qed.
Definition wkTm_red_lam
{B : Type}
{F : Type}
{ar : F → ty B}
{C1 C2 : con B}
(w : wk C1 C2)
{A1 A2 : ty B}
(t : tm ar C2 (A1 ⟶ A2))
(f : tm ar (A1 ,, C1) A2)
(q : wkTm t w = λ f)
: { t' : tm ar (A1 ,, C2) A2 | t = λ t' }.
Proof.
exact (wkTm_red_lam_help w t f eq_refl q).
Qed.
Proposition wkTm_red_step
{B : Type}
{F : Type}
{ar : F → ty B}
{C1 C2 : con B}
{w : wk C1 C2}
{A : ty B}
{t1 t2 : tm ar C1 A}
(p : wWeakened w t1)
(r : t1 ~>β t2)
: { q : wWeakened w t2 & term_of p ~>β term_of q }.
Proof.
revert p.
revert w.
revert C2.
induction r ; intros C2 w p.
- destruct p as [t' p].
destruct t' ; simpl in × ; try discriminate.
assert (p1 := App_eq_Ty p).
assert (p2 := App_eq_fst p).
assert (p3 := App_eq_snd p).
dependent destruction p.
simpl in ×.
specialize (IHr _ _ (exist _ t'1 p2)).
destruct IHr as [q Hq].
destruct q as [v q].
unshelve eexists.
+ unshelve eexists.
× refine (v · t'2).
× simpl.
subst.
reflexivity.
+ simpl.
apply App_l.
assumption.
- destruct p as [t' p].
destruct t' ; simpl in × ; try discriminate.
assert (p1 := App_eq_Ty p).
assert (p2 := App_eq_fst p).
assert (p3 := App_eq_snd p).
dependent destruction p.
simpl in ×.
specialize (IHr _ _ (exist _ t'2 p3)).
destruct IHr as [q Hq].
destruct q as [v q].
unshelve eexists.
+ unshelve eexists.
× refine (t'1 · v).
× simpl.
subst.
reflexivity.
+ simpl.
apply App_r.
assumption.
- destruct p as [t' p].
destruct (wkTm_red_lam w t' f1 p) as [x e].
subst.
pose (q' := Lam_eq p).
specialize (IHr _ (Keep A1 w) (exist _ _ q')).
destruct IHr as [z Hz].
destruct z as [z Hz'].
unshelve eexists.
+ unshelve eexists.
× refine (λ z).
× simpl.
rewrite Hz'.
reflexivity.
+ simpl.
apply CLam.
assumption.
- induction r.
simpl in ×.
destruct p as [t' p].
destruct t' ; simpl in × ; try discriminate.
assert (p1 := App_eq_Ty p).
subst.
assert (p2 := App_eq_fst p).
assert (p3 := App_eq_snd p).
rewrite (UIP (App_eq_Ty p) eq_refl) in p2.
rewrite (UIP (App_eq_Ty p) eq_refl) in p3.
simpl in ×.
destruct (wkTm_red_lam w t'1 f p2) as [x' e].
subst.
simpl in ×.
unshelve eexists.
+ unshelve eexists.
× exact (subTm x' (beta_sub t'2)).
× abstract
(rewrite <- (Lam_eq p2) ;
rewrite !wkTm_is_subTm ;
rewrite !subTm_comp ;
f_equal ;
simpl ; cbn ;
rewrite Sub_id_left ;
f_equal ;
unfold beta_sub ;
simpl ;
rewrite dropSub_is_compSubWk ;
rewrite <- compSub_compWkSub ;
simpl ; cbn;
rewrite compWkSub_id ;
rewrite Sub_id_right ;
reflexivity).
+ simpl.
apply CStep.
apply Beta.
Qed.
Proposition wkTm_red
{B : Type}
{F : Type}
{ar : F → ty B}
{C1 C2 : con B}
(w : wk C1 C2)
{A : ty B}
{t1 t2 : tm ar C1 A}
(p : wWeakened w t1)
(r : t1 ~>β× t2)
: { q : wWeakened w t2 & term_of p ~>β× term_of q }.
Proof.
induction r as [ ? ? r | ? ? ? r1 IHr1 r2 IHr2].
- pose (wkTm_red_step p r) as H.
destruct H as [q Hq].
∃ q.
apply betaRed_step.
exact Hq.
- specialize (IHr1 p).
destruct IHr1 as [q Hq].
specialize (IHr2 q).
destruct IHr2 as [q' Hq'].
∃ q'.
exact (beta_Trans Hq Hq').
Qed.
{B : Type}
{F : Type}
{ar : F → ty B}
{C1 C2 : con B}
(w : wk C1 C2)
{A : ty B}
{t : tm ar C2 A}
(Ht : is_BaseTm t)
: is_BaseTm (wkTm t w).
Proof.
induction t ; try contradiction.
apply I.
Qed.
Definition wWeakened
{B : Type}
{F : Type}
{ar : F → ty B}
{C1 C2 : con B}
(w : wk C1 C2)
{A : ty B}
(t : tm ar C1 A)
: Type
:= { t' : tm ar C2 A | wkTm t' w = t }.
Definition term_of
{B : Type}
{F : Type}
{ar : F → ty B}
{C1 C2 : con B}
{w : wk C1 C2}
{A : ty B}
{t : tm ar C1 A}
(p : wWeakened w t)
: tm ar C2 A.
Proof.
destruct p as [x e].
exact x.
Defined.
Definition term_of_eq
{B : Type}
{F : Type}
{ar : F → ty B}
{C1 C2 : con B}
{w : wk C1 C2}
{A : ty B}
{t : tm ar C1 A}
(p : wWeakened w t)
: wkTm (term_of p) w = t.
Proof.
destruct p as [x e].
exact e.
Defined.
Definition wkTm_red_lam_help
{B : Type}
{F : Type}
{ar : F → ty B}
{C1 C2 : con B}
(w : wk C1 C2)
{A1 A2 A' : ty B}
(t : tm ar C2 A')
(f : tm ar (A1 ,, C1) A2)
(p : A' = (A1 ⟶ A2))
(q : wkTm (transport _ p t) w = λ f)
: { t' : tm ar (A1 ,, C2) A2 | transport _ p t = λ t' }.
Proof.
destruct t ; try (subst ; simpl in × ; discriminate).
- enough (is_BaseTm (λ f)) by contradiction.
rewrite <- q.
apply is_BaseTm_wkTm.
apply transport_BaseTm.
apply I.
- dependent destruction p ; simpl.
∃ t.
reflexivity.
Qed.
Definition wkTm_red_lam
{B : Type}
{F : Type}
{ar : F → ty B}
{C1 C2 : con B}
(w : wk C1 C2)
{A1 A2 : ty B}
(t : tm ar C2 (A1 ⟶ A2))
(f : tm ar (A1 ,, C1) A2)
(q : wkTm t w = λ f)
: { t' : tm ar (A1 ,, C2) A2 | t = λ t' }.
Proof.
exact (wkTm_red_lam_help w t f eq_refl q).
Qed.
Proposition wkTm_red_step
{B : Type}
{F : Type}
{ar : F → ty B}
{C1 C2 : con B}
{w : wk C1 C2}
{A : ty B}
{t1 t2 : tm ar C1 A}
(p : wWeakened w t1)
(r : t1 ~>β t2)
: { q : wWeakened w t2 & term_of p ~>β term_of q }.
Proof.
revert p.
revert w.
revert C2.
induction r ; intros C2 w p.
- destruct p as [t' p].
destruct t' ; simpl in × ; try discriminate.
assert (p1 := App_eq_Ty p).
assert (p2 := App_eq_fst p).
assert (p3 := App_eq_snd p).
dependent destruction p.
simpl in ×.
specialize (IHr _ _ (exist _ t'1 p2)).
destruct IHr as [q Hq].
destruct q as [v q].
unshelve eexists.
+ unshelve eexists.
× refine (v · t'2).
× simpl.
subst.
reflexivity.
+ simpl.
apply App_l.
assumption.
- destruct p as [t' p].
destruct t' ; simpl in × ; try discriminate.
assert (p1 := App_eq_Ty p).
assert (p2 := App_eq_fst p).
assert (p3 := App_eq_snd p).
dependent destruction p.
simpl in ×.
specialize (IHr _ _ (exist _ t'2 p3)).
destruct IHr as [q Hq].
destruct q as [v q].
unshelve eexists.
+ unshelve eexists.
× refine (t'1 · v).
× simpl.
subst.
reflexivity.
+ simpl.
apply App_r.
assumption.
- destruct p as [t' p].
destruct (wkTm_red_lam w t' f1 p) as [x e].
subst.
pose (q' := Lam_eq p).
specialize (IHr _ (Keep A1 w) (exist _ _ q')).
destruct IHr as [z Hz].
destruct z as [z Hz'].
unshelve eexists.
+ unshelve eexists.
× refine (λ z).
× simpl.
rewrite Hz'.
reflexivity.
+ simpl.
apply CLam.
assumption.
- induction r.
simpl in ×.
destruct p as [t' p].
destruct t' ; simpl in × ; try discriminate.
assert (p1 := App_eq_Ty p).
subst.
assert (p2 := App_eq_fst p).
assert (p3 := App_eq_snd p).
rewrite (UIP (App_eq_Ty p) eq_refl) in p2.
rewrite (UIP (App_eq_Ty p) eq_refl) in p3.
simpl in ×.
destruct (wkTm_red_lam w t'1 f p2) as [x' e].
subst.
simpl in ×.
unshelve eexists.
+ unshelve eexists.
× exact (subTm x' (beta_sub t'2)).
× abstract
(rewrite <- (Lam_eq p2) ;
rewrite !wkTm_is_subTm ;
rewrite !subTm_comp ;
f_equal ;
simpl ; cbn ;
rewrite Sub_id_left ;
f_equal ;
unfold beta_sub ;
simpl ;
rewrite dropSub_is_compSubWk ;
rewrite <- compSub_compWkSub ;
simpl ; cbn;
rewrite compWkSub_id ;
rewrite Sub_id_right ;
reflexivity).
+ simpl.
apply CStep.
apply Beta.
Qed.
Proposition wkTm_red
{B : Type}
{F : Type}
{ar : F → ty B}
{C1 C2 : con B}
(w : wk C1 C2)
{A : ty B}
{t1 t2 : tm ar C1 A}
(p : wWeakened w t1)
(r : t1 ~>β× t2)
: { q : wWeakened w t2 & term_of p ~>β× term_of q }.
Proof.
induction r as [ ? ? r | ? ? ? r1 IHr1 r2 IHr2].
- pose (wkTm_red_step p r) as H.
destruct H as [q Hq].
∃ q.
apply betaRed_step.
exact Hq.
- specialize (IHr1 p).
destruct IHr1 as [q Hq].
specialize (IHr2 q).
destruct IHr2 as [q' Hq'].
∃ q'.
exact (beta_Trans Hq Hq').
Qed.
Definition betaRed_step_Wk
{B F : Type}
{ar : F → ty B}
{C1 C2 : con B}
{A : ty B}
{t1 t2 : tm ar C2 A}
(w : wk C1 C2)
(p : t1 ~>β t2)
: wkTm t1 w ~>β wkTm t2 w.
Proof.
revert w.
revert C1.
induction p ; intros C1 w ; simpl.
- exact (App_l _ (IHp _ w)).
- exact (App_r _ (IHp _ w)).
- exact (CLam (IHp _ (Keep A1 w))).
- apply CStep.
induction r.
rewrite !wkTm_is_subTm.
rewrite subTm_comp.
unfold beta_sub.
rewrite <- beta_sub_help.
rewrite <- subTm_comp.
apply Beta.
Qed.
Definition betaRed_Wk
{B F : Type}
{ar : F → ty B}
{C1 C2 : con B}
{A : ty B}
{t1 t2 : tm ar C2 A}
(w : wk C1 C2)
(p : t1 ~>β× t2)
: wkTm t1 w ~>β× wkTm t2 w.
Proof.
revert w.
revert C1.
induction p ; intros C1 w ; simpl.
- apply betaRed_step.
apply betaRed_step_Wk.
exact r.
- exact (beta_Trans (IHp1 C1 w) (IHp2 C1 w)).
Qed.
{B F : Type}
{ar : F → ty B}
{C1 C2 : con B}
{A : ty B}
{t1 t2 : tm ar C2 A}
(w : wk C1 C2)
(p : t1 ~>β t2)
: wkTm t1 w ~>β wkTm t2 w.
Proof.
revert w.
revert C1.
induction p ; intros C1 w ; simpl.
- exact (App_l _ (IHp _ w)).
- exact (App_r _ (IHp _ w)).
- exact (CLam (IHp _ (Keep A1 w))).
- apply CStep.
induction r.
rewrite !wkTm_is_subTm.
rewrite subTm_comp.
unfold beta_sub.
rewrite <- beta_sub_help.
rewrite <- subTm_comp.
apply Beta.
Qed.
Definition betaRed_Wk
{B F : Type}
{ar : F → ty B}
{C1 C2 : con B}
{A : ty B}
{t1 t2 : tm ar C2 A}
(w : wk C1 C2)
(p : t1 ~>β× t2)
: wkTm t1 w ~>β× wkTm t2 w.
Proof.
revert w.
revert C1.
induction p ; intros C1 w ; simpl.
- apply betaRed_step.
apply betaRed_step_Wk.
exact r.
- exact (beta_Trans (IHp1 C1 w) (IHp2 C1 w)).
Qed.
Rewriting is closed under substitution
Definition betaRed_step_sub
{B F : Type}
{ar : F → ty B}
{C1 C2 : con B}
{A : ty B}
{t1 t2 : tm ar C2 A}
(s : sub ar C1 C2)
(p : t1 ~>β t2)
: subTm t1 s ~>β subTm t2 s.
Proof.
revert s.
revert C1.
induction p ; intros C1 s ; simpl.
- exact (App_l _ (IHp _ s)).
- exact (App_r _ (IHp _ s)).
- exact (CLam (IHp _ (keepSub A1 s))).
- apply CStep.
induction r.
simpl.
pose (Beta (subTm f (keepSub A1 s)) (subTm x s)) as p.
unfold beta_sub in ×.
assert (subTm (subTm f (keepSub A1 s)) (idSub C1 _ && subTm x s)
=
subTm (subTm f (idSub C _ && x)) s)
as H.
{
rewrite subTm_comp.
unfold keepSub.
rewrite dropSub_is_compSubWk.
simpl ; cbn.
rewrite <- compSub_compWkSub.
simpl ; cbn.
rewrite compWkSub_id.
rewrite Sub_id_right.
rewrite subTm_comp.
simpl ; cbn.
rewrite Sub_id_left.
reflexivity.
}
rewrite H in p.
exact p.
Qed.
Definition betaRed_sub
{B F : Type}
{ar : F → ty B}
{C1 C2 : con B}
{A : ty B}
{t1 t2 : tm ar C2 A}
(s : sub ar C1 C2)
(p : t1 ~>β× t2)
: subTm t1 s ~>β× subTm t2 s.
Proof.
revert s.
revert C1.
induction p ; intros C1 s ; simpl.
- apply betaRed_step.
apply betaRed_step_sub.
exact r.
- exact (beta_Trans (IHp1 C1 s) (IHp2 C1 s)).
Qed.
{B F : Type}
{ar : F → ty B}
{C1 C2 : con B}
{A : ty B}
{t1 t2 : tm ar C2 A}
(s : sub ar C1 C2)
(p : t1 ~>β t2)
: subTm t1 s ~>β subTm t2 s.
Proof.
revert s.
revert C1.
induction p ; intros C1 s ; simpl.
- exact (App_l _ (IHp _ s)).
- exact (App_r _ (IHp _ s)).
- exact (CLam (IHp _ (keepSub A1 s))).
- apply CStep.
induction r.
simpl.
pose (Beta (subTm f (keepSub A1 s)) (subTm x s)) as p.
unfold beta_sub in ×.
assert (subTm (subTm f (keepSub A1 s)) (idSub C1 _ && subTm x s)
=
subTm (subTm f (idSub C _ && x)) s)
as H.
{
rewrite subTm_comp.
unfold keepSub.
rewrite dropSub_is_compSubWk.
simpl ; cbn.
rewrite <- compSub_compWkSub.
simpl ; cbn.
rewrite compWkSub_id.
rewrite Sub_id_right.
rewrite subTm_comp.
simpl ; cbn.
rewrite Sub_id_left.
reflexivity.
}
rewrite H in p.
exact p.
Qed.
Definition betaRed_sub
{B F : Type}
{ar : F → ty B}
{C1 C2 : con B}
{A : ty B}
{t1 t2 : tm ar C2 A}
(s : sub ar C1 C2)
(p : t1 ~>β× t2)
: subTm t1 s ~>β× subTm t2 s.
Proof.
revert s.
revert C1.
induction p ; intros C1 s ; simpl.
- apply betaRed_step.
apply betaRed_step_sub.
exact r.
- exact (beta_Trans (IHp1 C1 s) (IHp2 C1 s)).
Qed.
Import AFSNotation.
Rewriting is closed under weakening
Definition Rew_Wk
{B F R : Type}
{X : afs B F R}
{C1 C2 : con B}
{A : ty B}
{t1 t2 : tm X C2 A}
(w : wk C1 C2)
(p : rew X t1 t2)
: rew X (wkTm t1 w) (wkTm t2 w).
Proof.
revert w.
revert C1.
induction p ; intros C1 w ; simpl.
- apply rew_step.
revert C1 w.
induction r ; intros C1 w.
+ exact (App_l _ (IHr _ w)).
+ exact (App_r _ (IHr _ w)).
+ exact (CLam (IHr _ (Keep A1 w))).
+ apply CStep.
induction r.
× induction b.
rewrite !wkTm_is_subTm.
rewrite subTm_comp.
unfold beta_sub.
rewrite <- beta_sub_help.
rewrite <- subTm_comp.
apply AFSBeta.
apply Beta.
× rewrite !wkTm_is_subTm.
rewrite !subTm_comp.
apply AFSRew.
- exact (rew_Trans (IHp1 C1 w) (IHp2 C1 w)).
Qed.
{B F R : Type}
{X : afs B F R}
{C1 C2 : con B}
{A : ty B}
{t1 t2 : tm X C2 A}
(w : wk C1 C2)
(p : rew X t1 t2)
: rew X (wkTm t1 w) (wkTm t2 w).
Proof.
revert w.
revert C1.
induction p ; intros C1 w ; simpl.
- apply rew_step.
revert C1 w.
induction r ; intros C1 w.
+ exact (App_l _ (IHr _ w)).
+ exact (App_r _ (IHr _ w)).
+ exact (CLam (IHr _ (Keep A1 w))).
+ apply CStep.
induction r.
× induction b.
rewrite !wkTm_is_subTm.
rewrite subTm_comp.
unfold beta_sub.
rewrite <- beta_sub_help.
rewrite <- subTm_comp.
apply AFSBeta.
apply Beta.
× rewrite !wkTm_is_subTm.
rewrite !subTm_comp.
apply AFSRew.
- exact (rew_Trans (IHp1 C1 w) (IHp2 C1 w)).
Qed.
Rewriting is closed under substitution
Definition Rew_sub
{B F R : Type}
{X : afs B F R}
{C1 C2 : con B}
{A : ty B}
{t1 t2 : tm X C2 A}
(s : sub _ C1 C2)
(p : rew X t1 t2)
: rew X (subTm t1 s) (subTm t2 s).
Proof.
revert s.
revert C1.
induction p ; intros C1 s ; simpl.
- apply rew_step.
revert C1 s.
induction r ; intros C1 s.
+ exact (App_l _ (IHr _ s)).
+ exact (App_r _ (IHr _ s)).
+ exact (CLam (IHr _ (keepSub A1 s))).
+ apply CStep.
induction r.
× induction b.
simpl.
apply AFSBeta.
pose (Beta (subTm f (keepSub A1 s)) (subTm x s)) as p.
unfold beta_sub in ×.
assert (subTm (subTm f (keepSub A1 s)) (idSub C1 (Arity X) && subTm x s)
=
subTm (subTm f (idSub C (Arity X) && x)) s)
as H.
{
rewrite subTm_comp.
unfold keepSub.
rewrite dropSub_is_compSubWk.
simpl ; cbn.
rewrite <- compSub_compWkSub.
simpl ; cbn.
rewrite compWkSub_id.
rewrite Sub_id_right.
rewrite subTm_comp.
simpl ; cbn.
rewrite Sub_id_left.
reflexivity.
}
rewrite H in p.
exact p.
× rewrite !subTm_comp.
apply AFSRew.
- exact (rew_Trans (IHp1 C1 s) (IHp2 C1 s)).
Qed.
{B F R : Type}
{X : afs B F R}
{C1 C2 : con B}
{A : ty B}
{t1 t2 : tm X C2 A}
(s : sub _ C1 C2)
(p : rew X t1 t2)
: rew X (subTm t1 s) (subTm t2 s).
Proof.
revert s.
revert C1.
induction p ; intros C1 s ; simpl.
- apply rew_step.
revert C1 s.
induction r ; intros C1 s.
+ exact (App_l _ (IHr _ s)).
+ exact (App_r _ (IHr _ s)).
+ exact (CLam (IHr _ (keepSub A1 s))).
+ apply CStep.
induction r.
× induction b.
simpl.
apply AFSBeta.
pose (Beta (subTm f (keepSub A1 s)) (subTm x s)) as p.
unfold beta_sub in ×.
assert (subTm (subTm f (keepSub A1 s)) (idSub C1 (Arity X) && subTm x s)
=
subTm (subTm f (idSub C (Arity X) && x)) s)
as H.
{
rewrite subTm_comp.
unfold keepSub.
rewrite dropSub_is_compSubWk.
simpl ; cbn.
rewrite <- compSub_compWkSub.
simpl ; cbn.
rewrite compWkSub_id.
rewrite Sub_id_right.
rewrite subTm_comp.
simpl ; cbn.
rewrite Sub_id_left.
reflexivity.
}
rewrite H in p.
exact p.
× rewrite !subTm_comp.
apply AFSRew.
- exact (rew_Trans (IHp1 C1 s) (IHp2 C1 s)).
Qed.