Adding GRealize to uni_step.

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

diff --git a/matita/matita/lib/turing/if_machine.ma b/matita/matita/lib/turing/if_machine.ma
index 6248ab7e7cfabcd0ae366162ff9268c272791e8a..f778ff3085c6f8af5b1e6bbc2b0c18481184ee47 100644 (file)
--- a/matita/matita/lib/turing/if_machine.ma
+++ b/matita/matita/lib/turing/if_machine.ma
@@ -236,6 +236,7 @@ lemma sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,acc.
 qed.
  
 (* we can probably use acc_sem_if to prove sem_if *)
+(* for sure we can use acc_sem_if_guarded to prove acc_sem_if *)
 lemma acc_sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc.
   M1 ⊨ [acc: Rtrue, Rfalse]  → M2 ⊨ R2 → M3 ⊨ R3 → 
   ifTM sig M1 (single_finalTM … M2) M3 acc ⊨
@@ -333,3 +334,117 @@ lemma acc_sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,R5,acc.
      |#H cases (Houtc1 H) #t3 * #Hleft #Hright @Hsub1 // ]
   |#H cases (Houtc2 H) #t3 * #Hleft #Hright @Hsub2 // ]
 qed.
+
+lemma sem_single_final_guarded: ∀sig.∀M: TM sig.∀Pre,R.
+  GRealize sig M Pre R → GRealize sig (single_finalTM sig M) Pre R.
+#sig #M #Pre #R #HR #intape #HPre 
+cases (sem_seq_guarded ??????? HR (Realize_to_GRealize ?? (λt.True) ? (sem_nop …)) ?? HPre) //
+#k * #outc * #Hloop * #ta * #Hta whd in ⊢ (%→?); #Houtc
+@(ex_intro ?? k) @(ex_intro ?? outc) %  [ @Hloop | >Houtc // ]
+qed.
+    
+lemma acc_sem_if_guarded: ∀sig,M1,M2,M3,P,P2,Rtrue,Rfalse,R2,R3,acc.
+  M1 ⊨ [acc: Rtrue, Rfalse]  → 
+  (GRealize ? M2 P2 R2) → (∀t,t0.P t → Rtrue t t0 → P2 t0) → 
+  M3 ⊨ R3 → 
+  accGRealize ? (ifTM sig M1 (single_finalTM … M2) M3 acc) 
+    (inr … (inl … (inr … start_nop))) P (Rtrue ∘ R2) (Rfalse ∘ R3).
+#sig #M1 #M2 #M3 #P #P2 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HP2 #HR3 #t #HPt 
+cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse 
+cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
+  [lapply (sem_single_final_guarded … HR2) -HR2 #HR2
+   cases (HR2 (ctape sig ? outc1) ?)
+   [|@HP2 [||@HMtrue @(\P Hacc)] // ]
+   #k2 * #outc2 * #Hloop2 #HM2
+   @(ex_intro … (k1+k2)) 
+   @(ex_intro … (lift_confR … (lift_confL … outc2))) %
+    [%
+      [@(loop_merge ?????????
+         (mk_config ? (states sig (ifTM sig M1 (single_finalTM … M2) M3 acc))
+          (inr (states sig M1) ? (inl ? (states sig M3) (start sig (single_finalTM sig M2)))) (ctape ?? outc1) )
+         ? 
+         (loop_lift ??? 
+          (lift_confL sig (states ? M1) (FinSum (states ? (single_finalTM … M2)) (states ? M3)))
+          (step sig M1) (step sig (ifTM sig M1 (single_finalTM ? M2) M3 acc)) 
+          (λc.halt sig M1 (cstate … c)) 
+          (λc.halt_liftL ?? (halt sig M1) (cstate … c)) 
+          … Hloop1))
+        [* *
+          [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
+          | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
+        |#c0 #Hhalt >(step_if_liftM1 … Hhalt) // 
+        |#x <p_halt_liftL %
+        |whd in ⊢ (??%?); >(config_expand ?? outc1);
+         whd in match (lift_confL ????);
+         >(trans_if_M1true_acc … Hacc) 
+          [% | @(loop_Some ?????? Hloop1)]
+        |cases outc1 #s1 #t1 %
+        |@(loop_lift ??? 
+           (λc.(lift_confR … (lift_confL sig (states ? (single_finalTM ? M2)) (states ? M3) c)))
+           … Hloop2) 
+          [ * #s2 #t2 %
+          | #c0 #Hhalt >(step_if_liftM2 … Hhalt) // ]
+        ]
+      |#_ @(ex_intro … (ctape ?? outc1)) % 
+        [@HMtrue @(\P Hacc) | >(config_expand ?? outc2) @HM2 ]
+      ]
+    |>(config_expand ?? outc2) whd in match (lift_confR ????);
+     * #H @False_ind @H @eq_f @eq_f >(config_expand ?? outc2)
+     @single_final // @(loop_Some ?????? Hloop2)
+    ]
+  |cases (HR3 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM3
+   @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confR … outc2))) %
+    [%
+      [@(loop_merge ?????????
+         (mk_config ? (states sig (ifTM sig M1 (single_finalTM … M2) M3 acc))
+          (inr (states sig M1) ? (inr (states sig (single_finalTM ? M2)) ? (start sig M3))) (ctape ?? outc1) )
+         ? 
+         (loop_lift ??? 
+          (lift_confL sig (states ? M1) (FinSum (states ? (single_finalTM … M2)) (states ? M3)))
+          (step sig M1) (step sig (ifTM sig M1 (single_finalTM ? M2) M3 acc)) 
+          (λc.halt sig M1 (cstate … c)) 
+          (λc.halt_liftL ?? (halt sig M1) (cstate … c)) 
+          … Hloop1))
+        [* *
+          [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
+          | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
+        |#c0 #Hhalt >(step_if_liftM1 … Hhalt) // 
+        |#x <p_halt_liftL %
+        |whd in ⊢ (??%?); >(config_expand ?? outc1);
+         whd in match (lift_confL ????);
+         >(trans_if_M1true_notacc … Hacc) 
+          [% | @(loop_Some ?????? Hloop1)]
+        |cases outc1 #s1 #t1 %
+        |@(loop_lift ??? 
+           (λc.(lift_confR … (lift_confR sig (states ? (single_finalTM ? M2)) (states ? M3) c)))
+           … Hloop2) 
+          [ * #s2 #t2 %
+          | #c0 #Hhalt >(step_if_liftM3 … Hhalt) // ]
+        ]
+      |>(config_expand ?? outc2) whd in match (lift_confR ????);
+       #H destruct (H) 
+      ]
+    |#_ @(ex_intro … (ctape ?? outc1)) % 
+      [@HMfalse @(\Pf Hacc) | >(config_expand ?? outc2) @HM3 ]
+    ]
+  ]
+qed.
+    
+lemma acc_sem_if_app_guarded: ∀sig,M1,M2,M3,P,P2,Rtrue,Rfalse,R2,R3,R4,R5,acc.
+  M1 ⊨ [acc: Rtrue, Rfalse] → 
+  (GRealize ? M2 P2 R2) → (∀t,t0.P t → Rtrue t t0 → P2 t0) → 
+  M3 ⊨ R3 → 
+  (∀t1,t2,t3. Rtrue t1 t3 → R2 t3 t2 → R4 t1 t2) → 
+  (∀t1,t2,t3. Rfalse t1 t3 → R3 t3 t2 → R5 t1 t2) → 
+  accGRealize ? (ifTM sig M1 (single_finalTM … M2) M3 acc) 
+    (inr … (inl … (inr … start_nop))) P R4 R5 .
+#sig #M1 #M2 #M3 #P #P2 #Rtrue #Rfalse #R2 #R3 #R4 #R5 #acc
+#HRacc #HRtrue #Hinv #HRfalse #Hsub1 #Hsub2 
+#t #HPt cases (acc_sem_if_guarded … HRacc HRtrue Hinv HRfalse t HPt)
+#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.
+
+