From Coq Require Import List.
From PCF2.Autosubst Require Import unscoped pcf_2.
From PCF2 Require Import pcf_2_system RPS CE CE_facts preliminaries RPS RPS_facts.
From PCF2.external.Synthetic Require Import Definitions.
Set Default Goal Selector "!".
Fixpoint G (sys: rps_system) :=
match sys with
|nil => tt
|cons p sys' =>
match snd p with
|true => trny (fst p) (G sys') bot
|false => trny (fst p) bot (G sys')
end
end.
Lemma G_typed (sys: rps_system) (T: ty):
rps_system_well_formed sys T -> cons T nil ⊢ G sys: Base.
Proof.
induction sys; cbn.
- intros _. assert (H: T :: nil = nil ++ T :: nil) by easy.
rewrite H. now eapply type_weakening.
- intros sys_wf. rewrite riq_sys_wf_cons_char in sys_wf.
destruct sys_wf as [sys_wf typed_a].
destruct (snd a).
+ constructor; eauto.
+ constructor; eauto.
Qed.
Lemma G_steps (sys: rps_system) (sol: tm) (T: ty):
nil ⊢ sol: T -> rps_system_well_formed sys T -> Subst_tm (scons sol ids) (G sys) ≻* tt \/ Subst_tm (scons sol ids) (G sys) ≻* bot.
Proof.
intros typed_sol sys_wf.
induction sys; cbn in *.
- now left.
- rewrite riq_sys_wf_cons_char in sys_wf. destruct sys_wf as [sys_wf typed_a].
assert (nil ⊢ Subst_tm (scons sol ids) (fst a): Base).
+ eapply subst_preserves.
2: eauto.
eapply subst_well_typed_singleton; eauto.
+ destruct (weak_normalisation_comp (Subst_tm (scons sol ids) (fst a)) H) as [trm [stp val]]; destruct trm; try easy; destruct (snd a) eqn: e; subst; cbn.
* destruct (IHsys sys_wf).
-- left. now rewrite stp, IfT.
-- right. now rewrite stp, IfT.
* right. now rewrite stp, IfT.
* right. now rewrite stp, IfF.
* destruct (IHsys sys_wf).
-- left. now rewrite stp, IfF.
-- right. now rewrite stp, IfF.
* right. now rewrite stp, IfB.
* right. now rewrite stp, IfB.
Qed.
Lemma G_subst (sys: rps_system) (T: ty) σ:
rps_system_well_formed sys T -> Subst_tm σ (G sys) = Subst_tm (scons (σ 0) ids) (G sys).
Proof.
intros sys_wf. eapply subst_charact_typed.
- apply G_typed; eauto.
- intros n A H. destruct n; cbn in H; eauto.
destruct n; easy.
Qed.
Lemma G_solves (sys: rps_system) (sol: tm) (T: ty):
nil ⊢ sol: T -> rps_system_well_formed sys T -> solves_rps_system sys sol <-> Subst_tm (scons sol ids) (G sys) ≻* tt.
Proof.
intros typed_sol sys_wf. split.
- intros solves. induction sys; cbn.
+ easy.
+ rewrite riq_sys_wf_cons_char in sys_wf. destruct sys_wf as [sys_wf a_typ]. rewrite res_ineq_sys_val_cons_char in solves. destruct solves as [sys_sol new_sol]. destruct (snd a) eqn: e; cbn.
* destruct (weak_normalisation_comp (Subst_tm (scons sol ids) (fst a))) as [trm [a_stp a_frm]].
-- eapply subst_preserves; eauto. now eapply subst_well_typed_singleton.
-- destruct trm; try easy.
++ rewrite a_stp, IfT. apply IHsys; eauto.
++ exfalso. cbn in new_sol. inv new_sol.
** enough (bot = tt) by easy. apply bval_steps_char; eauto.
** enough (ff = tt) by easy. apply bval_steps_char; eauto.
destruct H. enough (ff = z) by now subst.
eapply evaluates_to_same; eauto. split; eauto.
++ exfalso. cbn in new_sol. inv new_sol.
** enough (bot = tt) by easy. apply bval_steps_char; eauto.
** enough (bot = tt) by easy. apply bval_steps_char; eauto.
destruct H. enough (bot = z) by now subst.
eapply evaluates_to_same; eauto. split; eauto.
* destruct (weak_normalisation_comp (Subst_tm (scons sol ids) (fst a))) as [trm [a_stp a_frm]].
-- eapply subst_preserves; eauto. now eapply subst_well_typed_singleton.
-- destruct trm; try easy.
++ exfalso. cbn in new_sol. inv new_sol.
** enough (bot = ff) by easy. apply bval_steps_char; eauto.
** enough (tt = ff) by easy. apply bval_steps_char; eauto.
destruct H. enough (tt = z) by now subst.
eapply evaluates_to_same; eauto. split; eauto.
++ rewrite a_stp, IfF. apply IHsys; eauto.
++ exfalso. cbn in new_sol. inv new_sol.
** enough (bot = ff) by easy. apply bval_steps_char; eauto.
** enough (bot = ff) by easy. apply bval_steps_char; eauto.
destruct H. enough (bot = z) by now subst.
eapply evaluates_to_same; eauto. split; eauto.
- intros H. induction sys as [ | a sys].
+ eapply Forall_nil.
+ cbn. rewrite riq_sys_wf_cons_char in sys_wf. destruct sys_wf as [sys_wf a_typ].
cbn in H. eapply res_ineq_sys_val_cons_char.
destruct (weak_normalisation_comp (Subst_tm (scons sol ids) (fst a))) as [trm [a_stp a_frm]].
* eapply subst_preserves; eauto. now eapply subst_well_typed_singleton.
* split.
-- apply IHsys; eauto. destruct trm; try easy; destruct (snd a) eqn: e; cbn in H; cbn; subst.
++ enough (H1: Subst_tm (scons sol ids) (G sys) ⇓ tt) by now destruct H1.
eapply (eval_step (trny (Subst_tm (scons sol ids) (fst a)) (Subst_tm (scons sol ids) (G sys)) bot)).
** now rewrite a_stp, IfT.
** split; eauto.
++ enough (H1: tt = bot) by now easy.
eapply bval_steps_char; eauto.
eapply (eval_step (trny (Subst_tm (scons sol ids) (fst a)) bot (Subst_tm (scons sol ids) (G sys)))).
** now rewrite a_stp, IfT.
** split; eauto.
++ enough (H1: tt = bot) by now easy.
eapply bval_steps_char; eauto.
eapply (eval_step (trny (Subst_tm (scons sol ids) (fst a)) (Subst_tm (scons sol ids) (G sys)) bot)).
** now rewrite a_stp, IfF.
** split; eauto.
++ enough (H1: Subst_tm (scons sol ids) (G sys) ⇓ tt) by now destruct H1.
eapply (eval_step (trny (Subst_tm (scons sol ids) (fst a)) bot (Subst_tm (scons sol ids) (G sys)))).
** now rewrite a_stp, IfF.
** split; eauto.
++ enough (H1: tt = bot) by now easy.
eapply bval_steps_char; eauto.
eapply (eval_step (trny (Subst_tm (scons sol ids) (fst a)) (Subst_tm (scons sol ids) (G sys)) bot)).
** now rewrite a_stp, IfB.
** split; eauto.
++ enough (H1: tt = bot) by now easy.
eapply bval_steps_char; eauto.
eapply (eval_step (trny (Subst_tm (scons sol ids) (fst a)) bot (Subst_tm (scons sol ids) (G sys)))).
** now rewrite a_stp, IfB.
** split; eauto.
-- destruct trm; try easy; destruct (snd a) eqn: e; cbn in *; subst.
++ eapply (norm_comp _ _ tt); split; eauto.
++ enough (tt = bot) by easy.
eapply bval_steps_char; eauto.
eapply (eval_step (trny (Subst_tm (scons sol ids) (fst a)) bot (Subst_tm (scons sol ids) (G sys)))).
** now rewrite a_stp, IfT.
** split; eauto.
++ enough (tt = bot) by easy.
eapply bval_steps_char; eauto.
eapply (eval_step (trny (Subst_tm (scons sol ids) (fst a)) (Subst_tm (scons sol ids) (G sys)) bot)).
** now rewrite a_stp, IfF.
** split; eauto.
++ eapply (norm_comp _ _ ff); split; eauto.
++ enough (tt = bot) by easy.
eapply bval_steps_char; eauto.
eapply (eval_step (trny (Subst_tm (scons sol ids) (fst a)) (Subst_tm (scons sol ids) (G sys)) bot)).
** now rewrite a_stp, IfB.
** split; eauto.
++ enough (tt = bot) by easy.
eapply bval_steps_char; eauto.
eapply (eval_step (trny (Subst_tm (scons sol ids) (fst a)) bot (Subst_tm (scons sol ids) (G sys)))).
** now rewrite a_stp, IfB.
** split; eauto.
Qed.
Lemma G_charact' (T: ty) (sys: rps_system):
rps_system_well_formed sys T -> nil ⊢ lam (G sys) ≡ lam bot: T ⟶ Base <-> ~ rps_system_solvable sys T.
Proof.
intros sys_wf. split.
- intros equiv [sol [sol_typed Hsol]]. destruct equiv as [le ge].
assert (lam (G sys) ≤c lam bot : T ⟶ Base ).
+ eapply obs_preorder_empty_imp_obs_preorder_closed.
2-3: eauto. constructor. now eapply G_typed.
+ rewrite obs_preorder_closed_fun_char in H. 2: constructor; eapply G_typed. 2-3: eauto.
specialize (H sol sol_typed). rewrite Beta, Beta in H. rewrite (closed_subst bot) in H. 2: easy.
rewrite (G_solves sys sol T sol_typed sys_wf) in Hsol.
enough (tt = bot) by easy.
eapply (evaluates_to_same (Subst_tm (scons sol ids) (G sys))).
all: split; eauto.
now apply base_preord_le_bot.
- intros H. split.
+ intros σ subst_wt. rewrite closed_subst.
2: eapply typed_empty_closed; constructor; eapply G_typed; eauto.
rewrite closed_subst. 2: firstorder.
eapply obs_preorder_closed_fun_char.
1, 2: constructor. 1: eapply G_typed. 1, 2: easy.
intros a typed_a.
rewrite Beta, Beta.
rewrite (closed_subst bot).
2: easy.
constructor.
destruct (G_steps sys a T typed_a sys_wf).
2: easy.
exfalso. apply H. exists a. split; eauto.
erewrite G_solves; eauto.
+ intros σ subst_wt. rewrite closed_subst.
2: firstorder. rewrite closed_subst.
2: eapply typed_empty_closed; constructor; eapply G_typed; eauto.
eapply obs_preorder_closed_fun_char.
1, 2: constructor. 2: eapply G_typed. 1, 2: easy.
intros x typed_x. constructor. rewrite Beta.
rewrite closed_subst; eauto. firstorder.
Qed.
Lemma reduces_co_RPS_CE_closed:
reduces (complement RPS) CE.
Proof.
exists (fun p => ((lam (G (fst (proj1_sig p))), lam bot), (snd (proj1_sig p)) ⟶ Base)).
intros [[sys T] H]; cbn. erewrite cont_equiv_obs_equiv_agree. 1: now rewrite (G_charact' T sys H).
1: constructor; now apply G_typed. constructor. assert (eq: T :: nil = nil ++ T :: nil) by easy.
rewrite eq. now apply type_weakening.
Qed.