Require Import Prelims.

Inductive label := τ | β.
Definition τβ_rel A := label -> A -> A -> Prop.
Definition any {A} (R:τβ_rel A) (x y:A) := exists l, R l x y.
Hint Unfold any.

Structure Machine :=
  {
    M_A :> Type ;
    M_rel : τβ_rel M_A
  }.
Local Notation "(≻τ)" := (@M_rel _ τ).
Local Notation "a '≻τ' a'" := (@M_rel _ τ a a') (at level 40).
Local Notation "a '≻β' a'" := (@M_rel _ β a a') (at level 40).

(*Definition M_any (A : Machine) (a a' : A) := (a ≻τ a' \/ a ≻β a').*)

Canonical Structure Machine_ARS (A : Machine) : ARS :=
  {|
    ARS_X := A ;
    ARS_R := any (@M_rel A)
  |}.

Coercion Machine_ARS : Machine >-> ARS.

Section absSim.

  Section refine_ARS.

    Variable X : ARS.
    Variable A : Machine.

    Variable refines: A -> X -> Prop.
    Notation "a ≫ x" := (refines a x) (at level 70).

    Definition refinement_ARS :=
      (forall a x, a ≫ x -> reducible (≻) x -> reducible (≻) a) /\
      (forall a a' x, a ≫ x -> a ≻τ a' -> a' ≫ x) /\
      (forall a a' x, a ≫ x -> a ≻β a' -> exists x', a' ≫ x' /\ x ≻ x') /\
      (forall a x, a ≫ x -> terminatesOn (≻τ) a).

  End refine_ARS.

  Section assume_refine.

    Variable A : Machine.
    Variable X : ARS.
    Notation "a ▷τ a'" := (@evaluates (Build_ARS (M_rel τ)) a a') (at level 40).

    Variable refines: A -> X -> Prop.
    Notation "a ≫ x" := (refines a x) (at level 70).

    Hypothesis refinement : refinement_ARS refines.

    Section Correctness.
      Variable a : A. Variable x : X.
      Hypothesis H : a ≫ x.

      Lemma upSim a' :
        a ▷ a' -> exists x', a' ≫ x' /\ x ▷ x'.
      Proof with eauto 9 using evaluates.
        destruct refinement as (R1 & R2 & R3 & R4). intros eva.
        induction eva as [ | a a' a'' [ [] H0 ]] in x, H; cbn in *. 1-2:now eauto 10 using evaluates.
        destruct (R3 _ _ _ H H0) as (? & ? & ?).
        edestruct IHeva as (? & ? & ?)...
      Qed.

      Lemma rightValue a' x' :
        (* unique normal forms for X would also suffice *)
        a ▷ a' -> a' ≫ x' -> functional refines -> x ▷ x'.
      Proof.
        intros (? & Href1 & ?) % upSim Href2 FN. now rewrite (FN _ _ _ Href2 Href1).
      Qed.

      Lemma termination_propagates :
        terminatesOn (≻X) x -> terminatesOn (≻A) a.
      Proof.
        destruct refinement as (R1 & R2 & R3 & R4).
        intros N. induction N as [x wf H0] in a, H |- *.
        induction (R4 a x H).
        constructor. intros a' [ [] Hstep].
        - eauto.
        - eapply R3 in Hstep as (? & ? & ?); eauto.
      Qed.

      Lemma evaluation_propagates:
        terminatesOn (≻X) x -> computable (≻A) ->
        exists (a':A), a ▷ a'.
      Proof.
        intros Hter C. specialize Hter as Hter % termination_propagates % terminates_normalizes. all: eauto using evaluates.
      Qed.

      Lemma tau_evaluates_evaluates a' : ~ reducible (≻X) x -> a ▷τ a' -> a ▷ a'.
      Proof.
        intros H2. destruct refinement as (R1 & R2 & R3 & R4). induction 1 as [a |] in x, H, H2 ; cbn in *.
        - econstructor. intros (? & [] & ?). eauto. destruct (R3 _ _ _ H H1) as (? & ? & ?). eauto.
        - econstructor. exists τ. eauto. eauto.
      Qed.

      Lemma evaluates_tau a' a'' : a ▷τ a' -> (evaluates (X := A) a' a'') -> a ▷ a''.
      Proof.
        induction 1 in a'', H; cbn in *.
        - eauto.
        - intros. eapply IHevaluates in H2.
          + econstructor. exists τ. eauto. eauto.
          + eapply refinement; eauto.
      Qed.

    End Correctness.

    Section top_down.
      Variable FN :functional (≻X).
      Variable C : computable (X:=A) (≻τ).

      Lemma tau_eval a x a' :
        a ≫ x -> a ▷τ a' -> a' ≫ x.
      Proof.
        intros H. destruct refinement as (R1 & R2 & R3 & R4).
        induction 1; eauto.
      Qed.

      Lemma one_downSim a x x' :
        a ≫ x -> x ≻ x' -> exists a' a'', a ▷τ a'' /\ a'' ≻β a' /\ a' ≫ x'.
      Proof.
        intros H H1. destruct refinement as (R1 & R2 & R3 & R4). cbn in *.
        destruct (@terminates_normalizes (Build_ARS (M_rel τ)) C _ (R4 _ _ H)) as [a'' H2].
        edestruct (R1 _ _ (tau_eval H H2)) as [a' [[] H3]]. eexists; eauto.
        - exists a', a''. edestruct evaluates_irred; eauto.
        - exists a',a''. repeat split; eauto. destruct (R3 _ _ _ (tau_eval H H2) H3) as (x'' & ? & H5).
          now rewrite (FN H1 H5).
      Qed.

      Lemma downSim a x x' :
      a ≫ x -> x ▷ x' -> exists a', a ▷ a' /\ a' ≫ x'.
    Proof.
      intros H H1. destruct refinement as (R1 & R2 & R3 & R4). induction H1 in a, H |- *; cbn in *;[intros|].
      - destruct (@terminates_normalizes (Build_ARS (M_rel τ)) C _ (R4 _ _ H)) as [a' H2].
        exists a'. split. eapply tau_evaluates_evaluates; eauto. eapply tau_eval; eauto.
      - destruct (one_downSim H H0) as (a' & a'' & ? & ? & ?). cbn in *.
        destruct (IHevaluates _ H4) as (a''' & ? & ?).
        exists a'''. split. eapply evaluates_tau; eauto. econstructor. exists β. eauto. eauto. eauto.
    Qed.

  End top_down.

  End assume_refine.

  Section refine_M.

    Variable A : Machine.
    Variable B : Machine.

    Variable refines: A -> B -> Prop.
    Notation "a ≫ b" := (refines a b) (at level 70).

    Definition refinement_M :=
      (forall a b, a ≫ b -> reducible (≻) b -> reducible (≻) a) /\
      (forall a a' b, a ≫ b -> a ≻τ a' -> exists b', a' ≫ b' /\ b ≻τ b') /\
      (forall a a' b, a ≫ b -> a ≻β a' -> exists b', a' ≫ b' /\ b ≻β b').

  End refine_M.

  Lemma composition (A B : Machine) (X : ARS) (R : A -> B -> Prop) (S : B -> X -> Prop) :
    refinement_M R -> refinement_ARS S -> refinement_ARS (fun a c => exists b, R a b /\ S b c).
  Proof.
    intros (H & H0 & H1) (H2 & H3 & H4 & H5). do 3 try split; intros.
    - destruct H6 as (? & ? & ?). eauto.
    - destruct H6 as (? & ? & ?). destruct (H0 _ _ _ H6 H7) as (? & ? & ?). eauto.
    - destruct H6 as (? & ? & H8). destruct (H1 _ _ _ H6 H7) as (? & ? & H10).
      destruct (H4 _ _ _ H8 H10) as (? & ? & ?). eauto.
    - destruct H6 as (? & ? & H7). specialize (H5 _ _ H7).
      clear H7. induction H5 in a, H6. econstructor. intros ? H7.
      destruct (H0 _ _ _ H6 H7) as (? & ? & ?). eauto.
  Qed.

End absSim.