Z theorem

z.v

Require Import Relations.
From mathcomp Require Import all_ssreflect.
From Autosubst Require Import Autosubst.

Hint Constructors clos_refl_trans.

Section ARS.
  Variable A : Type.
  Variable R : A -> A -> Prop.

  Definition confluent :=
    forall x y, clos_refl_trans _ R x y ->
      forall z, clos_refl_trans _ R x z ->
      exists w, clos_refl_trans _ R y w /\ clos_refl_trans _ R z w.

  Definition semi_confluent :=
    forall x y, R x y ->
      forall z, clos_refl_trans _ R x z ->
      exists w, clos_refl_trans _ R y w /\ clos_refl_trans _ R z w.

  Theorem semi_confluent_impl_confluent :
    semi_confluent ->
    confluent.
  Proof.
    move => Hsemi ? ? /clos_rt_rt1n_iff.
    elim => [ | ? ? ? HR ? IH ? /(Hsemi _ _ HR) [ ? [ /IH [ ? [ ] ] ] ] ]; eauto.
  Qed.

  Theorem Z map :
    (forall x y, R x y -> clos_refl_trans _ R y (map x)) ->
    (forall x y, R x y -> clos_refl_trans _ R (map x) (map y)) ->
    confluent.
  Proof.
    move => Zproperty1 Zproperty2.
    have monotonicity : forall x y,
      clos_refl_trans _ R x y ->
      clos_refl_trans _ R (map x) (map y).
    { induction 1; eauto. }
    apply: semi_confluent_impl_confluent => ? ? ? ? /clos_rt_rtn1_iff Hrt.
    inversion Hrt; subst; eauto.
    move: (H0) => /clos_rt_rtn1_iff /monotonicity ?.
    eauto 6.
  Qed.
End ARS.

Section Lambda.
  Inductive term :=
    | Var of var
    | Abs of {bind term}
    | App of term & term.

  Instance Ids_term : Ids term. derive. Defined.
  Instance Rename_term : Rename term. derive. Defined.
  Instance Subst_term : Subst term. derive. Defined.
  Instance SubstLemmas_term : SubstLemmas term. derive. Qed.

  Inductive red : term -> term -> Prop :=
    | red_appl t1 t1' t2 : red t1 t1' -> red (App t1 t2) (App t1' t2)
    | red_appr t1 t2 t2' : red t2 t2' -> red (App t1 t2) (App t1 t2')
    | red_abs t t' : red t t' -> red (Abs t) (Abs t')
    | red_beta t11 t2 : red (App (Abs t11) t2) t11.[t2/].

  Hint Constructors red.

  Lemma ered_appabs t11 t2 t :
    t = t11.[t2/] ->
    red (App (Abs t11) t2) t.
  Proof. by move => ->. Qed.

  Lemma red_abs_multi t t' :
    clos_refl_trans _ red t t' ->
    clos_refl_trans _ red (Abs t) (Abs t').
  Proof. induction 1; eauto. Qed.

  Lemma red_appl_multi t1 t1' t2 :
    clos_refl_trans _ red t1 t1' ->
    clos_refl_trans _ red (App t1 t2) (App t1' t2).
  Proof. induction 1; eauto. Qed.

  Lemma red_appr_multi t1 t2 t2' :
    clos_refl_trans _ red t2 t2' ->
    clos_refl_trans _ red (App t1 t2) (App t1 t2').
  Proof. induction 1; eauto. Qed.

  Corollary red_app_multi t1 t2 t1' t2' :
    clos_refl_trans _ red t1 t1' ->
    clos_refl_trans _ red t2 t2' ->
    clos_refl_trans _ red (App t1 t2) (App t1' t2').
  Proof.
    intros ? ?.
    apply: (rt_trans _ _ _ (App t1' t2)).
    - apply red_appl_multi; eauto.
    - apply red_appr_multi; eauto.
  Qed.

    Lemma red_abs_multi_inv_aux t0 t0' :
    clos_refl_trans_1n _ red t0 t0' ->
    forall t t',
    t0 = Abs t ->
    t0' = Abs t' ->
    clos_refl_trans _ red t t'.
  Proof.
    induction 1 => ? ?; inversion 1; inversion 1; subst; eauto.
    inversion H. subst. eauto.
  Qed.

  Corollary red_abs_multi_inv t t' :
    clos_refl_trans _ red (Abs t) (Abs t') ->
    clos_refl_trans _ red t t'.
  Proof. move => /clos_rt_rt1n_iff /red_abs_multi_inv_aux. eauto. Qed.

  Hint Resolve red_abs_multi red_appl_multi red_appr_multi red_app_multi.

  Lemma red_rename t t' :
    red t t' ->
    forall r,
    red (rename r t) (rename r t').
  Proof.
    induction 1 => /= ?; eauto.
    apply: ered_appabs.
    autosubst.
  Qed.

  Lemma red_rename_multi r t t' :
    clos_refl_trans _ red t t' ->
    clos_refl_trans _ red (rename r t) (rename r t').
  Proof.
    Local Hint Resolve red_rename.
    induction 1 => /=; eauto.
  Qed.

  Lemma red_subst t t' :
    red t t' ->
    forall s,
    red t.[s] t'.[s].
  Proof.
    induction 1 => /= ?; eauto.
    apply: ered_appabs.
    autosubst.
  Qed.

  Lemma red_subst_multi_aux t : forall s s',
    (forall x, clos_refl_trans _ red (s x) (s' x)) ->
    clos_refl_trans _ red t.[s] t.[s'].
  Proof.
    induction t => /= ? ? Hs; eauto.
    apply: red_abs_multi.
    apply: IHt => [ [ | ? ] //= ].
    exact: red_rename_multi.
  Qed.

  Corollary red_subst_multi t t' s s' :
    clos_refl_trans _ red t t' ->
    (forall x, clos_refl_trans _ red (s x) (s' x)) ->
    clos_refl_trans _ red t.[s] t'.[s'].
  Proof.
    Local Hint Resolve red_subst.
    move => Hrt ?.
    apply: rt_trans.
    - exact: red_subst_multi_aux.
    - induction Hrt; eauto.
  Qed.

  Fixpoint development t :=
    match t with
    | Var x => Var x
    | Abs t => Abs (development t)
    | App (Abs t11) t2 => (development t11).[development t2/]
    | App t1 t2 => App (development t1) (development t2)
    end.

  Lemma development_red_multi : forall t,
    clos_refl_trans _ red t (development t).
  Proof. elim => /= [ | | [ ] /= ]; eauto. Qed.

  Hint Resolve development_red_multi.

  Lemma development_rename : forall t r,
    rename r (development t) = development (rename r t).
  Proof.
    elim => /= [ // | ? ? ? | [ ? | ? | ? ? ] /= IHt1 ? IHt2 r ]; f_equal; eauto.
    move: IHt2 (IHt1 r) => <-. inversion 1.
    autosubst.
  Qed.

  Lemma development_subst : forall t s s',
    (forall x, s x = development (s' x)) ->
    clos_refl_trans _ red (development t).[s] (development t.[s']).
  Proof.
    elim => [ /= ? ? ? -> // | ? IH ? ? Hs | [ x | t11 | ? ? ] /= IHt1 t2 IHt2 s s' Hs ]; eauto.
    - apply: red_abs_multi.
      apply: IH => [ [ | ? ] //= ].
      by rewrite /up /funcomp /scons Hs development_rename.
    - move: (s' x) (Hs x) => [ ? | ? | ? ? ] /= ->; eauto.
    - rewrite (_ : (development t11).[development t2/].[s] = (development t11).[up s].[(development t2).[s]/]).
      { apply: red_subst_multi => [ | [ | ? ] /= ]; eauto.
        apply: red_abs_multi_inv. eauto. }
      autosubst.
  Qed.

  Theorem red_confluent : confluent _ red.
  Proof.
    apply: (Z _ _ development); induction 1 => /=; eauto.
    - inversion H; subst; eauto.
      apply: rt_trans.
      + exact: rt_step.
      + apply: red_subst_multi => [ | [ | ? ] //= ].
        exact: (red_abs_multi_inv _ _ IHred).
    - case t1; eauto.
    - by apply: red_subst_multi => [ | [ | ? ] /= ].
    - inversion H; subst; eauto.
      + apply: red_subst_multi; eauto.
        exact: (red_abs_multi_inv _ _ IHred).
      + apply: (rt_trans _ _ _ (App (development t11.[t0/]) (development t2))).
        * apply: red_appl_multi.
          by apply: development_subst => [ [ | ? ] ].
        * case t11.[t0/] => /=; eauto.
    - case t1 => ?; eauto.
      by apply: red_subst_multi => [ | [ | ? ] /= ].
    - by apply: development_subst => [ [ | ? ] ].
  Qed.

End Lambda.