match termination

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

diff --git a/matita/matita/lib/turing/multi_universal/match.ma b/matita/matita/lib/turing/multi_universal/match.ma
index ff31367f72edfd37d0d0438ca41c27feed5dbfb1..d05a8c35a4bb2dec46b1a65b566d908605f72e24 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/match.ma
+++ b/matita/matita/lib/turing/multi_universal/match.ma
@@ -579,4 +579,110 @@ lapply (sem_while … (sem_match_step src dst sig n is_startc is_endc Hneq Hsrc
     ]
   ]
 ]
+qed.
+
+definition Pre_match_m ≝ 
+  λsrc,sig,n,is_startc,is_endc.λt: Vector (tape sig) (S n).
+  ∃start,xs,end.
+  nth src (tape sig) t (niltape sig) = midtape ? [] start (xs@[end]) ∧
+  is_startc start = true ∧
+  (∀c.c ∈ (xs@[end]) = true → is_startc c = false) ∧
+  (∀c.c ∈ (start::xs) = true → is_endc c = false) ∧
+  is_endc end = true.
+  
+lemma terminate_match_m :
+  ∀src,dst,sig,n,is_startc,is_endc,t.
+  src ≠ dst → src < S n → dst < S n → 
+  Pre_match_m src sig n is_startc is_endc t → 
+  match_m src dst sig n is_startc is_endc ↓ t.
+#src #dst #sig #n #is_startc #is_endc #t #Hneq #Hsrc #Hdst * #start * #xs * #end
+* * * * #Hmid_src #Hstart #Hnotstart #Hnotend #Hend
+@(terminate_while … (sem_match_step src dst sig n is_startc is_endc Hneq Hsrc Hdst)) //
+<(change_vec_same … t dst (niltape ?))
+lapply (refl ? (nth dst (tape sig) t (niltape ?))) 
+cases (nth dst (tape sig) t (niltape ?)) in ⊢ (???%→?);
+[ #Htape_dst % #t1 whd in ⊢ (%→?); >nth_change_vec_neq [|@sym_not_eq //]
+  >Hmid_src #HR cases (HR ? (refl ??)) -HR
+  >nth_change_vec // >Htape_dst normalize in ⊢ (%→?);
+  * #H @False_ind @H %
+| #x0 #xs0 #Htape_dst % #t1 whd in ⊢ (%→?); >nth_change_vec_neq [|@sym_not_eq //]
+  >Hmid_src #HR cases (HR ? (refl ??)) -HR
+  >nth_change_vec // >Htape_dst normalize in ⊢ (%→?);
+  * #H @False_ind @H %
+| #x0 #xs0 #Htape_dst % #t1 whd in ⊢ (%→?); >nth_change_vec_neq [|@sym_not_eq //]
+  >Hmid_src #HR cases (HR ? (refl ??)) -HR
+  >nth_change_vec // >Htape_dst normalize in ⊢ (%→?);
+  * #H @False_ind @H %
+| #ls #s #rs lapply s -s lapply ls -ls lapply Hmid_src lapply t -t elim rs
+  [#t #Hmid_src #ls #s #Hmid_dst % #t1 whd in ⊢ (%→?); >nth_change_vec_neq [|@sym_not_eq //]
+   >Hmid_src >nth_change_vec // >Hmid_dst #HR cases (HR ? (refl ??)) -HR #_
+   #HR cases (HR Hstart Hnotstart)
+   cases (true_or_false (start == s)) #Hs
+   [ lapply (\P Hs) -Hs #Hs <Hs #_ #Htrue
+     cut (∃ci,xs1.xs@[end] = ci::xs1)
+     [ cases xs
+       [ %{end} %{[]} %
+       | #x1 #xs1 %{x1} %{(xs1@[end])} % ] ] * #ci * #xs1 #Hxs
+     >Hxs in Htrue; #Htrue
+     cases (Htrue [ ] start [ ] ? xs1 ? [ ] (refl ??) (refl ??) ?)
+     [ * #_ * #H @False_ind @H % ]
+     #c0 #Hc0 @Hnotend >(memb_single … Hc0) @memb_hd
+   | lapply (\Pf Hs) -Hs #Hs #Htrue #_
+     cases (Htrue ? (refl ??) Hs) -Htrue #Ht1 #_ %
+     #t2 whd in ⊢ (%→?); #HR cases (HR start ?)
+     [ >Ht1 >nth_change_vec // normalize in ⊢ (%→?); * #H @False_ind @H %
+     | >Ht1 >nth_change_vec_neq [|@sym_not_eq //]
+       >nth_change_vec_neq [|@sym_not_eq //] >Hmid_src % ]
+   ]
+  |#r0 #rs0 #IH #t #Hmid_src #ls #s #Hmid_dst % #t1 whd in ⊢ (%→?);
+   >nth_change_vec_neq [|@sym_not_eq //] >Hmid_src
+   #Htrue cases (Htrue ? (refl ??)) -Htrue #_ #Htrue
+   <(change_vec_same … t1 dst (niltape ?))
+   cases (Htrue Hstart Hnotstart) -Htrue
+   cases (true_or_false (start == s)) #Hs
+   [ lapply (\P Hs) -Hs #Hs <Hs #_ #Htrue
+    cut (∃ls0,xs0,ci,rs,rs0.
+      nth src ? t (niltape ?) = midtape sig [ ] start (xs0@ci::rs) ∧
+      nth dst ? t (niltape ?) = midtape sig ls0 s (xs0@rs0) ∧
+      (is_endc ci = true ∨ (is_endc ci = false ∧ (∀b,tlb.rs0 = b::tlb → ci ≠ b))))
+    [cases (comp_list ? (xs@[end]) (r0::rs0) is_endc) #xs0 * #xs1 * #xs2
+      * * * #Hxs #Hrs #Hxs0notend #Hcomp >Hrs
+      cut (∃y,ys. xs1 = y::ys)
+      [ lapply Hxs0notend lapply Hxs lapply xs0 elim xs
+        [ *
+          [ normalize #Hxs1 <Hxs1 #_ %{end} %{[]} %
+          | #z #zs normalize in ⊢ (%→?); #H destruct (H) #H
+            lapply (H ? (memb_hd …)) -H >Hend #H1 destruct (H1)
+          ]
+        | #y #ys #IH0 * 
+          [ normalize in ⊢ (%→?); #Hxs1 <Hxs1 #_ %{y} %{(ys@[end])} %
+          | #z #zs normalize in ⊢ (%→?); #H destruct (H) #Hmemb
+            @(IH0 ? e0 ?) #c #Hc @Hmemb @memb_cons // ] ] ] * #y * #ys #Hxs1
+      >Hxs1 in Hxs; #Hxs >Hmid_src >Hmid_dst >Hxs >Hrs
+      %{ls} %{xs0} %{y} %{ys} %{xs2}
+      % [ % // | @Hcomp // ] ]
+    * #ls0 * #xs0 * #ci * #rs * #rs0 * * #Hmid_src' #Hmid_dst' #Hcomp
+    <Hmid_src in Htrue; >nth_change_vec // >Hs #Htrue destruct (Hs)
+    lapply (Htrue ??????? Hmid_src' Hmid_dst' ?) -Htrue
+    [ #c0 #Hc0 @Hnotend cases (orb_true_l … Hc0) -Hc0 #Hc0
+      [ whd in ⊢ (??%?); >Hc0 %
+      | @memb_cons >Hmid_src in Hmid_src'; #Hmid_src' destruct (Hmid_src')
+        lapply e0 -e0 @(list_elim_left … rs)
+        [ #e0 destruct (e0) lapply (append_l1_injective_r ?????? e0) //
+        | #x1 #xs1 #_ >append_cons in ⊢ (???%→?);
+          <associative_append #e0 lapply (append_l1_injective_r ?????? e0) //
+          #e1 >e1 @memb_append_l1 @memb_append_l1 // ] ]
+    | * * #Hciendc cases rs0 in Hcomp;
+      [ #_ * #H @False_ind @H %
+      | #r1 #rs1 * [ >Hciendc #H destruct (H) ]
+        * #_ #Hcomp lapply (Hcomp ?? (refl ??)) -Hcomp #Hcomp #_ #Htrue
+        cases (Htrue ?? (refl ??) Hcomp) #Ht1 #_ >Ht1 @(IH ?? (s::ls) r0)
+        [ >nth_change_vec_neq [|@sym_not_eq //]
+          >nth_change_vec_neq [|@sym_not_eq //] @Hmid_src
+        | >nth_change_vec // >Hmid_dst % ] ] ]
+  | >Hmid_dst >nth_change_vec // lapply (\Pf Hs) -Hs #Hs #Htrue #_
+    cases (Htrue ? (refl ??) Hs) #Ht1 #_ >Ht1 @(IH ?? (s::ls) r0)
+    [ >nth_change_vec_neq [|@sym_not_eq //]
+      >nth_change_vec_neq [|@sym_not_eq //] @Hmid_src
+    | >nth_change_vec // ] ] ] ]
 qed.
\ No newline at end of file