Require Import HOcore.Prelim.

Require Import HOcore.Compat
               HOcore.HoCore
               HOcore.Multiset
               HOcore.Ren
               HOcore.Subst
               HOcore.Bis.

Global Instance inj_ren_clos_compat_for_s_ho_out:
  Compat s_ho_out decidable_inj_ren_clos.
Proof.
  intros x y H1 p' q' [xi [sigma [p [q [[H41 H42] [H51 [H52 H6]]]]]]]. subst.
  intros a p'' p' H6.
  destruct (step_out_preserv_ren H6) as [p2' [p2'' [H7 [H81 H82]]]].
  subst.
  destruct (H1 p q H51 a p2'' p2' H82) as [q2'' [q2' [H7 [H8 H9]]]].
  exists q2''.[ren xi], q2'.[ren xi]. repeat split.
  - now apply step_out_substit with (sigma := ren xi) in H7.
  - exists xi, sigma, p2', q2'. repeat split; auto.
  - exists xi, sigma, p2'', q2''. repeat split; auto.
Qed.

(* Injective renaming function is compatible for s_ho_in *)
Global Instance inj_ren_clos_compat_for_s_ho_in:
  Compat s_ho_in decidable_inj_ren_clos.
Proof.
  intros x y H1 p' q' [xi [sigma [p [q [[H41 H42] [H51 [H52 H53]]]]]]].
  subst.
  intros a p' H6.
  destruct (step_in_preserv_ren H6) as [p2' [H71 H72]]. subst.
  destruct (H1 p q H51 a p2' H72) as [q2' [H7 H8]].
  exists q2'.[up (ren xi)]. split.
  - eapply step_in_substit; eauto.
  - exists (upren xi), (up sigma), p2', q2'.
    repeat split; asimpl; eauto.
    + pose (H9 := upren_preserv_inj).
      specialize (H9 xi sigma H41). now asimpl in H9.
    + intros n.
      destruct n.
      * left. exists 0. now asimpl.
      * {
          destruct (H42 n) as [[n' H9] | H9].
          - left. exists (S n'). asimpl. now rewrite H9.
          - right. intros [n' H91].
            destruct n'.
            + asimpl in H91. omega.
            + apply H9. exists n'. asimpl in H91.
              congruence.
        }
Qed.

Global Instance inj_ren_clos_compat_for_s_var_cxt:
  Compat s_var_cxt decidable_inj_ren_clos.
Proof.
  intros x y H1 p' q' [xi [sigma [p [q [[H21 H22] [H31 [H32 H33]]]]]]].
  subst.
  intros n C H4.
  destruct (step_var_cxt_preserv_ren H4) as [n2 [p2' [H5 [H6 H7]]]].
  subst.
  destruct (H1 p q H31 n2 p2' H7) as [q2' [H51 H52]].
  eexists. split.
  - apply step_var_cxt_substit_ren. eauto.
  - hnf.
    exists (upren xi), (up sigma). exists p2', q2'. split.
    + apply upren_preserv_dec_inj_ren. split; auto.
    + now repeat split.
Qed.

Global Instance inj_ren_clos_compat_for_s_var_multi:
  Compat s_var_multi decidable_inj_ren_clos.
Proof.
  intros x y H1 p' q' [xi [sigma [p [q [[H21 H22] [H31 [H32 H33]]]]]]].
  subst.
  specialize (H1 p q H31).
  - intros n.
    destruct (H22 n) as [[v H6] | H6]; clear H22.
    + rewrite <- H6.
      specialize (H1 v).
      rewrite renaming_preserv_count with (xi := xi) (sigma := sigma) in H1; auto.
      remember (mult (count q) v) as z.
      rewrite renaming_preserv_count with (xi := xi) (sigma := sigma) in Heqz; auto. subst z.
      auto.
    + assert (H7: forall n', xi n' <> n).
      { repeat intro. apply H6. eexists. eauto. }
      assert (mult (count p.[ren xi]) n = 0).
      {
        clear H1 H31.
        induction p; try (asimpl; omega).
        - asimpl. specialize (H7 v).
          simpl.
          destruct (nat_dec (xi v) n).
          + exfalso. now apply H7.
          + omega.
        - asimpl. rewrite union_mult. omega.
      }
      omega.
Qed.