(* ** Abstract Reduction Systems *)
(* from Semantics Lecture at Programming Systems Lab, https://www.ps.uni-saarland.de/courses/sem-ws13/ *)

Require Export Undecidability.Shared.Libs.PSL.Base Lia.

Module ARSNotations.
  Notation "p '<=1' q" := ( x, p x q x) (at level 70).
  Notation "p '=1' q" := ( x, p x q x) (at level 70).
  Notation "R '<=2' S" := ( x y, R x y S x y) (at level 70).
  Notation "R '=2' S" := ( x y, R x y S x y) (at level 70).
End ARSNotations.

Import ARSNotations.

(* Relational composition *)

Definition rcomp X Y Z (R : X Y Prop) (S : Y Z Prop)
: X Z Prop :=
   x z y, R x y S y z.

(* Power predicates *)

Require Import Arith.
Definition pow X R n : X X Prop := it (rcomp R) n eq.

Definition functional {X Y} (R: X Y Prop) := x y1 y2, R x R x = .
Definition terminal {X Y} (R: X Y Prop) x:= y, R x y.

Section FixX.
  Variable X : Type.
  Implicit Types R S : X X Prop.
  Implicit Types x y z : X.

  Definition reflexive R := x, R x x.
  Definition symmetric R := x y, R x y R y x.
  Definition transitive R := x y z, R x y R y z R x z.

  (* Reflexive transitive closure *)

  Inductive star R : X X Prop :=
  | starR x : star R x x
  | starC x y z : R x y star R y z star R x z.

  Definition evaluates R x y := star R x y terminal R y.

  (* Making first argument a non-uniform parameter doesn't simplify the induction principle. *)

  Lemma star_simpl_ind R (p : X Prop) y :
    p y
    ( x x', R x x' star R x' y p x' p x)
     x, star R x y p x.
  Proof.
    intros A B. induction 1; eauto.
  Qed.


  Lemma star_trans R:
    transitive (star R).
  Proof.
    induction 1; eauto using star.
  Qed.


  Lemma R_star R: R <=2 star R.
  Proof.
    eauto using star.
  Qed.


  Instance star_PO R: PreOrder (star R).
  Proof.
    constructor;repeat intro;try eapply star_trans; now eauto using star.
  Qed.


  (* Power characterization *)

  Lemma star_pow R x y :
    star R x y n, pow R n x y.
  Proof.
    split; intros A.
    - induction A as [|x x' y B _ [n IH]].
      + exists 0. reflexivity.
               + exists (S n), x'. auto.
               - destruct A as [n A].
                 revert x A. induction n; intros x A.
                 + destruct A. constructor.
                 + destruct A as [x' [A B]]. econstructor; eauto.
  Qed.


  Lemma pow_star R x y n:
    pow R n x y star R x y.
  Proof.
    intros A. erewrite star_pow. eauto.
  Qed.


  (* Equivalence closure *)

  Inductive ecl R : X X Prop :=
  | eclR x : ecl R x x
  | eclC x y z : R x y ecl R y z ecl R x z
  | eclS x y z : R y x ecl R y z ecl R x z.

  Lemma ecl_trans R :
    transitive (ecl R).
  Proof.
    induction 1; eauto using ecl.
  Qed.


  Lemma ecl_sym R :
    symmetric (ecl R).
  Proof.
    induction 1; eauto using ecl, (@ecl_trans R).
  Qed.


  Lemma star_ecl R :
    star R <=2 ecl R.
  Proof.
    induction 1; eauto using ecl.
  Qed.


  (* Diamond, confluence, Church-Rosser *)

  Definition joinable R x y :=
     z, R x z R y z.

  Definition diamond R :=
     x y z, R x y R x z joinable R y z.

  Definition confluent R := diamond (star R).

  Definition semi_confluent R :=
     x y z, R x y star R x z joinable (star R) y z.

  Definition church_rosser R :=
    ecl R <=2 joinable (star R).

  Goal R, diamond R semi_confluent R.
  Proof.
    intros R A x y z B C.
    revert x C y B.
    refine (star_simpl_ind _ _).
    - intros y C. exists y. eauto using star.
    - intros x x' C D IH y E.
      destruct (A _ _ _ C E) as [v [F G]].
      destruct (IH _ F) as [u [H I]].
      assert (J:= starC G H).
      exists u. eauto using star.
  Qed.


  Lemma diamond_to_semi_confluent R :
    diamond R semi_confluent R.
  Proof.
    intros A x y z B C. revert y B.
    induction C as [|x x' z D _ IH]; intros y B.
    - exists y. eauto using star.
             - destruct (A _ _ _ B D) as [v [E F]].
               destruct (IH _ F) as [u [G H]].
               exists u. eauto using star.
  Qed.


  Lemma semi_confluent_confluent R :
    semi_confluent R confluent R.
  Proof.
    split; intros A x y z B C.
    - revert y B.
      induction C as [|x x' z D _ IH]; intros y B.
      + exists y. eauto using star.
               + destruct (A _ _ _ D B) as [v [E F]].
                 destruct (IH _ E) as [u [G H]].
                 exists u. eauto using (@star_trans R).
               - apply (A x y z); eauto using star.
  Qed.


  Lemma diamond_to_confluent R :
    diamond R confluent R.
  Proof.
    intros A. apply semi_confluent_confluent, diamond_to_semi_confluent, A.
  Qed.


  Lemma confluent_CR R :
    church_rosser R confluent R.
  Proof.
    split; intros A.
    - intros x y z B C. apply A.
      eauto using (@ecl_trans R), star_ecl, (@ecl_sym R).
    - intros x y B. apply semi_confluent_confluent in A.
      induction B as [x|x x' y C B IH|x x' y C B IH].
      + exists x. eauto using star.
               + destruct IH as [z [D E]]. exists z. eauto using star.
               + destruct IH as [u [D E]].
                 destruct (A _ _ _ C D) as [z [F G]].
                 exists z. eauto using (@star_trans R).
  Qed.


  (* End Semantics Library *)


  (* Uniform confluence and parametrized confluence *)

  Definition uniform_confluent (R : X X Prop ) := s t1 t2, R s R s = u, R u R u.

  Lemma functional_uc R :
    functional R uniform_confluent R.
  Proof.
    intros F ? ? ? . left. eapply F. all:eauto.
  Qed.


  Lemma pow_add R n m (s t : X) : pow R (n + m) s t rcomp (pow R n) (pow R m) s t.
  Proof.
    revert m s t; induction n; intros m s t.
    - simpl. split; intros. econstructor. split. unfold pow. simpl. reflexivity. eassumption.
      destruct H as [u [ ]]. unfold pow in . simpl in *. subst s. eassumption.
    - simpl in *; split; intros.
      + destruct H as [u [ ]].
        change (it (rcomp R) (n + m) eq) with (pow R (n+m)) in .
        rewrite IHn in .
        destruct as [u' [A B]]. unfold pow in A.
        econstructor.
        split. econstructor. repeat split; repeat eassumption. eassumption.
      + destruct H as [u [ ]].
        destruct as [u' [A B]].
        econstructor. split. eassumption. change (it (rcomp R) (n + m) eq) with (pow R (n + m)).
        rewrite IHn. econstructor. split; eassumption.
  Qed.


  Lemma rcomp_eq (R S R' S' : X X Prop) (s t : X) : (R =2 R') (S =2 S') (rcomp R S s t rcomp R' S' s t).
  Proof.
    intros A B.
    split; intros H; destruct H as [u [ ]];
    eapply A in ; eapply B in ;
    econstructor; split; eassumption.
  Qed.


  Lemma eq_ref : (R : X X Prop), R =2 R.
  Proof.
    split; tauto.
  Qed.


  Lemma rcomp_1 (R : X X Prop): R =2 pow R 1.
  Proof.
    intros s t; split;unfold pow in *; simpl in *; intros H.
    - econstructor. split; eauto.
    - destruct H as [u [ ]]; subst u; eassumption.
  Qed.


  Lemma parametrized_semi_confluence (R : X X Prop) (m : ) (s t1 t2 : X) :
    uniform_confluent R
    pow R m s
    R s
     k l u,
      k 1 l m pow R k u pow R l u m + k = S l.
  Proof.
    intros unifConfR; revert s ; induction m; intros s s_to_t1 s_to_t2.
    - unfold pow in s_to_t1. simpl in *. subst s.
      exists 1, 0, .
      repeat split; try .
      econstructor. split; try eassumption; econstructor.
    - destruct s_to_t1 as [v [s_to_v v_to_t1]].
      destruct (unifConfR _ _ _ s_to_v s_to_t2) as [H | [u [v_to_u t2_to_u]]].
      + subst v. eexists 0, m, ; repeat split; try ; eassumption.
      + destruct (IHm _ _ _ v_to_t1 v_to_u) as [k [l [u' H]]].
        eexists k, (S l), u'; repeat split; try ; try tauto.
        econstructor. split. eassumption. tauto.
  Qed.


  Lemma rcomp_comm R m (s t : X) : rcomp R (it (rcomp R) m eq) s t rcomp (it (rcomp R) m eq) R s t.
  Proof.
    split; intros H;
    [rewrite (rcomp_eq s t (rcomp_1 R) (eq_ref _)) in H;
      rewrite (rcomp_eq s t (eq_ref _) (rcomp_1 R)) |
     rewrite (rcomp_eq s t (eq_ref _) (rcomp_1 R)) in H;
       rewrite (rcomp_eq s t (rcomp_1 R) (eq_ref _))];
    change ((it (rcomp R) m eq)) with (pow R m) in *;
    try rewrite pow_add in *;
    rewrite plus_comm; eassumption.
  Qed.


  Lemma parametrized_confluence (R : X X Prop) (m n : ) (s t1 t2 : X) :
    uniform_confluent R
    pow R m s
    pow R n s
     k l u,
      k n l m pow R k u pow R l u m + k = n + l.
  Proof.
    revert n s ; induction m; intros n s unifConR s_to_t1 s_to_t2.
    - unfold pow in s_to_t1. simpl in s_to_t1. subst s.
      exists n, 0, . repeat split; try now . eassumption.
    - unfold pow in s_to_t1. simpl in *.
      destruct s_to_t1 as [v [s_to_v v_to_t1]].
      destruct (parametrized_semi_confluence unifConR s_to_t2 s_to_v) as
          [k [l [u [k_lt_1 [l_lt_n [t2_to_u [v_to_u H]]]]]]].
      destruct (IHm _ _ _ _ unifConR v_to_t1 v_to_u) as
          [l'[k'[u'[ [ [t1_to_u' [u_to_u' ]]]]]]].
      exists l', (k + k'), u'.
      repeat split; try . eassumption.
      rewrite pow_add.
      econstructor; split; eassumption.
  Qed.


  Lemma uniform_confluent_noloop R x y:
    uniform_confluent R
    star R x y ( y', R y y')
     z k, star R x z pow R (S k) z z.
  Proof.
    intros UC (&)%star_pow Term (z&&&RL).
    induction in ,RL,|-*.
    -edestruct parametrized_confluence with (m:=) (n:=S + ) as (&&?&?&?&?&?&?).
     1,2:eassumption.
     now eapply pow_add;eexists;split;eassumption.
     destruct . destruct .
     +now .
     +destruct as (?&?&_). edestruct Term. eauto.
     +destruct as (?&?&_). edestruct Term. eauto.
    -edestruct parametrized_semi_confluence with (R:=R) (2:= ) as (&?&?&?&?&?&?&?). 1,2:eassumption.
     destruct . 2:{ destruct as (?&?&_). edestruct Term. eauto. }
     cbn in ;inv .
     eapply . all:eauto.
  Qed.


 Lemma uc_terminal R x y z n:
    uniform_confluent R
    R x y
    pow R n x z
    terminal R z
     n' , n = S n' pow R n' y z.
  Proof.
    intros ? ? ? ter. edestruct parametrized_semi_confluence as (k&?&?&?&?&R'&?&?). 1-3:now eauto.
    destruct k as [|].
    -inv R'. rewrite plus_n_O in *. eauto.
    -edestruct R' as (?&?&?). edestruct ter. eauto.
  Qed.


  (* classical *)
  Definition classical R x := terminal R x y, R x y.

  (* Strong normalisation *)

  Inductive SN R : X Prop :=
  | SNC x : ( y, R x y SN R y) SN R x.

  Fact SN_unfold R x :
    SN R x y, R x y SN R y.
  Proof.
    split.
    - destruct 1 as [x H]. exact H.
    - intros H. constructor. exact H.
  Qed.


End FixX.

Existing Instance star_PO.

(* A notion of a reduction sequence which keeps track of the largest occuring state *)

Inductive redWithMaxSize {X} (size:X ) (step : X X Prop): X X Prop:=
  redWithMaxSizeR m s: m = size s redWithMaxSize size step m s s
| redWithMaxSizeC s s' t m m': step s s' redWithMaxSize size step m' s' t m = max (size s) m' redWithMaxSize size step m s t.

Lemma redWithMaxSize_ge X size step (s t:X) m:
  redWithMaxSize size step m s t size s m size t m.
Proof.
  induction 1;subst;firstorder (repeat eapply Nat.max_case_strong; try ).
Qed.


Lemma redWithMaxSize_trans X size step (s t u:X) m1 m2 m3:
 redWithMaxSize size step s t redWithMaxSize size step t u max = redWithMaxSize size step s u.
Proof.
  induction 1 in ,u,|-*;intros.
  -specialize (redWithMaxSize_ge ) as [].
   revert ;
     repeat eapply Nat.max_case_strong; subst m;intros. all:replace with by . all:eauto.
  - specialize (redWithMaxSize_ge ) as [].
    specialize (redWithMaxSize_ge ) as [].
    eassert (:=Max.le_max_l _ _);rewrite in .
    eassert (:=Max.le_max_r _ _);rewrite in .
    econstructor. eassumption.

    eapply IHredWithMaxSize. eassumption. reflexivity.
    subst m;revert ;repeat eapply Nat.max_case_strong;intros;try .
Qed.


Lemma redWithMaxSize_star {X} f (step : X X Prop) n x y:
  redWithMaxSize f step n x y star step x y.
Proof.
  induction 1;eauto using star.
Qed.


Lemma terminal_noRed {X} (R:XXProp) x y :
  terminal R x star R x y x = y.
Proof.
  intros ? R'. inv R'. easy. edestruct H. eassumption.
Qed.


Lemma unique_normal_forms {X} (R:XXProp) x y:
  confluent R ecl R x y terminal R x terminal R y x = y.
Proof.
  intros CR%confluent_CR E .
  specialize (CR _ _ E) as (z&&).
  apply terminal_noRed in . apply terminal_noRed in . 2-3:eassumption. congruence.
Qed.


Instance ecl_Equivalence {X} (R:XXProp) : Equivalence (ecl R).
Proof.
  split.
  -constructor.
  -apply ecl_sym.
  -apply ecl_trans.
Qed.


Instance star_ecl_subrel {X} (R:XXProp) : subrelation (star R) (ecl R).
Proof.
  intro. eapply star_ecl.
Qed.


Instance pow_ecl_subrel {X} (R:XXProp) n : subrelation (pow R n) (ecl R).
Proof.
  intros ? ? H%pow_star. now rewrite H.
Qed.


Lemma uniform_confluence_parameterized_terminal (X : Type) (R : X X Prop) (m n : ) (s t1 t2 : X):
  uniform_confluent R terminal R
  pow R m s pow R n s n', pow R n' m = n + n'.
Proof.
  intros .
  specialize (parametrized_confluence ) as (&n'&?&?&?&R'&?&?).
  destruct .
  -inv R'. exists n'. intuition.
  -exfalso. destruct R' as (?&?&?). eapply . eauto.
Qed.


Lemma uniform_confluence_parameterized_both_terminal (X : Type) (R : X X Prop) (n1 n2 : ) (s t1 t2 : X):
  uniform_confluent R terminal R terminal R
  pow R s pow R s = = .
Proof.
  intros .
  specialize (parametrized_confluence ) as (&n'&?&?&?&R'&R''&?).
  destruct . destruct n'.
  -inv R'. inv . split;first [ | easy].
  -exfalso. destruct R'' as (?&?&?). eapply . eauto.
  -exfalso. destruct R' as (?&?&?). eapply . eauto.
Qed.


Lemma uniform_confluent_confluent (X : Type) (R : X X Prop):
  uniform_confluent R confluent R.
Proof.
  intros H x y y' Hy Hy'. apply ARS.star_pow in Hy as (?&Hy). apply ARS.star_pow in Hy' as (?&Hy').
  edestruct parametrized_confluence as (?&?&z&?&?&?&?&?).
  eassumption. exact Hy. exact Hy'. exists z. split;eapply pow_star. all:eauto.
Qed.


Definition computesRel {X Y} (f : X option Y) (R:X Y Prop) :=
   x, match f x with
         Some y R x y
       | None terminal R x
       end.

Definition evaluatesIn (X : Type) (R : X X Prop) n (x y : X) := pow R n x y terminal R y.

Lemma evalevaluates_evaluatesIn X (step:XXProp) s t:
  evaluates step s t k, evaluatesIn step k s t.
Proof.
  intros [(R&?)%star_pow ?]. unfold evaluatesIn. eauto.
Qed.