From Coq Require Import Strings.String.
Require Import terms.
Require Import subst.
Require Import subtype.
Require Import typing.

Reserved Notation " s '-->α' t " (at level 40).
Reserved Notation " s '-->β' t " (at level 40).

Inductive expr_alpha : expr_term -> expr_term -> Prop :=
  | EAlpha_Rename : forall x x' τ e,
    (expr_abs x τ e) -->α (expr_abs x' τ (expr_subst x (expr_var x') e))

  | EAlpha_TyRename : forall α α' e,
    (expr_ty_abs α e) -->α (expr_ty_abs α' (expr_specialize α (type_var α') e))

  | EAlpha_SubAbs : forall x τ e e',
    (e -->α e') ->
    [{ λ x , τ ↦ e }] -->α [{ λ x , τ ↦ e' }]

  | EAlpha_SubTyAbs : forall α e e',
    (e -->α e') ->
    [{ Λ α ↦ e }] -->α [{ Λ α ↦ e' }]

  | EAlpha_SubApp1 : forall e1 e1' e2,
    (e1 -->α e1') ->
    [{ e1 e2 }] -->α [{ e1' e2 }]

  | EAlpha_SubApp2 : forall e1 e2 e2',
    (e2 -->α e2') ->
    [{ e1 e2 }] -->α [{ e1 e2' }]

where "s '-->α' t" := (expr_alpha s t).


Example a1 : polymorphic_identity1 -->α polymorphic_identity2.
Proof.
  unfold polymorphic_identity1.
  unfold polymorphic_identity2.
  apply EAlpha_SubTyAbs.
  apply EAlpha_Rename.
Qed.


Inductive beta_step : expr_term -> expr_term -> Prop :=
  | E_App1 : forall e1 e1' e2,
    e1 -->β e1' ->
    [{ e1 e2 }] -->β [{ e1' e2 }]

  | E_App2 : forall v1 e2 e2',
    (is_value v1) ->
    e2 -->β e2' ->
    [{ v1 e2 }] -->β [{ v1 e2' }]

  | E_TypApp : forall e e' τ,
    e -->β e' ->
    [{ Λ τ ↦ e }] -->β [{ Λ τ ↦ e' }]

  | E_TypAppLam : forall α e τ,
    [{ (Λ α ↦ e) # τ }] -->β (expr_specialize α τ e)

  | E_AppLam : forall x τ e a,
    [{ (λ x , τ ↦ e) a }] -->β (expr_subst x a e)

  | E_AppMorph : forall x τ e a,
    [{ (λ x , τ ↦morph e) a }] -->β (expr_subst x a e)

  | E_Let : forall x e a,
    [{ let x := a in e }] -->β (expr_subst x a e)

  | E_StripAscend : forall τ e,
    [{ e as τ }] -->β e

  | E_StripDescend : forall τ e,
    [{ e des τ }] -->β e

  | E_Ascend : forall τ e e',
    (e -->β e') ->
    [{ e as τ }] -->β [{ e' as τ }]

  | E_AscendCollapse : forall τ' τ e,
    [{ (e as τ) as τ' }] -->β [{ e as (τ'~τ) }]

  | E_DescendCollapse : forall τ' τ e,
    (τ':<=τ) ->
    [{ (e des τ') des τ }] -->β [{ e des τ }]

where "s '-->β' t" := (beta_step s t).

Inductive multi {X : Type} (R : X -> X -> Prop) : X -> X -> Prop :=
  | Multi_Refl : forall (x : X), multi R x x
  | Multi_Step : forall (x y z : X),
                    R x y ->
                    multi R y z ->
                    multi R x z.

Notation " s -->α* t " := (multi expr_alpha s t) (at level 40).
Notation " s -->β* t " := (multi beta_step s t) (at level 40).



Example reduce1 :
  [{
    let "deg2turns" :=
       (λ"x",$"Angle"$~$"Degrees"$~$"ℝ"$
                ↦morph ((%"/"% (%"x"% des $"ℝ"$) %"360"%) as $"Angle"$~$"Turns"$))
    in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$) )
  }]
  -->β*
  [{
     ((%"/"% %"60"%) %"360"%) as $"Angle"$~$"Turns"$
  }].
Proof.
  apply Multi_Step with (y:=[{ (λ"x",$"Angle"$~$"Degrees"$~$"ℝ"$
                ↦morph (((%"/"% (%"x"% des $"ℝ"$)) %"360"%) as $"Angle"$~$"Turns"$)) (%"60"% as $"Angle"$~$"Degrees"$) }]).
  apply E_Let.

  apply Multi_Step with (y:=(expr_subst "x" [{%"60"% as $"Angle"$~$"Degrees"$}]  [{ (((%"/"% (%"x"% des $"ℝ"$)) %"360"%) as $"Angle"$~$"Turns"$) }])).
  apply E_AppMorph.
  simpl.

  apply Multi_Step with (y:=[{ ((%"/"% (%"60"% as $"Angle"$~$"Degrees"$)) %"360"%) as $"Angle"$~$"Turns"$ }]).
  apply E_Ascend.
  apply E_App1.
  apply E_App2.
  apply V_Abs, VAbs_Var.
  apply E_StripDescend.

  apply Multi_Step with (y:=[{ (%"/"% %"60"% %"360"%) as $"Angle"$~$"Turns"$ }]).
  apply E_Ascend.
  apply E_App1.
  apply E_App2.
  apply V_Abs, VAbs_Var.
  apply E_StripAscend.

  apply Multi_Refl.
Qed.