From Undecidability Require Import Hoare.HoareLogic.
From Undecidability.TM Require Import TMTac.
From Undecidability.TM Require Export CodeTM LiftTapes ChangeAlphabet.



Section RegSpec.

  Variable sig : Type.

  Local Notation "sig '^+'" := ((boundary + sig) % type) (at level 0) : type_scope.

  Inductive RegSpec : Type :=
  | Contains {sigX X : Type} {cX : codable sigX X} (r : Retract sigX sig) : X RegSpec
  | Contains_size {sigX X : Type} {cX : codable sigX X} (r : Retract sigX sig) : X RegSpec
  | Void : RegSpec
  | Void_size : RegSpec
  | Custom : (tape sig^+ Prop) RegSpec.
  Definition tspec_single (spec : RegSpec) (t : tape sig^+) : Prop :=
    match spec with
    | Contains r x t ≃(r) x
    | Contains_size r x s t ≃(r; s) x
    | Void isVoid t
    | Void_size s isVoid_size t s
    | Custom p p t
    end.

  Lemma tspec_single_Contains_size_Contains {sigX X : Type} {cX : codable sigX X} (r : Retract sigX sig) (x : X) (s : ) (t : tape sig^+) :
    tspec_single (Contains_size r x s) t tspec_single (Contains r x) t.
  Proof. cbn. auto. Qed.

  Definition SpecV n := Vector.t (RegSpec) n.
  Definition Spec n :Type := list Prop * SpecV n.

  Definition tspec {n : } (spec : Spec n) : Assert sig^+ n :=
    match spec with
    | (P,spec) (t : tapes sig^+ n)
       List.fold_right and ( (i : Fin.t n), tspec_single spec[@i] t[@i]) P
    end.

  Arguments tspec : simpl never.

  Lemma tspecE {n : } Ps Pv t:
  tspec (n:=n) (Ps,Pv) t (List.fold_right and True Ps (i : Fin.t n), tspec_single Pv[@i] t[@i]).
  Proof.
    cbn. induction Ps;cbn in *. easy. intros []. specialize (IHPs ) as [H' ?]. split. all:eauto.
  Qed.


  Lemma tspecI {n : } P t:
  (List.fold_right and True (fst P))
   ( (i : Fin.t n), tspec_single (snd P)[@i] t[@i])
   tspec (n:=n) P t.
  Proof.
    destruct P as (Ps&P). induction Ps;cbn in *. easy. intros H' ?. split. now eapply H';left.
    eapply IHPs. all:easy.
  Qed.


Lemma tspec_iff {n : } Ps Pv t:
  tspec (n:=n) (Ps,Pv) t (List.fold_right and True Ps (i : Fin.t n), tspec_single Pv[@i] t[@i]).
Proof. split. eapply tspecE;eauto. intros []. eapply tspecI;eauto. Qed.

Lemma tspec_Entails {n : } Ps Pv:
Entails (tspec (n:=n) (Ps,Pv)) ( t List.fold_right and True Ps (i : Fin.t n), tspec_single Pv[@i] t[@i]).
Proof. apply EntailsI. now setoid_rewrite tspec_iff. Qed.


  Definition withSpace_single (P : RegSpec) (size : ) :=
    match P with
    | Contains r x Contains_size r x size
    | Void Void_size size
    | _ P
    end.

  Definition withSpace {n : } (P : SpecV n) (spaces : Vector.t n) : SpecV n :=
    Vector.map2 withSpace_single P spaces.

  Lemma tspec_single_withSpace_tspec_single (P : RegSpec) (size : ) t :
    tspec_single (withSpace_single P size) t tspec_single P t.
  Proof. intros. destruct P; cbn in *; auto. Qed.

  Lemma tspec_withSpace_tspec {n : } Q P (s : Vector.t n) t :
    tspec (Q,withSpace P s) t tspec (Q,P) t.
  Proof. unfold withSpace. intros [HP H]%tspecE. apply tspecI. easy. intros i; specialize (H i). simpl_vector in *. eapply tspec_single_withSpace_tspec_single; eauto. Qed.


  Definition dummy_size (t : tape sig^+) (P : RegSpec) : :=
    match P with
    | Contains r x length (left t)
    | Void length (tape_local_l t)
    | _ 0
    end.

  Lemma tspec_single_tspec_single_withSpace (P : RegSpec) t :
    tspec_single P t tspec_single (withSpace_single P (dummy_size t P)) t.
  Proof. intros H. destruct P; cbn in *; eauto. Qed.

  Definition dummy_sizes (n : ) (t : tapes sig^+ n) (P : SpecV n) : Vector.t n :=
     Vector.map2 dummy_size t P.

  Lemma tspec_tspec_withSpace (n : ) Q (P : SpecV n) t :
    tspec (Q,P) t tspec (Q,withSpace P (dummy_sizes t P)) t.
  Proof.
    unfold withSpace, dummy_sizes in *. intros [HP ?]%tspecE. eapply tspecI. cbn in *; auto.
    intros i; specialize (H i); cbn in *. simpl_vector. now apply tspec_single_tspec_single_withSpace.
  Qed.



End RegSpec.

Arguments Custom {sig}.
Arguments Void {sig}.
Arguments Void_size {sig}.
Arguments dummy_sizes : simpl never.
Hint Resolve tspec_single_Contains_size_Contains : core.

Declare Scope spec_scope.
Delimit Scope spec_scope with spec.
Bind Scope spec_scope with Spec.
Notation "'≃≃(' S ')'" := (tspec S%spec) (at level 0, S at level 200, no associativity, format "'≃≃(' S ')'").
Notation "'≃≃(' P ',' S ')'" := (tspec (P%list,S%vector)) (at level 0, P at level 200, S at level 200, no associativity, format "'≃≃(' P ',' S ')'").

Notation "t ≃≃ S" := (tspec S%spec t) (at level 70, no associativity).

Notation "≃( I ) x" := (Contains I x) (at level 70, I at level 200, no associativity, format "'≃(' I ')' x").
Notation "≃( I ';' s ) x" := (Contains_size I s x) (at level 70, I at level 200, s at level 200, no associativity, format "'≃(' I ';' s ')' x").

Arguments tspec _%spec _.

Fixpoint implList (Ps : list Prop) (Q : Prop) :=
  match Ps with
    [] Q
  | P::Ps P implList Ps Q
  end.
Arguments implList !_ _.

Instance fold_right_impl' : Proper ( Basics.impl --> Basics.impl Basics.impl) (implList).
Proof. intros xs;induction xs;cbn;intros ? H';inv H';cbn. easy. firstorder. Qed.

Instance fold_right_iff : Proper ( iff iff iff) (implList).
Proof. intros xs;induction xs;cbn;intros ? H';inv H';cbn. easy. firstorder. Qed.

Lemma implList_iff P (Ps : list Prop):
  implList Ps P
   (List.fold_right and True Ps P).
Proof.
  induction Ps in P|-*;cbn. firstorder. setoid_rewrite IHPs. tauto.
Qed.


Lemma implListE P (Ps : list Prop): implList Ps P (List.fold_right and True Ps P).
Proof. now rewrite implList_iff. Qed.

Lemma implListI (P:Prop) (Ps : list Prop): (List.fold_right and True Ps P) implList Ps P.
Proof. now rewrite implList_iff. Qed.

Instance Forall2_refl X (R: X _): Reflexive R Reflexive ( R).
Proof. intros ? xs;induction xs;eauto. Qed.

Lemma tspec_introPure (sig: finType) (n : ) P (Ps : SpecV sig n) Q:
  implList P (Entails (≃≃([],Ps)) Q)
   Entails (tspec (P,Ps)) Q.
Proof.
  setoid_rewrite Entails_iff. rewrite implList_iff. intros H ? []%tspecE. eapply H. eassumption. now apply tspecI.
Qed.


Lemma tspec_revertPure (sig: finType) (n : ) (P0:Prop) P (Ps : SpecV sig n) Q:
  
   Entails (tspec (::P,Ps)) Q
   Entails (tspec (P,Ps)) Q.
Proof.
  setoid_rewrite Entails_iff. unfold tspec;cbn. intuition.
Qed.


Lemma Triple_introPure (F sig: finType) (n : ) P (Ps : SpecV sig n) Q (pM : pTM sig^+ F n) :
  implList P (Triple (≃≃([],Ps)) pM Q)
   Triple (tspec (P,Ps)) pM Q.
Proof.
  intros. rewrite tspec_Entails. apply Triple_and_pre. cbn in H. now rewrite implList_iff.
Qed.


Lemma TripleT_introPure (sig F : finType) (n : ) P (Ps : SpecV sig n) Q k (pM : pTM sig^+ F n) :
  implList P (TripleT (≃≃([],Ps)) k pM Q)
   TripleT (tspec (P,Ps)) k pM Q.
Proof.
  intros. rewrite tspec_Entails. apply TripleT_and_pre. cbn in H. now rewrite implList_iff.
Qed.



Definition SpecVTrue {sig : Type} {n : } : SpecV sig n := Vector.const (Custom ( _ True)) n.


Arguments tspec : simpl never.

Definition appSize {n : } : Vector.t () n Vector.t n Vector.t n :=
   fs s tabulate ( i fs[@i] s[@i]).


Lemma Triple_RemoveSpace_ex (n : ) (sig : finType) (F : Type) X
(P : SpecV sig n) P' (M : pTM sig^+ F n) Q Q' Ctx (fs : _ Vector.t () n) :
  ( s, Triple (tspec (P',withSpace P s)) M ( y t x:X, Ctx x (tspec (Q' x y,withSpace (Q x y) (appSize (fs x) s)) t)))
  ( x, Proper (Basics.impl Basics.impl) (Ctx x))
  Triple (tspec (P',P)) M ( y t x, Ctx x (tspec (Q' x y ,Q x y) t)).
Proof.
  intros HTrip Hctx. setoid_rewrite Triple_iff in HTrip. rewrite Triple_iff.
  eapply Realise_monotone with
  (R' := tin '(yout, tout) s, tspec (P',withSpace P s) tin
     x:X, Ctx x (tspec (Q' x yout,withSpace (Q x yout) (appSize (fs x) s)) tout)).
  - unfold Triple_Rel, Realise in *. intros tin k outc HLoop. intros s HP.
    specialize HTrip with (1 := HLoop) (2 := HP) as [x H'']. eexists. eauto.
  - clear HTrip. intros tin (yout, tout). intros H HP.
    specialize (H (dummy_sizes tin P)). spec_assert H by now apply tspec_tspec_withSpace.
    destruct H as (x&H). exists x. eapply Hctx. 2:eassumption.
    intro H'. now apply tspec_withSpace_tspec in H'.
Qed.


Lemma Triple_RemoveSpace (n : ) (sig : finType) (F : Type) (P : SpecV sig n) P' (M : pTM sig^+ F n) (Q : F SpecV sig n) Q' (fs : Vector.t () n) :
  ( s, Triple (tspec (P',withSpace P s)) M ( y tspec (Q' y,withSpace (Q y) (appSize fs s))))
  Triple (tspec (P',P)) M ( y tspec (Q' y ,Q y)).
Proof.
  intro HTrip. setoid_rewrite Triple_iff in HTrip. rewrite Triple_iff.
  eapply Realise_monotone with (R' := tin '(yout, tout) s, tspec (P',withSpace P s) tin tspec (Q' yout,withSpace (Q yout) (appSize fs s)) tout).
  - unfold Triple_Rel, Realise in *. intros tin k outc HLoop. intros s HP.
    now specialize HTrip with (1 := HLoop) (2 := HP).
  - clear HTrip. intros tin (yout, tout). intros H HP.
    specialize (H (dummy_sizes tin P)). spec_assert H by now apply tspec_tspec_withSpace.
    now apply tspec_withSpace_tspec in H.
Qed.


Lemma TripleT_RemoveSpace (n : ) (sig : finType) (F : Type) P' (P : SpecV sig n) (k : ) (M : pTM sig^+ F n) Q' (Q : F SpecV sig n) (fs : Vector.t () n) :
  ( s, TripleT (tspec (P',withSpace P s)) k M ( y tspec (Q' y,withSpace (Q y) (appSize fs s))))
  TripleT (tspec (P',P)) k M ( y tspec (Q' y,Q y)).
Proof.
  intros HTrip. split.
  - eapply Triple_RemoveSpace. intros s. apply HTrip.
  - setoid_rewrite TripleT_iff in HTrip.
   eapply TerminatesIn_monotone with (T' := tin k' tspec (P',P) tin k k').
    + unfold Triple_TRel, TerminatesIn in *. intros tin k' (HP&Hk).
      specialize (HTrip (dummy_sizes tin P)) as (_&HT).
      specialize HT with ( := tin) ( := k). spec_assert HT as (conf&HLoop).
      { split. now apply tspec_tspec_withSpace. reflexivity. }
      exists conf. eapply loop_monotone; eauto.
    + unfold Triple_TRel. intros tin k' (HP&Hk). eauto.
Qed.


Instance fold_right_and : Proper (iff iff iff) (fold_right and).
Proof. intros ? ? ? xs;induction xs;cbn;intros ? H';inv H';cbn. easy. firstorder. Qed.

Instance fold_right_and' : Proper (Basics.impl iff Basics.impl) (fold_right and).
Proof. intros ? ? ? xs;induction xs;cbn;intros ? H';inv H';cbn. easy. firstorder. Qed.

Lemma tspec_solve (sig : Type) (n : ) (t : tapes (boundary+sig) n) (R : SpecV sig n) P:
List.fold_right and ( i, tspec_single R[@i] t[@i]) P
  tspec (P,R) t.
Proof. refine ( P P). Qed.

Lemma tspec_space_solve (sig : Type) (n : ) (t : tapes (boundary+sig) n) (R : SpecV sig n) P (ss : Vector.t n) :
  List.fold_right and ( i, tspec_single (withSpace_single R[@i] ss[@i]) t[@i]) P
  tspec (P,withSpace R ss) t.
Proof. unfold withSpace. intros. apply tspec_solve. simpl_vector. auto. Qed.

Lemma tspec_ext (sig : finType) (n : ) (t : tapes (boundary+sig) n) (P P' : list Prop) (R R' : Vector.t (RegSpec sig) n) :
  tspec (P',R') t
  implList P' (List.fold_right and True P)
  ( i, tspec_single R'[@i] t[@i] tspec_single R[@i] t[@i])
  tspec (P,R) t.
Proof.
  intros [HP ]%tspecE . eapply tspecI.
  eapply implList_iff. 2:eassumption. eapply fold_right_impl'. 2:reflexivity. 2:eassumption. easy.
  intros i; specialize ( i); specialize ( i); eauto.
Qed.


Lemma tspec_space_ext (sig : finType) (n : ) (t : tapes (boundary+sig) n) (P P':list Prop) (R R' : SpecV sig n)
      (ss ss' : Vector.t n) :
  tspec (P',withSpace R' ss') t
  implList P' (List.fold_right and True P)
  ( i, tspec_single (withSpace_single R'[@i] ss'[@i]) t[@i] tspec_single (withSpace_single R[@i] ss[@i]) t[@i])
  tspec (P,withSpace R ss) t.
Proof.
  unfold withSpace. intros [HP ]%tspecE . eapply tspecI.
  eapply implList_iff. 2:eassumption. eapply fold_right_impl'. 2:reflexivity. 2:eassumption. easy.
  intros i; specialize ( i); specialize ( i); eauto.
  cbn. simpl_vector in *; cbn. eauto.
Qed.



Section Lifting.

  Variable (sig : Type).

  Variable (m n : ).

  Variable (P : @SpecV sig n).

  Variable (I : Vector.t (Fin.t n) m).   Hypothesis (HI : dupfree I).

  Definition Downlift : @SpecV sig m :=
    (select I P).

  Lemma tape_fulfill_Downlift_select P' tp :
    tspec (P',P) tp
    tspec (P',Downlift) (select I tp).
  Proof.
    unfold Downlift.
    intros [? H]%tspecE.
    eapply tspecI. easy.
    intros i;cbn. rewrite !select_nth. easy.
  Qed.


  Definition Frame (Q : @SpecV sig m) : @SpecV sig n := fill I P Q.

End Lifting.

Lemma LiftTapes_Spec_ex (sig : finType) X (F : finType) (m n : ) (I : Vector.t (Fin.t n) m)
P' P Q' Q (pM : pTM sig^+ F m) :
  dupfree I
  Triple (tspec (P',Downlift P I)) pM ( y t x:X, tspec (Q' x y,Q x y) t)
  Triple (tspec (P',P)) (LiftTapes pM I) ( y t x, tspec (Q' x y,Frame P I (Q x y)) t ).
Proof.
  unfold Frame. rewrite !Triple_iff.
  intros HDup HTrip.
  eapply Realise_monotone.
  { apply LiftTapes_Realise. assumption. apply HTrip. }
  {
    intros tin (yout, tout) (H&HInj). cbn -[Downlift tspec] in *.
    intros HP.
    spec_assert H by now apply tape_fulfill_Downlift_select.
    destruct H as [x H].
    eapply tspecE in H as [H' H]. eapply tspecE in HP as [HP' HP].
    exists x.
    eapply tspecI;cbn.
    { clear - H' HP'. induction P';cbn in *. all:firstorder. }
    clear H' HP'.
    hnf. intros j. decide (Vector.In j I) as [HD|HD].
    - unfold Frame.
      apply vect_nth_In' in HD as (ij&HD).
      erewrite fill_correct_nth; eauto.
      specialize (H ij).
      now rewrite select_nth, HD in H.
    - unfold Frame. rewrite fill_not_index; eauto.
      specialize (HInj j HD). rewrite HInj. now apply HP.
  }
Qed.


Lemma LiftTapes_Spec (sig : finType) (F : finType) (m n : ) (I : Vector.t (Fin.t n) m) P' (P : SpecV sig n) Q' (Q : F SpecV sig m) (pM : pTM sig^+ F m) :
  dupfree I
  Triple (tspec (P',Downlift P I)) pM ( y tspec (Q' y,Q y))
  Triple (tspec (P',P)) (LiftTapes pM I) ( y tspec (Q' y,Frame P I (Q y))).
Proof.
  unfold Frame. rewrite !Triple_iff.
  intros HDup HTrip.
  eapply Realise_monotone.
  { apply LiftTapes_Realise. assumption. apply HTrip. }
  {
    intros tin (yout, tout) (H&HInj). cbn -[Downlift tspec] in *.
    intros HP.
    spec_assert H by now apply tape_fulfill_Downlift_select.
    eapply tspecE in H as [H' H]. eapply tspecE in HP as [HP' HP].
    eapply tspecI;cbn.
    { clear - H' HP'. induction P';cbn in *. all:firstorder. }
    clear H' HP'.
    hnf. intros j. decide (Vector.In j I) as [HD|HD].
    - unfold Frame.
      apply vect_nth_In' in HD as (ij&HD).
      erewrite fill_correct_nth; eauto.
      specialize (H ij).
      now rewrite select_nth, HD in H.
    - unfold Frame. rewrite fill_not_index; eauto.
      specialize (HInj j HD). rewrite HInj. now apply HP.
  }
Qed.


Lemma LiftTapes_Spec_con (sig : finType) (F : finType) (m n : ) (I : Vector.t (Fin.t n) m) P' (P : SpecV sig n) Q' (Q : F SpecV sig m) R' (R : F SpecV sig n) (pM : pTM sig^+ F m) :
  dupfree I
  Triple (tspec (P',Downlift P I)) pM ( y tspec (Q' y,Q y))
  ( yout, Entails (tspec (Q' yout,Frame P I (Q yout))) (tspec (R' yout,R yout)))
  Triple (tspec (P',P)) (LiftTapes pM I) ( y tspec (R' y,R y)).
Proof.
   intros ? ? %asPointwise. eapply LiftTapes_Spec. all:easy.
Qed.



Lemma LiftTapes_SpecT (sig F : finType)(m n : ) (I : Vector.t (Fin.t n) m) P' (P : SpecV sig n) (k : ) Q' (Q : F SpecV sig m) (pM : pTM sig^+ F m) :
  dupfree I
  TripleT (tspec (P',Downlift P I)) k pM ( y tspec (Q' y,Q y))
  TripleT (tspec (P',P)) k (LiftTapes pM I) ( y tspec (Q' y,Frame P I (Q y))).
Proof.
  intros HDup (HTrip&HTrip').
  split.
  - apply LiftTapes_Spec; eauto.
  - eapply TerminatesIn_monotone.
    + apply LiftTapes_Terminates; eauto.
    + intros tin k' (H&H'). split; auto.
      now apply tape_fulfill_Downlift_select.
Qed.


Lemma LiftTapes_SpecT_con (sig : finType) (F : finType) (m n : ) (I : Vector.t (Fin.t n) m)
P' (P : SpecV sig n) Q' (Q : F SpecV sig m) R' (R : F SpecV sig n)
      (k : ) (pM : pTM sig^+ F m) :
  dupfree I
  TripleT (tspec (P',Downlift P I)) k pM ( y tspec (Q' y,Q y))
  ( yout, Entails (tspec (Q' yout,Frame P I (Q yout))) (tspec (R' yout,R yout)))
  TripleT (tspec (P',P)) k (LiftTapes pM I) ( y tspec (R' y,R y)).
Proof. eauto using ConsequenceT_post, LiftTapes_SpecT. Qed.

Lemma Downlift_withSpace (m n : ) (sig : Type) (P : SpecV sig n) (I : Vector.t (Fin.t n) m) (ss : Vector.t n) :
  Downlift (withSpace P ss) I = withSpace (Downlift P I) (select I ss).
Proof.
  unfold withSpace, Downlift.
  eapply VectorSpec.eq_nth_iff; intros ? ? .
  simpl_vector. rewrite !select_nth. simpl_vector. reflexivity.
Qed.


Lemma tspec_Downlift_withSpace (m n : ) (sig : Type) P' (P : SpecV sig n) (I : Vector.t (Fin.t n) m) (ss : Vector.t n):
  Entails ≃≃( P', Downlift (sig:=sig) (m:=m) (n:=n) (withSpace P ss) I) ≃≃( P',withSpace (Downlift P I) (select I ss)).
Proof. rewrite Entails_iff. intros H. erewrite Downlift_withSpace; eauto. Qed.

Lemma Triple_Downlift_withSpace (m n : ) (sig : finType) P' (P : SpecV sig n) (I : Vector.t (Fin.t n) m) (ss : Vector.t n)
      (F : Type) (M : pTM sig^+ F m) (Q : F Assert sig^+ m) :
  Triple (tspec (P',withSpace (Downlift P I) (select I ss))) M Q
  Triple (tspec (P',Downlift (withSpace P ss) I)) M Q.
Proof. now rewrite tspec_Downlift_withSpace. Qed.

Lemma TripleT_Downlift_withSpace (m n : ) (sig : finType) P' (P : SpecV sig n) (I : Vector.t (Fin.t n) m) (ss : Vector.t n)
      (F : Type) (k : ) (M : pTM sig^+ F m) (Q : F Assert sig^+ m) :
  TripleT (tspec (P',withSpace (Downlift P I) (select I ss))) k M Q
  TripleT (tspec (P',Downlift (withSpace P ss) I)) k M Q.
Proof. now rewrite tspec_Downlift_withSpace. Qed.

Instance dec_ex_fin (n : ) (P : Fin.t n Prop) (decP: (i : Fin.t n), dec (P i)) : dec ( (i : Fin.t n), P i).
Proof.
  induction n.
  - right. intros (i&?). destruct_fin i.
  - decide (P ).
    + left. eauto.
    + specialize (IHn ( i P (Fin.FS i))). spec_assert IHn as [IH|IH] by eauto.
      * left. destruct IH as (i&IH). exists (Fin.FS i). eauto.
      * right. intros (j&H). pose proof (fin_destruct_S j) as [(j'&) | ]; eauto.
Qed.


Lemma Frame_withSpace (m n : ) (sig : Type) (P : SpecV sig n) (P' : SpecV sig m) (I : Vector.t (Fin.t n) m) (ss : Vector.t n) (ss' : Vector.t m) :
  dupfree I
  Frame (withSpace P ss) I (withSpace P' ss') = withSpace (Frame P I P') (fill I ss ss').
Proof.
  intros Hdup. unfold Frame,withSpace.
  eapply VectorSpec.eq_nth_iff; intros ? i .
  simpl_vector.
  decide ( j, I[@j]=i) as [(j&Hj)|Hj].
  + erewrite !fill_correct_nth by eauto. now simpl_vector.
  + assert (not_index I i).
    { hnf. intros (k&) % vect_nth_In'. contradict Hj. eauto. }
    erewrite !fill_not_index by eauto. now simpl_vector.
Qed.



Lemma tspec_Frame_withSpace'
      (m n : ) (I : Vector.t (Fin.t n) m):
  dupfree I (sig : Type) Q (P : SpecV sig n) (P' : SpecV sig m) (ss : Vector.t n) (ss' : Vector.t m),
  Entails ≃≃( Q , Frame (withSpace P ss) I (withSpace P' ss')) ≃≃( Q, withSpace (Frame P I P') (fill I ss ss')).
Proof. intros **. erewrite Frame_withSpace; eauto. Qed.



Lemma LiftTapes_Spec_space (sig F : finType) (m n : ) (I : Vector.t (Fin.t n) m) P' (P : SpecV sig n) Q' (Q : F SpecV sig m) (pM : pTM sig^+ F m)
     (ss : Vector.t n) (ss' : Vector.t m) :
  dupfree I
  Triple (tspec (P',withSpace (Downlift P I) (select I ss))) pM ( y tspec (Q' y,withSpace (Q y) ss'))
  Triple (tspec (P',withSpace P ss)) (LiftTapes pM I) ( y tspec (Q' y,withSpace (Frame P I (Q y)) (fill I ss ss'))).
Proof.
  intros . rewrite Downlift_withSpace in . apply LiftTapes_Spec in . setoid_rewrite tspec_Frame_withSpace' in . all:eauto.
Qed.


Lemma LiftTapes_SpecT_space (sig F : finType) (m n : ) (I : Vector.t (Fin.t n) m) P' (P : SpecV sig n) (k : ) Q' (Q : F SpecV sig m) (pM : pTM sig^+ F m)
     (ss : Vector.t n) (ss' : Vector.t m) :
  dupfree I
  TripleT (tspec (P',withSpace (Downlift P I) (select I ss))) k pM ( y tspec (Q' y,withSpace (Q y) ss'))
  TripleT (tspec (P',withSpace P ss)) k (LiftTapes pM I) ( y tspec (Q' y,withSpace (Frame P I (Q y)) (fill I ss ss'))).
Proof.
  intros . rewrite Downlift_withSpace in . apply LiftTapes_SpecT in . setoid_rewrite tspec_Frame_withSpace' in . all:eauto.
Qed.


Lemma LiftTapes_Spec_space_con (sig : finType) (F : finType) (m n : ) (I : Vector.t (Fin.t n) m)
      P' (P : SpecV sig n) Q' (Q : F SpecV sig m) R' (R : F SpecV sig n) (ss : Vector.t n) (ss' : Vector.t m) (ss'' : Vector.t n)
      (pM : pTM sig^+ F m) :
  dupfree I
  Triple (tspec (P',withSpace (Downlift P I) (select I ss))) pM ( y tspec (Q' y,withSpace (Q y) ss'))
  ( yout, Entails (tspec (Q' yout,withSpace (Frame P I (Q yout)) (fill I ss ss'))) (tspec (R' yout,withSpace (R yout) ss'')))
  Triple (tspec (P',withSpace P ss)) (LiftTapes pM I) ( y tspec (R' y,withSpace (R y) ss'')).
Proof.
  intros %asPointwise. rewrite Downlift_withSpace in . apply LiftTapes_Spec in .
  setoid_rewrite tspec_Frame_withSpace' in . all:easy.
Qed.


Lemma LiftTapes_SpecT_space_con (sig : finType) (F : finType) (m n : ) (I : Vector.t (Fin.t n) m)
      P' (P : SpecV sig n) Q' (Q : F SpecV sig m) R' (R : F SpecV sig n) (ss : Vector.t n) (ss' : Vector.t m) (ss'' : Vector.t n)
      (k : ) (pM : pTM sig^+ F m) :
  dupfree I
  TripleT (tspec (P',withSpace (Downlift P I) (select I ss))) k pM ( y tspec (Q' y,withSpace (Q y) ss'))
  ( yout, Entails (tspec (Q' yout,withSpace (Frame P I (Q yout)) (fill I ss ss'))) (tspec (R' yout,withSpace (R yout) ss'')))
  TripleT (tspec (P',withSpace P ss)) k (LiftTapes pM I) ( y tspec (R' y,withSpace (R y) ss'')).
Proof.
  intros %asPointwise. rewrite Downlift_withSpace in . apply LiftTapes_SpecT in .
  setoid_rewrite tspec_Frame_withSpace' in . all:easy.
Qed.




Section AlphabetLifting.

  Variable (sig : Type).
  Variable (retr : Retract sig ).

  Definition LiftSpec_single (T : RegSpec sig) : RegSpec :=
    match T with
    | Contains r x Contains (ComposeRetract retr r) x
    | Contains_size r x s Contains_size (ComposeRetract retr r) x s
    | Void Void
    | Void_size s Void_size s
    | Custom p Custom ( t p (surjectTape (Retr_g) (inl UNKNOWN) t))
    end.

  Variable (n : ).

  Definition LiftSpec (T : SpecV sig n) : SpecV n :=
    Vector.map LiftSpec_single T.

  Lemma LiftSpec_surjectTape_tspec_single t T :
    tspec_single (LiftSpec_single T) t
    tspec_single T (surjectTape Retr_g (inl UNKNOWN) t).
  Proof. destruct T; cbn in *; intros; simpl_surject; eauto. Qed.

  Lemma LiftSpec_surjectTape_tspec_single' t T :
    tspec_single T (surjectTape Retr_g (inl UNKNOWN) t)
    tspec_single (LiftSpec_single T) t.
  Proof. destruct T; cbn in *; intros; simpl_surject; eauto. Qed.

  Lemma LiftSpec_surjectTapes_tspec tin P' P :
    tin ≃≃ (P', LiftSpec P)
    surjectTapes Retr_g (inl UNKNOWN) tin ≃≃ (P',P).
  Proof.
    intros (H'&H)%tspecE. eapply tspecI. easy.
    intros i; specialize (H i); cbn. unfold LiftSpec in *.
    simpl_tape in *. now apply LiftSpec_surjectTape_tspec_single.
  Qed.


  Lemma LiftSpec_surjectTapes_tspec' tin P P':
    surjectTapes Retr_g (inl UNKNOWN) tin ≃≃ (P',P)
    tin ≃≃ (P',LiftSpec P).
  Proof.
    intros (H'&H)%tspecE. eapply tspecI. easy. unfold LiftSpec in *.
    intros i; specialize (H i); cbn.
    simpl_tape in *. now apply LiftSpec_surjectTape_tspec_single'.
  Qed.



End AlphabetLifting.

Lemma LiftSpec_withSpace_single (sig tau : Type) (I : Retract sig ) (P : RegSpec sig) (s : ) :
  LiftSpec_single I (withSpace_single P s) = withSpace_single (LiftSpec_single I P) s.
Proof. destruct P; cbn; eauto. Qed.

Lemma LiftSpec_withSpace (sig tau : Type) (n : ) (I : Retract sig ) (P : SpecV sig n) (ss : Vector.t n) :
  LiftSpec I (withSpace P ss) = withSpace (LiftSpec I P) ss.
Proof.
  eapply VectorSpec.eq_nth_iff; intros ? ? . unfold LiftSpec, withSpace.
  simpl_vector. apply LiftSpec_withSpace_single.
Qed.


Section AlphabetLifting'.

  Variable (sig : finType) (n : ).
  Variable (retr : Retract sig ).


  Lemma ChangeAlphabet_Spec_ex (F : finType) X P' (Ctx : X Prop Prop) (P : SpecV sig n) (pM : pTM sig^+ F n) Q' (Q : X F SpecV sig n) :
    Triple (tspec (P',P)) pM ( y t x:X, Ctx x (tspec (Q' x y,Q x y) t))
    ( x, Proper (Basics.impl Basics.impl) (Ctx x))
    Triple (tspec (P',LiftSpec retr P)) (ChangeAlphabet pM retr)
      ( yout t x, Ctx x (tspec (Q' x yout,LiftSpec retr (Q x yout)) t)).
  Proof.
    rewrite !Triple_iff. intros HTrip HCtx. eapply Realise_monotone.
    - TM_Correct. eassumption.
    - intros tin (yout, tout) H Henc. cbn in *.
      spec_assert H by now apply LiftSpec_surjectTapes_tspec.
      destruct H as (x&H). exists x. cbv in HCtx. eapply HCtx. 2:apply H.
      now apply LiftSpec_surjectTapes_tspec'.
  Qed.


  Lemma ChangeAlphabet_Spec (F : finType) P' (P : SpecV sig n) (pM : pTM sig^+ F n) Q' (Q : F SpecV sig n) :
    Triple (tspec (P',P)) pM ( yout tspec (Q' yout,Q yout))
    Triple (tspec (P',LiftSpec retr P)) (ChangeAlphabet pM retr) ( yout tspec (Q' yout,LiftSpec retr (Q yout))).
  Proof.
    rewrite !Triple_iff. intros HTrip. eapply Realise_monotone.
    - TM_Correct. eassumption.
    - intros tin (yout, tout) H Henc. cbn in *.
      spec_assert H by now apply LiftSpec_surjectTapes_tspec.
      now apply LiftSpec_surjectTapes_tspec'.
  Qed.


  Lemma ChangeAlphabet_SpecT (F : finType) P' (P : SpecV sig n) (k : ) (pM : pTM sig^+ F n) Q' (Q : F SpecV sig n) :
    TripleT (tspec (P',P)) k pM ( yout tspec (Q' yout, Q yout))
    TripleT (tspec (P',LiftSpec retr P)) k (ChangeAlphabet pM retr) ( yout tspec (Q' yout,LiftSpec retr (Q yout))).
  Proof.
    intros HTrip. split.
    { apply ChangeAlphabet_Spec. eapply TripleT_Triple; eauto. }
    {
      eapply TerminatesIn_monotone.
      - TM_Correct. apply HTrip.
      - unfold Triple_TRel. intros tin k' (H&Hk). cbn. split; auto.
        now apply LiftSpec_surjectTapes_tspec.
    }
  Qed.



  Lemma ChangeAlphabet_Spec_pre_post (F : finType)
        P0 (P : SpecV sig n) (P' : SpecV n)
        (pM : pTM sig^+ F n)
        Q0 (Q : F SpecV sig n) (Q' : F SpecV n) :
    Triple (tspec (,P)) pM ( yout tspec ( yout, Q yout) )
    (Entails ≃≃( ,P') ≃≃( ,LiftSpec retr P))
    ( yout, Entails ≃≃( yout, LiftSpec retr (Q yout)) ≃≃( ( yout,Q' yout)))
    Triple (tspec (, P')) (ChangeAlphabet pM retr) ( yout tspec ( yout, Q' yout)).
  Proof.
    intros .
    eapply Consequence.
    - apply ChangeAlphabet_Spec. apply .
    - apply .
    - apply .
  Qed.


  Lemma ChangeAlphabet_SpecT_pre_post (F : finType)
        P0 (P : SpecV sig n) (P' : SpecV n)
        (k : ) (pM : pTM sig^+ F n)
        Q0 (Q : F SpecV sig n) (Q' : F SpecV n) :
    TripleT (tspec (,P)) k pM ( yout tspec ( yout, Q yout) )
    (Entails ≃≃( ,P') ≃≃( ,LiftSpec retr P))
    ( yout, Entails ≃≃( yout, LiftSpec retr (Q yout)) ≃≃( ( yout,Q' yout)))
    TripleT (tspec (, P')) k (ChangeAlphabet pM retr) ( yout tspec ( yout, Q' yout)).
  Proof.
    intros .
    eapply ConsequenceT.
    - apply ChangeAlphabet_SpecT. apply .
    - apply .
    - apply .
    - reflexivity.
  Qed.



  Lemma ChangeAlphabet_Spec_pre (F : finType)
        P0 (P : SpecV sig n) (P' : SpecV n)
        (pM : pTM sig^+ F n)
        Q0 (Q : F SpecV sig n) :
    Triple (tspec (,P)) pM ( yout tspec ( yout, Q yout))
    (Entails ≃≃( ,P') ≃≃( , LiftSpec retr P))
    Triple (tspec (,P')) (ChangeAlphabet pM retr) ( yout tspec ( yout,LiftSpec retr (Q yout))).
  Proof.
    intros .
    eapply Consequence.
    - apply ChangeAlphabet_Spec. apply .
    - apply .
    - eauto.
  Qed.


  Lemma ChangeAlphabet_SpecT_pre (F : finType)
        P0 (P : SpecV sig n) (P' : SpecV n)
        (k : ) (pM : pTM sig^+ F n)
        Q0 (Q : F SpecV sig n) :
    TripleT (tspec (,P)) k pM ( yout tspec ( yout, Q yout))
    (Entails ≃≃( , P') ≃≃( ,LiftSpec retr P))
    TripleT (tspec (,P')) k (ChangeAlphabet pM retr) ( yout tspec ( yout,LiftSpec retr (Q yout))).
  Proof.
    intros .
    eapply ConsequenceT.
    - apply ChangeAlphabet_SpecT. apply .
    - apply .
    - eauto.
    - reflexivity.
  Qed.



  Lemma ChangeAlphabet_Spec_space_pre_post (F : finType)
        P0 (P : SpecV sig n) (P' : SpecV n)
        (pM : pTM sig^+ F n)
        Q0 (Q : F SpecV sig n) (Q' : F SpecV n)
        (ss ss' : Vector.t n) :
    Triple (tspec (,withSpace P ss)) pM ( yout tspec ( yout,withSpace (Q yout) ss'))
    (Entails ≃≃( , withSpace P' ss) ≃≃( , withSpace (LiftSpec retr P) ss))
    ( yout, Entails ≃≃( yout, withSpace (LiftSpec retr (Q yout)) ss') (tspec ( yout,withSpace (Q' yout) ss')))
    Triple (tspec (,withSpace P' ss)) (ChangeAlphabet pM retr) ( yout tspec ( yout, withSpace (Q' yout) ss')).
  Proof.
    intros .
    eapply Consequence.
    - apply ChangeAlphabet_Spec. apply .
    - rewrite LiftSpec_withSpace. apply .
    - setoid_rewrite Entails_iff. cbn. intros. rewrite LiftSpec_withSpace in H. now apply .
  Qed.


  Lemma ChangeAlphabet_SpecT_space_pre_post (F : finType)
        P0 (P : SpecV sig n) (P' : SpecV n)
        (k : ) (pM : pTM sig^+ F n)
        Q0 (Q : F SpecV sig n) (Q' : F SpecV n)
        (ss ss' : Vector.t n) :
        TripleT (tspec (,withSpace P ss)) k pM ( yout tspec ( yout,withSpace (Q yout) ss'))
        (Entails ≃≃( , withSpace P' ss) ≃≃( , withSpace (LiftSpec retr P) ss))
        ( yout, Entails ≃≃( yout, withSpace (LiftSpec retr (Q yout)) ss') (tspec ( yout,withSpace (Q' yout) ss')))
        TripleT (tspec (,withSpace P' ss)) k (ChangeAlphabet pM retr) ( yout tspec ( yout, withSpace (Q' yout) ss')).
  Proof.
    intros .
    eapply ConsequenceT.
    - apply ChangeAlphabet_SpecT. apply .
    - rewrite LiftSpec_withSpace. apply .
    - setoid_rewrite Entails_iff. cbn. intros. rewrite LiftSpec_withSpace in H. now apply .
    - reflexivity.
  Qed.



  Lemma ChangeAlphabet_Spec_space_pre (F : finType)
        P0 (P : SpecV sig n) (P' : SpecV n)
        (pM : pTM sig^+ F n)
        Q0 (Q : F SpecV sig n)
        (ss ss' : Vector.t n) :
    Triple (tspec (,withSpace P ss)) pM ( yout tspec ( yout,withSpace (Q yout) ss'))
    Entails ≃≃( , withSpace P' ss) ≃≃( , withSpace (LiftSpec retr P) ss)
    Triple (tspec (, withSpace P' ss)) (ChangeAlphabet pM retr) ( yout tspec ( yout, withSpace (LiftSpec retr (Q yout)) ss')).
  Proof.
    intros .
    eapply Consequence.
    - apply ChangeAlphabet_Spec. apply .
    - rewrite LiftSpec_withSpace. apply .
    - setoid_rewrite Entails_iff. cbn. intros. rewrite LiftSpec_withSpace in H. now apply H.
  Qed.


  Lemma ChangeAlphabet_SpecT_space_pre (F : finType)
        P0 (P : SpecV sig n) (P' : SpecV n)
        (k : ) (pM : pTM sig^+ F n)
        Q0 (Q : F SpecV sig n)
        (ss ss' : Vector.t n) :
    TripleT (tspec (,withSpace P ss)) k pM ( yout tspec ( yout, withSpace (Q yout) ss'))
    Entails ≃≃( , withSpace P' ss) ≃≃( , withSpace (LiftSpec retr P) ss)
    TripleT (tspec (, withSpace P' ss)) k (ChangeAlphabet pM retr) ( yout tspec ( yout,withSpace (LiftSpec retr (Q yout)) ss')).
  Proof.
    intros .
    eapply ConsequenceT.
    - apply ChangeAlphabet_SpecT. apply .
    - rewrite LiftSpec_withSpace. apply .
    - setoid_rewrite Entails_iff. cbn. intros. rewrite LiftSpec_withSpace in H. now apply H.
    - reflexivity.
  Qed.


End AlphabetLifting'.


Global Arguments withSpace : simpl never.


Notation "'SpecFalse'" := ([False],_): spec_scope.