Set Implicit Arguments.
Require Import Morphisms Setoid.
From Undecidability.HOU Require Import std.std.
From Undecidability.HOU.calculus Require Import prelim terms semantics.

Set Default Proof Using "Type".

Section Confluence.

  Context {X: Const}.

  Reserved Notation "s ≫ t" (at level 60).

  Inductive par : exp X exp X Prop :=
  | parVar x: var x var x
  | parConst c: const c const c
  | parLam s s': s s' ( s) s'
  | parBeta s s' t t' u: s s' t t' u = s' t' ( s) t u
  | parApp s s' t t': s s' t t' s t s' t'
  where "s ≫ t" := (par s t).

  Hint Constructors par : core.

  Lemma refl_par: s, s s.
  Proof. induction s; eauto. Qed.


  Hint Immediate refl_par : core.

  Global Instance refl_par_inst: Reflexive par.
  Proof.
    intros ?; eapply refl_par.
  Qed.


  Lemma ren_compatible_par s s' delta:
    s s' ren s ren s'.
  Proof.
    induction 1 in |-*; cbn; eauto; subst.
    econstructor; eauto. now asimpl.
  Qed.


  Lemma subst_compatible_par s s' sigma sigma':
    s s' ( x, x x) ( s) ( s').
  Proof.
    induction 1 in , |-*; cbn; eauto.
    - intros; econstructor; eapply IHpar.
      intros []; cbn; eauto using ren_compatible_par.
    - intros; econstructor.
      eapply with ( := up ); eauto.
      intros []; cbn; eauto using ren_compatible_par.
      eapply ; eauto.
      subst; now asimpl.
  Qed.


  Global Instance par_lam_proper: Proper (star par ++> star par) lam.
  Proof.
    intros s s' H; induction H; eauto.
  Qed.


  Global Instance par_app_proper: Proper (star par ++> star par ++> star par) app.
  Proof.
    intros s s' H; induction H; intros t t' H'; induction H'; eauto.
  Qed.


  Global Instance sandwich_step: subrelation step par.
  Proof.
    intros ??; induction 1; eauto.
  Qed.


  Global Instance sandwich_steps: subrelation par (star step).
  Proof.
    intros ??; induction 1; eauto.
    - rewrite IHpar; eauto.
    - rewrite , , stepBeta; eauto.
    - rewrite , ; eauto.
  Qed.


  Fixpoint (e: exp X) :=
    match e with
    | var x var x
    | const c const c
    | s ( s)
    | app ( s) t ( s) ( t)
    | app s t ( s) ( t)
    end.

  Lemma tak_fun_rho: tak_fun par .
  Proof.
    intros s t H; induction H; cbn; eauto.
    - subst u; eapply subst_compatible_par; eauto.
      intros []; cbn; eauto.
    - destruct s; eauto.
      inv H; inv .
      econstructor; eauto.
  Qed.


  Lemma confluence_step: confluent (@step X).
  Proof.
    eapply TMT.
    eapply sandwich_step. eapply sandwich_steps.
    typeclasses eauto.
    eapply tak_fun_rho.
  Qed.


End Confluence.

Notation "s ≫ t" := (par s t) (at level 60).
#[export] Hint Resolve confluence_step tak_fun_rho : core.