middot notation

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

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index 80e3d4aaaaf650d4420628dc631b33a1e6cfde6d..e117fc7be167bf4bb034fc0d4c84d06ca31ee2dc 100644 (file)
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -183,6 +183,11 @@ lemma loop_eq : ∀sig,f,q,i,j,a,x,y.
 ]
 qed.
 
+lemma loop_p_true : 
+  ∀A,k,f,p,a.p a = true → loop A (S k) f p a = Some ? a.
+#A #k #f #p #a #Ha normalize >Ha %
+qed.
+
 lemma loop_Some : 
   ∀A,k,f,p,a,b.loop A k f p a = Some ? b → p b = true.
 #A #k #f #p elim k 
@@ -209,6 +214,10 @@ qed.
 definition loopM ≝ λsig,M,i,cin.
   loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) cin.
 
+lemma loopM_unfold : ∀sig,M,i,cin.
+  loopM sig M i cin = loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) cin.
+// qed.
+
 definition initc ≝ λsig.λM:TM sig.λt.
   mk_config sig (states sig M) (start sig M) t.
 
@@ -248,6 +257,44 @@ definition accRealize ≝ λsig.λM:TM sig.λacc:states sig M.λRtrue,Rfalse.
   loopM sig M i (initc sig M t) = Some ? outc ∧
     (cstate ?? outc = acc → Rtrue t (ctape ?? outc)) ∧ 
     (cstate ?? outc ≠ acc → Rfalse t (ctape ?? outc)).
+    
+notation "M ⊨ [q: R1,R2]" non associative with precedence 45 for @{ 'cmodels $M $q $R1 $R2}.
+interpretation "conditional realizability" 'cmodels M q R1 R2 = (accRealize ? M q R1 R2).
+
+(******************************** monotonicity ********************************)
+lemma Realize_to_Realize : ∀alpha,M,R1,R2.
+  R1 ⊆ R2 → Realize alpha M R1 → Realize alpha M R2.
+#alpha #M #R1 #R2 #Himpl #HR1 #intape
+cases (HR1 intape) -HR1 #k * #outc * #Hloop #HR1
+@(ex_intro ?? k) @(ex_intro ?? outc) % /2/
+qed.
+
+lemma WRealize_to_WRealize: ∀sig,M,R1,R2.
+  R1 ⊆ R2 → WRealize sig M R1 → WRealize ? M R2.
+#alpha #M #R1 #R2 #Hsub #HR1 #intape #i #outc #Hloop
+@Hsub @(HR1 … i) @Hloop
+qed.
+
+lemma acc_Realize_to_acc_Realize: ∀sig,M.∀q:states sig M.∀R1,R2,R3,R4. 
+  R1 ⊆ R3 → R2 ⊆ R4 → M ⊨ [q:R1,R2] → M ⊨ [q:R3,R4].
+#alpha #M #q #R1 #R2 #R3 #R4 #Hsub13 #Hsub24 #HRa #intape
+cases (HRa intape) -HRa #k * #outc * * #Hloop #HRtrue #HRfalse 
+@(ex_intro ?? k) @(ex_intro ?? outc) % 
+  [ % [@Hloop] #Hq @Hsub13 @HRtrue // | #Hq @Hsub24 @HRfalse //]
+qed.
+
+(**************************** A canonical relation ****************************)
+
+definition R_TM ≝ λsig.λM:TM sig.λq.λt1,t2.
+∃i,outc.
+  loopM ? M i (mk_config ?? q t1) = Some ? outc ∧ 
+  t2 = (ctape ?? outc).
+  
+lemma R_TM_to_R: ∀sig,M,R. ∀t1,t2. 
+  M ⊫ R → R_TM ? M (start sig M) t1 t2 → R t1 t2.
+#sig #M #R #t1 #t2 whd in ⊢ (%→?); #HMR * #i * #outc *
+#Hloop #Ht2 >Ht2 @(HMR … Hloop)
+qed.
 
 (******************************** NOP Machine *********************************)
 
@@ -295,14 +342,9 @@ definition seq ≝ λsig. λM1,M2 : TM sig.
     (λs.match s with 
       [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]). 
 
-notation "a · b" non associative with precedence 65 for @{ 'middot $a $b}.
+notation "a · b" right associative with precedence 65 for @{ 'middot $a $b}.
 interpretation "sequential composition" 'middot a b = (seq ? a b).
 
-definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
-  ∃am.R1 a1 am ∧ R2 am a2.
-  
-interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
-
 definition lift_confL ≝ 
   λsig,S1,S2,c.match c with 
   [ mk_config s t ⇒ mk_config sig (FinSum S1 S2) (inl … s) t ].