From 31cb2f0b374657eb5acb95708443e2c1b8481891 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 12 Jun 2012 09:46:36 +0000
Subject: [PATCH] several changes

---
 matita/matita/lib/turing/mono.ma              | 35 ++++++++++++
 .../matita/lib/turing/universal/move_tape.ma  |  7 ---
 .../matita/lib/turing/universal/normalTM.ma   | 10 ++--
 matita/matita/lib/turing/universal/tuples.ma  |  4 +-
 .../matita/lib/turing/universal/uni_step.ma   | 16 +++---
 .../matita/lib/turing/universal/universal.ma  | 55 ++++++-------------
 6 files changed, 68 insertions(+), 59 deletions(-)

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index e559c88db..8ac107226 100644
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -261,6 +261,41 @@ definition accRealize ≝ λsig.λM:TM sig.λacc:states sig M.λRtrue,Rfalse.
 notation "M ⊨ [q: R1,R2]" non associative with precedence 45 for @{ 'cmodels $M $q $R1 $R2}.
 interpretation "conditional realizability" 'cmodels M q R1 R2 = (accRealize ? M q R1 R2).
 
+(******************************** monotonicity ********************************)
+lemma Realize_to_Realize : ∀alpha,M,R1,R2.
+  R1 ⊆ R2 → Realize alpha M R1 → Realize alpha M R2.
+#alpha #M #R1 #R2 #Himpl #HR1 #intape
+cases (HR1 intape) -HR1 #k * #outc * #Hloop #HR1
+@(ex_intro ?? k) @(ex_intro ?? outc) % /2/
+qed.
+
+lemma WRealize_to_WRealize: ∀sig,M,R1,R2.
+  R1 ⊆ R2 → WRealize sig M R1 → WRealize ? M R2.
+#alpha #M #R1 #R2 #Hsub #HR1 #intape #i #outc #Hloop
+@Hsub @(HR1 … i) @Hloop
+qed.
+
+lemma acc_Realize_to_acc_Realize: ∀sig,M.∀q:states sig M.∀R1,R2,R3,R4. 
+  R1 ⊆ R3 → R2 ⊆ R4 → M ⊨ [q:R1,R2] → M ⊨ [q:R3,R4].
+#alpha #M #q #R1 #R2 #R3 #R4 #Hsub13 #Hsub24 #HRa #intape
+cases (HRa intape) -HRa #k * #outc * * #Hloop #HRtrue #HRfalse 
+@(ex_intro ?? k) @(ex_intro ?? outc) % 
+  [ % [@Hloop] #Hq @Hsub13 @HRtrue // | #Hq @Hsub24 @HRfalse //]
+qed.
+
+(**************************** A canonical relation ****************************)
+
+definition R_TM ≝ λsig.λM:TM sig.λq.λt1,t2.
+∃i,outc.
+  loopM ? M i (mk_config ?? q t1) = Some ? outc ∧ 
+  t2 = (ctape ?? outc).
+  
+lemma R_TM_to_R: ∀sig,M,R. ∀t1,t2. 
+  M ⊫ R → R_TM ? M (start sig M) t1 t2 → R t1 t2.
+#sig #M #R #t1 #t2 whd in ⊢ (%→?); #HMR * #i * #outc *
+#Hloop #Ht2 >Ht2 @(HMR … Hloop)
+qed.
+
 (******************************** NOP Machine *********************************)
 
 (* NO OPERATION
diff --git a/matita/matita/lib/turing/universal/move_tape.ma b/matita/matita/lib/turing/universal/move_tape.ma
index ecc9fa208..ab16d56c7 100644
--- a/matita/matita/lib/turing/universal/move_tape.ma
+++ b/matita/matita/lib/turing/universal/move_tape.ma
@@ -626,13 +626,6 @@ cases (Hconcrete … Htable ? Ht1) //
       ] ] ] 
 | #x #Hx @Hbits @memb_append_l1 @Hx ]
 qed. 
-  
-lemma Realize_to_Realize : 
-  ∀alpha,M,R1,R2.(∀t1,t2.R1 t1 t2 → R2 t1 t2) → Realize alpha M R1 → Realize alpha M R2.
-#alpha #M #R1 #R2 #Himpl #HR1 #intape
-cases (HR1 intape) -HR1 #k * #outc * #Hloop #HR1
-@(ex_intro ?? k) @(ex_intro ?? outc) % /2/
-qed.
 
 lemma sem_move_tape_l_abstract : Realize … move_tape_l R_move_tape_l_abstract.
 @(Realize_to_Realize … mtl_concrete_to_abstract) //
diff --git a/matita/matita/lib/turing/universal/normalTM.ma b/matita/matita/lib/turing/universal/normalTM.ma
index 686b91099..370c9476e 100644
--- a/matita/matita/lib/turing/universal/normalTM.ma
+++ b/matita/matita/lib/turing/universal/normalTM.ma
@@ -89,21 +89,21 @@ definition nconfig ≝ λn. config FinBool (initN n).
 
 (******************************** tuples **************************************)
 
-(* By general results on FinSets we know that there is every function f between
-two finite sets A and B can be described by means of a finite graph of pairs
+(* By general results on FinSets we know that every function f between two 
+finite sets A and B can be described by means of a finite graph of pairs
 〈a,f a〉. Hence, the transition function of a normal turing machine can be
 described by a finite set of tuples 〈i,c〉,〈j,action〉〉 of the following type:
   (Nat_to n × (option FinBool)) × (Nat_to n × (option (FinBool × move))).  
-Unfortunately this description is not suitable for an Universal Machine, since
+Unfortunately this description is not suitable for a Universal Machine, since
 such a machine must work with a fixed alphabet, while the size on n is unknown.
 Hence, we must pass from natural numbers to a representation for them on a 
 finitary, e.g. binary, alphabet. In general, we shall associate
-to a pair 〈〈i,c〉,〈j,action〉〉 a tuples with the following syntactical structure
+to a pair 〈〈i,c〉,〈j,action〉〉 a tuple with the following syntactical structure
            |w_ix,w_jy,z
 where 
 1. "|" and "," are special characters used as delimiters;
 2. w_i and w_j are list of booleans representing the states $i$ and $j$; 
-3. x is special symbol null if C=None and is a if c=Some a
+3. x is special symbol null if c=None and is a if c=Some a
 4. y and z are both null if action = None, and are equal to b,m' if 
    action = Some b,m; 
 5. finally, m' = 0 if m = L, m' = 1 if m=R and m' = null if m = N
diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma
index 6e09b9d52..5f743e2c8 100644
--- a/matita/matita/lib/turing/universal/tuples.ma
+++ b/matita/matita/lib/turing/universal/tuples.ma
@@ -124,8 +124,8 @@ qed.
 
 lemma trans_to_match:
   ∀n.∀h.∀trans: trans_source n → trans_target n.
-  ∀inp,outp,qin,cin,qout,cout,mv. trans inp = outp →
-  tuple_encoding n h 〈inp,outp〉 = mk_tuple qin cin qout cout mv →
+  ∀s,t,qin,cin,qout,cout,mv. trans s = t →
+  tuple_encoding n h 〈s,t〉 = mk_tuple qin cin qout cout mv →
   match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_list n h (graph_enum ?? trans))).
 #n #h #trans #inp #outp #qin #cin #qout #cout #mv #Htrans #Htuple 
 @(tuple_to_match … (refl…)) <Htuple @mem_map_forward 
diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma
index 395decac2..39b05addf 100644
--- a/matita/matita/lib/turing/universal/uni_step.ma
+++ b/matita/matita/lib/turing/universal/uni_step.ma
@@ -240,7 +240,7 @@ cases HR -HR
   ]
 qed. *)
 
-definition exec_move ≝ 
+definition exec_action ≝ 
   seq ? init_copy
     (seq ? copy
       (seq ? (move_r …) move_tape)).
@@ -255,7 +255,7 @@ definition map_move ≝
        mv ≠ null → c1 ≠ null
      dal fatto che c1 e mv sono contenuti nella table
  *)
-definition R_exec_move ≝ λt1,t2.
+definition R_exec_action ≝ λt1,t2.
   ∀n,curconfig,ls,rs,c0,c1,s0,s1,table1,newconfig,mv,table2.
   table_TM n (table1@〈comma,false〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2) → 
   no_marks curconfig → only_bits (curconfig@[〈s0,false〉]) → 
@@ -329,7 +329,7 @@ qed.
 
 *)
 
-lemma sem_exec_move : Realize ? exec_move R_exec_move.
+lemma sem_exec_action : Realize ? exec_action R_exec_action.
 #intape
 cases (sem_seq … sem_init_copy
         (sem_seq … sem_copy
@@ -451,7 +451,7 @@ if is_false(current) (* current state is not final *)
     match_tuple;
     if is_marked(current) = false (* match ok *)
       then 
-           exec_move
+           exec_action
            move_r;
       else sink;
    else nop;
@@ -462,7 +462,7 @@ definition uni_step ≝
     (single_finalTM ? (seq ? init_match
       (seq ? match_tuple
         (ifTM ? (test_char ? (λc.¬is_marked ? c))
-          (seq ? exec_move (move_r …))
+          (seq ? exec_action (move_r …))
           (nop ?) (* sink *)
           tc_true))))
     (nop ?)
@@ -489,14 +489,16 @@ definition R_uni_step_false ≝ λt1,t2.
   
 axiom sem_match_tuple : Realize ? match_tuple R_match_tuple.
 
+definition us_acc : states ? uni_step ≝ (inr … (inl … (inr … start_nop))).
+
 lemma sem_uni_step :
-  accRealize ? uni_step (inr … (inl … (inr … start_nop)))
+  accRealize ? uni_step us_acc
      R_uni_step_true R_uni_step_false. 
 @(acc_sem_if_app STape … (sem_test_char ? (λc:STape.\fst c == bit false))
    (sem_seq … sem_init_match      
      (sem_seq … sem_match_tuple        
        (sem_if … (* ????????? (sem_test_char …  (λc.¬is_marked FSUnialpha c)) *)
-          (sem_seq … sem_exec_move (sem_move_r …))
+          (sem_seq … sem_exec_action (sem_move_r …))
           (sem_nop …))))
    (sem_nop …)
    …)
diff --git a/matita/matita/lib/turing/universal/universal.ma b/matita/matita/lib/turing/universal/universal.ma
index 3350b0965..3ed3015be 100644
--- a/matita/matita/lib/turing/universal/universal.ma
+++ b/matita/matita/lib/turing/universal/universal.ma
@@ -121,18 +121,9 @@ definition high_move ≝ λc,mv.
   | _ ⇒ None ?
   ].
 
-(* lemma high_of_lift ≝ ∀ls,c,rs.
-  high_tape ls c rs = *)
-
 definition map_move ≝ 
   λc,mv.match c with [ null ⇒ None ? | _ ⇒ Some ? 〈c,false,move_of_unialpha mv〉 ].
 
-(* axiom high_tape_move : ∀t1,ls,c,rs, c1,mv.
-  legal_tape ls c rs →
-  t1 = lift_tape ls c rs →
-  high_tape_from_tape (tape_move STape t1 (map_move c1 mv)) =
-    tape_move FinBool (high_tape_from_tape t1) (high_move c1 mv). *)
-
 definition low_step_R_true ≝ λt1,t2.
   ∀M:normalTM.
   ∀c: nconfig (no_states M). 
@@ -281,7 +272,7 @@ midtape STape (〈grid,false〉::ls)
   ]
 qed.
 
-lemma unistep_to_low_step: ∀t1,t2.
+lemma unistep_true_to_low_step: ∀t1,t2.
   R_uni_step_true t1 t2 → low_step_R_true t1 t2.
 #t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step * #n #posn #t #h * #qin #tape #eqt1
 cases (low_config_eq … eqt1) 
@@ -324,41 +315,38 @@ lapply (Huni_step n table q_low_hd (\fst qout_low_hd)
     ]
   ]
 qed.
-    
+
 definition low_step_R_false ≝ λt1,t2.
   ∀M:normalTM.
   ∀c: nconfig (no_states M).  
     t1 = low_config M c → halt ? M (cstate … c) = true  ∧ t1 = t2.
 
+lemma unistep_false_to_low_step: ∀t1,t2.
+  R_uni_step_false t1 t2 → low_step_R_false t1 t2.
+#t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step * #n #posn #t #h * #qin #tape #eqt1
+cases (low_config_eq … eqt1) #low_left * #low_right * #table * #q_low_hd * #q_low_tl * #current_low
+***** #_ #_ #_ #Hqin #_ #Ht1 whd in match (halt ???);
+cases (Huni_step (h qin) ?) [/2/] >Ht1 whd in ⊢ (??%?); @eq_f
+normalize in Hqin; destruct (Hqin) %
+qed.
+
 definition low_R ≝ λM,qstart,R,t1,t2.
     ∀tape1. t1 = low_config M (mk_config ?? qstart tape1) → 
     ∃q,tape2.R tape1 tape2 ∧
     halt ? M q = true ∧ t2 = low_config M (mk_config ?? q tape2).
 
-definition R_TM ≝ λsig.λM:TM sig.λq.λt1,t2.
-∃i,outc.
-  loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (mk_config ?? q t1) = Some ? outc ∧ 
-  t2 = (ctape ?? outc).
-
-(*
-definition universal_R ≝ λM,R,t1,t2. 
-    Realize ? M R →    
-    ∀tape1,tape2.
-    R tape1 tape 2 ∧
-    t1 = low_config M (initc ? M tape1) ∧
-    ∃q.halt ? M q = true → t2 = low_config M (mk_config ?? q tape2).*)
-
-axiom uni_step: TM STape.
-axiom us_acc: states ? uni_step.
-
-axiom sem_uni_step: accRealize ? uni_step us_acc low_step_R_true low_step_R_false.
+lemma sem_uni_step1: 
+  uni_step ⊨ [us_acc: low_step_R_true, low_step_R_false].
+@(acc_Realize_to_acc_Realize … sem_uni_step) 
+  [@unistep_true_to_low_step | @unistep_false_to_low_step ]
+qed. 
 
 definition universalTM ≝ whileTM ? uni_step us_acc.
 
 theorem sem_universal: ∀M:normalTM. ∀qstart.
   WRealize ? universalTM (low_R M qstart (R_TM FinBool M qstart)).
 #M #q #intape #i #outc #Hloop
-lapply (sem_while … sem_uni_step intape i outc Hloop)
+lapply (sem_while … sem_uni_step1 intape i outc Hloop)
   [@daemon] -Hloop 
 * #ta * #Hstar generalize in match q; -q 
 @(star_ind_l ??????? Hstar)
@@ -393,15 +381,6 @@ lapply (sem_while … sem_uni_step intape i outc Hloop)
   ]
 qed.
 
-lemma R_TM_to_R: ∀sig,M,R. ∀t1,t2. 
-  WRealize sig M R → R_TM ? M (start ? M) t1 t2 → R t1 t2.
-#sig #M #R #t1 #t2 whd in ⊢ (%→?); #HMR * #i * #outc *
-#Hloop #Ht2 >Ht2 @(HMR … Hloop)
-qed.
-
-axiom WRealize_to_WRealize: ∀sig,M,R1,R2.
-  (∀t1,t2.R1 t1 t2 → R2 t1 t2) → WRealize sig M R1 → WRealize ? M R2.
-
 theorem sem_universal2: ∀M:normalTM. ∀R.
   WRealize ? M R → WRealize ? universalTM (low_R M (start ? M) R).
 #M #R #HMR lapply (sem_universal … M (start ? M)) @WRealize_to_WRealize
-- 
2.39.2