From 70279506c9837750cccf925dc9840b0b3d9951a5 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 7 May 2012 13:13:32 +0000
Subject: [PATCH] Prove di terminazione

---
 matita/matita/lib/turing/mono.ma              | 11 +++-
 .../lib/turing/universal/move_char_c.ma       | 26 ++++++++++
 matita/matita/lib/turing/while_machine.ma     | 50 +++++++++++++++++++
 3 files changed, 86 insertions(+), 1 deletion(-)

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index fae3c7673..a9092336d 100644
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -239,7 +239,16 @@ definition WRealize ≝ λsig.λM:TM sig.λR:relation (tape sig).
 ∀t,i,outc.
   loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc → 
   R t (ctape ?? outc).
-  
+
+definition Terminate ≝ λsig.λM:TM sig.λt. ∃i,outc.
+  loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc.
+
+lemma WRealize_to_Realize : ∀sig.∀M: TM sig.∀R.
+  (∀t.Terminate sig M t) → WRealize sig M R → Realize sig M R.
+#sig #M #R #HT #HW #t cases (HT … t) #i * #outc #Hloop 
+@(ex_intro … i) @(ex_intro … outc) % // @(HW … i) //
+qed.
+
 lemma loop_eq : ∀sig,f,q,i,j,a,x,y. 
   loop sig i f q a = Some ? x → loop sig j f q a = Some ? y → x = y.
 #sig #f #q #i #j @(nat_elim2 … i j)
diff --git a/matita/matita/lib/turing/universal/move_char_c.ma b/matita/matita/lib/turing/universal/move_char_c.ma
index 685f32782..6bd3cef9b 100644
--- a/matita/matita/lib/turing/universal/move_char_c.ma
+++ b/matita/matita/lib/turing/universal/move_char_c.ma
@@ -228,4 +228,30 @@ lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%]
       >reverse_cons >associative_append @IH //
     ]
   ]
+qed.
+
+lemma terminate_move_char_c :
+  ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha (a::ls) b rs →  
+  (b = sep ∨ memb ? sep rs = true) → Terminate alpha (move_char_c alpha sep) t.
+#alpha #sep #t #b #a #ls #rs #Ht #Hsep
+@(terminate_while … (sem_mcc_step alpha sep))
+  [%
+  |generalize in match Hsep; -Hsep
+   generalize in match Ht; -Ht
+   generalize in match ls; -ls
+   generalize in match a; -a
+   generalize in match b; -b
+   generalize in match t; -t
+   elim rs 
+    [#t #b #a #ls #Ht #Hsep % #tinit 
+     whd in ⊢ (%→?); #H @False_ind
+     cases (H … Ht) #Hb #_ cases Hb #eqb @eqb 
+     cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
+    |#r0 #rs0 #Hind #t #b #a #ls #Ht #Hsep % #tinit
+     whd in ⊢ (%→?); #H 
+     cases (H … Ht) #Hbsep #Htinit
+     @(Hind … Htinit) cases Hsep 
+      [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
+        [#eqsep %1 >(\P eqsep) // | #H %2 //]
+  ]
 qed.
\ No newline at end of file
diff --git a/matita/matita/lib/turing/while_machine.ma b/matita/matita/lib/turing/while_machine.ma
index 52a0a79b7..d57824644 100644
--- a/matita/matita/lib/turing/while_machine.ma
+++ b/matita/matita/lib/turing/while_machine.ma
@@ -61,6 +61,12 @@ lemma halt_while_acc :
 cases (halt sig M acc) %
 qed.
 
+lemma halt_while_not_acc : 
+  ∀sig,M,acc,s.s == acc = false → halt sig (whileTM sig M acc) s = halt sig M s.
+#sig #M #acc #s #neqs normalize >neqs 
+cases (halt sig M s) %
+qed.
+
 lemma step_while_acc :
  ∀sig,M,acc,c.cstate ?? c = acc → 
    step sig (whileTM sig M acc) c = initc … (ctape ?? c).
@@ -123,6 +129,50 @@ cases (loop_split ?? (λc. halt sig M (cstate ?? c)) ????? Hloop)
  ]
 qed.
 
+theorem terminate_while: ∀sig,M,acc,Rtrue,Rfalse,t.
+  halt sig M acc = true →
+  accRealize sig M acc Rtrue Rfalse → 
+  WF ? (inv … Rtrue) t → Terminate sig (whileTM sig M acc) t.
+#sig #M #acc #Rtrue #Rfalse #t #Hacctrue #HM #HWF elim HWF
+#t1 #H #Hind cases (HM … t1) #i * #outc * * #Hloop
+#Htrue #Hfalse cases (true_or_false (cstate … outc == acc)) #Hcase
+  [cases (Hind ? (Htrue … (\P Hcase))) #iwhile * #outcfinal
+   #Hloopwhile @(ex_intro … (i+iwhile)) 
+   @(ex_intro … outcfinal) @(loop_merge … outc … Hloopwhile)
+    [@(λc.halt sig M (cstate … c))
+    |* #s0 #t0 normalize cases (s0 == acc) normalize
+     [ cases (halt sig M s0) // 
+     | cases (halt sig M s0) normalize //
+     ]
+    |@(loop_lift ?? i (λc.c) ? 
+                (step ? (whileTM ? M acc)) ? 
+                (λc.halt sig M (cstate ?? c)) ?? 
+                ?? Hloop)
+     [ #x %
+     | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
+       [%
+       |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
+     ]
+   |@step_while_acc @(\P Hcase)
+   |>(\P Hcase) @halt_while_acc
+   ]
+ |@(ex_intro … i) @(ex_intro … outc)
+  @(loop_lift_acc ?? i (λc.c) ?????? (λc.cstate ?? c == acc) ???? Hloop)
+   [#x #Hx >(\P Hx) //
+   |#x @halt_while_not_acc
+   |#x #H whd in ⊢ (??%%); >while_trans_false [%]
+    % #eqx >eqx in H; >Hacctrue #H destruct
+   |@Hcase
+   ]
+ ]
+qed.
+
+(*
+axiom terminate_while: ∀sig,M,acc,Rtrue,Rfalse,t.
+  halt sig M acc = true →
+  accRealize sig M acc Rtrue Rfalse → 
+  ∃t1. Rfalse t t1 → Terminate sig (whileTM sig M acc) t.
+*)
 
 (* (*
 
-- 
2.39.2