renaming: rename tape_move_mono to doAct

theories/TM/Basic/Mono.v

@@ -47,7 +47,7 @@ Section DoAct.
   Definition DoAct : pTM sig unit 1 := (DoAct_TM; fun _ => tt).
 
   Definition DoAct_Rel : pRel sig unit 1 :=
-    Mk_R_p (ignoreParam (fun t t' => t' = tape_move_mono t act)).
+    Mk_R_p (ignoreParam (fun t t' => t' = doAct t act)).
 
   Lemma DoAct_Sem : DoAct ⊨c(1) DoAct_Rel.
   Proof. intros t. destruct_tapes. cbn. unfold initc; cbn. eexists (mk_mconfig _ _); cbn; eauto. Qed.

theories/TM/Combinators/Mirror.v

@@ -56,23 +56,21 @@ Section Mirror.
     current_chars (mirror_tapes t) = current_chars t.
   Proof. apply Vector.eq_nth_iff; intros i ? <-. autounfold with tape. now simpl_tape. Qed.
 
-  Lemma tape_move_mono_mirror_act (t : tape sig) (act : option sig * move) :
-    tape_move_mono (mirror_tape t) act = mirror_tape (tape_move_mono t (mirror_act act)).
+  Lemma doAct_mirror (t : tape sig) (act : option sig * move) :
+    doAct (mirror_tape t) act = mirror_tape (doAct t (mirror_act act)).
   Proof. now destruct act as [ [ s | ] [ | | ]]; cbn; simpl_tape. Qed.
 
-  Lemma tape_move_multi_mirror_acts (t : tapes sig n) (acts : Vector.t (option sig * move) n) :
-    tape_move_multi (mirror_tapes t) acts = mirror_tapes (tape_move_multi t (mirror_acts acts)).
-  Proof.
-    apply Vector.eq_nth_iff; intros i ? <-. unfold tape_move_multi, mirror_acts, mirror_tapes. simpl_tape. apply tape_move_mono_mirror_act.
-  Qed.
+  Lemma doAct_mirror_multi (t : tapes sig n) (acts : Vector.t (option sig * move) n) :
+    doAct_multi (mirror_tapes t) acts = mirror_tapes (doAct_multi t (mirror_acts acts)).
+  Proof. apply Vector.eq_nth_iff; intros i ? <-. unfold doAct_multi, mirror_acts, mirror_tapes. simpl_tape. apply doAct_mirror. Qed.
 
   Lemma mirror_step c :
     step (M := projT1 pM) (mirrorConf c) = mirrorConf (step (M := projT1 Mirror) c).
   Proof.
-    unfold step; cbn -[tape_move_multi]. unfold Mirror_trans. cbn.
+    unfold step; cbn -[doAct_multi]. unfold Mirror_trans. cbn.
     destruct c as [q t]; cbn. rewrite current_chars_mirror_tapes.
     destruct (trans (q, current_chars t)) as [q' acts].
-    unfold mirrorConf; cbn. f_equal. apply tape_move_multi_mirror_acts.
+    unfold mirrorConf; cbn. f_equal. apply doAct_mirror_multi.
   Qed.
 
   Lemma mirror_lift k c1 c2 :

theories/TM/Combinators/Switch.v

@@ -113,7 +113,7 @@ Section Switch.
     unfold lift_confL, lift_confR. cbn. unfold haltConf in Halt.
     unfold step at 1; cbn.
     rewrite Halt. f_equal.
-    apply tape_move_nop_action.
+    apply doAct_nop.
   Qed.
 
   (** The starting configuration of [Switch] corresponds to the starting configuration of [M1]. *)

theories/TM/Combinators/While.v

@@ -66,7 +66,7 @@ Section While.
   Proof.
     intros HHalt HRepeat. unfold haltConf in HHalt.
     destruct c as [q t]; cbn in *.
-    unfold step. cbn -[tape_move_multi] in *. rewrite HHalt. unfold initc. f_equal. apply tape_move_nop_action.
+    unfold step. cbn -[doAct_multi] in *. rewrite HHalt. unfold initc. f_equal. apply doAct_nop.
   Qed.
 
   Lemma While_split k (c1 c3 : mconfig sig (states (projT1 pM)) n) :

theories/TM/Compound/CopySymbols.v

@@ -42,7 +42,7 @@ Section CopySymbols.
              tout[@Fin1] = tape_write tin[@Fin1] (Some x) /\
              yout = Some tt (* break *)
         else tout[@Fin0] = tape_move_right tin[@Fin0] /\
-             tout[@Fin1] = tape_move_mono tin[@Fin1] (Some x, R) /\
+             tout[@Fin1] = doAct tin[@Fin1] (Some x, R) /\
              yout = None (* continue *)
       | _ => tout = tin /\
             yout = Some tt
@@ -83,7 +83,7 @@ Section CopySymbols.
     | Some s =>
       if f s
       then (fst tin, tape_write (snd tin) (Some s))
-      else CopySymbols_Fun (tape_move_right (fst tin), tape_move_mono (snd tin) (Some s, R))
+      else CopySymbols_Fun (tape_move_right (fst tin), doAct (snd tin) (Some s, R))
     | _ => tin
     end.
   Proof.
@@ -98,7 +98,7 @@ Section CopySymbols.
   Lemma CopySymbols_false s t1 t2 :
     current t1 = Some s ->
     f s = false ->
-    CopySymbols_Fun (t1, t2) = CopySymbols_Fun (tape_move_right t1, tape_move_mono t2 (Some s, R)).
+    CopySymbols_Fun (t1, t2) = CopySymbols_Fun (tape_move_right t1, doAct t2 (Some s, R)).
   Proof. intros HCurrent Hs. rewrite CopySymbols_Fun_equation. cbn. now rewrite HCurrent, Hs. Qed.
 
   Lemma CopySymbols_true s t1 t2 :
@@ -186,7 +186,7 @@ Section CopySymbols.
     | Some s =>
       if f s
       then (fst tin, tape_write (snd tin) (Some s))
-      else CopySymbols_L_Fun (tape_move_left (fst tin), tape_move_mono (snd tin) (Some s, L))
+      else CopySymbols_L_Fun (tape_move_left (fst tin), doAct (snd tin) (Some s, L))
     | _ => tin
     end.
   Proof.

theories/TM/Compound/MoveToSymbol.v

@@ -44,7 +44,7 @@ Section MoveToSymbol.
       match current t1 with
       | Some s => if (f s)
                  then tape_write t1 (Some (g s))
-                 else tape_move_mono t1 (Some (g s), R)
+                 else doAct t1 (Some (g s), R)
       | _ => t1
       end.
 
@@ -95,7 +95,7 @@ Section MoveToSymbol.
     match current t with
     | Some m => if f m
                then tape_write t (Some (g m))
-               else MoveToSymbol_Fun (tape_move_mono t (Some (g m), R))
+               else MoveToSymbol_Fun (doAct t (Some (g m), R))
     | _ => t
     end.
   Proof.
@@ -128,7 +128,7 @@ Section MoveToSymbol.
   Lemma MoveToSymbol_Step_false t x :
     current t = Some x ->
     f x = false ->
-    MoveToSymbol_Step_Fun t = tape_move_mono t (Some (g x), R).
+    MoveToSymbol_Step_Fun t = doAct t (Some (g x), R).
   Proof.
     intros H1 H2. unfold MoveToSymbol_Step_Fun. destruct t; cbn in *; inv H1. rewrite H2. auto.
   Qed.
@@ -144,7 +144,7 @@ Section MoveToSymbol.
   Lemma MoveToSymbol_skip t s :
     current t = Some s ->
     f s = false ->
-    MoveToSymbol_Fun (tape_move_mono t (Some (g s), R)) = MoveToSymbol_Fun t.
+    MoveToSymbol_Fun (doAct t (Some (g s), R)) = MoveToSymbol_Fun t.
   Proof. intros H1 H2. cbn. symmetry. rewrite MoveToSymbol_Fun_equation. cbn. now rewrite H1, H2. Qed.
 
   Definition MoveToSymbol_Rel : Rel (tapes sig 1) (unit * tapes sig 1) :=
@@ -178,7 +178,7 @@ Section MoveToSymbol.
 
   Function MoveToSymbol_steps (t : tape sig) { measure rlength t } : nat :=
     match current t with
-    | Some m => if f m then 4 else 4 + (MoveToSymbol_steps (tape_move_mono t (Some (g m), R)))
+    | Some m => if f m then 4 else 4 + (MoveToSymbol_steps (doAct t (Some (g m), R)))
     | _ => 4
     end.
   Proof.
@@ -206,7 +206,7 @@ Section MoveToSymbol.
           * rewrite MoveToSymbol_steps_equation in HT. rewrite E in HT. omega.
         + destruct (current tin[@Fin0]) eqn:E.
           * destruct (f e) eqn:Ef; inv H0. rewrite MoveToSymbol_steps_equation in HT. rewrite E, Ef in HT.
-            exists (MoveToSymbol_steps (tape_move_mono tin[@Fin0] (Some (g e), R))). cbn.
+            exists (MoveToSymbol_steps (doAct tin[@Fin0] (Some (g e), R))). cbn.
             split.
             -- unfold MoveToSymbol_Step_Fun. rewrite E, Ef. cbn. reflexivity.
             -- rewrite <- HT. cbn. omega.
@@ -227,7 +227,7 @@ Section MoveToSymbol.
     | Some s  =>
       if f s
       then tape_write t (Some (g s))
-      else MoveToSymbol_L_Fun (tape_move_mono t (Some (g s), L))
+      else MoveToSymbol_L_Fun (doAct t (Some (g s), L))
     | _ => t
     end.
   Proof. intros. unfold llength. cbn. simpl_tape. destruct t; cbn in *; inv teq. omega. Qed.
@@ -269,7 +269,7 @@ Section MoveToSymbol.
 
   Function MoveToSymbol_L_steps (t : tape sig) { measure llength t } : nat :=
     match current t with
-    | Some s => if f s then 4 else 4 + (MoveToSymbol_L_steps (tape_move_mono t (Some (g s), L)))
+    | Some s => if f s then 4 else 4 + (MoveToSymbol_L_steps (doAct t (Some (g s), L)))
     | _ => 4
     end.
   Proof. intros. unfold llength. cbn. simpl_tape. destruct t; cbn in *; inv teq. omega. Qed.

theories/TM/Compound/WriteString.v

@@ -24,7 +24,7 @@ Section Write_String.
     match str with
     | nil => t
     | [x] => tape_write t (Some x)
-    | x :: str' => WriteString_Fun (tape_move_mono t (Some x, D)) str'
+    | x :: str' => WriteString_Fun (doAct t (Some x, D)) str'
     end.
 
   Lemma Write_String_nil (sig' : Type) (t : tape sig') :

theories/TM/Lifting/LiftAlphabet.v

@@ -134,13 +134,13 @@ Section LiftAlphabet.
     fun c => mk_mconfig (cstate c) (injectTapes Retr_f (ctapes c)).
 *)
 
-  Lemma tape_move_mono_surject :
+  Lemma doAct_surject :
     forall (tape : tape tau) (act : option sig * move) (d : sig),
-      tape_move_mono (surjectTape Retr_g d tape) act =
-      surjectTape Retr_g d (tape_move_mono tape (map_act Retr_f act)).
+      doAct (surjectTape Retr_g d tape) act =
+      surjectTape Retr_g d (doAct tape (map_act Retr_f act)).
   Proof.
     intros tape. intros (w,m) d; cbn.
-    unfold surjectTape, tape_move_mono, tape_move, tape_write, surject; cbn.
+    unfold surjectTape, doAct, tape_move, tape_write, surject; cbn.
     destruct tape, m, w; cbn; f_equal; try retract_adjoint; auto.
     - destruct l; cbn; f_equal; now retract_adjoint.
     - destruct l; cbn; f_equal; now retract_adjoint.
@@ -159,10 +159,10 @@ Section LiftAlphabet.
     step (M := projT1 pMSig) (surjectConf c) = surjectConf (step (M := LiftAlphabet_TM) c).
   Proof.
     unfold surjectConf. destruct c as [q t]. cbn in *.
-    unfold step. cbn -[tape_move_multi].
+    unfold step. cbn -[doAct_multi].
     rewrite current_chars_surjectTapes.
     destruct (trans (q, surjectReadSymbols (current_chars t))) eqn:E. cbn.
-    f_equal. unfold tape_move_multi, surjectTapes. apply Vector.eq_nth_iff; intros i ? <-. simpl_tape. apply tape_move_mono_surject.
+    f_equal. unfold doAct_multi, surjectTapes. apply Vector.eq_nth_iff; intros i ? <-. simpl_tape. apply doAct_surject.
   Qed.
 
   Lemma LiftAlphabet_lift (c1 c2 : mconfig tau (states LiftAlphabet_TM) n) (k : nat) :

theories/TM/Lifting/LiftTapes.v

@@ -186,10 +186,10 @@ Section LiftNM.
     current_chars (select I t) = select I (current_chars t).
   Proof. unfold current_chars, select. apply Vector.eq_nth_iff; intros i ? <-. now simpl_tape. Qed.
 
-  Lemma tape_move_multi_select (t : tapes sig n) act :
-    tape_move_multi (select I t) act = select I (tape_move_multi t (fill_default I (None, N) act)).
+  Lemma doAct_select (t : tapes sig n) act :
+    doAct_multi (select I t) act = select I (doAct_multi t (fill_default I (None, N) act)).
   Proof.
-    unfold tape_move_multi, select. apply Vector.eq_nth_iff; intros i ? <-. simpl_tape.
+    unfold doAct_multi, select. apply Vector.eq_nth_iff; intros i ? <-. simpl_tape.
     unfold fill_default. f_equal. symmetry. now apply fill_correct_nth.
   Qed.
 
@@ -198,10 +198,10 @@ Section LiftNM.
   Proof.
     unfold selectConf. unfold step; cbn.
     destruct c1 as [q t] eqn:E1.
-    unfold step in *. cbn -[current_chars tape_move_multi] in *.
+    unfold step in *. cbn -[current_chars doAct_multi] in *.
     rewrite current_chars_select.
     destruct (trans (q, select I (current_chars t))) as (q', act) eqn:E; cbn.
-    f_equal. apply tape_move_multi_select.
+    f_equal. apply doAct_select.
   Qed.
 
   Lemma LiftTapes_lift (c1 c2 : mconfig sig (states LiftTapes_TM) n) (k : nat) :

theories/TM/TM.v

@@ -184,12 +184,12 @@ Section Fix_Sigma.
     end.
 
   (** A single step of the machine *)
-  Definition tape_move_mono (t : tape) (mv : option sig * move) :=
+  Definition doAct (t : tape) (mv : option sig * move) :=
     tape_move (tape_write t (fst mv)) (snd mv).
 
   (** One step on each tape *)
-  Definition tape_move_multi (n : nat) (ts : tapes n) (actions : Vector.t (option sig * move) n) :=
-    Vector.map2 tape_move_mono ts actions.
+  Definition doAct_multi (n : nat) (ts : tapes n) (actions : Vector.t (option sig * move) n) :=
+    Vector.map2 doAct ts actions.
 
   (** Read characters on all tapes *)
   Definition current_chars (n : nat) (tapes : tapes n) := Vector.map current tapes.
@@ -268,10 +268,10 @@ Section Nop_Action.
 
   Definition nop_action := Vector.const (@None sig, N) n.
 
-  Lemma tape_move_nop_action tapes :
-    tape_move_multi tapes nop_action = tapes.
+  Lemma doAct_nop tapes :
+    doAct_multi tapes nop_action = tapes.
   Proof.
-    unfold nop_action, tape_move_multi.
+    unfold nop_action, doAct_multi.
     apply Vector.eq_nth_iff; intros ? i <-.
     erewrite Vector.nth_map2; eauto.
     rewrite Vector.const_nth.
@@ -731,7 +731,7 @@ Section Semantics.
   Definition step {n} (M:mTM n) : mconfig (states M) n -> mconfig (states M) n :=
     fun c =>
       let (news,actions) := trans (cstate c, current_chars  (ctapes c)) in 
-      mk_mconfig news (tape_move_multi (ctapes c) actions).
+      mk_mconfig news (doAct_multi (ctapes c) actions).
 
   Definition haltConf {n} (M : mTM n) : mconfig (states M) n -> bool := fun c => halt (cstate c).