Set Implicit Arguments.
Require Import RelationClasses Morphisms List Arith Lia Init.Nat Setoid.
From Undecidability.HOU Require Import std.std calculus.calculus unification.unification.
From Undecidability.HOU Require Import third_order.pcp third_order.encoding.
Import ListNotations.

Set Default Proof Using "Type".

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.

  Lemma HGamma₀s₀A₀ (S: list card) :
    [Arr (repeat (alpha alpha) (length S)) alpha; (alpha alpha) alpha] ⊢( 3)
    (lambda lambda lambda h (AppR f (Enc 1 2 (heads S))) (AppR f (repeat (var (u 1)) (length S)))) :
    ((alpha alpha) (alpha alpha) (alpha alpha alpha) alpha).
  Proof.
    do 4 econstructor. econstructor. econstructor; cbn; (eauto 1); cbn; (eauto 2).
    - eapply AppR_ordertyping with (L := repeat (alpha alpha) (length S) ); simplify.
      erewrite <-map_length; eapply Enc_typing.
      all: econstructor; (eauto 2).
      simplify; cbn; (eauto 3).
    - 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 3).
  Qed.

  Lemma HGamma₀t₀A₀ (S: list card) :
    [Arr (repeat (alpha alpha) (length S)) alpha; (alpha alpha) alpha] ⊢( 3)
    (lambda lambda lambda h (AppR f (Enc 1 2 (tails S))) (var (u 1) (g (var (u 1))))) :
    ((alpha alpha) (alpha alpha) (alpha alpha alpha) alpha).
  Proof with cbn [ord' ord alpha]; simplify; cbn; (eauto 3).
    do 4 econstructor. econstructor. econstructor; (eauto 2)...
    cbn; (eauto 4).
    2: do 2 econstructor...
    2 - 3: econstructor...
    eapply AppR_ordertyping with (L := repeat (alpha alpha) (length S)); simplify.
    erewrite <-map_length; eapply Enc_typing.
    all: econstructor...
  Qed.

  Instance PCP_to_U (S: list card) : orduni 3 X.
  Proof with cbn [ord' ord alpha]; simplify; cbn; (eauto 2).
    refine {|
      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₀ := HGamma₀s₀A₀ S;
      H2₀ := HGamma₀t₀A₀ S;
    |}.
  Defined.

  Section ForwardDirection.

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


    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 2).
      simplify; (eauto 2).
      econstructor; (eauto 2).
    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 2).
      unfold ginst; cbn [ren]; erewrite stepBeta.
      2: asimpl; simplify; cbn; unfold funcomp; (eauto 2).
      cbn [ren]. rewrite it_up_ren_ge; simplify; (eauto 2).
      asimpl. rewrite select_variables_subst; simplify; (eauto 2).
      rewrite select_repeated; (eauto 2).
      unfold ginst; cbn; asimpl; simplify.
      rewrite sapp_ge_in; simplify; (eauto 3).
      replace (_ - _) with 3 by lia.
      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 2).
        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).
        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 2).
        rewrite ginst_equivalence; (eauto 2).
        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 using x t sigma N H1 EQ.
      intros H2; edestruct @end_head_var with (X:=X) as (h' & T & s' & H5 & ?); (eauto 2). 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 1); simplify.
        destruct s'; cbn in *; intuition.
        rewrite H in EQ1. 2: rewrite H; (eauto 3).
        exfalso. symmetry in EQ1.
        eapply equiv_neq_var_app; (eauto 1); simplify; (eauto 3).
      + exists h'. exists t1. intuition. eauto using nth_error_Some_lt.
      Unshelve. exact 0.
    Qed.

  End BackwardDirection.

  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 lia.
    eapply repeated_app_inv in H1 as (H1 & H3 & H4); (eauto 2).
    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 lia; 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 lia; clear H1; subst.
    rewrite !AppR_Lambda' in EQ1, EQ2; simplify; (eauto 2).
    rewrite AppR_Lambda' in EQ2; simplify; (eauto 2).
    rewrite it_up_var_sapp in EQ1; simplify; intros; try lia.
    rewrite !it_up_var_sapp in EQ2; simplify; intros; try lia.

    destruct (AppL_decomposition (AppR x T') (|S2|)) as [[I t] (H1&H2&H3)].
    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. cbn -[add] in *.
      rewrite !select_variables_subst in EQ2.
      rewrite !select_variables_subst in EQ1.
      all: simplify; (eauto 2).
      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).
      2 - 3: split; intros EQ3;
        eapply end_is_var_typed in EQ3 as (? & ? & ? & ?); cbn; simplify.
      6, 9, 15, 21 :now eauto.
      3, 8, 13, 16 : now eauto.
      2, 6, 10, 13: eapply H3; cbn; (eauto 1); cbn; now simplify in *.
      3, 5, 8, 11: eauto.
      3, 5, 9: eauto. 3, 4, 6:eauto.
      2 - 3: intros; cbn; unfold funcomp, u, v; intuition discriminate.
      exists I; intuition; eauto using nats_lt; (eauto 2).
      2: rewrite <-!select_map; (eauto 2).
      subst; cbn [map select concat AppL] in H6, EQ1.
      eapply end_is_var in EQ1 as (? & ? & ? & ?);
        eauto; simplify.
      eapply H3; cbn; (eauto 1); cbn; now simplify in *.
      intros; cbn; intuition; discriminate.
      intros ? ? % repeated_in; subst; (eauto 2).
    + eapply id in T2 as T3.
      eapply AppR_ordertyping_inv in T2 as (L' & T2 & T4).
      destruct x as [i | | |]; cbn in H; (eauto 2).
      * inv T4.
        assert (i < length S2 \/ i >= length S2) as [H42|H42] by lia.
        ** rewrite nth_error_app1, nth_error_repeated in H6; simplify; (eauto 2).
           injection H6 as H6. eapply (f_equal ord) in H6. simplify in H6.
           symmetry in H6; eapply Nat.eq_le_incl in H6; simplify in H6.
           intuition. cbn in H6. lia.
        ** rewrite <-H2 in EQ1. asimpl in EQ1. rewrite sapp_ge_in in EQ1; simplify; (eauto 2).
           eapply equiv_head_equal in EQ1; simplify; cbn; (eauto 2).
           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.