X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Finject.ma;h=d7851d85f938ba480045bd170c5e6c2f1a1af493;hb=9def1b8a298aac85a7abdc75c4a33657fe7e6df7;hp=2de2caa83ff8e9149d2173f14c618c592642ed8a;hpb=cf097061bef43a9170c7776000c7f865f6c59b50;p=helm.git

diff --git a/matita/matita/lib/turing/inject.ma b/matita/matita/lib/turing/inject.ma
index 2de2caa83..d7851d85f 100644
--- a/matita/matita/lib/turing/inject.ma
+++ b/matita/matita/lib/turing/inject.ma
@@ -49,11 +49,13 @@ whd in match (step ????); >(current_chars_change_vec … lein)
 >(eq_pair_fst_snd … (trans sig M ?)) whd in ⊢ (??%?→?); #H
 >(inject_trans_def sig n i lein M … (eq_pair_fst_snd … ))
 whd in ⊢ (??%?); @eq_f2 [destruct (H) // ]
-@(eq_vec … (niltape ?)) #i0 #lei0n 
->nth_change_vec_neq >nth_change_vec_neq 
- … (tr
-// qed.
-
+@(eq_vec … (niltape ?)) #i0 #lei0n
+cases (decidable_eq_nat … i i0) #Hii0
+[ >Hii0 >nth_change_vec // >pmap_change >nth_change_vec // destruct (H) //
+| >nth_change_vec_neq // >pmap_change >nth_change_vec_neq 
+  >tape_move_null_action //
+]
+qed.
 
 lemma halt_inject: ∀sig,n,M,i,x.
   cic:/matita/turing/turing/halt.fix(0,2,9) sig n (inject_TM sig M n i) x
@@ -64,13 +66,13 @@ lemma de_option: ∀A,a,b. Some A a = Some A b → a = b.
 #A #a #b #H destruct //
 qed. 
 
-lemma loop_inject: ∀sig,n,M,i,k,ins,int,outs,outt,vt.
+lemma loop_inject: ∀sig,n,M,i,k,ins,int,outs,outt,vt.i < S n → 
  loopM sig M k (mk_config ?? ins int) = Some ? (mk_config ?? outs outt) → 
  cic:/matita/turing/turing/loopM.def(11) sig n (inject_TM sig M n i) k (mk_mconfig ?? n ins (change_vec ?? vt int i))
   =Some ? (mk_mconfig sig ? n outs (change_vec ?? vt outt i)).
 #sig #n #M #i #k elim k -k
-  [#ins #int #outs #outt #vt normalize in ⊢ (%→?); #H destruct
-  |#k #Hind #ins #int #outs #outt #vt whd in ⊢ (??%?→??%?);
+  [#ins #int #outs #outt #vt #Hin normalize in ⊢ (%→?); #H destruct
+  |#k #Hind #ins #int #outs #outt #vt #Hin whd in ⊢ (??%?→??%?);
    >halt_inject whd in match (cstate ????);
    cases (true_or_false (halt sig M ins)) #Hhalt >Hhalt 
    whd in ⊢ (??%?→??%?);
@@ -84,17 +86,14 @@ lemma loop_inject: ∀sig,n,M,i,k,ins,int,outs,outt,vt.
         |destruct (H) //
         ]
       ]
-    |>(config_expand … (step ???)) #H <(Hind … H) 
-     >loopM_unfold @eq_f >(mconfig_expand … (step ????)) 
-     @eq_f2 [ normalize in ⊢ (???%);
-  |%[>nth_change_vec // @le_S_S //
-    |#j #i >nth_change_vec_neq //
+    |>(config_expand … (step ???)) #H <(Hind … H) // 
+     >loopM_unfold @eq_f >inject_step //
     ]
   ]
+qed.
 
 (*
 lemma cstate_inject: ∀sig,n,M,i,x. *)
-  
 
 definition inject_R ≝ λsig.λR:relation (tape sig).λn,i:nat.
   λv1,v2: (Vector (tape sig) (S n)).
@@ -126,34 +125,29 @@ theorem sem_inject: ∀sig.∀M:TM sig.∀R.∀n,i.
  i≤n → M ⊨ R → inject_TM sig M n i ⊨ inject_R sig R n i. 
 #sig #M #R #n #i #lein #HR #vt cases (HR (nth i ? vt (niltape ?)))
 #k * * #outs #outt * #Hloop #HRout @(ex_intro ?? k) 
-@(ex_intro ?? (mk_mconfig ?? n outs (change_vec ? (S n) vt outt i))) % 
-  [elim k in Hloop;
-    [normalize in ⊢ (%\to ?); #H destruct
-    |#k0 #Hind whd in ⊢ (??%?→??%?);
-     >halt_inject whd in match (cstate ????);
-     whd in match (cstate sig (states sig M)
-       (initc sig M (nth i (tape sig) vt (niltape sig)))); 
-     cases (true_or_false (halt sig M (start sig M))) #Hhalt >Hhalt 
-     whd in ⊢ (??%?→??%?);
-      [#H @eq_f whd in ⊢ (??%?); lapply (de_option ??? H) -H 
-       whd  in ⊢ (??%?→?); #H @eq_f2  
-        [whd in ⊢ (??%?); destruct (H) //
-        |@(eq_vec … (niltape ?)) #j #lejn
-         cases (true_or_false (eqb i j)) #eqij
-          [>(eqb_true_to_eq … eqij) >nth_change_vec //
-           <(eqb_true_to_eq … eqij) destruct (H) //
-          |>nth_change_vec_neq // @(eqb_false_to_not_eq … eqij)
-          ]
-        ]
-      |#H <Hind //
+@(ex_intro ?? (mk_mconfig ?? n outs (change_vec ? (S n) vt outt i))) %
+  [whd in ⊢ (??(?????%)?); <(change_vec_same ?? vt i (niltape ?)) in ⊢ (??%?);
+   @loop_inject /2 by refl, trans_eq, le_S_S/
   |%[>nth_change_vec // @le_S_S //
     |#j #i >nth_change_vec_neq //
     ]
   ]
-          
-  
-  
-
-  
-
+qed.
 
+theorem acc_sem_inject: ∀sig.∀M:TM sig.∀Rtrue,Rfalse,acc.∀n,i.
+ i≤n → M ⊨ [ acc : Rtrue, Rfalse ] → 
+ inject_TM sig M n i ⊨ [ acc : inject_R sig Rtrue n i, inject_R sig Rfalse n i ]. 
+#sig #M #Rtrue #Rfalse #acc #n #i #lein #HR #vt cases (HR (nth i ? vt (niltape ?)))
+#k * * #outs #outt * * #Hloop #HRtrue #HRfalse @(ex_intro ?? k) 
+@(ex_intro ?? (mk_mconfig ?? n outs (change_vec ? (S n) vt outt i))) % [ %
+  [whd in ⊢ (??(?????%)?); <(change_vec_same ?? vt i (niltape ?)) in ⊢ (??%?);
+   @loop_inject /2 by refl, trans_eq, le_S_S/
+  |#Hqtrue %
+    [>nth_change_vec /2 by le_S_S/
+    |#j #Hneq >nth_change_vec_neq //
+    ] ]
+  |#Hqfalse %
+    [>nth_change_vec /2 by le_S_S/ @HRfalse @Hqfalse
+    |#j #Hneq >nth_change_vec_neq //
+    ] ]
+qed.
\ No newline at end of file