Require Import Coq.Lists.List.
From PCF2 Require Import pcf_2 unscoped pcf_2_system pcf_2_contexts preliminaries.
Set Default Goal Selector "!".
Definition pre_order Γ A s t :=
forall (ctxt: pctxt), ctxt_typed ctxt Γ A nil Base -> forall v, (fill ctxt s) ⇓ v -> (fill ctxt t) ⇓ v.
Definition cont_equiv Γ A s t :=
forall (ctxt: pctxt), ctxt_typed ctxt Γ A nil Base -> forall v, (fill ctxt s) ⇓ v <-> (fill ctxt t) ⇓ v.
Inductive obs_preord_base: tm -> tm -> Prop :=
|norm_bot_min x y: x ≻* bot -> obs_preord_base x y
|norm_comp x y z: x ⇓ z -> y ⇓ z -> obs_preord_base x y.
Hint Constructors obs_preord_base : core.
Fixpoint obs_preord_closed (A: ty): tm -> tm -> Prop :=
fun x y =>
match A with
| Base => obs_preord_base x y
| Fun A B => forall a b, nil ⊢ a: A -> nil ⊢ b: A -> obs_preord_closed A a b -> obs_preord_closed B (app x a) (app y b)
end.
Definition obs_preord (Γ: context) (A: ty): tm -> tm -> Prop :=
fun x y => forall σ, subst_well_typed nil Γ σ -> obs_preord_closed A (Subst_tm σ x) (Subst_tm σ y).
Definition subst_rel (Γ: context) (σ1 : nat -> tm) (σ2 : nat -> tm) :=
forall n T, nth_error Γ n = Some T -> obs_preord_closed T (σ1 n) (σ2 n).
Definition strong_obs_preord (Γ: context) (A: ty): tm -> tm -> Prop :=
fun t1 t2 => forall σ1, nil ⊢ σ1 [ Γ ] -> forall σ2, nil ⊢ σ2 [ Γ ] -> subst_rel Γ σ1 σ2
-> obs_preord_closed A (Subst_tm σ1 t1) (Subst_tm σ2 t2).
Definition obs_equiv Γ A x y := obs_preord Γ A x y /\ obs_preord Γ A y x.
Notation "Γ ⊢ x ≤ y : A" := (obs_preord Γ A x y) (at level 50, x, y, A at next level).
Notation "x ≤c y : A" := (obs_preord_closed A x y) (at level 50, y, A at next level).
Notation "x ≤b y" := (obs_preord_base x y) (at level 50, y at next level).
Notation "Γ ⊢ x ≡ y : A" := (obs_equiv Γ A x y) (at level 50, x, y, A at next level).
Notation "Γ ⊢ x ≡c y : A" := (cont_equiv Γ A x y) (at level 50, x, y, A at next level).
Lemma obs_preord_closed_steps A s s' t t':
nil ⊢ s: A -> nil ⊢ t: A -> s ≻ s' -> t ≻ t'
-> s' ≤c t': A -> s ≤c t : A.
Proof.
induction A in s, s', t, t' |- *.
- intros typed_s typed_t step_s step_t order_s'_t'.
red in order_s'_t'. cbn.
inv order_s'_t'.
+ eapply norm_bot_min. rewrite step_s. all: apply H.
+ eapply norm_comp. 1: eapply step_eval with (t := s'); eauto.
eapply step_eval with (t := t'); eauto.
- intros typed_s typed_t step_s step_t order_s'_t'.
intros a b typed_a typed_b order_a_b.
specialize (IHA2 (app s a) (app s' a)).
specialize (IHA2 (app t b) (app t' b)).
eapply IHA2.
all: eauto.
Qed.
Lemma strong_obs_preord_steps Γ A s s' t t':
Γ ⊢ s: A -> Γ ⊢ t: A -> s ≻ s' -> t ≻ t'
-> strong_obs_preord Γ A s' t' -> strong_obs_preord Γ A s t.
Proof.
intros typed_s typed_t step_s step_t order_s'_t' σ1 subst1_wt σ2 subst2_wt rel.
eapply obs_preord_closed_steps; eauto.
all: eapply subst_preserves_step; eauto.
Qed.
Lemma strong_obs_preord_refl Γ A s:
typed Γ s A -> strong_obs_preord Γ A s s.
Proof.
induction 1; intros σ1 subst1_wt σ2 subst2_wt rel; cbn.
1-3: econstructor 2; firstorder.
- now eapply rel.
- intros a b typed_a typed_b order_a_b.
eapply obs_preord_closed_steps; eauto.
+ econstructor; eauto.
eapply subst_preserves with (e := lam _); eauto.
+ econstructor; eauto.
eapply subst_preserves with (e := lam _); eauto.
+ erewrite subst_concat. 1: erewrite subst_concat. 1: eapply IHtyped.
{ intros []; cbn; eauto; congruence. }
{ intros []; cbn; eauto; congruence. }
all: eauto.
{ intros []; cbn; eauto; congruence. }
- red in IHtyped1. cbn in IHtyped1. eapply IHtyped1; eauto.
- specialize (IHtyped1 σ1 subst1_wt σ2 subst2_wt rel). cbn in IHtyped1.
specialize (IHtyped2 σ1 subst1_wt σ2 subst2_wt rel). cbn in IHtyped2.
specialize (IHtyped3 σ1 subst1_wt σ2 subst2_wt rel). cbn in IHtyped3.
inv IHtyped1.
+ constructor.
now rewrite H2, IfB.
+ destruct H2 as [H2 H2']. destruct H3 as [H3 H3']. destruct z; try easy.
* inv IHtyped2.
-- eapply norm_bot_min.
now rewrite H2, IfT, H4.
-- eapply norm_comp.
++ split. 1: now rewrite H2, IfT, H4. firstorder.
++ split. 1: now rewrite H3, IfT, H5. firstorder.
* inv IHtyped3.
-- eapply norm_bot_min.
now rewrite H2, IfF, H4.
-- eapply norm_comp.
++ split. 1: now rewrite H2, IfF, H4. firstorder.
++ split. 1: now rewrite H3, IfF, H5. firstorder.
* eapply norm_bot_min. now rewrite H2, IfB.
Qed.
Lemma subst_rel_nil σ1 σ2:
subst_rel nil σ1 σ2.
Proof.
red. intros n T H. destruct n; easy.
Qed.
Lemma obs_preord_closed_refl A s:
typed nil s A -> s ≤c s: A.
Proof.
intros typed_s.
assert (H: strong_obs_preord nil A s s).
- now apply strong_obs_preord_refl.
- red in H. enough (H1: subst_well_typed nil nil (fun n => var_tm n)).
1: enough (H2: subst_rel nil (fun n => var_tm n) (fun n => var_tm n)).
+ specialize (H (fun n => var_tm n) H1 (fun n => var_tm n) H1 H2).
erewrite closed_subst in H. 1: eauto. eapply typed_empty_closed. eauto.
+ apply subst_rel_nil.
+ apply subst_well_typed_nil_nil.
Qed.
Lemma strong_obs_preord_imp_obs_preord:
forall Γ A s t, strong_obs_preord Γ A s t -> Γ ⊢ s ≤ t : A.
Proof.
intros Γ A s t H σ subst_wf.
apply H. 1-2: eauto. intros n T H0.
apply obs_preord_closed_refl.
red in subst_wf. apply subst_wf. easy.
Qed.
Lemma obs_preord_refl Γ A s:
typed Γ s A -> Γ ⊢ s ≤ s : A.
Proof.
intros H.
apply strong_obs_preord_imp_obs_preord.
now apply strong_obs_preord_refl.
Qed.
Lemma obs_preord_closed_trans A s t u:
nil ⊢ s: A -> nil ⊢ t: A -> nil ⊢ u: A -> s ≤c t: A -> t ≤c u: A -> s ≤c u: A.
Proof.
intros typed_s typed_t typed_u order_s_t order_t_u.
induction A in s, t, u, typed_s, typed_t, typed_u, order_s_t, order_t_u |- *.
- inv order_s_t; inv order_t_u.
1-2: econstructor; eauto.
+ econstructor. rewrite H. enough (z = bot) by now subst.
destruct H0 as [H0 H0']. eapply evaluates_to_same. 1: split. 1: exact H0. all: firstorder.
+ eapply norm_comp. all: eauto. enough (z = z0) by now subst.
destruct H0 as [H0 H0']. eapply evaluates_to_same. 1: split. 1: exact H0. all: firstorder.
- intros a b typed_a typed_b order_a_b.
eapply IHA2.
1, 3: eauto.
+ eapply app_typed. 1: exact typed_t. eauto.
+ eapply order_s_t; eauto.
+ eapply order_t_u; eauto. now eapply obs_preord_closed_refl.
Qed.
Lemma obs_preord_trans Γ A s t u:
Γ ⊢ s: A -> Γ ⊢ t: A -> Γ ⊢ u: A -> Γ ⊢ s ≤ t : A -> Γ ⊢ t ≤ u : A -> Γ ⊢ s ≤ u : A.
Proof.
intros typed_s typed_t typed_u order_s_t order_t_u.
intros σ subst_wf. eapply (obs_preord_closed_trans _ _ (Subst_tm σ t) _).
all: eauto.
Qed.
Lemma obs_preord_closed_fun_char A B f g:
nil ⊢ f: (Fun A B) -> nil ⊢ g: (Fun A B) -> f ≤c g: (Fun A B) <-> forall x, nil ⊢ x: A -> (app f x) ≤c (app g x): B.
Proof.
intros typed_f typed_g.
split.
- intros H x typed_x. enough (H0: obs_preord_closed A x x).
+ specialize (H x x typed_x typed_x H0). easy.
+ apply obs_preord_closed_refl. easy.
- intros H a b typed_a typed_b order_a_b.
eapply (obs_preord_closed_trans _ _ (app g a) _).
1-3: eapply app_typed. all: eauto.
enough (H0: obs_preord_closed (Fun A B) g g).
+ eapply H0. all: easy.
+ now apply obs_preord_closed_refl.
Qed.
Lemma obs_preord_fun_char Γ A B f g:
Γ ⊢ f: (Fun A B) -> Γ ⊢ g: (Fun A B) -> Γ ⊢ f ≤ g: (Fun A B) <-> forall x, nil ⊢ x: A -> Γ ⊢ (app f x) ≤ (app g x): B.
Proof.
intros typed_f typed_g.
split.
- intros H x typed_x. enough (H0: obs_preord nil A x x).
+ intros σ subst_wf.
enough (H1: obs_preord_closed (Fun A B) (Subst_tm σ f) (Subst_tm σ g) <-> forall x, typed nil x A -> obs_preord_closed B (app (Subst_tm σ f) x) (app (Subst_tm σ g) x)).
* destruct H1 as [H1 H2]. cbn. rewrite (closed_subst x). 1: eapply H1. 1: apply H. all: eauto.
eapply typed_empty_closed. eauto.
* eapply obs_preord_closed_fun_char.
all: eapply subst_preserves; eauto.
+ now eapply obs_preord_refl.
- intros H σ subst_wf. enough (H1: obs_preord_closed (Fun A B) (Subst_tm σ f) (Subst_tm σ g) <-> forall x, typed nil x A -> obs_preord_closed B (app (Subst_tm σ f) x) (app (Subst_tm σ g) x)).
+ destruct H1 as [H1 H2]. apply H2. intros x typed_x.
specialize (H x typed_x σ subst_wf). cbn in H. rewrite (closed_subst x) in H; eauto.
eapply typed_empty_closed. exact typed_x.
+ eapply obs_preord_closed_fun_char.
all: eapply subst_preserves; eauto.
Qed.
Lemma obs_preord_closed_incl_step A e e':
nil ⊢ e: A -> e ≻ e' -> e ≤c e': A.
Proof.
induction A in e, e' |- *.
- intros typed_e step_e. cbn. destruct (weak_normalisation_comp e') as [v [eval_e' H]].
1: eapply type_preservation. all: eauto.
econstructor 2. { split. 1: rewrite step_e; apply eval_e'. easy. } split. 1: apply eval_e'. easy.
- intros typed_e step_e. erewrite obs_preord_closed_fun_char.
+ intros x typed_x. eapply IHA2. all: eauto.
+ eauto.
+ eapply type_preservation. all: eauto.
Qed.
Lemma obs_preord_incl_step Γ A e e':
Γ ⊢ e: A -> e ≻ e' -> Γ ⊢ e ≤ e': A.
Proof.
intros typed_e step_e σ subst_wt. eapply obs_preord_closed_incl_step.
- eapply subst_preserves. 1: exact subst_wt. eauto.
- eapply subst_preserves_step. easy.
Qed.
Lemma obs_preord_incl_steps Γ A e e':
Γ ⊢ e: A -> e ≻* e' -> Γ ⊢ e ≤ e': A.
Proof.
intros typed_e step_e. induction step_e.
- eapply obs_preord_incl_step; eauto.
- eapply obs_preord_refl; eauto.
- eapply obs_preord_trans with (t := y); eauto.
3: apply IHstep_e2.
all: eapply type_preservation; eauto.
Qed.
Lemma obs_preord_closed_incl_step' A e e':
nil ⊢ e: A -> e ≻ e' -> e' ≤c e: A.
Proof.
induction A in e, e' |- *.
- intros typed_e step_e. cbn. destruct (weak_normalisation_comp e') as [v [eval_e' H]].
1: eapply type_preservation. all: eauto.
econstructor 2. { split. 1: apply eval_e'. easy. } split. 1: rewrite step_e; apply eval_e'. easy.
- intros typed_e step_e. erewrite obs_preord_closed_fun_char.
+ intros x typed_x. eapply IHA2. all: eauto.
+ eapply type_preservation. all: eauto.
+ eauto.
Qed.
Lemma obs_preord_incl_step' Γ A e e':
Γ ⊢ e: A -> e ≻ e' -> Γ ⊢ e' ≤ e: A.
Proof.
intros typed_e step_e σ subst_wt. eapply obs_preord_closed_incl_step'.
- eapply subst_preserves. 1: exact subst_wt. eauto.
- eapply subst_preserves_step. easy.
Qed.
Lemma obs_preord_incl_steps' Γ A e e':
Γ ⊢ e: A -> e ≻* e' -> Γ ⊢ e' ≤ e: A.
Proof.
intros typed_e step_e. induction step_e.
- eapply obs_preord_incl_step'; eauto.
- eapply obs_preord_refl; eauto.
- eapply obs_preord_trans with (t := y); eauto.
3: apply IHstep_e2.
all: eapply type_preservation; eauto.
Qed.
Lemma steps_equiv Γ A e e':
Γ ⊢ e: A -> e ≻* e' -> Γ ⊢ e' ≡ e: A.
Proof.
intros. split.
- now eapply obs_preord_incl_steps'.
- now eapply obs_preord_incl_steps.
Qed.
Lemma steps_preserve_obs_preord Γ A s t s' t':
Γ ⊢ s: A -> Γ ⊢ t: A -> s ≻* s' -> t ≻* t' -> Γ ⊢ s ≤ t: A -> Γ ⊢ s' ≤ t': A.
Proof.
intros typed_s typed_t steps_s steps_t order_s_t.
assert (Γ ⊢ s': A).
1: now apply type_preservation with (s := s).
assert (Γ ⊢ t': A).
1: now apply type_preservation with (s := t).
apply obs_preord_trans with (t := s); eauto.
1: now apply obs_preord_incl_steps'.
apply obs_preord_trans with (t := t); eauto.
now apply obs_preord_incl_steps.
Qed.
Lemma steps_preserve_obs_preord_backward Γ A s t s' t':
Γ ⊢ s: A -> Γ ⊢ t: A -> s ≻* s' -> t ≻* t' -> Γ ⊢ s' ≤ t': A -> Γ ⊢ s ≤ t: A.
Proof.
intros typed_s typed_t steps_s steps_t order_s_t.
assert (Γ ⊢ s': A).
1: now apply type_preservation with (s := s).
assert (Γ ⊢ t': A).
1: now apply type_preservation with (s := t).
apply obs_preord_trans with (t := s'); eauto.
1: now apply obs_preord_incl_steps.
apply obs_preord_trans with (t := t'); eauto.
now apply obs_preord_incl_steps'.
Qed.
Require Import Setoid Morphisms.
Instance rewrite_in_obs_preord_base : Proper (steps ==> steps ==> iff) obs_preord_base.
intros ? ? ? ? ? ?.
split.
- intros ?. inv H1.
+ assert (x ⇓ bot).
* split; eauto.
* apply norm_bot_min.
eapply eval_step. all: eauto.
+ eapply norm_comp. 1: eapply eval_step; eauto.
eapply eval_step ; eauto.
- intros ?. inv H1.
+ apply norm_bot_min. rewrite H; eauto.
+ eapply norm_comp.
* split. 1: rewrite H. all: apply H2.
* split. 1: rewrite H0. all: apply H3.
Qed.
Instance rewrite_in_evaluates : Proper (steps ==> eq ==> iff) evaluates_to_base.
Proof.
intros ? ? ? ? ? ?. subst. split.
- intros ?. eapply eval_step; eauto.
- intros ?. eapply step_eval; eauto.
Qed.
Lemma obs_preord_base_bot t : obs_preord_base bot t.
Proof.
eapply norm_bot_min. eauto.
Qed.
Hint Immediate obs_preord_base_bot : core.
Lemma obs_preord_base_refl t : nil ⊢ t: Base -> t ≤b t.
Proof.
intros H. destruct (weak_normalisation_comp t H) as [v H0]. destruct H0 as [H0 H1].
destruct v; try easy.
1-3: eapply norm_comp; split; eauto.
Qed.
Hint Immediate obs_preord_base_refl : core.
Lemma evaluates_to_final s v : s ⇓ v -> v ⇓ v.
Proof.
firstorder.
Qed.
Hint Resolve evaluates_to_final : core.
Lemma obs_preord_context Γ Γ' A A' C s t:
Γ ⊢ s: A -> Γ ⊢ t: A -> C [Γ, A]: Γ', A' -> Γ ⊢ s ≤ t: A -> Γ' ⊢ (fill C s) ≤ (fill C t): A'.
Proof.
intros typed_s typed_t typed_c order_s_t.
induction typed_c in s, t, typed_s, typed_t, order_s_t |- *; intros σ subst_wt; cbn.
1: eauto.
- specialize (IHtyped_c s t typed_s typed_t order_s_t σ subst_wt).
inv IHtyped_c; cbn.
+ rewrite H1, IfB. eauto.
+ destruct H1 as [H1 H1v], H2 as [H2 H2v]. destruct z; try easy.
* rewrite H1, H2, !IfT. eapply obs_preord_base_refl. eauto.
* rewrite H1, H2, IfF. eapply obs_preord_base_refl. eauto.
* rewrite H1, IfB. eauto.
- specialize (IHtyped_c s t typed_s typed_t order_s_t σ subst_wt).
destruct (weak_normalisation_comp (Subst_tm σ trm1)) as [v H1]. 1: eauto.
destruct H1 as [H1 H1']. destruct v; try easy.
+ inv IHtyped_c.
* econstructor. rewrite H1, IfT, H2. eauto.
* rewrite H1, !IfT. eauto.
+ rewrite H1, !IfF. eapply obs_preord_base_refl. eauto.
+ eapply norm_bot_min. now rewrite H1, IfB.
- specialize (IHtyped_c s t typed_s typed_t order_s_t σ subst_wt).
destruct (weak_normalisation_comp (Subst_tm σ trm1)) as [v H1]. 1: eauto.
destruct H1 as [H1 H1']. destruct v; try easy.
+ rewrite H1, !IfT. eapply obs_preord_base_refl. eauto.
+ inv IHtyped_c.
* econstructor. rewrite H1, IfF, H2. eauto.
* rewrite H1, !IfF. eauto.
+ eapply norm_bot_min. now rewrite H1, IfB.
- enough (H: obs_preord_closed (Fun T A') (Subst_tm σ (lam (fill ctxt s))) (Subst_tm σ (lam (fill ctxt t)))).
+ eapply H; eauto.
+ erewrite obs_preord_closed_fun_char.
* intros x typed_x. specialize (IHtyped_c s t typed_s typed_t order_s_t).
eapply obs_preord_closed_steps.
3-4: cbn; eauto.
-- econstructor. 2: eauto. eapply subst_preserves. 1: eauto. econstructor. eapply fill_type. all: eauto.
-- econstructor. 2: eauto. eapply subst_preserves. 1: eauto. econstructor. eapply fill_type. all: eauto.
-- specialize (IHtyped_c (scons x σ)). erewrite subst_concat. 1: erewrite subst_concat.
1: eapply IHtyped_c; intros n ty H; destruct n; cbn in H. all: eauto. 1: injection H; intro eq; subst; now cbn.
1-2: eapply fill_type. all: eauto.
* eapply subst_preserves. 1: eauto. econstructor. eapply fill_type. all: eauto.
* eapply subst_preserves. 1: eauto. econstructor. eapply fill_type. all: eauto.
- assert (H0: obs_preord Γ' (Fun B C) (fill ctxt s) (fill ctxt t)).
+ eapply IHtyped_c.
all: eauto.
+ specialize (H0 σ subst_wt ).
eapply H0; eauto. eapply obs_preord_closed_refl; eauto.
- specialize (IHtyped_c s t typed_s typed_t order_s_t). assert (H1: obs_preord_closed (Fun B C) (Subst_tm σ trm) (Subst_tm σ trm)).
+ 1: eapply obs_preord_refl; eauto.
+ apply H1.
1-2: eapply subst_preserves; eauto; eapply fill_type; eauto.
now eapply IHtyped_c.
Qed.
Lemma obs_equiv_context Γ Γ' A A' C s t:
Γ ⊢ s: A -> Γ ⊢ t: A -> C [Γ, A]: Γ', A' -> Γ ⊢ s ≡ t: A -> Γ' ⊢ (fill C s) ≡ (fill C t): A'.
Proof.
intros typed_s typed_t typed_c equiv. destruct equiv. split; eapply obs_preord_context; eauto.
Qed.
Lemma obs_equiv_base_eval_same s t:
nil ⊢ s: Base -> nil ⊢ t: Base -> nil ⊢ s ≡ t : Base -> forall v, s ⇓ v -> t ⇓ v.
Proof.
intros typed_s typed_t [preord_s_t preord_t_s] v eval_s.
specialize (preord_s_t (fun n => var_tm n) (subst_well_typed_nil_nil _)).
specialize (preord_t_s (fun n => var_tm n) (subst_well_typed_nil_nil _)). asimpl in preord_s_t. asimpl in preord_t_s.
cbn in *.
inv preord_s_t.
- inv preord_t_s.
+ enough (v = bot) by now subst; split; eauto.
eapply (evaluates_to_same s); firstorder.
+ enough (v = z) by now subst; eauto.
eapply evaluates_to_same; eauto.
- enough (v = z) by now subst; eauto.
eapply evaluates_to_same; eauto.
Qed.
Lemma obs_equiv_imp_cont_pre_order Γ A s t:
Γ ⊢ s: A -> Γ ⊢ t: A -> Γ ⊢ s ≡ t: A -> pre_order Γ A s t.
Proof.
intros typed_s typed_t equiv C typed_c.
assert (H1: nil ⊢ fill C s ≡ fill C t: Base).
- eapply obs_equiv_context; eauto.
- eapply obs_equiv_base_eval_same; eauto.
all: eapply fill_type; eauto.
Qed.
Lemma cont_pre_order_imp_cont_equiv Γ A s t:
Γ ⊢ s: A -> pre_order Γ A s t -> Γ ⊢ s ≡c t: A.
Proof.
intros typed_s order C typed_c v.
split; eauto.
destruct (weak_normalisation_comp (fill C s)).
- eapply fill_type; eauto.
- intros H1. enough (v = x).
* subst; eauto.
* eapply evaluates_to_same; eauto.
Qed.
Lemma obs_equiv_imp_cont_equiv Γ A s t:
Γ ⊢ s: A -> Γ ⊢ t: A -> Γ ⊢ s ≡ t: A -> Γ ⊢ s ≡c t: A.
Proof.
intros typed_s typed_t equiv C typed_c v.
eapply cont_pre_order_imp_cont_equiv; eauto. now apply obs_equiv_imp_cont_pre_order.
Qed.
Lemma pre_order_imp_obs_preord_closed A s t:
nil ⊢ s: A -> nil ⊢ t: A -> pre_order nil A s t -> s ≤c t: A.
Proof.
intros typed_s typed_t H. induction A in s, t, typed_s, typed_t, H |- *.
- red in H. specialize (H pctxtHole). cbn in *.
destruct (weak_normalisation_comp s typed_s). eapply norm_comp; eauto.
- eapply obs_preord_closed_fun_char; eauto.
intros x typed_x. eapply IHA2.
1-2: eauto.
intros C typed_c v eval. red in H. specialize (H (concat C (pctxtAppL pctxtHole x))).
enough (H0: (fill (concat C (pctxtAppL pctxtHole x)) t) ⇓ v).
+ rewrite ctxt_concat_fill in H0. now cbn in H0.
+ eapply H.
* eapply ctxt_concat_typed; eauto.
* rewrite ctxt_concat_fill. now cbn.
Qed.
Fixpoint lam_subst (Γ: context) σ C :=
match Γ with
| nil => C
| cons A Γ' => lam_subst Γ' (fun n => σ (S n)) (pctxtAppL (pctxtLam C) (σ 0))
end.
Lemma lam_subst_concat Γ σ C1 C2:
lam_subst Γ σ (concat C1 C2) = concat (lam_subst Γ σ C1) C2.
Proof.
induction Γ in σ, C1, C2 |- *; eauto.
cbn. now erewrite <- IHΓ.
Qed.
Lemma lam_subst_step Γ σ A t:
Γ ⊢ t: A -> nil ⊢ σ[Γ]-> (fill (lam_subst Γ σ pctxtHole) t) ≻* (Subst_tm σ t).
Proof.
intros typed_t subst_wt. induction Γ in t, σ, typed_t, subst_wt |-*; cbn in *.
- erewrite closed_subst; eauto. eapply typed_empty_closed; eauto.
- enough (H: lam_subst Γ (fun n : nat => σ (S n)) (pctxtAppL (pctxtLam pctxtHole) (σ 0)) = concat (lam_subst Γ (fun n : nat => σ (S n)) pctxtHole) (pctxtAppL (pctxtLam pctxtHole) (σ 0))).
+ rewrite H. rewrite ctxt_concat_fill. cbn.
rewrite (IHΓ (fun n : nat => σ (S n)) (app (lam t) (σ 0))).
* rewrite subst_preserves_step. 2: econstructor. erewrite subst_shift; eauto.
* econstructor.
-- econstructor; eauto.
-- eapply (type_weakening nil); firstorder.
* intros n T H1. eapply subst_wt; eauto.
+ assert (H: lam_subst Γ (fun n : nat => σ (S n)) (concat pctxtHole (pctxtAppL (pctxtLam pctxtHole) (σ 0))) = concat (lam_subst Γ (fun n : nat => σ (S n)) pctxtHole) (pctxtAppL (pctxtLam pctxtHole) (σ 0))); eauto.
eapply lam_subst_concat.
Qed.
Lemma lam_subst_typed Γ A Γ' A' σ C:
nil ⊢ σ [Γ'] -> C[Γ, A]: Γ', A' -> (lam_subst Γ' σ C)[Γ, A]: nil, A'.
Proof.
intros subst_wt typed_c. induction Γ' in σ, C, typed_c, subst_wt |- *; eauto.
cbn. eapply IHΓ'; firstorder.
econstructor; eauto. eapply (type_weakening nil). firstorder.
Qed.
Lemma pre_order_imp_obs_preord Γ A s t:
Γ ⊢ s: A -> Γ ⊢ t: A -> pre_order Γ A s t -> Γ ⊢ s ≤ t: A.
Proof.
intros typed_s typed_t order σ subst_wt. eapply pre_order_imp_obs_preord_closed.
1-2: eauto.
intros C typed_c v eval_s. eapply eval_step. 1: eapply fill_step; eapply lam_subst_step. all: eauto.
red in order. rewrite <- ctxt_concat_fill. eapply order. 1: eapply ctxt_concat_typed. 1: exact typed_c.
+ eapply lam_subst_typed; eauto.
+ rewrite ctxt_concat_fill. eapply step_eval. 1: eapply fill_step. 1: eapply lam_subst_step. all: eauto.
Qed.
Definition rest_PCF Γ A := sig (fun t => Γ ⊢ t: A).
Definition obs_preord_rest Γ A (p1 p2: rest_PCF Γ A) := obs_preord Γ A (proj1_sig p1) (proj1_sig p2).
Instance obs_equiv_obs_preord Γ A: subrelation (obs_equiv Γ A) (obs_preord Γ A).
Proof.
firstorder.
Qed.
Instance obs_preord_PreOrder Γ A : PreOrder (obs_preord_rest Γ A).
Proof.
split.
- intros [s Hs]. now eapply obs_preord_refl.
- intros [s Hs] [t Ht] [u Hu]. now eapply obs_preord_trans.
Qed.
Lemma obs_equiv_rewrite_left Γ A s t u:
Γ ⊢ s: A -> Γ ⊢ t: A -> Γ ⊢ u: A -> Γ ⊢ s ≤ t: A -> Γ ⊢ s ≡ u: A -> Γ ⊢ u ≤ t: A.
Proof.
intros ? ? ? ? ?. destruct H3. now apply obs_preord_trans with (t := s).
Qed.
Lemma obs_equiv_rewrite_right Γ A s t u:
Γ ⊢ s: A -> Γ ⊢ t: A -> Γ ⊢ u: A -> Γ ⊢ s ≤ t: A -> Γ ⊢ t ≡ u: A -> Γ ⊢ s ≤ u: A.
Proof.
intros ? ? ? ? ?. destruct H3. now apply obs_preord_trans with (t := t).
Qed.
Lemma obs_equiv_refl Γ A s:
Γ ⊢ s: A -> Γ ⊢ s ≡ s: A.
Proof.
intros ?. split; now apply obs_preord_refl.
Qed.
Lemma obs_equiv_trans Γ A s t u:
Γ ⊢ s: A -> Γ ⊢ t: A -> Γ ⊢ u: A -> Γ ⊢ s ≡ t : A -> Γ ⊢ t ≡ u : A -> Γ ⊢ s ≡ u : A.
Proof.
intros ? ? ? ? ?.
destruct H2, H3. split; eapply obs_preord_trans with (t := t); eauto.
Qed.
From PCF2 Require Import pcf_2 unscoped pcf_2_system pcf_2_contexts preliminaries.
Set Default Goal Selector "!".
Definition pre_order Γ A s t :=
forall (ctxt: pctxt), ctxt_typed ctxt Γ A nil Base -> forall v, (fill ctxt s) ⇓ v -> (fill ctxt t) ⇓ v.
Definition cont_equiv Γ A s t :=
forall (ctxt: pctxt), ctxt_typed ctxt Γ A nil Base -> forall v, (fill ctxt s) ⇓ v <-> (fill ctxt t) ⇓ v.
Inductive obs_preord_base: tm -> tm -> Prop :=
|norm_bot_min x y: x ≻* bot -> obs_preord_base x y
|norm_comp x y z: x ⇓ z -> y ⇓ z -> obs_preord_base x y.
Hint Constructors obs_preord_base : core.
Fixpoint obs_preord_closed (A: ty): tm -> tm -> Prop :=
fun x y =>
match A with
| Base => obs_preord_base x y
| Fun A B => forall a b, nil ⊢ a: A -> nil ⊢ b: A -> obs_preord_closed A a b -> obs_preord_closed B (app x a) (app y b)
end.
Definition obs_preord (Γ: context) (A: ty): tm -> tm -> Prop :=
fun x y => forall σ, subst_well_typed nil Γ σ -> obs_preord_closed A (Subst_tm σ x) (Subst_tm σ y).
Definition subst_rel (Γ: context) (σ1 : nat -> tm) (σ2 : nat -> tm) :=
forall n T, nth_error Γ n = Some T -> obs_preord_closed T (σ1 n) (σ2 n).
Definition strong_obs_preord (Γ: context) (A: ty): tm -> tm -> Prop :=
fun t1 t2 => forall σ1, nil ⊢ σ1 [ Γ ] -> forall σ2, nil ⊢ σ2 [ Γ ] -> subst_rel Γ σ1 σ2
-> obs_preord_closed A (Subst_tm σ1 t1) (Subst_tm σ2 t2).
Definition obs_equiv Γ A x y := obs_preord Γ A x y /\ obs_preord Γ A y x.
Notation "Γ ⊢ x ≤ y : A" := (obs_preord Γ A x y) (at level 50, x, y, A at next level).
Notation "x ≤c y : A" := (obs_preord_closed A x y) (at level 50, y, A at next level).
Notation "x ≤b y" := (obs_preord_base x y) (at level 50, y at next level).
Notation "Γ ⊢ x ≡ y : A" := (obs_equiv Γ A x y) (at level 50, x, y, A at next level).
Notation "Γ ⊢ x ≡c y : A" := (cont_equiv Γ A x y) (at level 50, x, y, A at next level).
Lemma obs_preord_closed_steps A s s' t t':
nil ⊢ s: A -> nil ⊢ t: A -> s ≻ s' -> t ≻ t'
-> s' ≤c t': A -> s ≤c t : A.
Proof.
induction A in s, s', t, t' |- *.
- intros typed_s typed_t step_s step_t order_s'_t'.
red in order_s'_t'. cbn.
inv order_s'_t'.
+ eapply norm_bot_min. rewrite step_s. all: apply H.
+ eapply norm_comp. 1: eapply step_eval with (t := s'); eauto.
eapply step_eval with (t := t'); eauto.
- intros typed_s typed_t step_s step_t order_s'_t'.
intros a b typed_a typed_b order_a_b.
specialize (IHA2 (app s a) (app s' a)).
specialize (IHA2 (app t b) (app t' b)).
eapply IHA2.
all: eauto.
Qed.
Lemma strong_obs_preord_steps Γ A s s' t t':
Γ ⊢ s: A -> Γ ⊢ t: A -> s ≻ s' -> t ≻ t'
-> strong_obs_preord Γ A s' t' -> strong_obs_preord Γ A s t.
Proof.
intros typed_s typed_t step_s step_t order_s'_t' σ1 subst1_wt σ2 subst2_wt rel.
eapply obs_preord_closed_steps; eauto.
all: eapply subst_preserves_step; eauto.
Qed.
Lemma strong_obs_preord_refl Γ A s:
typed Γ s A -> strong_obs_preord Γ A s s.
Proof.
induction 1; intros σ1 subst1_wt σ2 subst2_wt rel; cbn.
1-3: econstructor 2; firstorder.
- now eapply rel.
- intros a b typed_a typed_b order_a_b.
eapply obs_preord_closed_steps; eauto.
+ econstructor; eauto.
eapply subst_preserves with (e := lam _); eauto.
+ econstructor; eauto.
eapply subst_preserves with (e := lam _); eauto.
+ erewrite subst_concat. 1: erewrite subst_concat. 1: eapply IHtyped.
{ intros []; cbn; eauto; congruence. }
{ intros []; cbn; eauto; congruence. }
all: eauto.
{ intros []; cbn; eauto; congruence. }
- red in IHtyped1. cbn in IHtyped1. eapply IHtyped1; eauto.
- specialize (IHtyped1 σ1 subst1_wt σ2 subst2_wt rel). cbn in IHtyped1.
specialize (IHtyped2 σ1 subst1_wt σ2 subst2_wt rel). cbn in IHtyped2.
specialize (IHtyped3 σ1 subst1_wt σ2 subst2_wt rel). cbn in IHtyped3.
inv IHtyped1.
+ constructor.
now rewrite H2, IfB.
+ destruct H2 as [H2 H2']. destruct H3 as [H3 H3']. destruct z; try easy.
* inv IHtyped2.
-- eapply norm_bot_min.
now rewrite H2, IfT, H4.
-- eapply norm_comp.
++ split. 1: now rewrite H2, IfT, H4. firstorder.
++ split. 1: now rewrite H3, IfT, H5. firstorder.
* inv IHtyped3.
-- eapply norm_bot_min.
now rewrite H2, IfF, H4.
-- eapply norm_comp.
++ split. 1: now rewrite H2, IfF, H4. firstorder.
++ split. 1: now rewrite H3, IfF, H5. firstorder.
* eapply norm_bot_min. now rewrite H2, IfB.
Qed.
Lemma subst_rel_nil σ1 σ2:
subst_rel nil σ1 σ2.
Proof.
red. intros n T H. destruct n; easy.
Qed.
Lemma obs_preord_closed_refl A s:
typed nil s A -> s ≤c s: A.
Proof.
intros typed_s.
assert (H: strong_obs_preord nil A s s).
- now apply strong_obs_preord_refl.
- red in H. enough (H1: subst_well_typed nil nil (fun n => var_tm n)).
1: enough (H2: subst_rel nil (fun n => var_tm n) (fun n => var_tm n)).
+ specialize (H (fun n => var_tm n) H1 (fun n => var_tm n) H1 H2).
erewrite closed_subst in H. 1: eauto. eapply typed_empty_closed. eauto.
+ apply subst_rel_nil.
+ apply subst_well_typed_nil_nil.
Qed.
Lemma strong_obs_preord_imp_obs_preord:
forall Γ A s t, strong_obs_preord Γ A s t -> Γ ⊢ s ≤ t : A.
Proof.
intros Γ A s t H σ subst_wf.
apply H. 1-2: eauto. intros n T H0.
apply obs_preord_closed_refl.
red in subst_wf. apply subst_wf. easy.
Qed.
Lemma obs_preord_refl Γ A s:
typed Γ s A -> Γ ⊢ s ≤ s : A.
Proof.
intros H.
apply strong_obs_preord_imp_obs_preord.
now apply strong_obs_preord_refl.
Qed.
Lemma obs_preord_closed_trans A s t u:
nil ⊢ s: A -> nil ⊢ t: A -> nil ⊢ u: A -> s ≤c t: A -> t ≤c u: A -> s ≤c u: A.
Proof.
intros typed_s typed_t typed_u order_s_t order_t_u.
induction A in s, t, u, typed_s, typed_t, typed_u, order_s_t, order_t_u |- *.
- inv order_s_t; inv order_t_u.
1-2: econstructor; eauto.
+ econstructor. rewrite H. enough (z = bot) by now subst.
destruct H0 as [H0 H0']. eapply evaluates_to_same. 1: split. 1: exact H0. all: firstorder.
+ eapply norm_comp. all: eauto. enough (z = z0) by now subst.
destruct H0 as [H0 H0']. eapply evaluates_to_same. 1: split. 1: exact H0. all: firstorder.
- intros a b typed_a typed_b order_a_b.
eapply IHA2.
1, 3: eauto.
+ eapply app_typed. 1: exact typed_t. eauto.
+ eapply order_s_t; eauto.
+ eapply order_t_u; eauto. now eapply obs_preord_closed_refl.
Qed.
Lemma obs_preord_trans Γ A s t u:
Γ ⊢ s: A -> Γ ⊢ t: A -> Γ ⊢ u: A -> Γ ⊢ s ≤ t : A -> Γ ⊢ t ≤ u : A -> Γ ⊢ s ≤ u : A.
Proof.
intros typed_s typed_t typed_u order_s_t order_t_u.
intros σ subst_wf. eapply (obs_preord_closed_trans _ _ (Subst_tm σ t) _).
all: eauto.
Qed.
Lemma obs_preord_closed_fun_char A B f g:
nil ⊢ f: (Fun A B) -> nil ⊢ g: (Fun A B) -> f ≤c g: (Fun A B) <-> forall x, nil ⊢ x: A -> (app f x) ≤c (app g x): B.
Proof.
intros typed_f typed_g.
split.
- intros H x typed_x. enough (H0: obs_preord_closed A x x).
+ specialize (H x x typed_x typed_x H0). easy.
+ apply obs_preord_closed_refl. easy.
- intros H a b typed_a typed_b order_a_b.
eapply (obs_preord_closed_trans _ _ (app g a) _).
1-3: eapply app_typed. all: eauto.
enough (H0: obs_preord_closed (Fun A B) g g).
+ eapply H0. all: easy.
+ now apply obs_preord_closed_refl.
Qed.
Lemma obs_preord_fun_char Γ A B f g:
Γ ⊢ f: (Fun A B) -> Γ ⊢ g: (Fun A B) -> Γ ⊢ f ≤ g: (Fun A B) <-> forall x, nil ⊢ x: A -> Γ ⊢ (app f x) ≤ (app g x): B.
Proof.
intros typed_f typed_g.
split.
- intros H x typed_x. enough (H0: obs_preord nil A x x).
+ intros σ subst_wf.
enough (H1: obs_preord_closed (Fun A B) (Subst_tm σ f) (Subst_tm σ g) <-> forall x, typed nil x A -> obs_preord_closed B (app (Subst_tm σ f) x) (app (Subst_tm σ g) x)).
* destruct H1 as [H1 H2]. cbn. rewrite (closed_subst x). 1: eapply H1. 1: apply H. all: eauto.
eapply typed_empty_closed. eauto.
* eapply obs_preord_closed_fun_char.
all: eapply subst_preserves; eauto.
+ now eapply obs_preord_refl.
- intros H σ subst_wf. enough (H1: obs_preord_closed (Fun A B) (Subst_tm σ f) (Subst_tm σ g) <-> forall x, typed nil x A -> obs_preord_closed B (app (Subst_tm σ f) x) (app (Subst_tm σ g) x)).
+ destruct H1 as [H1 H2]. apply H2. intros x typed_x.
specialize (H x typed_x σ subst_wf). cbn in H. rewrite (closed_subst x) in H; eauto.
eapply typed_empty_closed. exact typed_x.
+ eapply obs_preord_closed_fun_char.
all: eapply subst_preserves; eauto.
Qed.
Lemma obs_preord_closed_incl_step A e e':
nil ⊢ e: A -> e ≻ e' -> e ≤c e': A.
Proof.
induction A in e, e' |- *.
- intros typed_e step_e. cbn. destruct (weak_normalisation_comp e') as [v [eval_e' H]].
1: eapply type_preservation. all: eauto.
econstructor 2. { split. 1: rewrite step_e; apply eval_e'. easy. } split. 1: apply eval_e'. easy.
- intros typed_e step_e. erewrite obs_preord_closed_fun_char.
+ intros x typed_x. eapply IHA2. all: eauto.
+ eauto.
+ eapply type_preservation. all: eauto.
Qed.
Lemma obs_preord_incl_step Γ A e e':
Γ ⊢ e: A -> e ≻ e' -> Γ ⊢ e ≤ e': A.
Proof.
intros typed_e step_e σ subst_wt. eapply obs_preord_closed_incl_step.
- eapply subst_preserves. 1: exact subst_wt. eauto.
- eapply subst_preserves_step. easy.
Qed.
Lemma obs_preord_incl_steps Γ A e e':
Γ ⊢ e: A -> e ≻* e' -> Γ ⊢ e ≤ e': A.
Proof.
intros typed_e step_e. induction step_e.
- eapply obs_preord_incl_step; eauto.
- eapply obs_preord_refl; eauto.
- eapply obs_preord_trans with (t := y); eauto.
3: apply IHstep_e2.
all: eapply type_preservation; eauto.
Qed.
Lemma obs_preord_closed_incl_step' A e e':
nil ⊢ e: A -> e ≻ e' -> e' ≤c e: A.
Proof.
induction A in e, e' |- *.
- intros typed_e step_e. cbn. destruct (weak_normalisation_comp e') as [v [eval_e' H]].
1: eapply type_preservation. all: eauto.
econstructor 2. { split. 1: apply eval_e'. easy. } split. 1: rewrite step_e; apply eval_e'. easy.
- intros typed_e step_e. erewrite obs_preord_closed_fun_char.
+ intros x typed_x. eapply IHA2. all: eauto.
+ eapply type_preservation. all: eauto.
+ eauto.
Qed.
Lemma obs_preord_incl_step' Γ A e e':
Γ ⊢ e: A -> e ≻ e' -> Γ ⊢ e' ≤ e: A.
Proof.
intros typed_e step_e σ subst_wt. eapply obs_preord_closed_incl_step'.
- eapply subst_preserves. 1: exact subst_wt. eauto.
- eapply subst_preserves_step. easy.
Qed.
Lemma obs_preord_incl_steps' Γ A e e':
Γ ⊢ e: A -> e ≻* e' -> Γ ⊢ e' ≤ e: A.
Proof.
intros typed_e step_e. induction step_e.
- eapply obs_preord_incl_step'; eauto.
- eapply obs_preord_refl; eauto.
- eapply obs_preord_trans with (t := y); eauto.
3: apply IHstep_e2.
all: eapply type_preservation; eauto.
Qed.
Lemma steps_equiv Γ A e e':
Γ ⊢ e: A -> e ≻* e' -> Γ ⊢ e' ≡ e: A.
Proof.
intros. split.
- now eapply obs_preord_incl_steps'.
- now eapply obs_preord_incl_steps.
Qed.
Lemma steps_preserve_obs_preord Γ A s t s' t':
Γ ⊢ s: A -> Γ ⊢ t: A -> s ≻* s' -> t ≻* t' -> Γ ⊢ s ≤ t: A -> Γ ⊢ s' ≤ t': A.
Proof.
intros typed_s typed_t steps_s steps_t order_s_t.
assert (Γ ⊢ s': A).
1: now apply type_preservation with (s := s).
assert (Γ ⊢ t': A).
1: now apply type_preservation with (s := t).
apply obs_preord_trans with (t := s); eauto.
1: now apply obs_preord_incl_steps'.
apply obs_preord_trans with (t := t); eauto.
now apply obs_preord_incl_steps.
Qed.
Lemma steps_preserve_obs_preord_backward Γ A s t s' t':
Γ ⊢ s: A -> Γ ⊢ t: A -> s ≻* s' -> t ≻* t' -> Γ ⊢ s' ≤ t': A -> Γ ⊢ s ≤ t: A.
Proof.
intros typed_s typed_t steps_s steps_t order_s_t.
assert (Γ ⊢ s': A).
1: now apply type_preservation with (s := s).
assert (Γ ⊢ t': A).
1: now apply type_preservation with (s := t).
apply obs_preord_trans with (t := s'); eauto.
1: now apply obs_preord_incl_steps.
apply obs_preord_trans with (t := t'); eauto.
now apply obs_preord_incl_steps'.
Qed.
Require Import Setoid Morphisms.
Instance rewrite_in_obs_preord_base : Proper (steps ==> steps ==> iff) obs_preord_base.
intros ? ? ? ? ? ?.
split.
- intros ?. inv H1.
+ assert (x ⇓ bot).
* split; eauto.
* apply norm_bot_min.
eapply eval_step. all: eauto.
+ eapply norm_comp. 1: eapply eval_step; eauto.
eapply eval_step ; eauto.
- intros ?. inv H1.
+ apply norm_bot_min. rewrite H; eauto.
+ eapply norm_comp.
* split. 1: rewrite H. all: apply H2.
* split. 1: rewrite H0. all: apply H3.
Qed.
Instance rewrite_in_evaluates : Proper (steps ==> eq ==> iff) evaluates_to_base.
Proof.
intros ? ? ? ? ? ?. subst. split.
- intros ?. eapply eval_step; eauto.
- intros ?. eapply step_eval; eauto.
Qed.
Lemma obs_preord_base_bot t : obs_preord_base bot t.
Proof.
eapply norm_bot_min. eauto.
Qed.
Hint Immediate obs_preord_base_bot : core.
Lemma obs_preord_base_refl t : nil ⊢ t: Base -> t ≤b t.
Proof.
intros H. destruct (weak_normalisation_comp t H) as [v H0]. destruct H0 as [H0 H1].
destruct v; try easy.
1-3: eapply norm_comp; split; eauto.
Qed.
Hint Immediate obs_preord_base_refl : core.
Lemma evaluates_to_final s v : s ⇓ v -> v ⇓ v.
Proof.
firstorder.
Qed.
Hint Resolve evaluates_to_final : core.
Lemma obs_preord_context Γ Γ' A A' C s t:
Γ ⊢ s: A -> Γ ⊢ t: A -> C [Γ, A]: Γ', A' -> Γ ⊢ s ≤ t: A -> Γ' ⊢ (fill C s) ≤ (fill C t): A'.
Proof.
intros typed_s typed_t typed_c order_s_t.
induction typed_c in s, t, typed_s, typed_t, order_s_t |- *; intros σ subst_wt; cbn.
1: eauto.
- specialize (IHtyped_c s t typed_s typed_t order_s_t σ subst_wt).
inv IHtyped_c; cbn.
+ rewrite H1, IfB. eauto.
+ destruct H1 as [H1 H1v], H2 as [H2 H2v]. destruct z; try easy.
* rewrite H1, H2, !IfT. eapply obs_preord_base_refl. eauto.
* rewrite H1, H2, IfF. eapply obs_preord_base_refl. eauto.
* rewrite H1, IfB. eauto.
- specialize (IHtyped_c s t typed_s typed_t order_s_t σ subst_wt).
destruct (weak_normalisation_comp (Subst_tm σ trm1)) as [v H1]. 1: eauto.
destruct H1 as [H1 H1']. destruct v; try easy.
+ inv IHtyped_c.
* econstructor. rewrite H1, IfT, H2. eauto.
* rewrite H1, !IfT. eauto.
+ rewrite H1, !IfF. eapply obs_preord_base_refl. eauto.
+ eapply norm_bot_min. now rewrite H1, IfB.
- specialize (IHtyped_c s t typed_s typed_t order_s_t σ subst_wt).
destruct (weak_normalisation_comp (Subst_tm σ trm1)) as [v H1]. 1: eauto.
destruct H1 as [H1 H1']. destruct v; try easy.
+ rewrite H1, !IfT. eapply obs_preord_base_refl. eauto.
+ inv IHtyped_c.
* econstructor. rewrite H1, IfF, H2. eauto.
* rewrite H1, !IfF. eauto.
+ eapply norm_bot_min. now rewrite H1, IfB.
- enough (H: obs_preord_closed (Fun T A') (Subst_tm σ (lam (fill ctxt s))) (Subst_tm σ (lam (fill ctxt t)))).
+ eapply H; eauto.
+ erewrite obs_preord_closed_fun_char.
* intros x typed_x. specialize (IHtyped_c s t typed_s typed_t order_s_t).
eapply obs_preord_closed_steps.
3-4: cbn; eauto.
-- econstructor. 2: eauto. eapply subst_preserves. 1: eauto. econstructor. eapply fill_type. all: eauto.
-- econstructor. 2: eauto. eapply subst_preserves. 1: eauto. econstructor. eapply fill_type. all: eauto.
-- specialize (IHtyped_c (scons x σ)). erewrite subst_concat. 1: erewrite subst_concat.
1: eapply IHtyped_c; intros n ty H; destruct n; cbn in H. all: eauto. 1: injection H; intro eq; subst; now cbn.
1-2: eapply fill_type. all: eauto.
* eapply subst_preserves. 1: eauto. econstructor. eapply fill_type. all: eauto.
* eapply subst_preserves. 1: eauto. econstructor. eapply fill_type. all: eauto.
- assert (H0: obs_preord Γ' (Fun B C) (fill ctxt s) (fill ctxt t)).
+ eapply IHtyped_c.
all: eauto.
+ specialize (H0 σ subst_wt ).
eapply H0; eauto. eapply obs_preord_closed_refl; eauto.
- specialize (IHtyped_c s t typed_s typed_t order_s_t). assert (H1: obs_preord_closed (Fun B C) (Subst_tm σ trm) (Subst_tm σ trm)).
+ 1: eapply obs_preord_refl; eauto.
+ apply H1.
1-2: eapply subst_preserves; eauto; eapply fill_type; eauto.
now eapply IHtyped_c.
Qed.
Lemma obs_equiv_context Γ Γ' A A' C s t:
Γ ⊢ s: A -> Γ ⊢ t: A -> C [Γ, A]: Γ', A' -> Γ ⊢ s ≡ t: A -> Γ' ⊢ (fill C s) ≡ (fill C t): A'.
Proof.
intros typed_s typed_t typed_c equiv. destruct equiv. split; eapply obs_preord_context; eauto.
Qed.
Lemma obs_equiv_base_eval_same s t:
nil ⊢ s: Base -> nil ⊢ t: Base -> nil ⊢ s ≡ t : Base -> forall v, s ⇓ v -> t ⇓ v.
Proof.
intros typed_s typed_t [preord_s_t preord_t_s] v eval_s.
specialize (preord_s_t (fun n => var_tm n) (subst_well_typed_nil_nil _)).
specialize (preord_t_s (fun n => var_tm n) (subst_well_typed_nil_nil _)). asimpl in preord_s_t. asimpl in preord_t_s.
cbn in *.
inv preord_s_t.
- inv preord_t_s.
+ enough (v = bot) by now subst; split; eauto.
eapply (evaluates_to_same s); firstorder.
+ enough (v = z) by now subst; eauto.
eapply evaluates_to_same; eauto.
- enough (v = z) by now subst; eauto.
eapply evaluates_to_same; eauto.
Qed.
Lemma obs_equiv_imp_cont_pre_order Γ A s t:
Γ ⊢ s: A -> Γ ⊢ t: A -> Γ ⊢ s ≡ t: A -> pre_order Γ A s t.
Proof.
intros typed_s typed_t equiv C typed_c.
assert (H1: nil ⊢ fill C s ≡ fill C t: Base).
- eapply obs_equiv_context; eauto.
- eapply obs_equiv_base_eval_same; eauto.
all: eapply fill_type; eauto.
Qed.
Lemma cont_pre_order_imp_cont_equiv Γ A s t:
Γ ⊢ s: A -> pre_order Γ A s t -> Γ ⊢ s ≡c t: A.
Proof.
intros typed_s order C typed_c v.
split; eauto.
destruct (weak_normalisation_comp (fill C s)).
- eapply fill_type; eauto.
- intros H1. enough (v = x).
* subst; eauto.
* eapply evaluates_to_same; eauto.
Qed.
Lemma obs_equiv_imp_cont_equiv Γ A s t:
Γ ⊢ s: A -> Γ ⊢ t: A -> Γ ⊢ s ≡ t: A -> Γ ⊢ s ≡c t: A.
Proof.
intros typed_s typed_t equiv C typed_c v.
eapply cont_pre_order_imp_cont_equiv; eauto. now apply obs_equiv_imp_cont_pre_order.
Qed.
Lemma pre_order_imp_obs_preord_closed A s t:
nil ⊢ s: A -> nil ⊢ t: A -> pre_order nil A s t -> s ≤c t: A.
Proof.
intros typed_s typed_t H. induction A in s, t, typed_s, typed_t, H |- *.
- red in H. specialize (H pctxtHole). cbn in *.
destruct (weak_normalisation_comp s typed_s). eapply norm_comp; eauto.
- eapply obs_preord_closed_fun_char; eauto.
intros x typed_x. eapply IHA2.
1-2: eauto.
intros C typed_c v eval. red in H. specialize (H (concat C (pctxtAppL pctxtHole x))).
enough (H0: (fill (concat C (pctxtAppL pctxtHole x)) t) ⇓ v).
+ rewrite ctxt_concat_fill in H0. now cbn in H0.
+ eapply H.
* eapply ctxt_concat_typed; eauto.
* rewrite ctxt_concat_fill. now cbn.
Qed.
Fixpoint lam_subst (Γ: context) σ C :=
match Γ with
| nil => C
| cons A Γ' => lam_subst Γ' (fun n => σ (S n)) (pctxtAppL (pctxtLam C) (σ 0))
end.
Lemma lam_subst_concat Γ σ C1 C2:
lam_subst Γ σ (concat C1 C2) = concat (lam_subst Γ σ C1) C2.
Proof.
induction Γ in σ, C1, C2 |- *; eauto.
cbn. now erewrite <- IHΓ.
Qed.
Lemma lam_subst_step Γ σ A t:
Γ ⊢ t: A -> nil ⊢ σ[Γ]-> (fill (lam_subst Γ σ pctxtHole) t) ≻* (Subst_tm σ t).
Proof.
intros typed_t subst_wt. induction Γ in t, σ, typed_t, subst_wt |-*; cbn in *.
- erewrite closed_subst; eauto. eapply typed_empty_closed; eauto.
- enough (H: lam_subst Γ (fun n : nat => σ (S n)) (pctxtAppL (pctxtLam pctxtHole) (σ 0)) = concat (lam_subst Γ (fun n : nat => σ (S n)) pctxtHole) (pctxtAppL (pctxtLam pctxtHole) (σ 0))).
+ rewrite H. rewrite ctxt_concat_fill. cbn.
rewrite (IHΓ (fun n : nat => σ (S n)) (app (lam t) (σ 0))).
* rewrite subst_preserves_step. 2: econstructor. erewrite subst_shift; eauto.
* econstructor.
-- econstructor; eauto.
-- eapply (type_weakening nil); firstorder.
* intros n T H1. eapply subst_wt; eauto.
+ assert (H: lam_subst Γ (fun n : nat => σ (S n)) (concat pctxtHole (pctxtAppL (pctxtLam pctxtHole) (σ 0))) = concat (lam_subst Γ (fun n : nat => σ (S n)) pctxtHole) (pctxtAppL (pctxtLam pctxtHole) (σ 0))); eauto.
eapply lam_subst_concat.
Qed.
Lemma lam_subst_typed Γ A Γ' A' σ C:
nil ⊢ σ [Γ'] -> C[Γ, A]: Γ', A' -> (lam_subst Γ' σ C)[Γ, A]: nil, A'.
Proof.
intros subst_wt typed_c. induction Γ' in σ, C, typed_c, subst_wt |- *; eauto.
cbn. eapply IHΓ'; firstorder.
econstructor; eauto. eapply (type_weakening nil). firstorder.
Qed.
Lemma pre_order_imp_obs_preord Γ A s t:
Γ ⊢ s: A -> Γ ⊢ t: A -> pre_order Γ A s t -> Γ ⊢ s ≤ t: A.
Proof.
intros typed_s typed_t order σ subst_wt. eapply pre_order_imp_obs_preord_closed.
1-2: eauto.
intros C typed_c v eval_s. eapply eval_step. 1: eapply fill_step; eapply lam_subst_step. all: eauto.
red in order. rewrite <- ctxt_concat_fill. eapply order. 1: eapply ctxt_concat_typed. 1: exact typed_c.
+ eapply lam_subst_typed; eauto.
+ rewrite ctxt_concat_fill. eapply step_eval. 1: eapply fill_step. 1: eapply lam_subst_step. all: eauto.
Qed.
Definition rest_PCF Γ A := sig (fun t => Γ ⊢ t: A).
Definition obs_preord_rest Γ A (p1 p2: rest_PCF Γ A) := obs_preord Γ A (proj1_sig p1) (proj1_sig p2).
Instance obs_equiv_obs_preord Γ A: subrelation (obs_equiv Γ A) (obs_preord Γ A).
Proof.
firstorder.
Qed.
Instance obs_preord_PreOrder Γ A : PreOrder (obs_preord_rest Γ A).
Proof.
split.
- intros [s Hs]. now eapply obs_preord_refl.
- intros [s Hs] [t Ht] [u Hu]. now eapply obs_preord_trans.
Qed.
Lemma obs_equiv_rewrite_left Γ A s t u:
Γ ⊢ s: A -> Γ ⊢ t: A -> Γ ⊢ u: A -> Γ ⊢ s ≤ t: A -> Γ ⊢ s ≡ u: A -> Γ ⊢ u ≤ t: A.
Proof.
intros ? ? ? ? ?. destruct H3. now apply obs_preord_trans with (t := s).
Qed.
Lemma obs_equiv_rewrite_right Γ A s t u:
Γ ⊢ s: A -> Γ ⊢ t: A -> Γ ⊢ u: A -> Γ ⊢ s ≤ t: A -> Γ ⊢ t ≡ u: A -> Γ ⊢ s ≤ u: A.
Proof.
intros ? ? ? ? ?. destruct H3. now apply obs_preord_trans with (t := t).
Qed.
Lemma obs_equiv_refl Γ A s:
Γ ⊢ s: A -> Γ ⊢ s ≡ s: A.
Proof.
intros ?. split; now apply obs_preord_refl.
Qed.
Lemma obs_equiv_trans Γ A s t u:
Γ ⊢ s: A -> Γ ⊢ t: A -> Γ ⊢ u: A -> Γ ⊢ s ≡ t : A -> Γ ⊢ t ≡ u : A -> Γ ⊢ s ≡ u : A.
Proof.
intros ? ? ? ? ?.
destruct H2, H3. split; eapply obs_preord_trans with (t := t); eauto.
Qed.
Lemmas for reduction from RES to CE
Lemma obs_preord_empty_imp_obs_preord_closed A s t:
nil ⊢ s: A -> nil ⊢ t: A -> nil ⊢ s ≤ t: A -> s ≤c t: A.
Proof.
intros typed_s typed_t order_s_t.
specialize (order_s_t ids (subst_well_typed_nil_nil ids)).
rewrite (closed_subst s) in order_s_t; rewrite (closed_subst t) in order_s_t.
1: eauto.
all: eapply typed_empty_closed; eauto.
Qed.
Lemma base_preord_le_bot t:
t ≤c bot: Base -> t ≻* bot.
Proof.
inversion 1; subst; eauto.
enough (H2: bot = z).
- subst. now destruct H0.
- eapply evaluates_to_same; eauto. split; eauto.
Qed.
Lemma base_preord_tt_le t:
tt ≤b t -> t ≻* tt.
Proof.
inversion 1; subst.
- exfalso. enough (bot = tt) by easy.
apply bval_steps_char; easy.
- enough (z = tt).
+ destruct H1; now subst.
+ destruct H0; apply bval_steps_char; eauto.
Qed.
Lemma base_preord_ff_le t:
ff ≤b t -> t ≻* ff.
Proof.
inversion 1; subst.
- exfalso. enough (bot = ff) by easy.
apply bval_steps_char; easy.
- enough (z = ff).
+ destruct H1; now subst.
+ destruct H0; apply bval_steps_char; eauto.
Qed.
Lemma subst_equiv σ1 σ2 Γ Γ' t A:
Γ ⊢ t: A -> Γ' ⊢ σ1 [Γ] -> Γ' ⊢ σ2 [Γ] -> (forall n T, nth_error Γ n = Some T -> Γ' ⊢ σ1(n) ≡ σ2(n): T) -> Γ' ⊢ Subst_tm σ1 t ≡ Subst_tm σ2 t: A.
Proof.
intros typed_t subst1_wt subst2_wt H.
assert (H1: strong_obs_preord Γ A t t) by now apply strong_obs_preord_refl.
split.
- intros σ subst_wt. asimpl. apply H1.
1, 2: intros n T HT; unfold core.funcomp; eapply subst_preserves; eauto.
intros n T HT. enough (H2: Γ' ⊢ σ1 n ≤ σ2 n: T) by now apply H2.
now eapply H.
- intros σ subst_wt. asimpl. apply H1.
1, 2: intros n T HT; unfold core.funcomp; eapply subst_preserves; eauto.
intros n T HT. enough (H2: Γ' ⊢ σ2 n ≤ σ1 n : T) by now apply H2.
now eapply H.
Qed.
Lemma equiv_empty_imp_equiv_nonempty Γ s t A:
nil ⊢ s: A -> nil ⊢ t: A -> nil ⊢ s ≡ t: A -> Γ ⊢ s ≡ t: A.
Proof.
intros typed_s typed_t equiv. destruct equiv. split.
- intros σ _. rewrite closed_subst, closed_subst. 1: apply obs_preord_empty_imp_obs_preord_closed; eauto.
all: eapply typed_empty_closed; eauto.
- intros σ _. rewrite closed_subst, closed_subst. 1: apply obs_preord_empty_imp_obs_preord_closed; eauto.
all: eapply typed_empty_closed; eauto.
Qed.