From c62c83d3be87bfb0744902a5998e5708bc698cd7 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 1 Jun 2012 12:53:28 +0000
Subject: [PATCH] Ci siamo quasi

---
 .../lib/turing/universal/trans_to_tuples.ma   |  97 +++++-
 .../matita/lib/turing/universal/universal.ma  | 286 ++++++++++++++++--
 2 files changed, 353 insertions(+), 30 deletions(-)

diff --git a/matita/matita/lib/turing/universal/trans_to_tuples.ma b/matita/matita/lib/turing/universal/trans_to_tuples.ma
index 8b92473ce..09171b120 100644
--- a/matita/matita/lib/turing/universal/trans_to_tuples.ma
+++ b/matita/matita/lib/turing/universal/trans_to_tuples.ma
@@ -12,7 +12,6 @@
 
 
 include "turing/universal/tuples.ma".
-include "basics/fun_graph.ma".
 
 (* p < n is represented with a list of bits of lenght n with the
  p-th bit from left set to 1 *)
@@ -92,21 +91,23 @@ qed.
 definition tuple_type ≝ λn.
  (Nat_to n × (option FinBool)) × (Nat_to n × (option (FinBool × move))).  
 
-definition tuple_of_pair ≝ λn.λh:Nat_to n→bool. 
-  λp:tuple_type n.
-  let 〈inp,outp〉 ≝ p in
-  let 〈q,a〉 ≝ inp in
-  let cin ≝ match a with [ None ⇒ null | Some b ⇒ bit b ] in
-  let 〈qn,action〉 ≝ outp in
-  let 〈cout,mv〉 ≝ 
-    match action with 
+definition low_action ≝ λaction. 
+  match action with 
     [ None ⇒ 〈null,null〉
     | Some act ⇒ let 〈na,m〉 ≝ act in 
       match m with 
       [ R ⇒ 〈bit na,bit true〉
       | L ⇒ 〈bit na,bit false〉
       | N ⇒ 〈bit na,null〉]
-    ] in
+    ].
+
+definition tuple_of_pair ≝ λn.λh:Nat_to n→bool. 
+  λp:tuple_type n.
+  let 〈inp,outp〉 ≝ p in
+  let 〈q,a〉 ≝ inp in
+  let cin ≝ match a with [ None ⇒ null | Some b ⇒ bit b ] in
+  let 〈qn,action〉 ≝ outp in
+  let 〈cout,mv〉 ≝ low_action action in
   let qin ≝ m_bits_of_state n h q in
   let qout ≝ m_bits_of_state n h qn in
   mk_tuple qin 〈cin,false〉 qout 〈cout,false〉 〈mv,false〉.
@@ -209,6 +210,23 @@ lemma flatten_to_mem: ∀A,n,l,l1,l2.∀a:list A. 0 < n →
   ]
 qed.
 
+lemma tuple_to_match:  ∀n,h,l,qin,cin,qout,cout,mv,p.
+  p = mk_tuple qin cin qout cout mv 
+  → mem ? p (tuples_of_pairs n h l) →
+  match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h l)).
+#n #h #l #qin #cin #qout #cout #mv #p
+#Hp elim l 
+  [whd in ⊢ (%→?); @False_ind
+  |#p1 #tl #Hind *
+    [#H whd in match (tuples_of_pairs ???);
+     <H >Hp @mit_hd //
+    |#H whd in match (tuples_of_pairs ???); 
+     cases (is_tuple n h p1) #qin1 * #cin1 * #qout1 * #cout1 * #mv1
+     * #_ #Htuplep1 >Htuplep1 @mit_tl // @Hind //
+    ]
+  ]
+qed.
+
 axiom match_decomp: ∀n,l,qin,cin,qout,cout,mv.
   match_in_table (S n) qin cin qout cout mv l →
   ∃l1,l2. l = l1@(mk_tuple qin cin qout cout mv)@l2 ∧
@@ -310,3 +328,62 @@ cases (match_to_pair … Hmatch) -Hmatch * #s #t * #Heq #Hmem
 @mem_to_memb @Hmem 
 qed.
 
+(* da spistare *)
+lemma mem_map_forward: ∀A,B.∀f:A→B.∀a,l. 
+  mem A a l → mem B (f a) (map ?? f l).
+ #A #B #f #a #l elim l
+  [normalize @False_ind
+  |#b #tl #Hind * 
+    [#eqab <eqab normalize %1 % |#memtl normalize %2 @Hind @memtl]
+  ]
+qed.
+
+lemma memb_to_mem: ∀S:DeqSet.∀l,a. memb S a l =true → mem S a l.
+#S #l #a elim l 
+  [normalize #H destruct
+  |#b #tl #Hind #mema cases (orb_true_l … mema) 
+    [#eqab >(\P eqab) %1 % |#memtl %2 @Hind @memtl]
+  ]
+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_of_pair n h 〈inp,outp〉 = mk_tuple qin cin qout cout mv →
+  match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs 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 
+@(memb_to_mem (FinProd (trans_source n) (trans_target n)))
+@graph_enum_complete //
+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_of_pair n h 〈inp,outp〉 = mk_tuple qin cin qout cout mv →
+  match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs 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 
+@(memb_to_mem (FinProd (trans_source n) (trans_target n)))
+@graph_enum_complete //
+qed. *)
+
+
+(*
+lemma trans_to_match:
+  ∀n.∀h.∀trans: trans_source n → trans_target n.
+  ∀q,a,qn,action,qin,cin. trans 〈q,a〉 = 〈qn,action〉 →
+  qin = m_bits_of_state n h q →
+  cin = match a with [ None ⇒ null | Some b ⇒ bit b ] →
+  ∃qout,cout,mv. 
+  qout = m_bits_of_state n h qn ∧
+  (〈cout,mv〉 = match action with 
+    [ None ⇒ 〈null,null〉
+    | Some act ⇒ let 〈na,m〉 ≝ act in 
+      match m with [ R ⇒ 〈bit na,bit true〉 | L ⇒ 〈bit na,bit false〉 | N ⇒ 〈bit na,null〉] ]) ∧ 
+  match_in_table (S n) qin 〈cin,false〉 qout 〈cout,false〉 〈mv,false〉 (flatten ? (tuples_of_pairs n h (graph_enum ?? trans))).
+#n #h #trans #q #a #qn #action #qin #cin #Htrans #Hqin #Hcin
+@(ex_intro … (m_bits_of_state n h qn))
+@(ex_intro … ?) [|@(ex_intro ?) [| % [ % [% | //]]
+@(tuple_to_match … (refl…)) *)
\ No newline at end of file
diff --git a/matita/matita/lib/turing/universal/universal.ma b/matita/matita/lib/turing/universal/universal.ma
index a2f35fc78..3f8d2910c 100644
--- a/matita/matita/lib/turing/universal/universal.ma
+++ b/matita/matita/lib/turing/universal/universal.ma
@@ -66,6 +66,93 @@ lemma low_config_eq: ∀t,M,c. t = low_config M c →
 % [% [% [% [% // | // ] | // ] | // ] | >eqt //]
 qed.
 
+let rec to_bool_list (l: list (unialpha×bool)) ≝ 
+  match l with
+  [ nil ⇒ nil ?
+  | cons a tl ⇒ 
+    match \fst a with 
+    [bit b ⇒ b::to_bool_list tl
+    |_ ⇒ nil ?
+    ]
+  ].
+
+definition high_c ≝ λc:unialpha×bool.
+  match \fst c with
+  [ null ⇒ None ?
+  | bit b ⇒ Some ? b 
+  | _ ⇒ None ?].
+
+definition high_tape ≝ λls,c,rs.
+  mk_tape FinBool (to_bool_list ls) (high_c c) (to_bool_list rs).
+
+lemma high_tape_eq : ∀ls,c,rs. high_tape ls c rs =
+  mk_tape FinBool (to_bool_list ls) (high_c c) (to_bool_list rs).
+// qed.
+
+definition high_tape_from_tape ≝ λt:tape STape.
+  match t with
+  [niltape ⇒ niltape ?
+  |leftof a l ⇒ match \fst a with 
+     [bit b ⇒ leftof ? b (to_bool_list l)
+     |_ ⇒ niltape ?
+     ]
+  |rightof a r ⇒ match \fst a with 
+     [bit b ⇒ rightof ? b (to_bool_list r)
+     |_ ⇒ niltape ?
+     ]
+  |midtape l c r ⇒ high_tape l c r
+  ].
+
+lemma high_tape_of_lift : ∀ls,c,rs. legal_tape ls c rs →
+  high_tape ls c rs =
+    high_tape_from_tape (lift_tape ls c rs).
+#ls * #c #b #rs * #H cases c // 
+>high_tape_eq  
+* [ * [#H @False_ind /2/
+      | #Heq >Heq cases rs // * #a #b1 #tl 
+        whd in match (lift_tape ???); cases a // 
+      ]
+  |#Heq >Heq cases ls // * #a #b1 #tl 
+        whd in match (lift_tape ???); cases a //
+  ]
+qed.
+
+lemma bool_embedding: ∀l.
+  to_bool_list (map ?? (λb.〈bit b,false〉) l) = l.
+#l elim l // #a #tl #Hind normalize @eq_f @Hind
+qed.
+
+lemma current_embedding: ∀c.
+  high_c (〈match c with [None ⇒ null | Some b ⇒ bit b],false〉) = c.
+  * normalize // qed.
+
+lemma tape_embedding: ∀ls,c,rs.
+ high_tape 
+   (map ?? (λb.〈bit b,false〉) ls) 
+   (〈match c with [None ⇒ null | Some b ⇒ bit b],false〉)
+   (map ?? (λb.〈bit b,false〉) rs) = mk_tape ? ls c rs.
+#ls #c #rs >high_tape_eq >bool_embedding >bool_embedding
+>current_embedding %
+qed.
+
+definition high_move ≝ λc,mv.
+  match c with 
+  [ bit b ⇒ Some ? 〈b,move_of_unialpha 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). 
@@ -73,31 +160,190 @@ definition low_step_R_true ≝ λt1,t2.
     halt ? M (cstate … c) = false ∧
       t2 = low_config M (step ? M c).
 
+definition low_tape_aux : ∀M:normalTM.tape FinBool → tape STape ≝ 
+λM:normalTM.λt.
+  let current_low ≝ match current … t with 
+    [ None ⇒ None ? | Some b ⇒ Some ? 〈bit b,false〉] in
+  let low_left ≝ map … (λb.〈bit b,false〉) (left … t) in
+  let low_right ≝ map … (λb.〈bit b,false〉) (right … t) in
+  mk_tape STape low_left current_low low_right. 
+
+lemma left_of_low_tape: ∀M,t. 
+  left ? (low_tape_aux M t) = map … (λb.〈bit b,false〉) (left … t).
+#M * //
+qed. 
+
+lemma right_of_low_tape: ∀M,t. 
+  right ? (low_tape_aux M t) = map … (λb.〈bit b,false〉) (right … t).
+#M * //
+qed. 
+
+definition low_move ≝ λaction:option (bool × move).
+  match action with
+  [None ⇒ None ?
+  |Some act ⇒ Some ? (〈〈bit (\fst act),false〉,\snd act〉)].
+
+(* simulation lemma *)
+lemma low_tape_move : ∀M,action,t.
+  tape_move STape (low_tape_aux M t) (low_move action) =
+  low_tape_aux M (tape_move FinBool t action). 
+#M * // (* None *)
+* #b #mv #t cases mv cases t //
+  [#ls #c #rs cases ls //|#ls #c #rs cases rs //]
+qed.
+
+lemma left_of_lift: ∀ls,c,rs. left ? (lift_tape ls c rs) = ls.
+#ls * #c #b #rs cases c // cases ls // cases rs //
+qed.
+
+lemma right_of_lift: ∀ls,c,rs. legal_tape ls c rs →
+  right ? (lift_tape ls c rs) = rs.
+#ls * #c #b #rs * #_ cases c // cases ls cases rs // #a #tll #b #tlr
+#H @False_ind cases H [* [#H1 /2/ |#H1 destruct] |#H1 destruct]
+qed.
+
+
+lemma current_of_lift: ∀ls,c,b,rs. legal_tape ls 〈c,b〉 rs →
+  current STape (lift_tape ls 〈c,b〉 rs) =
+    match c with [null ⇒ None ? | _ ⇒ Some ? 〈c,b〉].
+#ls #c #b #rs cases c // whd in ⊢ (%→?); * #_ 
+* [* [#Hnull @False_ind /2/ | #Hls >Hls whd in ⊢ (??%%); cases rs //]
+  |#Hrs >Hrs whd in ⊢ (??%%); cases ls //]
+qed.
+
+lemma current_of_lift_None: ∀ls,c,b,rs. legal_tape ls 〈c,b〉 rs →
+  current STape (lift_tape ls 〈c,b〉 rs) = None ? →
+    c = null.
+#ls #c #b #rs #Hlegal >(current_of_lift … Hlegal) cases c normalize  
+  [#b #H destruct |// |3,4,5:#H destruct ]
+qed.
+
+lemma current_of_lift_Some: ∀ls,c,c1,rs. legal_tape ls c rs →
+  current STape (lift_tape ls c rs) = Some ? c1 →
+    c = c1.
+#ls * #c #cb #b #rs #Hlegal >(current_of_lift … Hlegal) cases c normalize 
+ [#b1 #H destruct // |#H destruct |3,4,5:#H destruct //]
+qed.
+
+lemma current_of_low_None: ∀M,t. current FinBool t = None ? → 
+  current STape (low_tape_aux M t) = None ?.
+#M #t cases t // #l #b #r whd in ⊢ ((??%?)→?); #H destruct
+qed.
+  
+lemma current_of_low_Some: ∀M,t,b. current FinBool t = Some ? b → 
+  current STape (low_tape_aux M t) = Some ? 〈bit b,false〉.
+#M #t cases t 
+  [#b whd in ⊢ ((??%?)→?); #H destruct
+  |#b #l #b1 whd in ⊢ ((??%?)→?); #H destruct
+  |#b #l #b1 whd in ⊢ ((??%?)→?); #H destruct
+  |#c #c1 #l #r whd in ⊢ ((??%?)→?); #H destruct %
+  ]
+qed.
+
+lemma current_of_low:∀M,tape,ls,c,rs. legal_tape ls c rs → 
+  lift_tape ls c rs = low_tape_aux M tape →
+  c = 〈match current … tape  with 
+       [ None ⇒ null | Some b ⇒ bit b], false〉.
+#M #tape #ls * #c #cb #rs #Hlegal #Hlift  
+cut (current ? (lift_tape ls 〈c,cb〉 rs) = current ? (low_tape_aux M tape))
+  [@eq_f @Hlift] -Hlift #Hlift
+cut (current … tape = None ? ∨ ∃b.current … tape = Some ? b)
+  [cases (current … tape) [%1 // | #b1 %2 /2/ ]] *  
+  [#Hcurrent >Hcurrent normalize
+   >(current_of_low_None …Hcurrent) in Hlift; #Hlift 
+   >(current_of_lift_None … Hlegal Hlift) 
+   @eq_f cases Hlegal * * #Hmarks #_ #_ #_ @(Hmarks 〈c,cb〉) @memb_hd
+  |* #b #Hcurrent >Hcurrent normalize
+   >(current_of_low_Some …Hcurrent) in Hlift; #Hlift 
+   @(current_of_lift_Some … Hlegal Hlift) 
+  ]
+qed.
+
+(*
+lemma current_of_low:∀M,tape,ls,c,rs. legal_tape ls c rs → 
+  lift_tape ls c rs = low_tape_aux M tape →
+  c = 〈match current … tape  with 
+       [ None ⇒ null | Some b ⇒ bit b], false〉.
+#M #tape #ls * #c #cb #rs * * #_ #H cases (orb_true_l … H)
+  [cases c [2,3,4,5: whd in ⊢ ((??%?)→?); #Hfalse destruct]
+   #b #_ #_ cases tape 
+    [whd in ⊢ ((??%%)→?); #H destruct
+    |#a #l whd in ⊢ ((??%%)→?); #H destruct 
+    |#a #l whd in ⊢ ((??%%)→?); #H destruct 
+    |#a #l #r whd in ⊢ ((??%%)→?); #H destruct //
+    ]
+  |cases c 
+    [#b whd in ⊢ ((??%?)→?); #Hfalse destruct
+    |3,4,5:whd in ⊢ ((??%?)→?); #Hfalse destruct]
+   #_ * [* [#Habs @False_ind /2/
+           |#Hls >Hls whd in ⊢ ((??%%)→?); *)
+          
+    
+(* sufficent conditions to have a low_level_config *)
+lemma is_low_config: ∀ls,c,rs,M,s,tape,qhd,q_tl,table.
+legal_tape ls c rs →
+table = flatten ? (tuples_of_pairs (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) →
+lift_tape ls c rs = low_tape_aux M tape →
+〈qhd,false〉::q_tl = m_bits_of_state (no_states M) (nhalt M) s →
+midtape STape (〈grid,false〉::ls) 
+  〈qhd,false〉 
+  (q_tl@c::〈grid,false〉::table@〈grid,false〉::rs) = 
+  low_config M (mk_config ?? s tape).
+#ls #c #rs #M #s #tape #qhd #q_tl #table #Hlegal #Htable
+#Hlift #Hstate whd in match (low_config ??); <Hstate 
+@eq_f3 
+  [@eq_f <(left_of_lift ls c rs) >Hlift //
+  | cut (∀A.∀a,b:A.∀l1,l2. a::l1 = b::l2 → a=b)
+    [#A #a #b #l1 #l2 #H destruct (H) %] #Hcut
+   @(Hcut …Hstate)
+  |@eq_f <(current_of_low … Hlegal Hlift) @eq_f @eq_f <Htable @eq_f @eq_f
+   <(right_of_lift ls c rs Hlegal) >Hlift @right_of_low_tape
+  ]
+qed.
+
 lemma unistep_to_low_step: ∀t1,t2.
   R_uni_step_true t1 t2 → low_step_R_true t1 t2.
-#t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step #M #c #eqt1
+#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
 ***** #Hlow_left #Hlow_right #Htable #Hq_low #Hcurrent_low #Ht1
-lapply (Huni_step ??????????????? Ht1)
-whd in match (low_config M c);
-
-definition R_uni_step_true ≝ λt1,t2.
-  ∀n,t0,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv.
-  table_TM (S n) (〈t0,false〉::table) → 
-  match_in_table (S n) (〈s0,false〉::curconfig) 〈c0,false〉
-    (〈s1,false〉::newconfig) 〈c1,false〉 〈mv,false〉 (〈t0,false〉::table) → 
-  legal_tape ls 〈c0,false〉 rs → 
-  t1 = midtape STape (〈grid,false〉::ls) 〈s0,false〉 
-    (curconfig@〈c0,false〉::〈grid,false〉::〈t0,false〉::table@〈grid,false〉::rs) → 
-  ∀t1'.t1' = lift_tape ls 〈c0,false〉 rs → 
-  s0 = bit false ∧
-  ∃ls1,rs1,c2.
-  (t2 = midtape STape (〈grid,false〉::ls1) 〈s1,false〉 
-    (newconfig@〈c2,false〉::〈grid,false〉::〈t0,false〉::table@〈grid,false〉::rs1) ∧
-   lift_tape ls1 〈c2,false〉 rs1 = 
-   tape_move STape t1' (map_move c1 mv) ∧ legal_tape ls1 〈c2,false〉 rs1).
-   
+letin trg ≝ (t 〈qin,current ? tape〉)
+letin qout_low ≝ (m_bits_of_state n h (\fst trg))
+letin qout_low_hd ≝ (hd ? qout_low 〈bit true,false〉)
+letin qout_low_tl ≝ (tail ? qout_low)
+letin low_act ≝ (low_action (\snd (t 〈qin,current ? tape〉)))
+letin low_cout ≝ (\fst low_act)
+letin low_m ≝ (\snd low_act)
+lapply (Huni_step n table q_low_hd (\fst qout_low_hd) 
+       current_low low_cout low_left low_right q_low_tl qout_low_tl low_m … Ht1) 
+  [@daemon
+  |>Htable
+   @(trans_to_match n h t 〈qin,current ? tape〉 … (refl …))
+   >Hq_low  >Hcurrent_low whd in match (mk_tuple ?????);
+   >(eq_pair_fst_snd … (t …)) whd in ⊢ (??%?);
+   >(eq_pair_fst_snd … (low_action …)) %
+  |//
+  |@daemon
+  ]
+-Ht1 #Huni_step lapply (Huni_step ? (refl …)) -Huni_step *
+#q_low_head_false * #ls1 * #rs1 * #c2 * * 
+#Ht2 #Hlift #Hlegal %
+  [whd in ⊢ (??%?); >q_low_head_false in Hq_low; 
+   whd in ⊢ ((???%)→?); generalize in match (h qin);
+   #x #H destruct (H) %
+  |>Ht2 whd in match (step ???); 
+   whd in match (trans ???); 
+   >(eq_pair_fst_snd … (t ?))
+   @is_low_config // >Hlift
+   <low_tape_move @eq_f2
+    [>Hlow_left >Hlow_right >Hcurrent_low whd in ⊢ (??%%); 
+     cases (current …tape) [%] #b whd in ⊢ (??%%); %
+    |whd in match low_cout; whd in match low_m; whd in match low_act; 
+     generalize in match (\snd (t ?)); * [%] * #b #mv
+     whd in  ⊢ (??(?(???%)?)%); cases mv % 
+    ]
+  ]
+qed.
     
 definition low_step_R_false ≝ λt1,t2.
   ∀M:normalTM.
-- 
2.39.2