From 1f740f74d94187a2376228a86faf79ea949c0dff Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 17 Jan 2013 12:59:25 +0000
Subject: [PATCH] normal and tuples

---
 .../lib/turing/multi_universal/alphabet.ma    |  34 +--
 .../lib/turing/multi_universal/normalTM.ma    | 231 ++++++++++++++++++
 .../lib/turing/multi_universal/tuples.ma      | 115 +++++++++
 3 files changed, 365 insertions(+), 15 deletions(-)
 create mode 100644 matita/matita/lib/turing/multi_universal/normalTM.ma
 create mode 100644 matita/matita/lib/turing/multi_universal/tuples.ma

diff --git a/matita/matita/lib/turing/multi_universal/alphabet.ma b/matita/matita/lib/turing/multi_universal/alphabet.ma
index 8a6859669..fdd433f07 100644
--- a/matita/matita/lib/turing/multi_universal/alphabet.ma
+++ b/matita/matita/lib/turing/multi_universal/alphabet.ma
@@ -1,18 +1,16 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic   
+    ||A||  Library of Mathematics, developed at the Computer Science 
+    ||T||  Department of the University of Bologna, Italy.           
+    ||I||                                                            
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_____________________________________________________________*)
 
 include "basics/finset.ma".
+include "basics/lists/list.ma".
 
 inductive unialpha : Type[0] ≝ 
 | bit  : bool → unialpha
@@ -46,5 +44,11 @@ definition FSUnialpha ≝
 
 (*************************** testing characters *******************************)
 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
-definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ].
-definition is_null ≝ λc.match c with [ null ⇒ true | _ ⇒ false ].
\ No newline at end of file
+definition is_bar ≝ λc:DeqUnialpha. c == bar.
+definition is_null ≝ λc:DeqUnialpha. c == null.
+
+definition only_bits ≝ λl.
+  ∀c.mem ? c l → is_bit c = true.
+
+definition no_bars ≝ λl.
+  ∀c.mem ? c l → is_bar c = false.
diff --git a/matita/matita/lib/turing/multi_universal/normalTM.ma b/matita/matita/lib/turing/multi_universal/normalTM.ma
new file mode 100644
index 000000000..13ef8a66c
--- /dev/null
+++ b/matita/matita/lib/turing/multi_universal/normalTM.ma
@@ -0,0 +1,231 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic   
+    ||A||  Library of Mathematics, developed at the Computer Science 
+    ||T||  Department of the University of Bologna, Italy.           
+    ||I||                                                            
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_____________________________________________________________*)
+
+include "turing/multi_universal/alphabet.ma".
+include "turing/mono.ma".
+
+(************************* turning DeqMove into a DeqSet **********************)
+definition move_eq ≝ λm1,m2:move.
+  match m1 with
+  [R ⇒ match m2 with [R ⇒ true | _ ⇒ false]
+  |L ⇒ match m2 with [L ⇒ true | _ ⇒ false]
+  |N ⇒ match m2 with [N ⇒ true | _ ⇒ false]].
+
+lemma move_eq_true:∀m1,m2.
+  move_eq m1 m2 = true ↔ m1 = m2.
+*
+  [* normalize [% #_ % |2,3: % #H destruct ]
+  |* normalize [1,3: % #H destruct |% #_ % ]
+  |* normalize [1,2: % #H destruct |% #_ % ]
+qed.
+
+definition DeqMove ≝ mk_DeqSet move move_eq move_eq_true.
+
+unification hint 0 ≔ ;
+    X ≟ DeqMove
+(* ---------------------------------------- *) ⊢ 
+    move ≡ carr X.
+
+unification hint  0 ≔ m1,m2; 
+    X ≟ DeqMove
+(* ---------------------------------------- *) ⊢ 
+    move_eq m1 m2 ≡ eqb X m1 m2.
+
+
+(************************ turning DeqMove into a FinSet ***********************)
+definition move_enum ≝ [L;R;N].
+
+lemma move_enum_unique: uniqueb ? [L;R;N] = true.
+// qed.
+
+lemma move_enum_complete: ∀x:move. memb ? x [L;R;N] = true.
+* // qed.
+
+definition FinMove ≝ 
+  mk_FinSet DeqMove [L;R;N] move_enum_unique move_enum_complete.
+
+unification hint  0 ≔ ; 
+    X ≟ FinMove
+(* ---------------------------------------- *) ⊢ 
+    move ≡ FinSetcarr X.
+
+(*************************** normal Turing Machines ***************************)
+
+(* A normal turing machine is just an ordinary machine where:
+  1. the tape alphabet is bool
+  2. the finite state are supposed to be an initial segment of the natural 
+     numbers. 
+  Formally, it is specified by a record with the number n of states, a proof
+  that n is positive, the transition function and the halting function.
+*)
+
+definition trans_source ≝ λn.
+  FinProd (initN n) (FinOption FinBool).
+  
+definition trans_target ≝ λn.
+  FinProd (FinProd (initN n) (FinOption FinBool)) FinMove.
+
+record normalTM : Type[0] ≝ 
+{ no_states : nat;
+  pos_no_states : (0 < no_states); 
+  ntrans : trans_source no_states → trans_target no_states;
+  nhalt : initN no_states → bool
+}.
+
+(* A normal machine is just a special case of Turing Machine. *)
+
+definition normalTM_to_TM ≝ λM:normalTM.
+  mk_TM FinBool (initN (no_states M)) 
+   (ntrans M) (mk_Sig ?? 0 (pos_no_states M)) (nhalt M).
+
+coercion normalTM_to_TM.
+
+definition nconfig ≝ λn. config FinBool (initN n).
+
+(******************************** tuples **************************************)
+
+(* 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 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,x〉,〈j,y,m〉〉 a tuple with the following syntactical structure
+           | w_i x w_j y m
+where 
+1. "|" is a special character used to separate tuples
+2. w_i and w_j are list of booleans representing the states $i$ and $j$; 
+3. x and y are encoding 
+4. finally, m ...
+*)
+
+definition mk_tuple ≝ λqin,cin,qout,cout,mv.
+  bar::qin@cin::qout@[cout;mv].
+
+definition tuple_TM : nat → list unialpha → Prop ≝ 
+ λn,t.∃qin,cin,qout,cout,mv.
+ only_bits qin ∧ only_bits qout ∧ cin ≠ bar ∧ cout ≠ bar ∧ mv ≠ bar ∧
+ |qin| = n ∧ |qout| = n ∧
+ t = mk_tuple qin cin qout cout mv. 
+
+(***************************** state encoding *********************************)
+(* p < n is represented with a list of bits of lenght n with the p-th bit from 
+left set to 1. An additional intial bit is set to 1 if the state is final and
+to 0 otherwise. *)
+ 
+let rec to_bitlist n p: list bool ≝
+  match n with [ O ⇒ [ ] | S q ⇒ (eqb p q)::to_bitlist q p].
+  
+let rec from_bitlist l ≝
+  match l with 
+  [ nil ⇒ 0 (* assert false *)
+  | cons b tl ⇒ if b then |tl| else from_bitlist tl].
+
+lemma bitlist_length: ∀n,p.|to_bitlist n p| = n.
+#n elim n normalize // 
+qed.
+
+lemma bitlist_inv1: ∀n,p.p<n → from_bitlist (to_bitlist n p) = p.
+#n elim n normalize -n
+  [#p #abs @False_ind /2/
+  |#n #Hind #p #lepn 
+   cases (le_to_or_lt_eq … (le_S_S_to_le … lepn))
+    [#ltpn lapply (lt_to_not_eq … ltpn) #Hpn
+     >(not_eq_to_eqb_false … Hpn) normalize @Hind @ltpn
+    |#Heq >(eq_to_eqb_true … Heq) normalize <Heq //
+    ]
+  ]
+qed.
+
+lemma bitlist_lt: ∀l. 0 < |l| → from_bitlist l < |l|.
+#l elim l normalize // #b #tl #Hind cases b normalize //
+#Htl cases (le_to_or_lt_eq … (le_S_S_to_le … Htl)) -Htl #Htl
+  [@le_S_S @lt_to_le @Hind //  
+  |cut (tl=[ ]) [/2 by append_l2_injective/] #eqtl >eqtl @le_n
+  ]
+qed.
+
+definition nat_of: ∀n. Nat_to n → nat.
+#n normalize * #p #_ @p
+qed. 
+
+definition bits_of_state ≝ λn.λh:Nat_to n → bool.λs:Nat_to n.
+   map ? unialpha (λx.bit x) (h s::(to_bitlist n (nat_of n s))).
+
+lemma only_bits_bits_of_state : ∀n,h,p. only_bits (bits_of_state n h p).
+#n #h #p #x whd in match (bits_of_state n h p);
+#H cases H -H 
+  [#H >H %
+  |elim (to_bitlist n (nat_of n p))
+    [@False_ind |#b #l #Hind #H cases H -H #H [>H % |@Hind @H ]]
+  ]
+qed.
+
+(******************************** action encoding *****************************)
+
+definition low_char ≝ λc. 
+  match c with 
+    [ None ⇒ null
+    | Some b ⇒ bit b
+    ].
+    
+definition low_mv ≝ λm. 
+  match m with 
+  [ R ⇒ bit true
+  | L ⇒ bit false
+  | N ⇒ null
+  ].
+
+(******************************** tuple encoding ******************************)
+definition tuple_type ≝ λn.
+ (Nat_to n × (option FinBool)) × (Nat_to n × (option FinBool) × move).  
+
+definition tuple_encoding ≝ λn.λh:Nat_to n→bool. 
+  λp:tuple_type n.
+  let 〈inp,outp〉 ≝ p in
+  let 〈q,a〉 ≝ inp in
+  let 〈qn,an,m〉 ≝ outp in
+  let qin ≝ bits_of_state n h q in
+  let qout ≝ bits_of_state n h qn in
+  let cin ≝ low_char a in
+  let cout ≝ low_char an in
+  let mv ≝ low_mv m in
+  mk_tuple qin cin qout cout mv.
+
+lemma is_tuple: ∀n,h,p. tuple_TM (S n) (tuple_encoding n h p).
+#n #h * * #q #a * * #qn #an #m
+%{(bits_of_state n h q)} %{(low_char a)} 
+%{(bits_of_state n h qn)} %{(low_char an)} %{(low_mv m)} 
+% // % 
+  [%[%[%[%[% /2/ |% cases a normalize [|#b] #H destruct]
+        |% cases an normalize [|#b] #H destruct]
+      |% cases m normalize #H destruct]
+    |>length_map normalize @eq_f //]
+  |>length_map normalize @eq_f //]
+qed. 
+
+definition tuple_length ≝ λn.2*n+4.
+
+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 normalize >length_append >Hqin -Hqin normalize >length_append 
+normalize >Hqout //
+qed.
+
+definition tuples_list ≝ λn.λh.map … (λp.tuple_encoding n h p).
+
+
+
+
diff --git a/matita/matita/lib/turing/multi_universal/tuples.ma b/matita/matita/lib/turing/multi_universal/tuples.ma
new file mode 100644
index 000000000..76e56068d
--- /dev/null
+++ b/matita/matita/lib/turing/multi_universal/tuples.ma
@@ -0,0 +1,115 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic   
+    ||A||  Library of Mathematics, developed at the Computer Science 
+    ||T||  Department of the University of Bologna, Italy.           
+    ||I||                                                            
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_____________________________________________________________*)
+
+
+(****************************** table of tuples *******************************)
+include "turing/multi_universal/normalTM.ma".
+
+(* a well formed table is a list of tuples *) 
+ 
+definition table_TM ≝ λn,l,h.flatten ? (tuples_list n h l).
+
+lemma table_TM_cons: ∀n,h,t,o. 
+  table_TM n (t::o) h = (tuple_encoding n h t)@(table_TM n o h).
+// qed.
+
+(************************** matching in a table *******************************)
+lemma list_to_table: ∀n,l,h,tup. mem ? tup (tuples_list n h l) →
+  ∃ll,lr.table_TM n l h = ll@tup@lr.
+#n #l #h #tup elim l 
+  [@False_ind
+  |#hd #tl #Hind *
+    [#Htup %{[]} %{(table_TM n tl h)} >Htup %
+    |#H cases (Hind H) #ll * #lr #H1
+     %{((tuple_encoding n h hd)@ll)} %{lr} 
+     >associative_append <H1 %
+    ]
+  ]
+qed.
+
+definition is_config : nat → list unialpha → Prop ≝  
+ λn,t.∃qin,cin.
+ only_bits qin ∧ cin ≠ bar ∧ |qin| = S n ∧ t = bar::qin@[cin].
+
+lemma compare_append : ∀A,l1,l2,l3,l4. l1@l2 = l3@l4 → 
+∃l:list A.(l1 = l3@l ∧ l4=l@l2) ∨ (l3 = l1@l ∧ l2=l@l4).
+#A #l1 elim l1
+  [#l2 #l3 #l4 #Heq %{l3} %2 % // @Heq
+  |#a1 #tl1 #Hind #l2 #l3 cases l3
+    [#l4 #Heq %{(a1::tl1)} %1 % // @sym_eq @Heq 
+    |#a3 #tl3 #l4 normalize in ⊢ (%→?); #Heq cases (Hind l2 tl3 l4 ?)
+      [#l * * #Heq1 #Heq2 %{l}
+        [%1 % // >Heq1 >(cons_injective_l ????? Heq) //
+        |%2 % // >Heq1 >(cons_injective_l ????? Heq) //
+        ]
+      |@(cons_injective_r ????? Heq) 
+      ]
+    ]
+  ]
+qed.
+
+lemma table_to_list: ∀n,l,h,c. is_config n c → 
+  (∃ll,lr.table_TM n l h = ll@c@lr) → 
+    ∃out,t. tuple_encoding n h t = (c@out) ∧ mem ? t l.
+#n #l #h #c * #qin * #cin * * * #H1 #H2 #H3 #H4  
+ * #ll * #lr lapply ll -ll elim l
+  [>H4 #ll cases ll normalize [|#hd #tl ] #Habs destruct
+  |#t1 #othert #Hind #ll >table_TM_cons #Htuple
+   cut (S n < |ll@c@lr|)
+     [<Htuple >length_append >(length_of_tuple  … (is_tuple … ))
+      /2 by transitive_lt, le_n/] #Hsplit lapply Htuple -Htuple
+   cases (is_tuple … n h t1) #q1 * #c1 * #q2 * #c2 * #m 
+   * * * * * * * #Hq1 #Hq2 #Hc1 #Hc2 #Hm #Hlen1 #Hlen2 
+   whd in ⊢ (???%→?); #Ht1 
+   (* if ll is empty we match the first tuple t1, otherwise
+      we match inside othert *)
+   cases ll
+    [>H4 >Ht1 normalize in ⊢ (???%→?); 
+     >associative_append whd in ⊢ (??%?→?); #Heq destruct (Heq) -Heq
+     >associative_append in e0; #e0
+     lapply (append_l1_injective  … e0) [>H3 @Hlen1] #Heq1
+     lapply (append_l2_injective  … e0) [>H3 @Hlen1]
+     normalize in ⊢ (???%→?); whd in ⊢ (??%?→?); #Htemp 
+     lapply (cons_injective_l ????? Htemp) #Hc1
+     lapply (cons_injective_r ????? Htemp) -Htemp #Heq2
+     %{(q2@[c2;m])} %{t1} % 
+      [>Ht1 >Heq1 >Hc1 @eq_f >associative_append % 
+      |%1 %
+      ]
+    |(* ll not nil *)
+     #b #tl >Ht1 normalize in ⊢ (???%→?); 
+     whd in ⊢ (??%?→?); #Heq destruct (Heq) 
+     cases (compare_append … e0) #l *
+      [* cases l 
+        [#_ #Htab cases (Hind [ ] (sym_eq … Htab)) #out * #t * #Ht #Hmemt
+         %{out} %{t} % // %2 //
+        |(* this case is absurd *) 
+         #al #tll #Heq1 >H4 #Heq2 @False_ind 
+         lapply (cons_injective_l ? bar … Heq2) #Hbar <Hbar in Heq1; #Heq1
+         @(absurd (mem ? bar (q1@(c1::q2@[c2; m]))))
+          [>Heq1 @mem_append_l2 %1 //
+          |% #Hmembar cases (mem_append ???? Hmembar) -Hmembar
+            [#Hmembar lapply(Hq1 bar Hmembar) normalize #Habs destruct (Habs)
+            |* [#Habs @absurd //]
+             #Hmembar cases (mem_append ???? Hmembar) -Hmembar
+              [#Hmembar lapply(Hq2 bar Hmembar) normalize #Habs destruct (Habs)
+              |* [#Habs @absurd //] #Hmembar @(absurd ?? Hm) @sym_eq @mem_single //
+              ]
+            ]
+          ]
+        ]
+      |* #Htl #Htab cases (Hind … Htab) #out * #t * #Ht #Hmemt
+       %{out} %{t} % // %2 //
+      ] 
+    ]
+  ]
+qed.
+
-- 
2.39.2