Require Import HOcore.Prelim.

Require Import HOcore.ComplLat
               HOcore.CondClos
               HOcore.Multiset
               HOcore.Subst
               HOcore.Bis.

(* Needs reflexivity, var bisim *)
Global Instance ho_out_substit_cond_clos:
  CondClos
    s_ho_out
    subst_clos
    refl_clos
    s_var_cxt.
Proof.
  intros x H1 H2 H32 p' q' [sigma [p [q [H4 [H5 H6]]]]]. subst.
  specialize (H2 p q H4).
  intros a p'' p' H5.
  apply step_out_inv_subst in H5.
  destruct H5 as [[p2' [p2'' [H5 [H6 H7]]]] | [n [p2' [C [H5 [H6 H7]]]]]]; subst.
  - rename p2'' into p''. rename p2' into p'.
    specialize (H32 p q H4 a p'' p' H5).
    destruct H32 as [q'' [q' H3]].
    decompose [and] H3. clear H3.
    repeat eexists; eauto.
    now apply step_out_substit.
  - rename p2' into p'.
    (* need var_bis *)
    specialize (H2 n C H6).
    destruct H2 as [q' [H7 H8]]. rename q' into C'.
    exists p'', C'.[p' .: sigma]. repeat split; auto.
    + eapply step_out_propagation_cxt. eauto. auto.
    + repeat eexists. intuition.
    + (* need refl *)
      apply subst_clos_ext. now apply H1.
Qed.

(* no need of refl, but need var bisim *)
Global Instance ho_in_substit_cond_clos:
  CondClos
    s_ho_in
    subst_clos
    (const bot2) (* no assumptions for y *)
    s_var_cxt.
Proof.
  intros x H1 H2 H32 p' q' [sigma [p [q [H7 [H8 H9]]]]]. subst.
  specialize (H32 p q H7).
  intros a p' H8.
  apply step_in_inv_subst in H8.
  destruct H8 as [[p2' [H8 H9]] | [n [p2' [C [H8 [H9 H10]]]]]]; subst.
  - rename p2' into p'.
    specialize (H32 a p' H8).
    destruct H32 as [q' H3].
    decompose [and] H3. clear H3.
    eexists. split.
    + eapply step_in_substit; eauto.
    + now repeat eexists.
  - rename p2' into p'.
    specialize (H2 p q H7 n C H9).
    destruct H2 as [q' H12].
    decompose [and] H12. clear H12.
    eexists. split.
    + eapply step_in_propagation_cxt; eauto.
    + repeat eexists. intuition.
Qed.

Global Instance var_substit_cond_clos:
  CondClos
    s_var_cxt
    subst_clos
    (const bot2)
    (const top2).
Proof.
  intros x H1 H2 H3 p' q' [sigma [p [q [H4 [H5 H6]]]]]. subst.
  intros n p' H5.
  apply step_var_cxt_inv_subst in H5.
  destruct H5 as [v [C [s [H5 [H6 H7]]]]]. subst.
  specialize (H3 p q H4 v C H5).
  destruct H3 as [C' [H7 H8]].
  eexists. split.
  - eapply context_fill_step_var_cxt; eauto.
  - now repeat eexists.
Qed.

Global Instance var_multi_substit_cond_clos:
  CondClos
    s_var_multi
    subst_clos
    id
    (const top2).
Proof.
  intros x H1 H2 H32 p' q' [sigma [p [q [H4 [H5 H6]]]]]. subst.
  hnf.
  - intros n.
    specialize (H32 p q H4).
    do 2 rewrite fin_sum_lemma.
    now apply mle_impl_less_equal_fin_sums.
Qed.