From 1ed95da08b483c7f7e69fc645bee455572cad031 Mon Sep 17 00:00:00 2001
From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Mon, 30 Apr 2012 15:12:42 +0000
Subject: [PATCH] More proofs in if-then-else machine.

---
 matita/matita/lib/turing/if_machine.ma | 52 ++++++++++++++++++--------
 matita/matita/lib/turing/mono.ma       | 45 +++++++++++++++++-----
 2 files changed, 72 insertions(+), 25 deletions(-)

diff --git a/matita/matita/lib/turing/if_machine.ma b/matita/matita/lib/turing/if_machine.ma
index 80598d29b..7b73d006d 100644
--- a/matita/matita/lib/turing/if_machine.ma
+++ b/matita/matita/lib/turing/if_machine.ma
@@ -39,7 +39,9 @@ definition ifTM ≝ λsig. λcondM,thenM,elseM : TM sig.
       [ inl _ ⇒ false 
       | inr s' ⇒ match s' with 
         [ inl s2 ⇒ halt sig thenM s2
-        | inr s3 ⇒ halt sig elseM s3 ]]). 
+        | inr s3 ⇒ halt sig elseM s3 ]]).
+        
+axiom daemon : ∀X:Prop.X. 
 
 theorem sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc.
   accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 → 
@@ -49,20 +51,40 @@ cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse
 cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
   [cases (HR2 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM2
    @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confL … outc2)))
-%
-[@(loop_split ??????????? (loop_liftL … Hloop1))
- [* *
-   [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
-   | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
- ||4:cases outc1 #s1 #t1 %
- |5:@(loop_liftR … Hloop2) 
- |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
-  generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10 
-  >(trans_liftL_true sig M1 M2 ??) 
-  [ whd in ⊢ (??%?); whd in ⊢ (???%);
-    @config_eq //
-  | @(loop_Some ?????? Hloop10) ]
- ]
+   %
+   [@(loop_split ??????????? 
+    (loop_lift ??? 
+      (lift_confL sig (states ? M1) (FinSum (states ? M2) (states ? M3)))
+      (step sig M1) (step sig (ifTM sig M1 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 @daemon  (* <step_lift_confL // *)
+     | #x <p_halt_liftL %
+     |6:cases outc1 #s1 #t1 %
+     |7:@(loop_lift … (initc ?? (ctape … outc1)) … Hloop2) 
+       [ * #s2 #t2 %
+       | #c0 #Hhalt @daemon (* <step_lift_confR // *) ]
+     |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
+      generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10 
+      >(trans_liftL_true sig M1 M2 ??) 
+       [ whd in ⊢ (??%?); whd in ⊢ (???%);
+         @config_eq whd in ⊢ (???%); //
+       | @(loop_Some ?????? Hloop10) ]       
+     ||4:cases outc1 #s1 #t1 %
+     |5:
+         
+         @(loop_liftR … Hloop2) 
+         |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
+          generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10 
+          >(trans_liftL_true sig M1 M2 ??) 
+           [ whd in ⊢ (??%?); whd in ⊢ (???%);
+             @config_eq //
+           | @(loop_Some ?????? Hloop10) ]
+           ]
 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))
   % //
 ]
diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index 4927c5806..a9a08213b 100644
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -254,6 +254,21 @@ whd in ⊢ (??(???%)?); whd in ⊢ (??%?);
 [% | //]
 qed.
 
+lemma loop_lift : ∀A,B,k,lift,f,g,h,hlift,c1,c2.
+  (∀x.hlift (lift x) = h x) → 
+  (∀x.h x = false → lift (f x) = g (lift x)) → 
+  loop A k f h c1 = Some ? c2 → 
+  loop B k g hlift (lift c1) = Some ? (lift … c2).
+#A #B #k #lift #f #g #h #hlift #c1 #c2 #Hfg #Hhlift
+generalize in match c1; elim k
+[#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
+|#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
+ cases (true_or_false (h c0)) #Hc0 >Hfg >Hc0
+ [ normalize #Heq destruct (Heq) %
+ | normalize <Hhlift // @IH ]
+qed.
+
+(* 
 lemma loop_liftL : ∀sig,k,M1,M2,c1,c2.
   loop ? k (step sig M1) (λc.halt sig M1 (cstate ?? c)) c1 = Some ? c2 →
     loop ? k (step sig (seq sig M1 M2)) 
@@ -292,6 +307,8 @@ elim k
    | <Hc0 cases c0 // ]
  ]
 qed.  
+
+*)
     
 lemma loop_Some : 
   ∀A,k,f,p,a,b.loop A k f p a = Some ? b → p b = true.
@@ -329,18 +346,26 @@ cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
 cases (HR2 (ctape sig (states ? M1) outc1)) #k2 * #outc2 * #Hloop2 #HM2
 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
 %
-[@(loop_split ??????????? (loop_liftL … Hloop1))
- [* *
+[@(loop_split ??????????? 
+   (loop_lift ??? (lift_confL sig (states sig M1) (states sig M2))
+   (step sig M1) (step sig (seq sig M1 M2)) 
+   (λ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) ]
- ||4:cases outc1 #s1 #t1 %
- |5:@(loop_liftR … Hloop2) 
- |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
-  generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10 
-  >(trans_liftL_true sig M1 M2 ??) 
-  [ whd in ⊢ (??%?); whd in ⊢ (???%);
-    @config_eq //
-  | @(loop_Some ?????? Hloop10) ]
+  || #c0 #Hhalt <step_lift_confL //
+  | #x <p_halt_liftL %
+  |6:cases outc1 #s1 #t1 %
+  |7:@(loop_lift … (initc ?? (ctape … outc1)) … Hloop2) 
+    [ * #s2 #t2 %
+    | #c0 #Hhalt <step_lift_confR // ]
+  |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
+   generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10 
+   >(trans_liftL_true sig M1 M2 ??) 
+    [ whd in ⊢ (??%?); whd in ⊢ (???%);
+      @config_eq whd in ⊢ (???%); //
+    | @(loop_Some ?????? Hloop10) ]
  ]
 | @(ex_intro … (ctape ? (FinSum (states ? M1) (states ? M2)) (lift_confL … outc1)))
   % // >eq_ctape_lift_conf_L >eq_ctape_lift_conf_R //
-- 
2.39.2