PR.sn_inductive_soundness_1a
Require Import stlc reduction sn_defs Coq.Program.Equality.
Set Implicit Arguments.
Unset Strict Implicit.
Lemma sn_preimage {m n} (f : tm m -> tm n) (s : tm m) :
(forall t u, step t u -> step (f t) (f u)) ->
sn (f s) -> sn s.
Proof.
intros H sns. dependent induction sns. apply snI. intros t st.
eapply H0; eauto.
Qed.
Lemma sn_appL {n} (s : tm n) (t : tm n) :
sn (app s t) -> sn s.
Proof. apply (@sn_preimage _ _ (fun s => app s t)); eauto using @step. Qed.
Lemma sn_subst_tm {m n} (f : fin m -> tm n) (s : tm m) :
sn (subst_tm f s) -> sn s.
Proof. apply sn_preimage. apply step_inst. Qed.
Lemma closed_lam {n} (s : tm (S n)) A:
sn (lam A s) <-> sn s.
Proof.
split.
- eapply sn_preimage. apply step_abs.
- induction 1 as [M H IH].
constructor. intros M' C. inv C. auto.
Qed.
Lemma closed_appR n (M: tm n) (N: tm n) :
sn (app M N) -> sn N.
Proof. eapply sn_preimage. apply step_appR. Qed.
Lemma closed_inl n (M: tm n) :
sn M -> sn (inl M).
Proof. induction 1 as [M H IH]. constructor. intros M' C. inv C. auto. Qed.
Lemma closed_inr n (M: tm n) :
sn M -> sn (inr M).
Proof. induction 1 as [M H IH]. constructor. intros M' C. inv C. auto. Qed.
Lemma closed_orelim n (M: tm n) (N1: tm (S n)) N2:
sn (orelim M N1 N2) -> sn M /\ sn N1 /\ sn N2.
Proof.
intros H. split.
- revert H. apply sn_preimage with (f := fun x => orelim x N1 N2).
intros t t' H. now apply step_orelim.
- split.
+ revert H. apply sn_preimage with (f := fun x => orelim M x N2).
intros. now apply step_orelimL.
+ revert H. eapply sn_preimage. apply step_orelimR.
Qed.
(* Weak Head Reduction *)
Inductive redsn : forall n, tm n -> tm n -> Prop :=
| redsn_beta n A (M: tm (S n)) (N: tm n) : sn N -> redsn (app (lam A M) N) (subst_tm (N.:ids) M)
| redsn_app n (R R' : tm n) (M : tm n) : redsn R R' -> redsn (app R M) (app R' M)
| redsn_or n (M M' : tm n) (N1 : tm (S n)) N2: redsn M M' -> redsn (orelim M N1 N2) (orelim M' N1 N2)
| redsn_caseL n (s: tm n) t t' (u: tm (S n)) : sn s -> sn t -> sn u -> t' = (t[s..]) -> redsn (orelim (inl s) t u) t'
| redsn_caseR n (s: tm n) (t: tm (S n)) u u': sn s -> sn t -> sn u -> u' = (u[s..]) -> redsn (orelim (inr s) t u) u'.
Lemma fundamental_backwards n (M: tm (S n)) (N: tm n) A :
sn N -> sn (subst_tm (N.: ids) M) -> sn (app (lam A M) N).
Proof.
intros sn_N sn_M'.
assert (H: sn M) by (now apply sn_subst_tm in sn_M').
revert M H sn_M'. induction sn_N as [N sn_N IH_N].
induction 1 as [M sn_M IH_M]. intros H. constructor. intros M' C. inv C.
- constructor. intros M' H'. inv H. now apply H.
- inv C. rename b2 into M'. eapply IH_M. assumption.
eauto using sn_mstep, mstep_beta, mstep_step.
- eapply IH_N; eauto.
+ now constructor.
+ eauto using sn_mstep, mstep_beta, mstep_step.
Qed.
Lemma fundamental_backwards_orl n (s : tm n) (t: tm (S n)) (u: tm (S n)):
sn s -> sn u -> sn (t[s..]) -> sn (orelim (inl s) t u).
Proof.
intros sn_s sn_u H. assert (H': sn t) by (now apply sn_subst_tm in H).
revert t H' u sn_u H.
induction sn_s as [s sn_s IHs].
induction 1 as [u sn_u IHu].
induction 1 as [t sn_t IHt]. intros H. constructor. intros s' D. inv D.
- inv D. apply IHs. assumption. now constructor. now constructor.
eauto using sn_mstep, mstep_beta, mstep_step.
- apply IHu; eauto. now constructor. eauto using sn_mstep, mstep_beta, mstep_step.
- eapply IHt; eauto.
- assumption.
Qed.
Lemma fundamental_backwards_orr n (s : tm n) (t: tm (S n)) (u: tm (S n)):
sn s -> sn t -> sn (u[s..]) -> sn (orelim (inr s) t u).
Proof.
intros sn_s sn_t H. assert (H': sn u) by (now apply sn_subst_tm in H).
revert u H' t sn_t H.
induction sn_s as [s sn_s IHs].
induction 1 as [t sn_t IHt].
induction 1 as [u sn_u IHu]. intros H. constructor. intros s' D. inv D.
- inv D. apply IHs; eauto. now constructor. now constructor.
eauto using sn_mstep, mstep_beta, mstep_step.
- eapply IHu; eauto.
- eapply IHt; eauto. now constructor. eauto using sn_mstep, mstep_beta, mstep_step.
- assumption.
Qed.
(* Neutral terms *)
Fixpoint neutral n (M: tm n) :=
match M with
| var_tm x => True
| app s t => neutral s
| orelim s t u => neutral s
| _ => False
end.
Lemma neutral_preservation n (M N: tm n):
neutral M -> step M N -> neutral N.
Proof. intros H. induction 1; simpl in *; intuition. Qed.
Lemma sn_app_neutral n (N : tm n) :
sn N -> forall (M: tm n), neutral M -> sn M -> sn (app M N).
Proof.
induction 1 as [N sn_N IH_N].
induction 2 as [M sn_M IH_M].
constructor. intros M' C. inv C.
- contradiction.
- eauto using neutral_preservation.
- eauto using snI.
Qed.
Lemma sn_case_neutral n (N1 : tm (S n)):
sn N1 -> forall N2, sn N2 -> forall (M: tm n), sn M -> neutral M -> sn (orelim M N1 N2).
Proof.
induction 1 as [N1 snN1 IHN1].
induction 1 as [N2 snN2 IHN2].
induction 1 as [M snM IHM].
intros H. constructor. intros M' H'. inv H'.
* apply IHM. assumption. eapply neutral_preservation; eassumption.
* now apply IHN1.
* now apply IHN2.
* contradiction.
* contradiction.
Qed.
Lemma sn_confluence n (M: tm n):
forall M' M'', redsn M M' -> step M M'' -> M' = M'' \/ exists M''', redsn M'' M''' /\ mstep M' M'''.
Proof.
induction M as [n x | n M IHM N IHN |n M IHM| n M IHM | n M IHM | n M IHM N1 IHN1 N2 IHN2]; intros M' M'' D E; inv D; inv E.
- now left.
- inv E. right. eexists. split.
+ now constructor.
+ apply mstep_inst. eauto using mstep_step.
- right. eexists. split. econstructor. inv H; eauto. apply mstep_beta; eauto using mstep_step.
- inv D.
- destruct (IHM _ _ D E) as [IH|(M''&IH1&IH2)].
+ subst. now left.
+ right. eexists. split.
* econstructor. eassumption.
* eapply mstep_app. assumption. constructor.
- right. eexists. split.
+ constructor. eassumption.
+ eapply mstep_app. constructor. eauto using mstep_step.
- destruct (IHM _ _ D E) as [-> | (M''&IH1&IH2)].
+ now left.
+ right. exists (orelim M'' N1 N2). split; [now constructor|].
eauto using mstep_orelim.
- right. exists (orelim M' t2 N2). split.
+ now constructor.
+ eauto using mstep_orelim, mstep_step.
- right. exists (orelim M' N1 u2). split.
* now constructor.
* eauto using mstep_orelim, mstep_step.
- inv D.
- inv D.
- inv E. right. exists (N1 [s2..]). split.
+ constructor; auto. inv H. now apply H.
+ apply mstep_beta; eauto using mstep_step.
- right. exists (t2[s..]). split.
+ constructor; eauto. inv H0. now apply H0.
+ apply mstep_beta; eauto using mstep_step.
- right. exists (N1[s..]). split.
+ constructor; auto. inv H1. now apply H1.
+ constructor.
- now left.
- inv E. right. exists (N2 [s2..]). split.
+ constructor; auto. inv H. now apply H.
+ apply mstep_beta; eauto using mstep_step.
- right. exists (N2[s..]). split.
+ constructor; auto. inv H0. now apply H0.
+ constructor.
- right. exists (u2[s..]). split.
+ constructor; auto. inv H1. now apply H1.
+ apply mstep_beta; eauto using mstep_step.
- now left.
Qed.
Lemma redsn_backwards n (M M': tm n):
redsn M M' -> sn M' -> sn M.
Proof.
induction 1 as [|n M M' N H IH|n M M' N1 N2 H IH|n s t t' u h1 h2 h3|n s t u u' h1 h2 h3].
- intros D. eapply fundamental_backwards; eauto.
- intros D. specialize (IH (sn_appL D)).
assert (sn_N: sn N) by (now apply closed_appR in D).
revert M IH M' D H.
induction sn_N as [N sn_N IH_N]. induction 1 as [M sn_M IH_M].
constructor. intros M_N C. inv C.
+ inv H.
+ destruct (sn_confluence H C) as [E|(M'''&C1&C2)].
* now subst.
* eapply IH_M with (M' := M'''); eauto.
eapply sn_mstep; [|eassumption]. eapply mstep_app; eauto.
+ eapply IH_N; eauto.
* now constructor.
* inv D. apply H. now constructor.
- intros D.
destruct (closed_orelim D) as (D1%IH&D2&D3). clear IH.
revert N1 D2 N2 D3 M' H D.
induction D1 as [M snM IHM].
induction 1 as [N1 snN1 IHN1].
induction 1 as [N2 snN2 IHN2].
constructor. intros M'' E. inv E.
+ destruct (sn_confluence H E) as [F|(M''&F1&F2)].
* now subst.
* apply IHM with (M' := M''); eauto. now constructor. now constructor.
eapply sn_mstep; [|eassumption]. eapply mstep_orelim; eauto.
+ eapply IHN1; eauto. now constructor. inv D. apply H0. now constructor.
+ eapply IHN2; eauto. inv D. eapply H0. now constructor.
+ inv H.
+ inv H.
- subst. intros H'. now apply fundamental_backwards_orl.
- subst. intros H'. now apply fundamental_backwards_orr.
Qed.
(forall t u, step t u -> step (f t) (f u)) ->
sn (f s) -> sn s.
Proof.
intros H sns. dependent induction sns. apply snI. intros t st.
eapply H0; eauto.
Qed.
Lemma sn_appL {n} (s : tm n) (t : tm n) :
sn (app s t) -> sn s.
Proof. apply (@sn_preimage _ _ (fun s => app s t)); eauto using @step. Qed.
Lemma sn_subst_tm {m n} (f : fin m -> tm n) (s : tm m) :
sn (subst_tm f s) -> sn s.
Proof. apply sn_preimage. apply step_inst. Qed.
Lemma closed_lam {n} (s : tm (S n)) A:
sn (lam A s) <-> sn s.
Proof.
split.
- eapply sn_preimage. apply step_abs.
- induction 1 as [M H IH].
constructor. intros M' C. inv C. auto.
Qed.
Lemma closed_appR n (M: tm n) (N: tm n) :
sn (app M N) -> sn N.
Proof. eapply sn_preimage. apply step_appR. Qed.
Lemma closed_inl n (M: tm n) :
sn M -> sn (inl M).
Proof. induction 1 as [M H IH]. constructor. intros M' C. inv C. auto. Qed.
Lemma closed_inr n (M: tm n) :
sn M -> sn (inr M).
Proof. induction 1 as [M H IH]. constructor. intros M' C. inv C. auto. Qed.
Lemma closed_orelim n (M: tm n) (N1: tm (S n)) N2:
sn (orelim M N1 N2) -> sn M /\ sn N1 /\ sn N2.
Proof.
intros H. split.
- revert H. apply sn_preimage with (f := fun x => orelim x N1 N2).
intros t t' H. now apply step_orelim.
- split.
+ revert H. apply sn_preimage with (f := fun x => orelim M x N2).
intros. now apply step_orelimL.
+ revert H. eapply sn_preimage. apply step_orelimR.
Qed.
(* Weak Head Reduction *)
Inductive redsn : forall n, tm n -> tm n -> Prop :=
| redsn_beta n A (M: tm (S n)) (N: tm n) : sn N -> redsn (app (lam A M) N) (subst_tm (N.:ids) M)
| redsn_app n (R R' : tm n) (M : tm n) : redsn R R' -> redsn (app R M) (app R' M)
| redsn_or n (M M' : tm n) (N1 : tm (S n)) N2: redsn M M' -> redsn (orelim M N1 N2) (orelim M' N1 N2)
| redsn_caseL n (s: tm n) t t' (u: tm (S n)) : sn s -> sn t -> sn u -> t' = (t[s..]) -> redsn (orelim (inl s) t u) t'
| redsn_caseR n (s: tm n) (t: tm (S n)) u u': sn s -> sn t -> sn u -> u' = (u[s..]) -> redsn (orelim (inr s) t u) u'.
Lemma fundamental_backwards n (M: tm (S n)) (N: tm n) A :
sn N -> sn (subst_tm (N.: ids) M) -> sn (app (lam A M) N).
Proof.
intros sn_N sn_M'.
assert (H: sn M) by (now apply sn_subst_tm in sn_M').
revert M H sn_M'. induction sn_N as [N sn_N IH_N].
induction 1 as [M sn_M IH_M]. intros H. constructor. intros M' C. inv C.
- constructor. intros M' H'. inv H. now apply H.
- inv C. rename b2 into M'. eapply IH_M. assumption.
eauto using sn_mstep, mstep_beta, mstep_step.
- eapply IH_N; eauto.
+ now constructor.
+ eauto using sn_mstep, mstep_beta, mstep_step.
Qed.
Lemma fundamental_backwards_orl n (s : tm n) (t: tm (S n)) (u: tm (S n)):
sn s -> sn u -> sn (t[s..]) -> sn (orelim (inl s) t u).
Proof.
intros sn_s sn_u H. assert (H': sn t) by (now apply sn_subst_tm in H).
revert t H' u sn_u H.
induction sn_s as [s sn_s IHs].
induction 1 as [u sn_u IHu].
induction 1 as [t sn_t IHt]. intros H. constructor. intros s' D. inv D.
- inv D. apply IHs. assumption. now constructor. now constructor.
eauto using sn_mstep, mstep_beta, mstep_step.
- apply IHu; eauto. now constructor. eauto using sn_mstep, mstep_beta, mstep_step.
- eapply IHt; eauto.
- assumption.
Qed.
Lemma fundamental_backwards_orr n (s : tm n) (t: tm (S n)) (u: tm (S n)):
sn s -> sn t -> sn (u[s..]) -> sn (orelim (inr s) t u).
Proof.
intros sn_s sn_t H. assert (H': sn u) by (now apply sn_subst_tm in H).
revert u H' t sn_t H.
induction sn_s as [s sn_s IHs].
induction 1 as [t sn_t IHt].
induction 1 as [u sn_u IHu]. intros H. constructor. intros s' D. inv D.
- inv D. apply IHs; eauto. now constructor. now constructor.
eauto using sn_mstep, mstep_beta, mstep_step.
- eapply IHu; eauto.
- eapply IHt; eauto. now constructor. eauto using sn_mstep, mstep_beta, mstep_step.
- assumption.
Qed.
(* Neutral terms *)
Fixpoint neutral n (M: tm n) :=
match M with
| var_tm x => True
| app s t => neutral s
| orelim s t u => neutral s
| _ => False
end.
Lemma neutral_preservation n (M N: tm n):
neutral M -> step M N -> neutral N.
Proof. intros H. induction 1; simpl in *; intuition. Qed.
Lemma sn_app_neutral n (N : tm n) :
sn N -> forall (M: tm n), neutral M -> sn M -> sn (app M N).
Proof.
induction 1 as [N sn_N IH_N].
induction 2 as [M sn_M IH_M].
constructor. intros M' C. inv C.
- contradiction.
- eauto using neutral_preservation.
- eauto using snI.
Qed.
Lemma sn_case_neutral n (N1 : tm (S n)):
sn N1 -> forall N2, sn N2 -> forall (M: tm n), sn M -> neutral M -> sn (orelim M N1 N2).
Proof.
induction 1 as [N1 snN1 IHN1].
induction 1 as [N2 snN2 IHN2].
induction 1 as [M snM IHM].
intros H. constructor. intros M' H'. inv H'.
* apply IHM. assumption. eapply neutral_preservation; eassumption.
* now apply IHN1.
* now apply IHN2.
* contradiction.
* contradiction.
Qed.
Lemma sn_confluence n (M: tm n):
forall M' M'', redsn M M' -> step M M'' -> M' = M'' \/ exists M''', redsn M'' M''' /\ mstep M' M'''.
Proof.
induction M as [n x | n M IHM N IHN |n M IHM| n M IHM | n M IHM | n M IHM N1 IHN1 N2 IHN2]; intros M' M'' D E; inv D; inv E.
- now left.
- inv E. right. eexists. split.
+ now constructor.
+ apply mstep_inst. eauto using mstep_step.
- right. eexists. split. econstructor. inv H; eauto. apply mstep_beta; eauto using mstep_step.
- inv D.
- destruct (IHM _ _ D E) as [IH|(M''&IH1&IH2)].
+ subst. now left.
+ right. eexists. split.
* econstructor. eassumption.
* eapply mstep_app. assumption. constructor.
- right. eexists. split.
+ constructor. eassumption.
+ eapply mstep_app. constructor. eauto using mstep_step.
- destruct (IHM _ _ D E) as [-> | (M''&IH1&IH2)].
+ now left.
+ right. exists (orelim M'' N1 N2). split; [now constructor|].
eauto using mstep_orelim.
- right. exists (orelim M' t2 N2). split.
+ now constructor.
+ eauto using mstep_orelim, mstep_step.
- right. exists (orelim M' N1 u2). split.
* now constructor.
* eauto using mstep_orelim, mstep_step.
- inv D.
- inv D.
- inv E. right. exists (N1 [s2..]). split.
+ constructor; auto. inv H. now apply H.
+ apply mstep_beta; eauto using mstep_step.
- right. exists (t2[s..]). split.
+ constructor; eauto. inv H0. now apply H0.
+ apply mstep_beta; eauto using mstep_step.
- right. exists (N1[s..]). split.
+ constructor; auto. inv H1. now apply H1.
+ constructor.
- now left.
- inv E. right. exists (N2 [s2..]). split.
+ constructor; auto. inv H. now apply H.
+ apply mstep_beta; eauto using mstep_step.
- right. exists (N2[s..]). split.
+ constructor; auto. inv H0. now apply H0.
+ constructor.
- right. exists (u2[s..]). split.
+ constructor; auto. inv H1. now apply H1.
+ apply mstep_beta; eauto using mstep_step.
- now left.
Qed.
Lemma redsn_backwards n (M M': tm n):
redsn M M' -> sn M' -> sn M.
Proof.
induction 1 as [|n M M' N H IH|n M M' N1 N2 H IH|n s t t' u h1 h2 h3|n s t u u' h1 h2 h3].
- intros D. eapply fundamental_backwards; eauto.
- intros D. specialize (IH (sn_appL D)).
assert (sn_N: sn N) by (now apply closed_appR in D).
revert M IH M' D H.
induction sn_N as [N sn_N IH_N]. induction 1 as [M sn_M IH_M].
constructor. intros M_N C. inv C.
+ inv H.
+ destruct (sn_confluence H C) as [E|(M'''&C1&C2)].
* now subst.
* eapply IH_M with (M' := M'''); eauto.
eapply sn_mstep; [|eassumption]. eapply mstep_app; eauto.
+ eapply IH_N; eauto.
* now constructor.
* inv D. apply H. now constructor.
- intros D.
destruct (closed_orelim D) as (D1%IH&D2&D3). clear IH.
revert N1 D2 N2 D3 M' H D.
induction D1 as [M snM IHM].
induction 1 as [N1 snN1 IHN1].
induction 1 as [N2 snN2 IHN2].
constructor. intros M'' E. inv E.
+ destruct (sn_confluence H E) as [F|(M''&F1&F2)].
* now subst.
* apply IHM with (M' := M''); eauto. now constructor. now constructor.
eapply sn_mstep; [|eassumption]. eapply mstep_orelim; eauto.
+ eapply IHN1; eauto. now constructor. inv D. apply H0. now constructor.
+ eapply IHN2; eauto. inv D. eapply H0. now constructor.
+ inv H.
+ inv H.
- subst. intros H'. now apply fundamental_backwards_orl.
- subst. intros H'. now apply fundamental_backwards_orr.
Qed.