Lemma valid_tail_ok s P : valid_from s P -> tail_ok (mwf s P).
Proof.
  destruct P as [|p P]; [left; reflexivity|].
  intros [[t Ht] _]. right. exists (2 * t), (1 :: mwf p P). cbn [mwf]. f_equal. lia.
Qed.

Lemma cnt1_valid P : valid P -> cnt P 1 = 0.
Proof.
  intros H. apply cnt_all_ge. apply valid_gt in H. eapply Forall_impl; [|exact H]. intros; cbn in *; lia.
Qed.

Lemma in_transfer Qi Qe P k k' u v kf : Forall (fun q => q < k) Qi ->
  Sh u v Qe (filter (fun p => kf <? p) P) -> k + u = k' + v -> kf < k' ->
  (In k (Qi ++ Qe) <-> In k' P).
Proof.
  intros HQi Hsh E Hk. rewrite in_app_iff, (Sh_in _ _ _ _ k k' Hsh E), (filter_in P kf k' Hk).
  rewrite Forall_forall in HQi.
  split; [intros [H|H]; [specialize (HQi _ H); lia | exact H] | intros H; right; exact H].
Qed.

Lemma sh_compose Qi Qe Qe' P n a a' k k' : Forall (fun q => q <= k) Qi -> n <= k' ->
  k + (n + 3) = k' + a ->
  Sh (k + 3) a' Qe' (filter (fun q => k <? q) (Qi ++ Qe)) ->
  Sh (n + 3) a Qe (filter (fun p => n <? p) P) ->
  Sh (k' + 3) a' Qe' (filter (fun p => k' <? p) P).
Proof.
  intros HQi Hn E H1 H2. rewrite (filter_lt_app _ _ _ HQi) in H1.
  pose proof (Sh_filter _ _ _ _ k k' H2 E) as H3. rewrite (filter_filter_lt P n k' Hn) in H3.
  apply (Sh_trans _ _ _ _ _ _ a _ _ _ H1 H3); lia.
Qed.

(* ---------- the orbit invariant and the absorption law (proof.md section 3) ---------- *)
(* Core P k a b Q: the marker tail Q of a T(a,b)/S(a,b) word splits into Qi (internal
   markers within reach, plus the one being absorbed when k is in P) and Qe (the
   unabsorbed original markers of P, at their exact shifted positions). *)
Definition Core (P : list nat) (k a b : nat) (Q : list nat) : Prop :=
  valid Q /\ 2 <= a /\ exists Qi Qe, Q = Qi ++ Qe /\ length Qi + a = b + 1 + ind P k /\
    Forall (fun q => q + 2 + ind P k <= a) Qi /\ Sh (k + 3) a Qe (filter (fun p => k <? p) P).

(* Inv(M,n), with alpha = cnt P n; T-word when n+alpha is odd, S-word when even *)
Definition Inv (P : list nat) (n : nat) (W : list nat) : Prop :=
  (Nat.Odd (n + cnt P n) /\ exists a Q, W = a :: 2 :: (n + cnt P n) :: mw Q /\
     Core P n a (n + cnt P n) Q) \/
  (Nat.Even (n + cnt P n) /\ exists a Q, W = 2 :: 2 :: a :: 2 :: (n + cnt P n - 1) :: mw Q /\
     Core P (S n) a (n + cnt P n - 1) Q).

Definition Claim (Lm : nat) : Prop :=
  forall Q k, k + length Q <= Lm -> valid Q -> exists W, Orb Q k W /\ (1 <= k -> Inv Q k W).

Lemma stepU P : valid P -> exists W', Ep (1 :: mw P) (cost P 0) W' /\ Inv P 1 W'.
Proof.
  intros HV0. assert (Hc : cost P 0 = 2).
  { unfold cost, ind. rewrite (cnt1_valid P HV0), cnt_0. reflexivity. }
  rewrite Hc. unfold Inv. rewrite (cnt1_valid P HV0).
  destruct P as [|p P'].
  - exists [2;2;1]. split; [apply U0|]. left. split; [exists 0; reflexivity|].
    exists 2, (@nil nat). split; [reflexivity|]. split; [exact I|]. split; [lia|]. exists (@nil nat), (@nil nat).
    split; [reflexivity|]. split; [reflexivity|]. split; constructor.
  - pose proof HV0 as HV. destruct HV as [[t Ht] HV']. pose proof (valid_gt _ _ HV') as Hg.
    destruct t as [|t].
    + replace p with 1 in * by lia.
      exists (3 :: 2 :: 1 :: mwf 1 P'). split.
      { apply (U2 0 (mwf 1 P')). apply valid_tail_ok. exact HV'. }
      left. split; [exists 0; reflexivity|].
      exists 3, (map (fun p => p - 1) P'). split.
      { unfold mw. rewrite <- (mwf_unshift 1 1 P'); [reflexivity | lia |].
        eapply Forall_impl; [|exact Hg]. cbn; intros; lia. }
      split; [apply (valid_unshift 0 1 P' HV')|]. split; [lia|].
      exists (@nil nat), (map (fun p => p - 1) P'). split; [reflexivity|].
      rewrite (ind_in (1 :: P') 1 HV0 (or_introl eq_refl)).
      split; [reflexivity|]. split; [constructor|].
      cbn [filter]. change (1 <? 1) with false. cbv iota.
      rewrite (filter_all P' 1 Hg).
      apply (Sh_unmap 3 1 P'). eapply Forall_impl; [|exact Hg]. cbn; intros; lia.
    + exists (2 :: 2 :: 1 :: S (S (2 * t)) :: 1 :: mwf p P'). split.
      { change (mw (p :: P')) with ((p - 0 + 1) :: 1 :: mwf p P').
        replace (p - 0 + 1) with (S (S (S (S (2 * t))))) by lia. apply U1. }
      left. split; [exists 0; reflexivity|].
      exists 2, (map (fun q => q - 2) (p :: P')). split.
      { unfold mw. cbn [map mwf]. rewrite (mwf_unshift p 2 P'); [| lia |].
        - do 4 f_equal. lia.
        - eapply Forall_impl; [|exact Hg]. cbn; intros; lia. }
      split.
      { apply (valid_unshift 0 2 (p :: P')). cbn [valid_from]. split; [exists t; lia | exact HV']. }
      split; [lia|].
      exists (@nil nat), (map (fun q => q - 2) (p :: P')). split; [reflexivity|].
      assert (Hn1 : ~ In 1 (p :: P')).
      { intros [H|H]; [lia|]. rewrite Forall_forall in Hg. specialize (Hg _ H). lia. }
      rewrite (ind_nin _ _ Hn1). split; [reflexivity|]. split; [constructor|].
      rewrite filter_all.
      * apply (Sh_unmap 2 2 (p :: P')). constructor; [lia|].
        eapply Forall_impl; [|exact Hg]. cbn; intros; lia.
      * constructor; [lia|]. eapply Forall_impl; [|exact Hg]. cbn; intros; lia.
Qed.

Lemma stepS P n a Q : valid P -> 1 <= n -> Nat.Even (n + cnt P n) ->
  Core P (S n) a (n + cnt P n - 1) Q ->
  exists W', Ep (2 :: 2 :: a :: 2 :: (n + cnt P n - 1) :: mw Q) (cost P n) W' /\ Inv P (S n) W'.
Proof.
  intros HV Hn [e He] (HVQ & Ha & Qi & Qe & -> & Hlen & Hfa & Hsh).
  assert (Hnin : ~ In n P).
  { intro Hin. destruct (parity_in 0 P n HV Hin) as [u Hu]. lia. }
  assert (HcS : cnt P (S n) = cnt P n) by (apply cnt_S_nin; exact Hnin).
  assert (Hcost : cost P n = 2) by (unfold cost, ind; lia).
  rewrite Hcost.
  assert (Ha3 : 2 + ind P (S n) <= a).
  { destruct Qi as [|q Qi'].
    - cbn [length] in Hlen. lia.
    - pose proof (valid_app_l _ _ HVQ) as Hq1. inversion Hq1; subst. inversion Hfa; subst. lia. }
  destruct a as [|a']; [lia|].
  destruct (n + cnt P n - 1) as [|b'] eqn:Hb; [lia|].
  exists (S (S a') :: 2 :: S (S (S b')) :: 2 :: 1 :: mw (Qi ++ Qe)). split.
  { apply ruleS. apply mw_tail_ok. exact HVQ. }
  left. split.
  { exists e. rewrite HcS. lia. }
  exists (S (S a')), (1 :: map (fun q => q + 1) (Qi ++ Qe)). split.
  { rewrite mw_cons1. rewrite HcS. do 3 f_equal. lia. }
  split; [apply valid_cons1; exact HVQ|]. split; [lia|].
  exists (1 :: map (fun q => q + 1) Qi), (map (fun q => q + 1) Qe).
  split; [rewrite map_app; reflexivity|].
  split; [cbn [length]; rewrite length_map; rewrite HcS; lia|].
  split.
  { constructor; [lia|]. apply Forall_map. eapply Forall_impl; [|exact Hfa]. cbn; intros; lia. }
  eapply Sh_eq; [apply Sh_map with (d := 1); exact Hsh | reflexivity | lia].
Qed.

Lemma stepT_nabs Lm P n a Q : Claim Lm -> valid P -> 1 <= n -> n + length P <= Lm ->
  Nat.Odd (n + cnt P n) -> ~ In n P -> Core P n a (n + cnt P n) Q ->
  exists W', Ep (a :: 2 :: (n + cnt P n) :: mw Q) (cost P n) W' /\ Inv P (S n) W'.
Proof.
  intros IH HV Hn HL [e He] Hnin (HVQ & Ha & Qi & Qe & -> & Hlen & Hfa & Hsh).
  assert (HcS : cnt P (S n) = cnt P n) by (apply cnt_S_nin; exact Hnin).
  assert (Hi0 : ind P n = 0) by (apply ind_nin; exact Hnin).
  rewrite Hi0 in Hlen, Hfa.
  assert (Hcost : cost P n = 2) by (unfold cost; lia). rewrite Hcost.
  assert (Hnin1 : ~ In (S n) P).
  { intro Hin. destruct (parity_in 0 P (S n) HV Hin) as [u Hu]. lia. }
  assert (HQe : Forall (fun q => a - 1 <= q) Qe).
  { apply (Sh_ge _ _ _ _ (a - 1) (S (S n)) Hsh); [|lia].
    intros p Hp. pose proof (filter_gt _ _ _ Hp) as H1. apply filter_In in Hp. destruct Hp as [Hp _].
    assert (p <> S n) by (intros ->; contradiction). lia. }
  assert (HQi : Forall (fun q => q < a - 1) Qi) by (eapply Forall_impl; [|exact Hfa]; cbn; intros; lia).
  assert (HcQ : cnt (Qi ++ Qe) (a - 1) = length Qi).
  { rewrite cnt_app, (cnt_all_lt _ _ HQi), (cnt_all_ge _ _ HQe). lia. }
  pose proof (filter_cnt_len P n) as HlP. pose proof (Sh_len _ _ _ _ Hsh) as HlQe.
  destruct (IH (Qi ++ Qe) (a - 1)) as (W1 & HO1 & HI1).
  { rewrite length_app. lia. }
  { exact HVQ. }
  specialize (HI1 ltac:(lia)).
  unfold Inv in HI1. rewrite HcQ in HI1.
  destruct HI1 as [[_ (a' & Q' & -> & HC')] | [[e' He'] _]]; [| exfalso; lia].
  assert (Hb : a - 1 + length Qi = n + cnt P n) by lia.
  rewrite Hb in *.
  exists (2 :: 2 :: a' :: 2 :: (n + cnt P n) :: mw Q'). split.
  { pose proof (ruleT a (n + cnt P n) (Qi ++ Qe) _ HO1 Ha ltac:(lia) HVQ ltac:(lia)) as HT.
    rewrite HcQ in HT. replace (n + cnt P n + 3 - a - length Qi) with 2 in HT by lia. exact HT. }
  right. split.
  { exists (e + 1). rewrite HcS. lia. }
  exists a', Q'. split.
  { rewrite HcS. do 5 f_equal. lia. }
  replace (S n + cnt P (S n) - 1) with (n + cnt P n) by lia.
  destruct HC' as (HVQ' & Ha' & Qi' & Qe' & -> & Hlen' & Hfa' & Hsh').
  assert (Hind : ind (Qi ++ Qe) (a - 1) = ind P (S (S n))).
  { apply ind_iff; [exact HVQ | exact HV | ].
    apply (in_transfer Qi Qe P (a - 1) (S (S n)) (n + 3) a n HQi Hsh); lia. }
  split; [exact HVQ'|]. split; [exact Ha'|].
  exists Qi', Qe'. split; [reflexivity|]. rewrite <- Hind. split; [lia|]. split; [exact Hfa'|].
  apply (sh_compose Qi Qe Qe' P n a a' (a - 1) (S (S n))); try assumption; try lia.
  eapply Forall_impl; [|exact HQi]. cbn; intros; lia.
Qed.

Lemma stepT_abs Lm P n a Q : Claim Lm -> valid P -> 1 <= n -> n + length P <= Lm ->
  Nat.Odd (n + cnt P n) -> In n P -> Core P n a (n + cnt P n) Q ->
  exists W', Ep (a :: 2 :: (n + cnt P n) :: mw Q) (cost P n) W' /\ Inv P (S n) W'.
Proof.
  intros IH HV Hn HL [e He] Hin (HVQ & Ha & Qi & Qe & -> & Hlen & Hfa & Hsh).
  assert (HcS : cnt P (S n) = S (cnt P n)) by (apply (cnt_S_in 0); assumption).
  assert (Hi1 : ind P n = 1) by (apply ind_in; assumption).
  rewrite Hi1 in Hlen, Hfa.
  assert (Hcost : cost P n = 3) by (unfold cost; lia). rewrite Hcost.
  assert (Ha3 : 3 <= a).
  { destruct Qi as [|q Qi'].
    - cbn [length] in Hlen. lia.
    - pose proof (valid_app_l _ _ HVQ) as Hq1. inversion Hq1; subst. inversion Hfa; subst. lia. }
  assert (HQe : Forall (fun q => a - 2 <= q) Qe).
  { apply (Sh_ge _ _ _ _ (a - 2) (S n) Hsh); [|lia].
    intros p Hp. apply filter_gt in Hp. lia. }
  assert (HQi : Forall (fun q => q < a - 2) Qi) by (eapply Forall_impl; [|exact Hfa]; cbn; intros; lia).
  assert (HcQ : cnt (Qi ++ Qe) (a - 2) = length Qi).
  { rewrite cnt_app, (cnt_all_lt _ _ HQi), (cnt_all_ge _ _ HQe). lia. }
  pose proof (filter_cnt_len P n) as HlP. pose proof (Sh_len _ _ _ _ Hsh) as HlQe.
  destruct (IH (Qi ++ Qe) (a - 2)) as (W2 & HO2 & HI2).
  { rewrite length_app. lia. }
  { exact HVQ. }
  specialize (HI2 ltac:(lia)).
  unfold Inv in HI2. rewrite HcQ in HI2.
  destruct HI2 as [[_ (a'' & Q'' & -> & HC'')] | [[e' He'] _]]; [| exfalso; lia].
  assert (Hb : a - 2 + length Qi = n + cnt P n) by lia.
  rewrite Hb in *.
  destruct HC'' as (HVQ'' & Ha'' & Qi'' & Qe'' & -> & Hlen'' & Hfa'' & Hsh'').
  exists (S (S a'') :: 2 :: S (S (n + cnt P n)) :: mw (map (fun q => q + 2) (Qi'' ++ Qe''))). split.
  { apply ruleX; try assumption; lia. }
  left. split.
  { exists (e + 1). rewrite HcS. lia. }
  exists (S (S a'')), (map (fun q => q + 2) (Qi'' ++ Qe'')). split.
  { rewrite HcS. do 3 f_equal. lia. }
  replace (S n + cnt P (S n)) with (S (S (n + cnt P n))) by lia.
  assert (Hind : ind (Qi ++ Qe) (a - 2) = ind P (S n)).
  { apply ind_iff; [exact HVQ | exact HV | ].
    apply (in_transfer Qi Qe P (a - 2) (S n) (n + 3) a n HQi Hsh); lia. }
  split; [apply valid_map2; exact HVQ''|]. split; [lia|].
  exists (map (fun q => q + 2) Qi''), (map (fun q => q + 2) Qe''). split; [apply map_app|].
  rewrite length_map. rewrite <- Hind. split; [lia|]. split.
  { apply Forall_map. eapply Forall_impl; [|exact Hfa'']. cbn; intros; lia. }
  assert (Hc : Sh (S n + 3) a'' Qe'' (filter (fun p => S n <? p) P)).
  { apply (sh_compose Qi Qe Qe'' P n a a'' (a - 2) (S n)); try assumption; try lia.
    eapply Forall_impl; [|exact HQi]. cbn; intros; lia. }
  eapply Sh_eq; [apply Sh_map with (d := 2); exact Hc | reflexivity | lia].
Qed.

Lemma step_lemma Lm : Claim Lm -> forall P n W, n + length P <= Lm -> valid P -> Orb P n W ->
  (1 <= n -> Inv P n W) -> exists W', Ep W (cost P n) W' /\ Inv P (S n) W'.
Proof.
  intros IH P n W HL HV HO HI. destruct n as [|n'].
  - inversion HO; subst. apply stepU; exact HV.
  - specialize (HI ltac:(lia)).
    destruct HI as [[Ho (a & Q & -> & HC)] | [He (a & Q & -> & HC)]].
    + destruct (in_dec Nat.eq_dec (S n') P) as [Hin | Hnin].
      * eapply stepT_abs; eauto; lia.
      * eapply stepT_nabs; eauto; lia.
    + eapply stepS; eauto; lia.
Qed.

Theorem main Lm : Claim Lm.
Proof.
  induction Lm as [|Lm IHL]; intros Q k Hk HV.
  - assert (k = 0) by lia. subst. exists (1 :: mw Q). split; [constructor | lia].
  - destruct k as [|k].
    + exists (1 :: mw Q). split; [constructor | lia].
    + destruct (IHL Q k ltac:(lia) HV) as (W & HO & HI).
      destruct (step_lemma Lm IHL Q k W ltac:(lia) HV HO HI) as (W' & HE & HI').
      exists W'. split; [econstructor; eauto | intros; exact HI'].
Qed.

(* ---------- top level ---------- *)
Lemma init : c0 -->* conf [] [3; 2; 1].
Proof. unfold conf, lside, rside. cbn [lpow app]. solve_init. Qed.

Lemma nonhalt : ~ halts tm c0.
Proof.
  eapply multistep_nonhalt; [apply init |].
  apply (progress_nonhalt_cond tm (nat * list nat) (0, [1]) (fun i => conf [] (3 :: 2 :: snd i))
           (fun i => Orb [] (fst i) (snd i) /\ (1 <= fst i -> Inv [] (fst i) (snd i)))).
  - intros [n W] [HO HI]. cbn [fst snd] in *.
    destruct (step_lemma n (main n) [] n W ltac:(cbn; lia) I HO HI) as (W' & HE & HI').
    exists (S n, W'). cbn [fst snd]. split.
    + apply Ep_tm in HE. replace (cost [] n) with 2 in HE by reflexivity. exact HE.
    + split; [econstructor; eauto | intros; exact HI'].
  - cbn [fst snd]. split; [exact (O0 []) | lia].
Qed.

Print Assumptions nonhalt.