Require Import Coq.Lists.List.
From PCF2.Autosubst Require Import pcf_2 unscoped.
From PCF2 Require Import CE pcf_2_system pcf_2_contexts preliminaries.
Set Default Goal Selector "!".
Definition cont_preorder Γ A s t :=
forall (ctxt: pctxt), ctxt_typed ctxt Γ A nil Base -> forall v, (fill ctxt s) ⇓ v -> (fill ctxt t) ⇓ v.
Definition subst_rel (Γ: context) (σ1 : nat -> tm) (σ2 : nat -> tm) :=
forall n T, nth_error Γ n = Some T -> obs_preorder_closed T (σ1 n) (σ2 n).
Definition strong_obs_preorder (Γ: context) (A: ty): tm -> tm -> Prop :=
fun t1 t2 => forall σ1, nil ⊢ σ1 [ Γ ] -> forall σ2, nil ⊢ σ2 [ Γ ] -> subst_rel Γ σ1 σ2
-> obs_preorder_closed A (Subst_tm σ1 t1) (Subst_tm σ2 t2).
Lemma obs_preorder_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_preorder_steps Γ A s s' t t':
Γ ⊢ s: A -> Γ ⊢ t: A -> s ≻ s' -> t ≻ t'
-> strong_obs_preorder Γ A s' t' -> strong_obs_preorder Γ 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_preorder_closed_steps; eauto.
all: eapply subst_preserves_step; eauto.
Qed.
Lemma strong_obs_preorder_refl Γ A s:
typed Γ s A -> strong_obs_preorder Γ 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_preorder_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_preorder_closed_refl A s:
typed nil s A -> s ≤c s: A.
Proof.
intros typed_s.
assert (H: strong_obs_preorder nil A s s).
- now apply strong_obs_preorder_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_preorder_imp_obs_preorder:
forall Γ A s t, strong_obs_preorder Γ 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_preorder_closed_refl.
red in subst_wf. apply subst_wf. easy.
Qed.
Lemma obs_preorder_refl Γ A s:
typed Γ s A -> Γ ⊢ s ≤ s : A.
Proof.
intros H.
apply strong_obs_preorder_imp_obs_preorder.
now apply strong_obs_preorder_refl.
Qed.
Lemma obs_preorder_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_preorder_closed_refl.
Qed.
Lemma obs_preorder_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_preorder_closed_trans _ _ (Subst_tm σ t) _).
all: eauto.
Qed.
Lemma obs_preorder_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_preorder_closed A x x).
+ specialize (H x x typed_x typed_x H0). easy.
+ apply obs_preorder_closed_refl. easy.
- intros H a b typed_a typed_b order_a_b.
eapply (obs_preorder_closed_trans _ _ (app g a) _).
1-3: eapply app_typed. all: eauto.
enough (H0: obs_preorder_closed (Fun A B) g g).
+ eapply H0. all: easy.
+ now apply obs_preorder_closed_refl.
Qed.
Lemma obs_preorder_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_preorder nil A x x).
+ intros σ subst_wf.
enough (H1: obs_preorder_closed (Fun A B) (Subst_tm σ f) (Subst_tm σ g) <-> forall x, typed nil x A -> obs_preorder_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_preorder_closed_fun_char.
all: eapply subst_preserves; eauto.
+ now eapply obs_preorder_refl.
- intros H σ subst_wf. enough (H1: obs_preorder_closed (Fun A B) (Subst_tm σ f) (Subst_tm σ g) <-> forall x, typed nil x A -> obs_preorder_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_preorder_closed_fun_char.
all: eapply subst_preserves; eauto.
Qed.
Lemma obs_preorder_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_preorder_closed_fun_char.
+ intros x typed_x. eapply IHA2. all: eauto.
+ eauto.
+ eapply type_preservation. all: eauto.
Qed.
Lemma obs_preorder_incl_step Γ A e e':
Γ ⊢ e: A -> e ≻ e' -> Γ ⊢ e ≤ e': A.
Proof.
intros typed_e step_e σ subst_wt. eapply obs_preorder_closed_incl_step.
- eapply subst_preserves. 1: exact subst_wt. eauto.
- eapply subst_preserves_step. easy.
Qed.
Lemma obs_preorder_incl_steps Γ A e e':
Γ ⊢ e: A -> e ≻* e' -> Γ ⊢ e ≤ e': A.
Proof.
intros typed_e step_e. induction step_e.
- eapply obs_preorder_incl_step; eauto.
- eapply obs_preorder_refl; eauto.
- eapply obs_preorder_trans with (t := y); eauto.
3: apply IHstep_e2.
all: eapply type_preservation; eauto.
Qed.
Lemma obs_preorder_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_preorder_closed_fun_char.
+ intros x typed_x. eapply IHA2. all: eauto.
+ eapply type_preservation. all: eauto.
+ eauto.
Qed.
Lemma obs_preorder_incl_step' Γ A e e':
Γ ⊢ e: A -> e ≻ e' -> Γ ⊢ e' ≤ e: A.
Proof.
intros typed_e step_e σ subst_wt. eapply obs_preorder_closed_incl_step'.
- eapply subst_preserves. 1: exact subst_wt. eauto.
- eapply subst_preserves_step. easy.
Qed.
Lemma obs_preorder_incl_steps' Γ A e e':
Γ ⊢ e: A -> e ≻* e' -> Γ ⊢ e' ≤ e: A.
Proof.
intros typed_e step_e. induction step_e.
- eapply obs_preorder_incl_step'; eauto.
- eapply obs_preorder_refl; eauto.
- eapply obs_preorder_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_preorder_incl_steps'.
- now eapply obs_preorder_incl_steps.
Qed.
Lemma steps_preserve_obs_preorder Γ 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_preorder_trans with (t := s); eauto.
1: now apply obs_preorder_incl_steps'.
apply obs_preorder_trans with (t := t); eauto.
now apply obs_preorder_incl_steps.
Qed.
Lemma steps_preserve_obs_preorder_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_preorder_trans with (t := s'); eauto.
1: now apply obs_preorder_incl_steps.
apply obs_preorder_trans with (t := t'); eauto.
now apply obs_preorder_incl_steps'.
Qed.
Require Import Setoid Morphisms.
Instance rewrite_in_obs_preorder_base : Proper (steps ==> steps ==> iff) obs_preorder_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_preorder_base_bot t : obs_preorder_base bot t.
Proof.
eapply norm_bot_min. eauto.
Qed.
Hint Immediate obs_preorder_base_bot : core.
Lemma obs_preorder_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_preorder_base_refl : core.
Lemma evaluates_to_final s v : s ⇓ v -> v ⇓ v.
Proof.
firstorder.
Qed.
Hint Resolve evaluates_to_final : core.
Lemma obs_preorder_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_preorder_base_refl. eauto.
* rewrite H1, H2, IfF. eapply obs_preorder_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_preorder_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_preorder_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_preorder_closed (Fun T A') (Subst_tm σ (lam (fill ctxt s))) (Subst_tm σ (lam (fill ctxt t)))).
+ eapply H; eauto.
+ erewrite obs_preorder_closed_fun_char.
* intros x typed_x. specialize (IHtyped_c s t typed_s typed_t order_s_t).
eapply obs_preorder_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_preorder Γ' (Fun B C) (fill ctxt s) (fill ctxt t)).
+ eapply IHtyped_c.
all: eauto.
+ specialize (H0 σ subst_wt ).
eapply H0; eauto. eapply obs_preorder_closed_refl; eauto.
- specialize (IHtyped_c s t typed_s typed_t order_s_t). assert (H1: obs_preorder_closed (Fun B C) (Subst_tm σ trm) (Subst_tm σ trm)).
+ 1: eapply obs_preorder_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_preorder_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 -> cont_preorder Γ 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 -> cont_preorder Γ 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_preorder_closed A s t:
nil ⊢ s: A -> nil ⊢ t: A -> cont_preorder 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_preorder_closed_fun_char; eauto.
intros x typed_x. eapply IHA2.
1-2: eauto.
intros C typed_c v eval. red in H. specialize (H (comp C (pctxtAppL pctxtHole x))).
enough (H0: (fill (comp C (pctxtAppL pctxtHole x)) t) ⇓ v).
+ rewrite ctxt_comp_fill in H0. now cbn in H0.
+ eapply H.
* eapply ctxt_comp_typed; eauto.
* rewrite ctxt_comp_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 Γ σ (comp C1 C2) = comp (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)) = comp (lam_subst Γ (fun n : nat => σ (S n)) pctxtHole) (pctxtAppL (pctxtLam pctxtHole) (σ 0))).
+ rewrite H. rewrite ctxt_comp_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)) (comp pctxtHole (pctxtAppL (pctxtLam pctxtHole) (σ 0))) = comp (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_preorder Γ A s t:
Γ ⊢ s: A -> Γ ⊢ t: A -> cont_preorder Γ A s t -> Γ ⊢ s ≤ t: A.
Proof.
intros typed_s typed_t order σ subst_wt. eapply pre_order_imp_obs_preorder_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_comp_fill. eapply order. 1: eapply ctxt_comp_typed. 1: exact typed_c.
+ eapply lam_subst_typed; eauto.
+ rewrite ctxt_comp_fill. eapply step_eval. 1: eapply fill_step. 1: eapply lam_subst_step. all: eauto.
Qed.
Lemma cont_equiv_imp_obs_equiv Γ A s t:
Γ ⊢ s: A -> Γ ⊢ t: A -> Γ ⊢ s ≡c t: A -> Γ ⊢ s ≡ t: A.
Proof.
intros typed_s typed_t H. split.
all: apply pre_order_imp_obs_preorder; eauto; intros C typed_C v eval_v;
specialize (H C typed_C v); firstorder.
Qed.
Lemma cont_equiv_obs_equiv_agree Γ A s t:
Γ ⊢ s: A -> Γ ⊢ t: A -> Γ ⊢ s ≡c t: A <-> Γ ⊢ s ≡ t: A.
Proof.
intros typed_s typed_t . split.
1: now apply cont_equiv_imp_obs_equiv.
now apply obs_equiv_imp_cont_equiv.
Qed.
Definition rest_PCF Γ A := sig (fun t => Γ ⊢ t: A).
Definition cont_equiv_rest Γ A (p1 p2: rest_PCF Γ A) := cont_equiv Γ A (proj1_sig p1) (proj1_sig p2).
Instance cont_equiv_Equiv Γ A : Equivalence (cont_equiv_rest Γ A).
Proof.
split.
1, 2: firstorder.
intros [s Hs] [t Ht] [u Hu] H1 H2. unfold cont_equiv_rest in *. cbn in *.
intros C HC v. specialize (H1 C HC v). specialize (H2 C HC v). firstorder.
Qed.
Instance obs_equiv_obs_preorder Γ A: subrelation (obs_equiv Γ A) (obs_preorder Γ A).
Proof.
firstorder.
Qed.
Definition obs_preorder_rest Γ A (p1 p2: rest_PCF Γ A) := obs_preorder Γ A (proj1_sig p1) (proj1_sig p2).
Instance obs_preorder_PreOrder Γ A : PreOrder (obs_preorder_rest Γ A).
Proof.
split.
- intros [s Hs]. now eapply obs_preorder_refl.
- intros [s Hs] [t Ht] [u Hu]. now eapply obs_preorder_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_preorder_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_preorder_trans with (t := t).
Qed.
Lemma obs_equiv_refl Γ A s:
Γ ⊢ s: A -> Γ ⊢ s ≡ s: A.
Proof.
intros ?. split; now apply obs_preorder_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_preorder_trans with (t := t); eauto.
Qed.
Definition obs_equiv_rest Γ A (p1 p2: rest_PCF Γ A) := obs_equiv Γ A (proj1_sig p1) (proj1_sig p2).
Instance obs_equiv_Equiv Γ A : Equivalence (obs_equiv_rest Γ A).
Proof.
split.
- intros [s Hs]. unfold obs_equiv_rest. cbn. now apply obs_equiv_refl.
- intros [s Hs] [t Ht]. unfold obs_equiv_rest in *. cbn in *. firstorder.
- intros [s Hs] [t Ht] [u Hu]. unfold obs_equiv_rest in *. cbn in *. now apply obs_equiv_trans.
Qed.
Lemma obs_preorder_empty_imp_obs_preorder_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_tt_le' t:
nil ⊢ t: Base -> nil ⊢ tt ≤ t: Base <-> t ≻* tt.
Proof.
intros typed_t. split. 2: { intro H. constructor 2 with (z := tt); firstorder. rewrite closed_subst. 1: easy. eapply typed_empty_closed; eauto. }
intro H. specialize (H ids (subst_well_typed_nil_nil ids)).
asimpl in H. inversion H; 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_tt_le'' t:
nil ⊢ t: Base -> t ≻* tt <-> nil ⊢ tt ≡ t: Base.
Proof.
intros typed_t. split.
- intro H. split.
+ intros σ _. rewrite closed_subst. 2: easy. rewrite closed_subst. 2: eapply typed_empty_closed. 2: eauto.
constructor 2 with (z := tt); firstorder.
+ intros σ _. rewrite closed_subst. 2: eapply typed_empty_closed. 2: eauto. rewrite closed_subst. 2: easy.
constructor 2 with (z := tt); firstorder.
- intros [H1 _]. specialize (H1 ids (subst_well_typed_nil_nil ids)).
asimpl in H1. inversion H1; subst.
+ exfalso. enough (bot = tt) by easy.
apply bval_steps_char; easy.
+ enough (z = tt).
* destruct H0; now subst.
* destruct H0; apply bval_steps_char; firstorder.
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 base_preord_ff_le' t:
nil ⊢ t: Base -> nil ⊢ ff ≤ t: Base <-> t ≻* ff.
Proof.
intros typed_t. split. 2: { intro H. constructor 2 with (z := ff); firstorder. rewrite closed_subst. 1: easy. eapply typed_empty_closed; eauto. }
intro H. specialize (H ids (subst_well_typed_nil_nil ids)).
asimpl in H. inversion H; 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 base_preord_ff_le'' t:
nil ⊢ t: Base -> t ≻* ff <-> nil ⊢ ff ≡ t: Base.
Proof.
intros typed_t. split.
- intro H. split.
+ intros σ _. rewrite closed_subst. 2: easy. rewrite closed_subst. 2: eapply typed_empty_closed. 2: eauto.
constructor 2 with (z := ff); firstorder.
+ intros σ _. rewrite closed_subst. 2: eapply typed_empty_closed. 2: eauto. rewrite closed_subst. 2: easy.
constructor 2 with (z := ff); firstorder.
- intros [H1 _]. specialize (H1 ids (subst_well_typed_nil_nil ids)).
asimpl in H1. inversion H1; subst.
+ exfalso. enough (bot = ff) by easy.
apply bval_steps_char; easy.
+ enough (z = ff).
* destruct H0; now subst.
* destruct H0; apply bval_steps_char; firstorder.
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_preorder Γ A t t) by now apply strong_obs_preorder_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_preorder_empty_imp_obs_preorder_closed; eauto.
all: eapply typed_empty_closed; eauto.
- intros σ _. rewrite closed_subst, closed_subst. 1: apply obs_preorder_empty_imp_obs_preorder_closed; eauto.
all: eapply typed_empty_closed; eauto.
Qed.
Lemma ineq_ren Γ Γ' s t A r:
ren_well_typed Γ' Γ r -> Γ ⊢ s ≤ t: A -> Γ' ⊢ ren_tm r s ≤ ren_tm r t: A.
Proof.
intros ren_wt H.
intros σ subst_wt.
assert (H1: nil ⊢ (core.funcomp σ r) [Γ]).
- intros n A' H2. unfold core.funcomp. apply subst_wt.
now apply ren_wt.
- specialize (H (core.funcomp σ r) H1). now asimpl.
Qed.
Lemma ineq_subst Γ Γ' s t A σ:
subst_well_typed Γ' Γ σ -> Γ ⊢ s ≤ t: A -> Γ' ⊢ Subst_tm σ s ≤ Subst_tm σ t: A.
Proof.
intros subst_wt H.
intros σ' subst_wt'. asimpl.
apply H. intros n T Hn. unfold core.funcomp.
eapply subst_preserves. 1: eauto.
now apply subst_wt.
Qed.
From PCF2.Autosubst Require Import pcf_2 unscoped.
From PCF2 Require Import CE pcf_2_system pcf_2_contexts preliminaries.
Set Default Goal Selector "!".
Definition cont_preorder Γ A s t :=
forall (ctxt: pctxt), ctxt_typed ctxt Γ A nil Base -> forall v, (fill ctxt s) ⇓ v -> (fill ctxt t) ⇓ v.
Definition subst_rel (Γ: context) (σ1 : nat -> tm) (σ2 : nat -> tm) :=
forall n T, nth_error Γ n = Some T -> obs_preorder_closed T (σ1 n) (σ2 n).
Definition strong_obs_preorder (Γ: context) (A: ty): tm -> tm -> Prop :=
fun t1 t2 => forall σ1, nil ⊢ σ1 [ Γ ] -> forall σ2, nil ⊢ σ2 [ Γ ] -> subst_rel Γ σ1 σ2
-> obs_preorder_closed A (Subst_tm σ1 t1) (Subst_tm σ2 t2).
Lemma obs_preorder_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_preorder_steps Γ A s s' t t':
Γ ⊢ s: A -> Γ ⊢ t: A -> s ≻ s' -> t ≻ t'
-> strong_obs_preorder Γ A s' t' -> strong_obs_preorder Γ 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_preorder_closed_steps; eauto.
all: eapply subst_preserves_step; eauto.
Qed.
Lemma strong_obs_preorder_refl Γ A s:
typed Γ s A -> strong_obs_preorder Γ 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_preorder_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_preorder_closed_refl A s:
typed nil s A -> s ≤c s: A.
Proof.
intros typed_s.
assert (H: strong_obs_preorder nil A s s).
- now apply strong_obs_preorder_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_preorder_imp_obs_preorder:
forall Γ A s t, strong_obs_preorder Γ 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_preorder_closed_refl.
red in subst_wf. apply subst_wf. easy.
Qed.
Lemma obs_preorder_refl Γ A s:
typed Γ s A -> Γ ⊢ s ≤ s : A.
Proof.
intros H.
apply strong_obs_preorder_imp_obs_preorder.
now apply strong_obs_preorder_refl.
Qed.
Lemma obs_preorder_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_preorder_closed_refl.
Qed.
Lemma obs_preorder_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_preorder_closed_trans _ _ (Subst_tm σ t) _).
all: eauto.
Qed.
Lemma obs_preorder_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_preorder_closed A x x).
+ specialize (H x x typed_x typed_x H0). easy.
+ apply obs_preorder_closed_refl. easy.
- intros H a b typed_a typed_b order_a_b.
eapply (obs_preorder_closed_trans _ _ (app g a) _).
1-3: eapply app_typed. all: eauto.
enough (H0: obs_preorder_closed (Fun A B) g g).
+ eapply H0. all: easy.
+ now apply obs_preorder_closed_refl.
Qed.
Lemma obs_preorder_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_preorder nil A x x).
+ intros σ subst_wf.
enough (H1: obs_preorder_closed (Fun A B) (Subst_tm σ f) (Subst_tm σ g) <-> forall x, typed nil x A -> obs_preorder_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_preorder_closed_fun_char.
all: eapply subst_preserves; eauto.
+ now eapply obs_preorder_refl.
- intros H σ subst_wf. enough (H1: obs_preorder_closed (Fun A B) (Subst_tm σ f) (Subst_tm σ g) <-> forall x, typed nil x A -> obs_preorder_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_preorder_closed_fun_char.
all: eapply subst_preserves; eauto.
Qed.
Lemma obs_preorder_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_preorder_closed_fun_char.
+ intros x typed_x. eapply IHA2. all: eauto.
+ eauto.
+ eapply type_preservation. all: eauto.
Qed.
Lemma obs_preorder_incl_step Γ A e e':
Γ ⊢ e: A -> e ≻ e' -> Γ ⊢ e ≤ e': A.
Proof.
intros typed_e step_e σ subst_wt. eapply obs_preorder_closed_incl_step.
- eapply subst_preserves. 1: exact subst_wt. eauto.
- eapply subst_preserves_step. easy.
Qed.
Lemma obs_preorder_incl_steps Γ A e e':
Γ ⊢ e: A -> e ≻* e' -> Γ ⊢ e ≤ e': A.
Proof.
intros typed_e step_e. induction step_e.
- eapply obs_preorder_incl_step; eauto.
- eapply obs_preorder_refl; eauto.
- eapply obs_preorder_trans with (t := y); eauto.
3: apply IHstep_e2.
all: eapply type_preservation; eauto.
Qed.
Lemma obs_preorder_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_preorder_closed_fun_char.
+ intros x typed_x. eapply IHA2. all: eauto.
+ eapply type_preservation. all: eauto.
+ eauto.
Qed.
Lemma obs_preorder_incl_step' Γ A e e':
Γ ⊢ e: A -> e ≻ e' -> Γ ⊢ e' ≤ e: A.
Proof.
intros typed_e step_e σ subst_wt. eapply obs_preorder_closed_incl_step'.
- eapply subst_preserves. 1: exact subst_wt. eauto.
- eapply subst_preserves_step. easy.
Qed.
Lemma obs_preorder_incl_steps' Γ A e e':
Γ ⊢ e: A -> e ≻* e' -> Γ ⊢ e' ≤ e: A.
Proof.
intros typed_e step_e. induction step_e.
- eapply obs_preorder_incl_step'; eauto.
- eapply obs_preorder_refl; eauto.
- eapply obs_preorder_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_preorder_incl_steps'.
- now eapply obs_preorder_incl_steps.
Qed.
Lemma steps_preserve_obs_preorder Γ 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_preorder_trans with (t := s); eauto.
1: now apply obs_preorder_incl_steps'.
apply obs_preorder_trans with (t := t); eauto.
now apply obs_preorder_incl_steps.
Qed.
Lemma steps_preserve_obs_preorder_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_preorder_trans with (t := s'); eauto.
1: now apply obs_preorder_incl_steps.
apply obs_preorder_trans with (t := t'); eauto.
now apply obs_preorder_incl_steps'.
Qed.
Require Import Setoid Morphisms.
Instance rewrite_in_obs_preorder_base : Proper (steps ==> steps ==> iff) obs_preorder_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_preorder_base_bot t : obs_preorder_base bot t.
Proof.
eapply norm_bot_min. eauto.
Qed.
Hint Immediate obs_preorder_base_bot : core.
Lemma obs_preorder_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_preorder_base_refl : core.
Lemma evaluates_to_final s v : s ⇓ v -> v ⇓ v.
Proof.
firstorder.
Qed.
Hint Resolve evaluates_to_final : core.
Lemma obs_preorder_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_preorder_base_refl. eauto.
* rewrite H1, H2, IfF. eapply obs_preorder_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_preorder_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_preorder_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_preorder_closed (Fun T A') (Subst_tm σ (lam (fill ctxt s))) (Subst_tm σ (lam (fill ctxt t)))).
+ eapply H; eauto.
+ erewrite obs_preorder_closed_fun_char.
* intros x typed_x. specialize (IHtyped_c s t typed_s typed_t order_s_t).
eapply obs_preorder_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_preorder Γ' (Fun B C) (fill ctxt s) (fill ctxt t)).
+ eapply IHtyped_c.
all: eauto.
+ specialize (H0 σ subst_wt ).
eapply H0; eauto. eapply obs_preorder_closed_refl; eauto.
- specialize (IHtyped_c s t typed_s typed_t order_s_t). assert (H1: obs_preorder_closed (Fun B C) (Subst_tm σ trm) (Subst_tm σ trm)).
+ 1: eapply obs_preorder_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_preorder_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 -> cont_preorder Γ 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 -> cont_preorder Γ 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_preorder_closed A s t:
nil ⊢ s: A -> nil ⊢ t: A -> cont_preorder 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_preorder_closed_fun_char; eauto.
intros x typed_x. eapply IHA2.
1-2: eauto.
intros C typed_c v eval. red in H. specialize (H (comp C (pctxtAppL pctxtHole x))).
enough (H0: (fill (comp C (pctxtAppL pctxtHole x)) t) ⇓ v).
+ rewrite ctxt_comp_fill in H0. now cbn in H0.
+ eapply H.
* eapply ctxt_comp_typed; eauto.
* rewrite ctxt_comp_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 Γ σ (comp C1 C2) = comp (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)) = comp (lam_subst Γ (fun n : nat => σ (S n)) pctxtHole) (pctxtAppL (pctxtLam pctxtHole) (σ 0))).
+ rewrite H. rewrite ctxt_comp_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)) (comp pctxtHole (pctxtAppL (pctxtLam pctxtHole) (σ 0))) = comp (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_preorder Γ A s t:
Γ ⊢ s: A -> Γ ⊢ t: A -> cont_preorder Γ A s t -> Γ ⊢ s ≤ t: A.
Proof.
intros typed_s typed_t order σ subst_wt. eapply pre_order_imp_obs_preorder_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_comp_fill. eapply order. 1: eapply ctxt_comp_typed. 1: exact typed_c.
+ eapply lam_subst_typed; eauto.
+ rewrite ctxt_comp_fill. eapply step_eval. 1: eapply fill_step. 1: eapply lam_subst_step. all: eauto.
Qed.
Lemma cont_equiv_imp_obs_equiv Γ A s t:
Γ ⊢ s: A -> Γ ⊢ t: A -> Γ ⊢ s ≡c t: A -> Γ ⊢ s ≡ t: A.
Proof.
intros typed_s typed_t H. split.
all: apply pre_order_imp_obs_preorder; eauto; intros C typed_C v eval_v;
specialize (H C typed_C v); firstorder.
Qed.
Lemma cont_equiv_obs_equiv_agree Γ A s t:
Γ ⊢ s: A -> Γ ⊢ t: A -> Γ ⊢ s ≡c t: A <-> Γ ⊢ s ≡ t: A.
Proof.
intros typed_s typed_t . split.
1: now apply cont_equiv_imp_obs_equiv.
now apply obs_equiv_imp_cont_equiv.
Qed.
Definition rest_PCF Γ A := sig (fun t => Γ ⊢ t: A).
Definition cont_equiv_rest Γ A (p1 p2: rest_PCF Γ A) := cont_equiv Γ A (proj1_sig p1) (proj1_sig p2).
Instance cont_equiv_Equiv Γ A : Equivalence (cont_equiv_rest Γ A).
Proof.
split.
1, 2: firstorder.
intros [s Hs] [t Ht] [u Hu] H1 H2. unfold cont_equiv_rest in *. cbn in *.
intros C HC v. specialize (H1 C HC v). specialize (H2 C HC v). firstorder.
Qed.
Instance obs_equiv_obs_preorder Γ A: subrelation (obs_equiv Γ A) (obs_preorder Γ A).
Proof.
firstorder.
Qed.
Definition obs_preorder_rest Γ A (p1 p2: rest_PCF Γ A) := obs_preorder Γ A (proj1_sig p1) (proj1_sig p2).
Instance obs_preorder_PreOrder Γ A : PreOrder (obs_preorder_rest Γ A).
Proof.
split.
- intros [s Hs]. now eapply obs_preorder_refl.
- intros [s Hs] [t Ht] [u Hu]. now eapply obs_preorder_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_preorder_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_preorder_trans with (t := t).
Qed.
Lemma obs_equiv_refl Γ A s:
Γ ⊢ s: A -> Γ ⊢ s ≡ s: A.
Proof.
intros ?. split; now apply obs_preorder_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_preorder_trans with (t := t); eauto.
Qed.
Definition obs_equiv_rest Γ A (p1 p2: rest_PCF Γ A) := obs_equiv Γ A (proj1_sig p1) (proj1_sig p2).
Instance obs_equiv_Equiv Γ A : Equivalence (obs_equiv_rest Γ A).
Proof.
split.
- intros [s Hs]. unfold obs_equiv_rest. cbn. now apply obs_equiv_refl.
- intros [s Hs] [t Ht]. unfold obs_equiv_rest in *. cbn in *. firstorder.
- intros [s Hs] [t Ht] [u Hu]. unfold obs_equiv_rest in *. cbn in *. now apply obs_equiv_trans.
Qed.
Lemma obs_preorder_empty_imp_obs_preorder_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_tt_le' t:
nil ⊢ t: Base -> nil ⊢ tt ≤ t: Base <-> t ≻* tt.
Proof.
intros typed_t. split. 2: { intro H. constructor 2 with (z := tt); firstorder. rewrite closed_subst. 1: easy. eapply typed_empty_closed; eauto. }
intro H. specialize (H ids (subst_well_typed_nil_nil ids)).
asimpl in H. inversion H; 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_tt_le'' t:
nil ⊢ t: Base -> t ≻* tt <-> nil ⊢ tt ≡ t: Base.
Proof.
intros typed_t. split.
- intro H. split.
+ intros σ _. rewrite closed_subst. 2: easy. rewrite closed_subst. 2: eapply typed_empty_closed. 2: eauto.
constructor 2 with (z := tt); firstorder.
+ intros σ _. rewrite closed_subst. 2: eapply typed_empty_closed. 2: eauto. rewrite closed_subst. 2: easy.
constructor 2 with (z := tt); firstorder.
- intros [H1 _]. specialize (H1 ids (subst_well_typed_nil_nil ids)).
asimpl in H1. inversion H1; subst.
+ exfalso. enough (bot = tt) by easy.
apply bval_steps_char; easy.
+ enough (z = tt).
* destruct H0; now subst.
* destruct H0; apply bval_steps_char; firstorder.
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 base_preord_ff_le' t:
nil ⊢ t: Base -> nil ⊢ ff ≤ t: Base <-> t ≻* ff.
Proof.
intros typed_t. split. 2: { intro H. constructor 2 with (z := ff); firstorder. rewrite closed_subst. 1: easy. eapply typed_empty_closed; eauto. }
intro H. specialize (H ids (subst_well_typed_nil_nil ids)).
asimpl in H. inversion H; 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 base_preord_ff_le'' t:
nil ⊢ t: Base -> t ≻* ff <-> nil ⊢ ff ≡ t: Base.
Proof.
intros typed_t. split.
- intro H. split.
+ intros σ _. rewrite closed_subst. 2: easy. rewrite closed_subst. 2: eapply typed_empty_closed. 2: eauto.
constructor 2 with (z := ff); firstorder.
+ intros σ _. rewrite closed_subst. 2: eapply typed_empty_closed. 2: eauto. rewrite closed_subst. 2: easy.
constructor 2 with (z := ff); firstorder.
- intros [H1 _]. specialize (H1 ids (subst_well_typed_nil_nil ids)).
asimpl in H1. inversion H1; subst.
+ exfalso. enough (bot = ff) by easy.
apply bval_steps_char; easy.
+ enough (z = ff).
* destruct H0; now subst.
* destruct H0; apply bval_steps_char; firstorder.
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_preorder Γ A t t) by now apply strong_obs_preorder_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_preorder_empty_imp_obs_preorder_closed; eauto.
all: eapply typed_empty_closed; eauto.
- intros σ _. rewrite closed_subst, closed_subst. 1: apply obs_preorder_empty_imp_obs_preorder_closed; eauto.
all: eapply typed_empty_closed; eauto.
Qed.
Lemma ineq_ren Γ Γ' s t A r:
ren_well_typed Γ' Γ r -> Γ ⊢ s ≤ t: A -> Γ' ⊢ ren_tm r s ≤ ren_tm r t: A.
Proof.
intros ren_wt H.
intros σ subst_wt.
assert (H1: nil ⊢ (core.funcomp σ r) [Γ]).
- intros n A' H2. unfold core.funcomp. apply subst_wt.
now apply ren_wt.
- specialize (H (core.funcomp σ r) H1). now asimpl.
Qed.
Lemma ineq_subst Γ Γ' s t A σ:
subst_well_typed Γ' Γ σ -> Γ ⊢ s ≤ t: A -> Γ' ⊢ Subst_tm σ s ≤ Subst_tm σ t: A.
Proof.
intros subst_wt H.
intros σ' subst_wt'. asimpl.
apply H. intros n T Hn. unfold core.funcomp.
eapply subst_preserves. 1: eauto.
now apply subst_wt.
Qed.