From PslBase Require Import Base FinTypes.
From Undecidability Require Import L.Functions.EqBool.
From Undecidability.L.Complexity Require Export Problems.Cook.PR FlatFinTypes MorePrelim.
Require Import Lia.

Inductive FlatPR := {
  Sigma : nat;
  offset : nat;
  width : nat;
  init : list nat;
  windows : list (PRWin nat);
  final : list (list nat);
  steps : nat
  }.

Definition PRWin_ofFlatType (win : PRWin nat) k:= list_ofFlatType k (prem win) /\ list_ofFlatType k (conc win).
Definition isValidFlatWindows (l : list (PRWin nat)) k := (forall win, win el l -> PRWin_ofFlatType win k).
Definition isValidFlatFinal (l : list (list nat)) k := (forall s, s el l -> list_ofFlatType k s).
Definition isValidFlatInitial (l : list nat) k := list_ofFlatType k l.

Definition FlatPR_wellformed fpr :=
  width fpr > 0
  /\ offset fpr > 0
  /\ (exists k, k > 0 /\ width fpr = k * offset fpr)
  /\ length (init fpr) >= width fpr
  /\ (forall win, win el windows fpr -> PRWin_of_size win (width fpr))
  /\ (exists k, length (init fpr) = k * offset fpr).

Definition isValidFlattening fpr :=
 list_ofFlatType (Sigma fpr) (init fpr)
  /\ (forall s, s el final fpr -> list_ofFlatType (Sigma fpr) s)
  /\ (forall win, win el windows fpr -> PRWin_ofFlatType win (Sigma fpr)).


Definition FlatPRLang (C : FlatPR) := FlatPR_wellformed C /\ isValidFlattening C
  /\ exists (sf : list nat), list_ofFlatType (Sigma C) sf
      /\ relpower (valid (offset C) (width C) (windows C)) (steps C) (init C) sf
      /\ satFinal (offset C) (length (init C)) (final C) sf.

Section fixInstance.
  Variable (fpr : FlatPR).
  Notation Sigma := (Sigma fpr).
  Notation offset := (offset fpr).
  Notation width := (width fpr).
  Notation init := (init fpr).
  Notation windows := (windows fpr).
  Notation final := (final fpr).
  Notation steps := (steps fpr).

  Context (A : FlatPR_wellformed fpr).
  Context (B : isValidFlattening fpr).

  Lemma p_invariant (p : list nat -> Prop) (a b : list nat) :
    p a
    -> (forall x y, p (x ++ y) <-> p x /\ p y)
    -> |a| >= width
    -> (forall x y u v win, rewritesHead win (u ++ x) (v ++ y) -> win el windows -> |u| = offset -> |v| = offset -> p v)
    -> (forall win, win el windows -> p (conc win))
    -> valid offset width windows a b
    -> p b.
  Proof.
    intros H H0 H1 G1 G2 H2.
    assert (valid offset width windows a b /\ |a| >= width) as H3%validDirect_valid by tauto. 2-4: apply A.
    clear H2 H1. induction H3.
    - clear G1.
      destruct A as (_ & _ & (k & _ & A2) & _ & A6 & _).
      destruct B as ( _ & _ & A5).
      specialize (A5 _ H3) as (A5 & A7).
      specialize H4 as ((rest' & H6') & (rest & H6)).       specialize (A6 _ H3) as (A6 & A6').
      subst. rewrite app_length in H2.
      assert (rest = []) as ->.
      {
        destruct rest'; cbn in H2; [ | lia]. rewrite !app_length in H1.
        destruct rest; [ easy | cbn in H1; lia].
      }
      rewrite app_nil_r. now apply G2.
    - rewrite H0. apply H0 in H. split; [ | apply IHvalidDirect; easy]. now eapply G1.
  Qed.

  Corollary valid_list_ofFlatType_invariant a b :
    list_ofFlatType Sigma a -> |a| >= width -> valid offset width windows a b -> list_ofFlatType Sigma b.
  Proof.
    intros H H0 H1. eapply (@p_invariant (list_ofFlatType Sigma)).
    - apply H.
    - intros. apply list_ofFlatType_app.
    - apply H0.
    - intros. destruct H2 as (_ & (c & H2)).
        destruct A as (_ & _ & A3 & _ & A1 & _ ). destruct B as ( _ & _ & A2).
        specialize (A1 _ H3) as (_ & A1). specialize (A2 _ H3) as (_ & A2).
        apply app_length_split in H2 as (u' & H2).
        * rewrite H2 in A2. now apply list_ofFlatType_app in A2.
        * destruct A3 as (ak & A3 & A4). nia.
    - intros. destruct B as (_ & _ & A1).
      apply A1 in H2 as (_ & H2). apply H2.
    - apply H1.
  Qed.

  Lemma relpower_valid_list_ofFlatType_invariant steps a b:
    list_ofFlatType Sigma a -> |a| >= width -> relpower (valid offset width windows) steps a b -> list_ofFlatType Sigma b.
  Proof.
    intros. induction H1; [easy | ].
    apply IHrelpower. eapply valid_list_ofFlatType_invariant, H1; [ apply H | ].
    - apply H0.
    - apply valid_length_inv in H1. lia.
  Qed.

End fixInstance.

Definition PRWin_ofFlatType_dec (Sigma : nat) (win : PRWin nat) := list_ofFlatType_dec Sigma (prem win) && list_ofFlatType_dec Sigma (conc win).
Lemma PRWin_ofFlatType_dec_correct win Sigma : PRWin_ofFlatType_dec Sigma win = true <-> PRWin_ofFlatType win Sigma.
Proof.
  unfold PRWin_ofFlatType_dec, PRWin_ofFlatType. rewrite andb_true_iff.
  rewrite !list_ofFlatType_dec_correct. easy.
Qed.

Definition FlatPR_wf_dec (fpr : FlatPR) :=
  leb 1 (width fpr)
  && leb 1 (offset fpr)
  && Nat.eqb (Nat.modulo (width fpr) (offset fpr)) 0
  && leb (width fpr) (|init fpr|)
  && forallb (PRWin_of_size_dec (width fpr)) (windows fpr)
  && Nat.eqb (Nat.modulo (|init fpr|) (offset fpr)) 0.
Definition isValidFlattening_dec (fpr : FlatPR) :=
  list_ofFlatType_dec (Sigma fpr) (init fpr)
  && forallb (list_ofFlatType_dec (Sigma fpr)) (final fpr)
  && forallb (PRWin_ofFlatType_dec (Sigma fpr)) (windows fpr).

Lemma FlatPR_wf_dec_correct (fpr : FlatPR) : FlatPR_wf_dec fpr = true <-> FlatPR_wellformed fpr.
Proof.
  unfold FlatPR_wf_dec, FlatPR_wellformed. rewrite !andb_true_iff, !and_assoc.
  rewrite !leb_iff. rewrite <- !(reflect_iff _ _ (Nat.eqb_spec _ _ )).
  rewrite !forallb_forall.
  setoid_rewrite PRWin_of_size_dec_correct.
  split; intros; repeat match goal with [H : _ /\ _ |- _] => destruct H end;
  repeat match goal with [ |- _ /\ _ ] => split end; try easy.
  - apply Nat.mod_divide in H1 as (k & H1); [ | lia].
    exists k; split; [ | apply H1 ]. destruct k; cbn in *; lia.
  - apply Nat.mod_divide in H4 as (k & H4); [ | lia]. exists k; apply H4.
  - apply Nat.mod_divide; [ lia | ]. destruct H1 as (k & _ & H1). exists k; apply H1.
  - apply Nat.mod_divide; [ lia | ]. apply H4.
Qed.

Lemma isValidFlattening_dec_correct (fpr : FlatPR) : isValidFlattening_dec fpr = true <-> isValidFlattening fpr.
Proof.
  unfold isValidFlattening_dec, isValidFlattening.
  rewrite !andb_true_iff, !and_assoc.
  rewrite !forallb_forall.
  setoid_rewrite PRWin_ofFlatType_dec_correct.
  setoid_rewrite list_ofFlatType_dec_correct.
  split; intros; repeat match goal with [H : _ /\ _ |- _] => destruct H end;
  repeat match goal with [ |- _ /\ _ ] => split end; try easy.
Qed.

Inductive isFlatPRWinOf (X : finType) (flatwin : PRWin nat) (win : PRWin X) :=
  mkIsFlatPRWinO (Hprem : isFlatListOf (prem flatwin) (prem win))
    (Hconc : isFlatListOf (conc flatwin) (conc win))
  : isFlatPRWinOf flatwin win.

Inductive isFlatWindowsOf (X : finType) (flatwindows : list (PRWin nat)) (windows : list (PRWin X)) :=
  mkIsFlatWindowsOf (Hsound : forall flatwin, flatwin el flatwindows -> exists win, win el windows /\ isFlatPRWinOf flatwin win)
    (Hcomplete : forall win, win el windows -> exists flatwin, flatwin el flatwindows /\ isFlatPRWinOf flatwin win)
  : isFlatWindowsOf flatwindows windows.

Inductive isFlatFinalOf (X : finType) (flatfinal : list (list nat)) (final : list (list X)) :=
  mkIsFlatFinalOf (Hsound : forall fin, fin el flatfinal -> exists fin', fin' el final /\ isFlatListOf fin fin')
    (Hcomplete : forall fin, fin el final -> exists fin', fin' el flatfinal /\ isFlatListOf fin' fin)
  : isFlatFinalOf flatfinal final.

Inductive isFlatPROf (fpr : FlatPR) (pr : PR) :=
  mkIsFlatPROf (HSigma : finRepr (PR.Sigma pr) (Sigma fpr))
    (HOffset : offset fpr = PR.offset pr)
    (HWidth : width fpr = PR.width pr)
    (HInit : isFlatListOf (init fpr) (PR.init pr))
    (HWindows : isFlatWindowsOf (windows fpr) (PR.windows pr))
    (HFinal : isFlatFinalOf (final fpr) (PR.final pr))
    (HSteps : steps fpr = PR.steps pr)
  : isFlatPROf fpr pr.

Lemma isFlatPROf_isValidFlattening (fpr : FlatPR) (pr : PR) : isFlatPROf fpr pr -> isValidFlattening fpr.
Proof.
  intros. destruct H.
  repeat split.
  - rewrite HSigma. now eapply isFlatListOf_list_ofFlatType.
  - intros s H0%HFinal. rewrite HSigma. destruct H0 as (s' & F1 & ->).
    eapply isFlatListOf_list_ofFlatType. unfold isFlatListOf. reflexivity.
  - apply HWindows in H. destruct H as (win' & F1 & F2).
    destruct F2 as (F2 & F3). rewrite HSigma.
    eapply isFlatListOf_list_ofFlatType, F2.
  - apply HWindows in H. destruct H as (win' & F1 & F2).
    destruct F2 as (F2 & F3). rewrite HSigma.
    eapply isFlatListOf_list_ofFlatType, F3.
Qed.

Lemma rewritesHead_flat_agree (X : finType) (windowsFin : list (PRWin X)) windowsFlat finStr finStr' flatStr flatStr' :
  isFlatListOf flatStr finStr
  -> isFlatListOf flatStr' finStr'
  -> isFlatWindowsOf windowsFlat windowsFin
  -> (exists win, win el windowsFin /\ rewritesHead win finStr finStr') <-> (exists win, win el windowsFlat /\ rewritesHead win flatStr flatStr').
Proof.
  intros. split; intros (win & H2 & H3).
  - apply H1 in H2 as (win' & F1 & F2). exists win'. split; [apply F1 | ].
    unfold rewritesHead, prefix in *. destruct H3 as ((b1 & ->) & (b2 & ->)).
    unfold isFlatListOf in H, H0.
    rewrite map_app in H, H0. split.
    + exists (map index b1). rewrite H. enough (map index (prem win) = prem win') as H2.
      { now setoid_rewrite H2. }
      destruct win; cbn.
      destruct F2. cbn in *. now rewrite Hprem.
    + exists (map index b2). rewrite H0. enough (map index (conc win) = conc win') as H2.
      { now setoid_rewrite H2. }
      destruct win; cbn.
      destruct F2. cbn in *. now rewrite Hconc.
  - apply H1 in H2 as (win' & F1 & F2). exists win'. split; [ apply F1 | ].
    unfold rewritesHead, prefix in *. destruct H3 as ((b1 & ->) & (b2 & ->)).
    unfold isFlatListOf in H, H0. split.
    + symmetry in H. apply map_eq_app in H as (finStr1 & finStr2 & -> & ? & ?).
      exists finStr2.
      enough (finStr1 = prem win') as H3 by (now setoid_rewrite H3).
      destruct F2. rewrite Hprem in H.
      apply map_injective in H; [easy | unfold injective; apply injective_index].
    + symmetry in H0. apply map_eq_app in H0 as (finStr1 & finStr2 & -> & ? & ?).
      exists finStr2.
      enough (finStr1 = conc win') as H3 by (now setoid_rewrite H3).
      destruct F2. rewrite Hconc in H0.
      apply Prelim.map_inj in H0; [easy | unfold injective; apply injective_index].
Qed.

Section fixFPRInstance.
  Variable (fpr : FlatPR).
  Notation Sigma := (Sigma fpr).
  Notation offset := (offset fpr).
  Notation width := (width fpr).
  Notation init := (init fpr).
  Notation windows := (windows fpr).
  Notation final := (final fpr).
  Notation steps := (steps fpr).

  Context (A : FlatPR_wellformed fpr).
  Context (B : isValidFlattening fpr).

  Lemma valid_flat_agree (X : finType) (fwindows : list (PRWin X)) s1 s2 fs1 fs2:
    isFlatListOf fs1 s1
    -> isFlatListOf fs2 s2
    -> isFlatWindowsOf windows fwindows
    -> valid offset width windows fs1 fs2 <-> valid offset width fwindows s1 s2.
  Proof.
    intros H H1 H2.
    split.
    - intros H3. revert s1 s2 H H1. induction H3; intros.
      + destruct s1; [ | now unfold isFlatListOf in H].
        destruct s2; [ | now unfold isFlatListOf in H1].
        constructor.
      + unfold isFlatListOf in H4, H5.
        symmetry in H4. apply map_eq_app in H4 as (ls1 & ls2 & -> & -> & ->).
        symmetry in H5. apply map_eq_app in H5 as (rs1 & rs2 & -> & -> & ->).
        constructor 2.
        2-4: now rewrite map_length in *.
        apply IHvalid; easy.
      + unfold isFlatListOf in H5, H6.
        symmetry in H5. apply map_eq_app in H5 as (ls1 & ls2 & -> & -> & ->).
        symmetry in H6. apply map_eq_app in H6 as (rs1 & rs2 & -> & -> & ->).
        assert (exists w, w el windows /\ rewritesHead w (map index ls1 ++ map index ls2) (map index rs1 ++ map index rs2)) as H5 by eauto.
        eapply rewritesHead_flat_agree in H5 as (finwin & H5 & H6).
        * econstructor 3. 2-3: now rewrite map_length in *.
          -- eapply IHvalid; easy.
          -- apply H5.
          -- apply H6.
        * clear H5 H6. apply isFlatListOf_app; easy.
        * clear H5 H6. apply isFlatListOf_app; easy.
        * clear H5 H6. apply H2.
    - intros H3. revert fs1 fs2 H H1 H2. induction H3; intros.
      + rewrite H, H1; cbn; constructor 1.
      + rewrite H2, H4. rewrite !map_app. constructor. 2-4: rewrite map_length; auto.
        now eapply IHvalid.
      + rewrite H4, H5. rewrite !map_app.
        assert (exists w, w el fwindows /\ rewritesHead w (u ++ a) (v++b)) as H7 by eauto.
        eapply rewritesHead_flat_agree in H7 as (finwin & H7 & H8). 2-4: eauto.
        econstructor 3. 2-3: rewrite map_length; auto.
        * now eapply IHvalid.
        * apply H7.
        * rewrite H4, H5 in H8. now rewrite !map_app in H8.
  Qed.

  Lemma valid_flat_isFlatListOf_invariant (X : finType) (s1 : list X) fs1 fs2:
    finRepr X Sigma
    -> isFlatListOf fs1 s1
    -> |fs1| >= width
    -> valid offset width windows fs1 fs2
    -> exists (s2 : list X), isFlatListOf fs2 s2.
  Proof.
    intros.
    apply isFlatListOf_list_ofFlatType in H0. rewrite <- H in H0.
    specialize (@valid_list_ofFlatType_invariant fpr A B fs1 fs2 H0 H1 H2) as H4.
    apply (finRepr_exists_list H) in H4. destruct H4 as (s2 & H4); easy.
  Qed.

  Lemma relpower_valid_flat_agree (X : finType) (finwindows : list (PRWin X)) s1 s2 fs1 fs2 n:
    finRepr X Sigma
    -> |fs1| >= width
    -> isFlatListOf fs1 s1
    -> isFlatListOf fs2 s2
    -> isFlatWindowsOf windows finwindows
    -> relpower (valid offset width windows) n fs1 fs2 <-> relpower (valid offset width finwindows) n s1 s2.
  Proof.
    intros H0 H1 H2 H3 H4. split.
    - intros H5. revert s1 s2 H2 H3. induction H5; intros.
      + specialize (isFlatListOf_functional H2 H3) as ->. eauto.
      + specialize (valid_flat_isFlatListOf_invariant H0 H2 H1 H) as (s3 & H6).
        specialize (valid_length_inv H) as H7. rewrite H7 in H1.
        specialize (IHrelpower H1 _ _ H6 H3).
        econstructor.
        * apply (valid_flat_agree H2 H6 H4) in H. apply H.
        * apply IHrelpower.
    - intros H5. clear H1.
      revert fs1 fs2 H2 H3. induction H5; intros.
      + specialize (isFlatListOf_injective H2 H3) as ->. constructor.
      + assert (isFlatListOf (map index b) b) as H1 by (unfold isFlatListOf; easy).
        specialize (IHrelpower _ _ H1 H3).
        apply (valid_flat_agree H2 H1 H4) in H. eauto.
  Qed.

  Lemma final_flat_agree (X : finType) (F : list (list X)) (f : list (list nat)) l:
    isFlatFinalOf f F -> forall s fs, isFlatListOf fs s -> satFinal offset l f fs <-> satFinal offset l F s.
  Proof.
    intros. split.
    - intros (subs & k & H1 & H2 & H3). apply H in H1 as (subs' & H4 & H5).
      exists subs', k. split; [ apply H4 | split; [ apply H2 | ]].
      unfold isFlatListOf in H0. rewrite H0 in H3. rewrite H5 in H3.
      destruct H3 as (b & H3). rewrite <- utils.map_skipn in H3.
      apply map_eq_app in H3 as (ls1 & ls2 & H3 & H6 & H7).
      rewrite H3.
      apply map_injective in H6; [ | apply injective_index].
      rewrite H6. now exists ls2.
    - intros (subs & k & H1 & H2 & H3). apply H in H1 as (subs' & H4 &H5).
      exists subs', k. split; [ apply H4 | split; [ apply H2 | ]].
      rewrite H5, H0. destruct H3 as (b & H3).
      exists (map index b). rewrite <- utils.map_skipn. rewrite H3.
      now rewrite !map_app.
  Qed.
End fixFPRInstance.

Lemma isFlatPROf_wf_equivalent (pr : PR) (fpr : FlatPR) :
  isFlatPROf fpr pr -> (FlatPR_wellformed fpr <-> PR_wellformed pr).
Proof.
  intros [H1 H2 H3 H4]. split; intros; unfold FlatPR_wellformed, PR_wellformed in *.
  - destruct H as (F1 & F2 & F3 & F4 & F5 & F6). repeat split.
    + easy.
    + easy.
    + destruct F3 as (k & F3 & F3'). exists k. nia.
    + rewrite -> H4 in F4. rewrite map_length in F4. lia.
    + apply HWindows in H as (flatwin & H & H5). apply F5 in H.
      destruct H5. destruct H as (H & _). rewrite Hprem in H. rewrite map_length in H. lia.
    + apply HWindows in H as (flatwin & H & H5). apply F5 in H.
      destruct H5. destruct H as (_ & H). rewrite Hconc in H. rewrite map_length in H. lia.
    + destruct F6 as (k & F6). rewrite H4 in F6. rewrite map_length in F6. exists k; nia.
  - destruct H as (F1 & F2 & F3 & F4 & F5 & F6). repeat split.
    + easy.
    + easy.
    + destruct F3 as (k & F3 & F3'). exists k. nia.
    + rewrite H4, map_length. lia.
    + apply HWindows in H as (finwin & H & H5). apply F5 in H.
      destruct H5. destruct H as (H & _). rewrite Hprem, map_length. lia.
    + apply HWindows in H as (finwin & H & H5). apply F5 in H.
      destruct H5. destruct H as (_ & H). rewrite Hconc, map_length. lia.
    + destruct F6 as (k & F6). rewrite H4, map_length. exists k. nia.
Qed.

Lemma isFlatPROf_equivalence (pr : PR) (fpr : FlatPR) :
  isFlatPROf fpr pr -> (FlatPRLang fpr <-> PRLang pr).
Proof.
  intros. split.
  - intros (H1 & H2 & H3). split; [ now eapply isFlatPROf_wf_equivalent | ].
    destruct H as [F1 F2 F3 F4 F5].
    destruct H3 as (sf & H3 & H4 & H5).
    apply (finRepr_exists_list F1) in H3 as (SF & H3).
    exists SF. split.
    + rewrite <- F2, <- F3, <- HSteps. eapply relpower_valid_flat_agree; eauto. apply H1.
    + rewrite <- F2. rewrite F4, map_length in H5. eapply final_flat_agree; eauto.
  - intros (H1 & H2). split; [ now eapply isFlatPROf_wf_equivalent | ].
    split; [now eapply isFlatPROf_isValidFlattening | ].
    destruct H as [F1 F2 F3 F4 F5].
    destruct H2 as (sf & H3 & H4).
    exists (map index sf). repeat split.
    + unfold list_ofFlatType, ofFlatType.
      setoid_rewrite in_map_iff. intros a (x & <- & H). rewrite F1. apply index_le.
    + eapply relpower_valid_flat_agree; eauto.
      * now rewrite isFlatPROf_wf_equivalent.
      * now eapply isFlatPROf_isValidFlattening with (pr := pr).
      * rewrite F4, map_length, F3. apply H1.
      * unfold isFlatListOf. reflexivity.
      * rewrite F2, F3, HSteps. apply H3.
    + eapply final_flat_agree; eauto.
      * unfold isFlatListOf; reflexivity.
      * rewrite F2, F4, map_length. apply H4.
Qed.


Require Import PslBase.FiniteTypes.VectorFin PslBase.FiniteTypes.Cardinality.
Import Coq.Init.Specif.
Lemma unflattenString (f : list nat) k : list_ofFlatType k f -> {f' : list (finType_CS (Fin.t k)) & isFlatListOf f f'}.
Proof.
  intros H.
  eapply finRepr_exists_list with (X := finType_CS (Fin.t k)) in H as (a' & H).
  2: { unfold finRepr. specialize (Card_Fint k). unfold Cardinality. easy. }
  eauto.
Qed.

Lemma unflattenWindow (w : PRWin nat) k : PRWin_ofFlatType w k -> {w' : PRWin (finType_CS (Fin.t k)) & isFlatPRWinOf w w'}.
Proof.
  intros. destruct w. destruct H as (H1 & H2). cbn in *.
  apply unflattenString in H1 as (prem' & H1).
  apply unflattenString in H2 as (conc' & H2).
  exists (Build_PRWin prem' conc'). split; easy.
Qed.

Lemma unflattenWindows (l : list (PRWin nat)) k : isValidFlatWindows l k -> {l' : list (PRWin (finType_CS (Fin.t k))) & isFlatWindowsOf l l'}.
Proof.
  intros. unfold isValidFlatWindows in H. induction l.
  - exists []. easy.
  - edestruct IHl as (l' & IH);[ easy | ]. specialize (H a (or_introl eq_refl)).
    apply unflattenWindow in H as (a' & H). exists (a' :: l'). split; intros.
    + destruct H0 as [-> | H0]; [easy | ]. apply IH in H0 as (win & ? & ?); eauto.
    + destruct H0 as [-> | H0]; [ easy | ]. apply IH in H0 as (win' & ? & ?); eauto.
Qed.

Lemma unflattenFinal (f : list (list nat)) k : isValidFlatFinal f k -> {f' : list (list (finType_CS (Fin.t k))) & isFlatFinalOf f f'}.
Proof.
  intros. unfold isValidFlatFinal in H. induction f; intros.
  - exists []; easy.
  - edestruct IHf as (f' & IH); [easy | ]. specialize (H a (or_introl eq_refl)).
    apply unflattenString in H as (a' &H).
    exists (a'::f'). split; intros.
    + destruct H0 as [-> | H0]; [easy | ]. apply IH in H0 as (? & ? & ?); eauto.
    + destruct H0 as [-> | H0]; [easy | ]. apply IH in H0 as (? & ? & ?); eauto.
Qed.

Lemma unflattenPR (f : FlatPR) : isValidFlattening f -> {f' : PR & isFlatPROf f f'}.
Proof.
  intros (H1 & H2 & H3).
  apply unflattenWindows in H3 as (w' & H3).
  apply unflattenFinal in H2 as (f' & H2).
  apply unflattenString in H1 as (i' & H1).
  exists (Build_PR (offset f) (width f) i' w' f' (steps f)).
  constructor; eauto.
  cbn. unfold finRepr. specialize (Card_Fint (Sigma f)). easy.
Qed.

From Undecidability.L.Tactics Require Import LTactics GenEncode.
From Undecidability.L.Datatypes Require Import LProd LOptions LLNat LLists.

Section fix_X.
  Variable (X:Type).
  Context `{X_registered : registered X}.

  Run TemplateProgram (tmGenEncode "PRWin_enc" (PRWin X)).
  Hint Resolve PRWin_enc_correct : Lrewrite.

  Global Instance term_Build_PRWin : computableTime' (@Build_PRWin X) (fun _ _ => (1, fun _ _ => (1, tt))).
  Proof.
    extract constructor. solverec.
  Defined.

  Definition cnst_prem := 5.
  Global Instance term_prem : computableTime' (@prem X) (fun _ _ => (cnst_prem, tt)).
  Proof.
    extract. unfold cnst_prem. solverec.
  Defined.

  Definition cnst_conc := 5.
  Global Instance term_conc : computableTime' (@conc X) (fun _ _ => (cnst_conc, tt)).
  Proof.
    extract. unfold cnst_conc. solverec.
  Defined.

  Definition c__sizePRWin := 4.
  Lemma PRWin_enc_size (win : PRWin X) : size (enc win) = size (enc (prem win)) + size (enc (conc win)) + c__sizePRWin.
  Proof.
    destruct win. cbn. unfold enc, c__sizePRWin. cbn. nia.
  Qed.
End fix_X.

Hint Resolve PRWin_enc_correct : Lrewrite.

Run TemplateProgram (tmGenEncode "FlatPR_enc" (FlatPR)).
Hint Resolve FlatPR_enc_correct : Lrewrite.

From Undecidability.L.Complexity Require Import PolyBounds.

Instance term_Build_FlatPR : computableTime' Build_FlatPR (fun _ _ => (1, fun _ _ => (1, fun _ _ => (1, fun _ _ => (1, fun _ _ => (1, fun _ _ => (1, fun _ _ => (1, tt)))))))).
Proof.
  extract constructor. solverec.
Defined.

Definition c__Sigma := 10.
Instance term_FlatPR_Sigma : computableTime' Sigma (fun _ _ => (c__Sigma, tt)).
Proof.
  extract. unfold c__Sigma. solverec.
Defined.

Definition c__offset := 10.
Instance term_FlatPR_offset : computableTime' offset (fun _ _ => (c__offset, tt)).
Proof.
  extract. unfold c__offset. solverec.
Defined.

Definition c__width := 10.
Instance term_FlatPR_width : computableTime' width (fun _ _ => (c__width, tt)).
Proof.
  extract. unfold c__width. solverec.
Defined.

Definition c__init := 10.
Instance term_FlatPR_init : computableTime' init (fun _ _ => (c__init, tt)).
Proof.
  extract. unfold c__init. solverec.
Defined.

Definition c__windows := 10.
Instance term_FlatPR_windows : computableTime' windows (fun _ _ => (c__windows, tt)).
Proof.
  extract. unfold c__windows. solverec.
Defined.

Definition c__final := 10.
Instance term_FlatPR_final : computableTime' final (fun _ _ => (c__final, tt)).
Proof.
  extract. unfold c__final. solverec.
Defined.

Definition c__steps := 10.
Instance term_FlatPR_steps : computableTime' steps (fun _ _ => (c__steps, tt)).
Proof.
  extract. unfold c__steps. solverec.
Defined.

Lemma FlatPR_enc_size (fpr : FlatPR) : size (enc fpr) = size (enc (Sigma fpr)) + size(enc (offset fpr)) + size (enc (width fpr)) + size (enc (init fpr)) + size (enc (windows fpr)) + size (enc (final fpr)) + size (enc (steps fpr)) + 9.
Proof.
  destruct fpr. cbn. unfold enc. cbn. nia.
Qed.

Section PRWin_of_size.
  Variable ( X : Type).
  Context `{X_registered : registered X}.

  Definition c__prwinOfSizeDec := 2 * (cnst_prem + 2 * 5 + cnst_conc + 6 + c__length).
  Definition PRWin_of_size_dec_time (width : nat) (win : PRWin X) := c__prwinOfSizeDec * (1 + |prem win| + |conc win|) + eqbTime (X := nat) (size (enc (|prem win|))) (size (enc width)) + eqbTime (X := nat) (size (enc (|conc win|))) (size (enc width)).
  Global Instance term_PRWin_of_size_dec : computableTime' (@PRWin_of_size_dec X) (fun width _ => (1, fun win _ => (PRWin_of_size_dec_time width win, tt))).
  Proof.
    extract. solverec. unfold PRWin_of_size_dec_time, c__prwinOfSizeDec. nia.
  Defined.

  Definition c__prwinOfSizeDecBound := c__prwinOfSizeDec + c__eqbComp nat.
  Lemma PRWin_of_size_dec_time_bound width (win : PRWin X) : PRWin_of_size_dec_time width win <= (size(enc win) + 1) * c__prwinOfSizeDecBound.
  Proof.
    unfold PRWin_of_size_dec_time. rewrite !eqbTime_le_l. rewrite !list_size_enc_length, !list_size_length.
    rewrite PRWin_enc_size. unfold c__prwinOfSizeDecBound, c__sizePRWin. nia.
  Qed.
End PRWin_of_size.

Definition c__FlatPRWfDec := 3 * c__leb2 + 4 * c__width + 3 * c__offset + 2 * 5 + 2 * c__init + 2 * c__length + c__windows + 32 + 4 * c__leb + 2 * c__eqbComp nat * size (enc 0).
Definition FlatPR_wf_dec_time x := 2 * c__length * (|init x|) + leb_time (width x) (|init x|) + forallb_time (@PRWin_of_size_dec_time nat (width x)) (windows x) + modulo_time (|init x|) (offset x) + modulo_time (width x) (offset x) + c__FlatPRWfDec.

Instance term_FlatPR_wf_dec : computableTime' FlatPR_wf_dec (fun fpr _ => (FlatPR_wf_dec_time fpr, tt)).
Proof.
  extract. solverec. unfold FlatPR_wf_dec_time, c__FlatPRWfDec, leb_time. rewrite !eqbTime_le_r.
  rewrite Nat.le_min_l. rewrite Nat.le_min_l.
  leq_crossout.
Defined.

Definition c__FlatPRWfDecBound := 2*(2 * c__length + c__leb + c__prwinOfSizeDecBound + c__forallb + 2 * c__moduloBound + c__FlatPRWfDec).
Definition poly__FlatPRWfDec n := (n*n + 2* n + 1) * c__FlatPRWfDecBound.

Lemma FlatPR_wf_dec_time_bound fpr :
  FlatPR_wf_dec_time fpr <= poly__FlatPRWfDec (size (enc fpr)).
Proof.
  unfold FlatPR_wf_dec_time. rewrite leb_time_bound_l.
  rewrite !modulo_time_bound. rewrite list_size_enc_length.
  rewrite list_size_length.
  erewrite forallb_time_bound_env.
  2: {
    split; [intros | ].
    - specialize (PRWin_of_size_dec_time_bound (X := nat) y a) as H1.
      instantiate (2:= fun n => (n + 1) * c__prwinOfSizeDecBound). nia.
    - smpl_inO.
  }
  rewrite list_size_length.
  replace_le (size(enc (windows fpr))) with (size (enc fpr)) by (rewrite FlatPR_enc_size; lia).
  replace_le (size(enc (init fpr))) with (size (enc fpr)) by (rewrite FlatPR_enc_size; lia).
  replace_le (size(enc (width fpr))) with (size (enc fpr)) by (rewrite FlatPR_enc_size; lia).
  replace_le (size(enc(offset fpr))) with (size (enc fpr)) by (rewrite FlatPR_enc_size; lia).
  unfold poly__FlatPRWfDec, c__FlatPRWfDecBound. nia.
Qed.
Lemma FlatPR_wf_dec_poly : monotonic poly__FlatPRWfDec /\ inOPoly poly__FlatPRWfDec.
Proof.
  unfold poly__FlatPRWfDec; split; smpl_inO.
Qed.


Definition c__PRWinOfFlatTypeDec := cnst_prem + cnst_conc +8.
Definition PRWin_ofFlatType_dec_time (sig : nat) (w : PRWin nat):= list_ofFlatType_dec_time sig (prem w) + list_ofFlatType_dec_time sig (conc w) + c__PRWinOfFlatTypeDec.
Instance term_PRWin_ofFlatType_dec : computableTime' PRWin_ofFlatType_dec (fun sig _ => (1, fun w _ => (PRWin_ofFlatType_dec_time sig w, tt))).
Proof.
  extract. solverec. unfold PRWin_ofFlatType_dec_time, c__PRWinOfFlatTypeDec. nia.
Defined.

Definition c__PRWinOfFlatTypeDecBound := 2 * (c__PRWinOfFlatTypeDec + 1).
Definition poly__PRWinOfFlatTypeDec n := (poly__listOfFlatTypeDec n + 1) * c__PRWinOfFlatTypeDecBound.
Lemma PRWin_ofFlatType_dec_time_bound sig w : PRWin_ofFlatType_dec_time sig w <= poly__PRWinOfFlatTypeDec (size (enc sig) + size (enc w)).
Proof.
  unfold PRWin_ofFlatType_dec_time. rewrite !list_ofFlatType_dec_time_bound.
  unfold poly__PRWinOfFlatTypeDec.
  poly_mono list_ofFlatType_dec_poly at 2.
  2: (replace_le (size (enc (conc w))) with (size (enc w)) by (rewrite PRWin_enc_size; lia)); reflexivity.
  poly_mono list_ofFlatType_dec_poly at 1.
  2: (replace_le (size (enc (prem w))) with (size (enc w)) by (rewrite PRWin_enc_size; lia)); reflexivity.
  unfold c__PRWinOfFlatTypeDecBound. nia.
Qed.
Lemma PRWin_ofFlatType_dec_poly : monotonic poly__PRWinOfFlatTypeDec /\ inOPoly poly__PRWinOfFlatTypeDec.
Proof.
  split; unfold poly__PRWinOfFlatTypeDec; smpl_inO; apply list_ofFlatType_dec_poly.
Qed.

Definition c__isValidFlatteningDec := 3 * c__Sigma + c__init + c__final + c__windows + 16.
Definition isValidFlattening_dec_time x := list_ofFlatType_dec_time (Sigma x) (init x) + forallb_time (list_ofFlatType_dec_time (Sigma x)) (final x)+ forallb_time (PRWin_ofFlatType_dec_time (Sigma x)) (windows x) + c__isValidFlatteningDec.
Instance term_isValidFlattening_dec : computableTime' isValidFlattening_dec (fun fpr _ => (isValidFlattening_dec_time fpr, tt)).
Proof.
  extract. solverec. unfold isValidFlattening_dec_time, c__isValidFlatteningDec.
  repeat change (fun x => ?h x) with h. solverec.
Defined.

Definition c__isValidFlatteningDecBound := 2 * c__forallb + c__isValidFlatteningDec.
Definition poly__isValidFlatteningDec n :=(n + 2) * poly__listOfFlatTypeDec n + (n + 1) * poly__PRWinOfFlatTypeDec n + (n + 1) * c__isValidFlatteningDecBound.
Lemma isValidFlattening_dec_time_bound fpr : isValidFlattening_dec_time fpr <= poly__isValidFlatteningDec (size (enc fpr)).
Proof.
  unfold isValidFlattening_dec_time.
  rewrite list_ofFlatType_dec_time_bound.
  erewrite forallb_time_bound_env.
  2: {
    split; [intros | ].
    - rewrite list_ofFlatType_dec_time_bound, Nat.add_comm; reflexivity.
    - apply list_ofFlatType_dec_poly.
  }
  erewrite forallb_time_bound_env.
  2 : {
    split; [intros | ].
    - rewrite PRWin_ofFlatType_dec_time_bound, Nat.add_comm; reflexivity.
    - apply PRWin_ofFlatType_dec_poly.
  }

  rewrite !list_size_length.
  poly_mono list_ofFlatType_dec_poly at 1.
  2: (replace_le (size (enc (Sigma fpr)) + size (enc (init fpr))) with (size (enc fpr)) by (rewrite FlatPR_enc_size; lia)); reflexivity.
  poly_mono list_ofFlatType_dec_poly at 2.
  2: (replace_le (size (enc (final fpr)) + size (enc (Sigma fpr))) with (size (enc fpr)) by (rewrite FlatPR_enc_size; lia)); reflexivity.
  replace_le (size (enc (final fpr))) with (size (enc fpr)) by (rewrite FlatPR_enc_size; lia) at 1.
  replace_le (size (enc (windows fpr))) with (size (enc fpr)) by (rewrite FlatPR_enc_size; lia) at 1.
  poly_mono PRWin_ofFlatType_dec_poly at 1.
  2: (replace_le (size (enc (windows fpr)) + size (enc (Sigma fpr))) with (size (enc fpr)) by (rewrite FlatPR_enc_size; lia)); reflexivity.
  unfold poly__isValidFlatteningDec, c__isValidFlatteningDecBound. nia.
Qed.
Lemma isValidFlatteningDec_poly : monotonic poly__isValidFlatteningDec /\ inOPoly poly__isValidFlatteningDec.
Proof.
  split; (unfold poly__isValidFlatteningDec; smpl_inO; [apply list_ofFlatType_dec_poly |apply PRWin_ofFlatType_dec_poly ]).
Qed.