From Undecidability Require Import MaxList.
From Undecidability Require Import TM.Util.TM_facts TM.Code.CodeTM.
From Undecidability Require Import TM.Util.VectorPrelim.
(* MOVE : this file contains general lemmas from is all over the place... *)
Lemma max_list_rec_eq_foldl (a : nat) (xs : list nat) :
fold_left max xs a = max_list_rec a xs.
Proof.
revert a. induction xs as [ | x xs IH]; intros; cbn in *.
- reflexivity.
- rewrite IH. rewrite !max_list_rec_max. nia.
Qed.
Lemma sizeOfmTapes_max_list_map (sig : Type) (n : nat) (T : tapes sig n) :
sizeOfmTapes T = max_list_map (@sizeOfTape _) (vector_to_list T).
Proof.
unfold sizeOfmTapes.
rewrite fold_left_vector_to_list.
rewrite <- vector_to_list_map.
unfold max_list_map, max_list.
apply max_list_rec_eq_foldl.
Qed.
Lemma sizeOfmTapes_upperBound (sig : Type) (n : nat) (tps : tapes sig n) :
forall t, Vector.In t tps -> sizeOfTape t <= sizeOfmTapes tps.
Proof. intros. rewrite sizeOfmTapes_max_list_map. apply max_list_map_ge. now apply vector_to_list_In. Qed.
From Undecidability Require Import L.Prelim.MoreList.
Lemma max_list_sumn l : max_list l <= sumn l.
Proof.
unfold max_list.
induction l;cbn. 2:rewrite max_list_rec_max'. all:nia.
Qed.
Lemma right_sizeOfTape sig' (t:tape sig') :
length (right t) <= sizeOfTape t.
Proof.
destruct t;cbn. all:autorewrite with list;cbn. all:nia.
Qed.
Lemma length_tape_local_right sig' (t:tape sig') :
length (tape_local (tape_move_right t)) <= sizeOfTape t.
Proof.
destruct t;cbn. 1-3:nia. rewrite tape_local_move_right'. autorewrite with list;cbn. all:nia.
Qed.
Lemma size_list X sigX (cX: codable sigX X) (l:list X) :
size l = sumn (map size l) + length l + 1.
Proof.
unfold size. cbn. rewrite encode_list_concat.
rewrite app_length, length_concat, map_map. cbn.
change S with (fun x => 1 + x). rewrite sumn_map_add,sumn_map_c. setoid_rewrite map_length.
cbn. nia.
Qed.
Lemma destruct_vector1 (X : Type) (v : Vector.t X 1) :
exists x, v = [| x |].
Proof. destruct_vector. eauto. Qed.