Set Implicit Arguments.
Require Import RelationClasses Morphisms List
        Omega Init.Nat Setoid std calculus unification.
Require Import third_order.pcp third_order.encoding.
Import ListNotations.

Huet Reduction

Section HuetReduction.

  Variable (X: Const).
  Let v n: fin := n.
  Let u n: fin := (S n).

  Let h: exp X := var 0.
  Let f: exp X := var 3.
  Let g: exp X := var 4.

Reduction Function

  Program Instance PCP_to_U (S: list card) : orduni 3 X :=
    {
      Gamma₀ := [Arr (repeat (alpha alpha) (length S)) alpha; (alpha alpha) alpha];
      s₀ := lambda lambda lambda h (AppR f (Enc 1 2 (heads S))) (AppR f (repeat (var (u 1)) (length S)));
      t₀ := lambda lambda lambda h (AppR f (Enc 1 2 (tails S))) (var (u 1) (g (var (u 1))));
      A₀ := (alpha alpha) (alpha alpha) (alpha alpha alpha) alpha;
      H1₀ := _;
      H2₀ := _;
    }.
  Next Obligation with cbn; eauto.
    do 4 econstructor. econstructor. econstructor; cbn; eauto; cbn; eauto.
    - eapply AppR_ordertyping with (L := repeat (alpha alpha) (length S) ); simplify.
      erewrite <-map_length; eapply Enc_typing.
      all: econstructor; eauto...
      simplify; cbn; eauto.
    - eapply AppR_ordertyping.
      + eapply repeated_ordertyping; simplify; eauto.
        intros s H'. eapply repeated_in in H'. subst.
        econstructor; cbn. 2: eauto. eauto...
      + econstructor; simplify; eauto...
  Qed.
  Next Obligation with cbn [ord' ord alpha]; simplify; cbn; eauto.
    do 4 econstructor. econstructor. econstructor; eauto...
    cbn; eauto.
    2: do 2 econstructor...
    2 - 3: econstructor...
    eapply AppR_ordertyping with (L := repeat (alpha alpha) (length S)); simplify; eauto.
    erewrite <-map_length; eapply Enc_typing.
    all: econstructor...
  Qed.

  Section ForwardDirection.

    Definition ginst (I: list nat) : exp X :=
      lambda AppL (repeat (var 0) (pred (|I|))) (var 1).

Forward Direction


    Lemma ginst_typing I:
      [alpha] ⊢(3) ginst I : (alpha alpha) alpha.
    Proof.
      econstructor. eapply AppL_ordertyping_repeated.
      eapply repeated_ordertyping.
      intros ? ? % repeated_in; subst; eauto.
      simplify; eauto.
      econstructor; eauto.
    Qed.

    Lemma ginst_equivalence I (S: stack):
      I <> nil -> I nats (length S) ->
      AppR (ren (add 3) (finst I (length S)))
           (repeat (var (u 1)) (| S |)) var (u 1) (ren (add 3) (ginst I) (var (u 1))).
    Proof.
      intros H H0. unfold finst. rewrite !Lambda_ren, !AppL_ren.
      rewrite !map_id_list.
      2: intros ? ?; mapinj; cbn; eapply H0, nats_lt in H3; now rewrite it_up_ren_lt.
      rewrite AppR_Lambda'; simplify; eauto.
      unfold ginst; cbn [ren]; erewrite stepBeta.
      2: asimpl; simplify; cbn; unfold funcomp; eauto.
      cbn [ren]. rewrite it_up_ren_ge; simplify; eauto.
      asimpl. rewrite select_variables_subst; simplify; eauto.
      rewrite select_repeated; eauto.
      unfold ginst; cbn; asimpl; simplify.
      rewrite sapp_ge_in; simplify; eauto.
      replace (_ - _) with 3 by omega.
      destruct I; intuition.
    Qed.


    Lemma PCP_MU S:
      PCP S -> OU 3 X (PCP_to_U S).
    Proof.
      intros (I & ? & ? & ?).
      pose (sigma := finst I (length S) .: ginst I .: var).
      exists [alpha]. exists sigma. split.
      - intros x A. destruct x as [| [| x]]; try discriminate; cbn.
        3: intros [] % nth_error_In.
        all: injection 1 as ?; subst.
        eapply finst_typing; eauto.
        eapply ginst_typing.
      - cbn -[ginst]. do 3 eapply equiv_lam_proper.
        eapply equiv_app_proper.
        eapply equiv_app_proper. reflexivity.
        all: unfold shift, var_zero.
        all: rewrite !AppR_subst; rewrite ?Enc_subst_id; eauto.
        2: rewrite map_id_list.
        3: intros ? ? % repeated_in; subst; reflexivity.
        all: cbn; rewrite !ren_plus_base, !ren_plus_combine;
          change (1 + 1 + 1) with 3.
        2: rewrite !AppL_ren; simplify; cbn [ren]; unfold upRen_exp_exp.
        2: unfold up_ren, funcomp; cbn [scons].
        replace (|S|) with (|heads S|) at 1 by now simplify.
        replace (|S|) with (|tails S|) at 1 by now simplify.
        rewrite !finst_equivalence, H1; simplify; eauto.
        rewrite ginst_equivalence; eauto.
        unfold ginst; asimpl. now simplify.
    Qed.

  End ForwardDirection.

  Section BackwardDirection.

    Variables (s t: exp X) (x: nat) (sigma: fin -> exp X) (S: list (exp X)).
    Hypothesis (H1: forall y, isVar (sigma y) /\ sigma y <> var x).
    Hypothesis (N: normal s).
    Hypothesis (EQ: S .+ sigma s (var x) t).

    Lemma end_is_var:
      (forall x, x S -> isVar x) -> exists i e, i < |S| /\ s = var i e.
    Proof.
      intros H2; edestruct end_head_var as (h' & T & s' & H5 & ?); eauto. subst s.
      destruct T as [| t1 [| t2 T]].
      all: cbn in EQ; specialize (H1 h').
      all: destruct (sigma h') eqn: H'; cbn in *; intuition.
      1, 3: eapply nth_error_In in H as H7; eapply H2 in H7.
      1, 2: eapply nth_error_sapp in H; rewrite ?H in EQ.
      + destruct s'; cbn in *; intuition. Discriminate.
      + rewrite AppR_subst in EQ; cbn in EQ.
        eapply equiv_app_elim in EQ as (EQ1 & EQ2); cbn; eauto; simplify.
        destruct s'; cbn in *; intuition.
        rewrite H in EQ1. 2: rewrite H; eauto.
        exfalso. symmetry in EQ1.
        eapply equiv_neq_var_app; eauto; simplify; eauto.
      + exists h'. exists t1. intuition. eauto using nth_error_Some_lt.
    Qed.

  End BackwardDirection.

Backward Direction

  Lemma MU_PCP S':
    NOU 3 (PCP_to_U S') -> PCP S'.
  Proof.
    intros (Delta & sigma & T & H & N); cbn in *.
    repeat apply equiv_lam_elim in H.
    eapply equiv_app_elim in H as [EQ2 EQ1]; cbn; intuition.
    eapply equiv_app_elim in EQ2 as [_ EQ2]; cbn; intuition.
    rewrite !AppR_subst in EQ1; rewrite !AppR_subst in EQ2.
    rewrite !Enc_subst_id in EQ2;try reflexivity.
    cbn in *. unfold funcomp in *.
    rewrite !ren_plus_base, !ren_plus_combine in *;
      change (1 + 1 + 1) with 3 in *.
    unfold shift, var_zero in *.
    rewrite map_id_list in EQ1; [| intros ? ? % repeated_in; now subst ].
    assert (Delta ⊢(3) sigma 0 : Arr (repeat (alpha alpha) (length S')) alpha) as T1
        by now apply T.
    specialize (N 0) as N2; eapply normal_nf in N2 as N3.
    destruct N3 as [k x t' T' Hi H ->].
    eapply Lambda_ordertyping_inv in T1 as (L & B & H0 & H1 & <-).
    eapply id in H0 as T2.
    assert (|L | <= |S'|) as L1 by
          (eapply (f_equal arity) in H1; simplify in H1; rewrite H1; eauto).
    symmetry in H1; eapply Arr_inversion in H1 as (L2 & H1 & H2); simplify; try omega.
    eapply repeated_app_inv in H1 as (H1 & H3 & H4); eauto.
    rewrite H4 in H2; subst B.
    rewrite H3 in *; simplify in *. clear H3 H4 L1. revert H0 H1 EQ1 EQ2 T2 N2.
    generalize (length L); generalize (length L2); clear L L2. intros l k H0 H1 EQ1 EQ2 T2 N2.
    edestruct (@list_decompose_alt k _ S') as (S1 & S2 & H4 & H5); try omega; subst S'.
    rewrite !Lambda_ren in EQ1; rewrite !Lambda_ren in EQ2.
    simplify in EQ1 EQ2; rewrite !AppR_app in EQ1; rewrite !AppR_app in EQ2.
    simplify in H1; assert (length S1 = l) as H2 by omega; clear H1; subst.
    rewrite !AppR_Lambda' in EQ1, EQ2; simplify; eauto.
    rewrite AppR_Lambda' in EQ2; simplify; eauto.
    rewrite it_up_var_sapp in EQ1; simplify; intros; try omega.
    rewrite !it_up_var_sapp in EQ2; simplify; intros; try omega.

    destruct (@AppL_largest _ (fun s => match s with var x => x < |S2| | _ => False end) (AppR x T'))
      as (S & t & H1 & H2 & H3). intros []; intuition; now right.
    assert (exists I, I nats (|S2|) /\ S = map var I) as [I []].
    - clear H2. induction S. exists nil; cbn; intuition.
      edestruct IHS as [I]; [firstorder|]. intuition; subst.
      specialize (H1 a); mp H1; [firstorder|].
      destruct a as [i| | |]; intuition. exists (i :: I); cbn.
      eapply lt_nats in H1. intuition.
    - clear H1. rewrite H2 in EQ1, EQ2.
      destruct S1.
      + rewrite H2 in *. assert (normal t) by now eapply normal_AppL_right, normal_Lambda.
        rewrite !AppL_subst in EQ1; rewrite !AppL_subst in EQ2. subst S. cbn -[add] in *.
        rewrite !select_variables_subst in EQ2.
        rewrite !select_variables_subst in EQ1.
        all: simplify; eauto.
        rewrite <-!select_map, !enc_concat in EQ2.
        eapply AppL_ordertyping_inv in T2 as (L' & B & H8 & H9).
        eapply enc_eq in EQ2; eauto.
        2 - 5: intros ? EQ3;
          eapply end_is_var_typed in EQ3 as (? & ? & ? & ?); cbn; simplify.
        (* close False goals *)
        2, 7, 12, 17: eapply H3; cbn; eauto; cbn; now simplify in *.
        (* close normal term goals *)
        3, 7, 11, 15: eauto.
        (* close Enc goals *)
        3, 6, 9, 12: reflexivity.
        (* close typing goals *)
        3, 5, 7, 9: eauto.
        (* close var goals *)
        2 - 5: intros; cbn; unfold funcomp, u, v; intuition discriminate.
        exists I; intuition; eauto using nats_lt.
        subst; cbn [map select concat AppL] in EQ2, EQ1.
        eapply end_is_var in EQ1 as (? & ? & ? & ?);
          eauto; simplify.
        eapply H3; cbn; eauto; cbn; now simplify in *.
        intros; cbn; intuition; discriminate.
        intros ? ? % repeated_in; subst; eauto.
        now rewrite !select_map in EQ2.
      + eapply id in T2 as T3.
        eapply AppR_ordertyping_inv in T2 as (L' & T2 & T4).
        destruct x as [i | | |]; cbn in H; eauto.
        * inv T4.
          assert (i < length S2 \/ i >= length S2) as [H42|H42] by omega.
          ** rewrite nth_error_app1, nth_error_repeated in H7; simplify; eauto.
             injection H7 as H7. eapply (f_equal ord) in H7. simplify in H7.
             symmetry in H7; eapply Nat.eq_le_incl in H7; simplify in H7.
             intuition. cbn in H7. omega.
          ** rewrite <-H2 in EQ1. asimpl in EQ1. rewrite sapp_ge_in in EQ1; simplify; eauto.
             eapply equiv_head_equal in EQ1; simplify; cbn; eauto.
             simplify in EQ1; cbn in EQ1. discriminate EQ1.
        * rewrite <-H2 in EQ1. exfalso. asimpl in EQ1.
          eapply equiv_head_equal in EQ1; cbn; simplify; cbn; intuition.
          cbn in EQ1; simplify in EQ1; discriminate.
  Qed.

  Theorem PCP_U3: PCP OU 3 X.
  Proof.
    exists PCP_to_U. intros C; split; eauto using PCP_MU.
    rewrite OU_NOU; eauto using MU_PCP.
  Qed.

End HuetReduction.