X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Ftrans_to_tuples.ma;h=09171b1202b5b74a00b48ea3aa32280483265637;hb=0460fd3dc2909efe0baa6592281d0cf0527165ff;hp=e40a0bbc8d5d5b446f7cdfb356154069a690ce9e;hpb=5fc2b08d86038360e588b8fff333a623964efabe;p=helm.git

diff --git a/matita/matita/lib/turing/universal/trans_to_tuples.ma b/matita/matita/lib/turing/universal/trans_to_tuples.ma
index e40a0bbc8..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〉.
@@ -158,10 +159,15 @@ letin mv ≝ match action with
  ]
 qed. 
 
-definition tuple_length ≝ λn.2*n+3.
+definition tuple_length ≝ λn.2*n+6.
 
-axiom length_of_tuple: ∀n,t. tuple_TM n t → 
+lemma length_of_tuple: ∀n,t. tuple_TM n t → 
   |t| = tuple_length n.
+#n #t * #qin * #cin * #qout * #cout * #mv *** #_
+#Hqin #Hqout #eqt >eqt whd in match (mk_tuple ?????); 
+normalize >length_append >Hqin -Hqin normalize 
+>length_append normalize >Hqout -Hqout //
+qed.
 
 definition move_eq ≝ λm1,m2:move.
   match m1 with
@@ -169,14 +175,14 @@ definition move_eq ≝ λm1,m2:move.
   |L ⇒ match m2 with [L ⇒ true | _ ⇒ false]
   |N ⇒ match m2 with [N ⇒ true | _ ⇒ false]].
   
-definition tuples_of_pairs ≝ λn.λh.map … (λp.(tuple_of_pair n h p)@[〈bar,false〉]).
+definition tuples_of_pairs ≝ λn.λh.map … (λp.tuple_of_pair n h p).
 
 definition flatten ≝ λA.foldr (list A) (list A) (append A) [].
 
 lemma wftable: ∀n,h,l.table_TM (S n) (flatten ? (tuples_of_pairs n h l)).
 #n #h #l elim l // -l #a #tl #Hind 
 whd in match (flatten … (tuples_of_pairs …));
->associative_append @ttm_cons //
+@ttm_cons //
 qed.
 
 lemma flatten_to_mem: ∀A,n,l,l1,l2.∀a:list A. 0 < n →
@@ -204,10 +210,27 @@ 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)@[〈bar,false〉])@l2 ∧
-    (∃q.|l1| = (S (tuple_length (S n)))*q) ∧ tuple_TM (S n) (mk_tuple qin cin qout cout mv).
+  ∃l1,l2. l = l1@(mk_tuple qin cin qout cout mv)@l2 ∧
+    (∃q.|l1| = (tuple_length (S n))*q) ∧ tuple_TM (S n) (mk_tuple qin cin qout cout mv).
 (*
 lemma match_tech: ∀n,l,qin,cin,qout,cout,mv.
   (∀t. mem ? t l → |t| = |mk_tuple qin cin qout cout mv|) →
@@ -219,14 +242,14 @@ lemma match_tech: ∀n,l,qin,cin,qout,cout,mv.
 
 lemma match_to_tuple: ∀n,h,l,qin,cin,qout,cout,mv.
   match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h l)) → 
-    ∃p. p = mk_tuple qin cin qout cout mv ∧ mem ? (p@[〈bar,false〉]) (tuples_of_pairs n h l).
+    ∃p. p = mk_tuple qin cin qout cout mv ∧ mem ? p (tuples_of_pairs n h l).
 #n #h #l #qin #cin #qout #cout #mv #Hmatch 
 @(ex_intro … (mk_tuple qin cin qout cout mv)) % //
 cases (match_decomp … Hmatch) #l1 * #l2 * * #Hflat #Hlen #Htuple
 @(flatten_to_mem … Hflat … Hlen)  
   [// 
   |@daemon
-  |>length_append >(length_of_tuple … Htuple) normalize //
+  |@(length_of_tuple … Htuple) 
   ]
 qed.
 
@@ -248,7 +271,7 @@ lemma match_to_pair: ∀n,h,l,qin,cin,qout,cout,mv.
 #n #h #l #qin #cin #qout #cout #mv #Hmatch 
 cases (match_to_tuple … Hmatch)
 #p * #eqp #memb 
-cases(mem_map … (λp.(tuple_of_pair n h p)@[〈bar,false〉]) … memb)
+cases(mem_map … (λp.tuple_of_pair n h p) … memb)
 #p1 * #Hmem #H @(ex_intro … p1) % /2/
 qed.
 
@@ -305,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