working on match

[helm.git] / matita / matita / lib / turing / turing.ma

diff --git a/matita/matita/lib/turing/turing.ma b/matita/matita/lib/turing/turing.ma
index c9412adb06d381aa158d3be3bb6b4aed5112e998..a8290de51d7d32eb365fa3b7fdc9786b3bc2a8bb 100644 (file)
--- a/matita/matita/lib/turing/turing.ma
+++ b/matita/matita/lib/turing/turing.ma
@@ -412,3 +412,57 @@ theorem sem_seq_app_guarded: ∀sig,n.∀M1,M2:mTM sig n.∀Pre1,Pre2,R1,R2,R3.
 % [@Hloop |@Hsub @Houtc]
 qed.
 
+theorem acc_sem_seq : ∀sig,n.∀M1,M2:mTM sig n.∀R1,Rtrue,Rfalse,acc.
+  M1 ⊨ R1 → M2 ⊨ [ acc: Rtrue, Rfalse ] → 
+  M1 · M2 ⊨ [ inr … acc: R1 ∘ Rtrue, R1 ∘ Rfalse ].
+#sig #n #M1 #M2 #R1 #Rtrue #Rfalse #acc #HR1 #HR2 #t 
+cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
+cases (HR2 (ctapes sig (states ?? M1) n outc1)) #k2 * #outc2 * * #Hloop2 
+#HMtrue #HMfalse
+@(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
+% [ %
+[@(loop_merge ??????????? 
+   (loop_lift ??? (lift_confL sig n (states sig n M1) (states sig n M2))
+   (step sig n M1) (step sig n (seq sig n M1 M2)) 
+   (λc.halt sig n M1 (cstate … c)) 
+   (λc.halt_liftL ?? (halt sig n M1) (cstate … c)) … Hloop1))
+  [ * *
+   [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
+   | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
+  || #c0 #Hhalt <step_seq_liftL //
+  | #x <p_halt_liftL %
+  |6:cases outc1 #s1 #t1 %
+  |7:@(loop_lift … (initc ??? (ctapes … outc1)) … Hloop2) 
+    [ * #s2 #t2 %
+    | #c0 #Hhalt <step_seq_liftR // ]
+  |whd in ⊢ (??(????%)?);whd in ⊢ (??%?);
+   generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10 
+   >(trans_liftL_true sig n M1 M2 ??) 
+    [ whd in ⊢ (??%?); whd in ⊢ (???%);
+      @mconfig_eq whd in ⊢ (???%); // 
+    | @(loop_Some ?????? Hloop10) ]
+ ]
+| >(mconfig_expand … outc2) in ⊢ (%→?); whd in ⊢ (??%?→?); 
+  #Hqtrue destruct (Hqtrue)
+  @(ex_intro … (ctapes ? (FinSum (states ?? M1) (states ?? M2)) ? (lift_confL … outc1)))
+  % // >eq_ctape_lift_conf_L >eq_ctape_lift_conf_R /2/ ]
+| >(mconfig_expand … outc2) in ⊢ (%→?); whd in ⊢ (?(??%?)→?); #Hqfalse
+  @(ex_intro … (ctapes ? (FinSum (states ?? M1) (states ?? M2)) ? (lift_confL … outc1)))
+  % // >eq_ctape_lift_conf_L >eq_ctape_lift_conf_R @HMfalse
+  @(not_to_not … Hqfalse) //
+]
+qed.
+
+lemma acc_sem_seq_app : ∀sig,n.∀M1,M2:mTM sig n.∀R1,Rtrue,Rfalse,R2,R3,acc.
+  M1 ⊨ R1 → M2 ⊨ [acc: Rtrue, Rfalse] → 
+    (∀t1,t2,t3. R1 t1 t3 → Rtrue t3 t2 → R2 t1 t2) → 
+    (∀t1,t2,t3. R1 t1 t3 → Rfalse t3 t2 → R3 t1 t2) → 
+    M1 · M2 ⊨ [inr … acc : R2, R3].    
+#sig #n #M1 #M2 #R1 #Rtrue #Rfalse #R2 #R3 #acc
+#HR1 #HRacc #Hsub1 #Hsub2 
+#t cases (acc_sem_seq … HR1 HRacc t)
+#k * #outc * * #Hloop #Houtc1 #Houtc2 @(ex_intro … k) @(ex_intro … outc)
+% [% [@Hloop
+     |#H cases (Houtc1 H) #t3 * #Hleft #Hright @Hsub1 // ]
+  |#H cases (Houtc2 H) #t3 * #Hleft #Hright @Hsub2 // ]
+qed.