From 0f08d4f03129147e75fe91fd850249d5e8e09ac8 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Mon, 14 Jan 2013 15:14:11 +0000 Subject: [PATCH] advancement in match --- .../lib/turing/multi_universal/compare.ma | 26 ++++++++-- .../lib/turing/multi_universal/match.ma | 49 ++++++++++--------- 2 files changed, 48 insertions(+), 27 deletions(-) diff --git a/matita/matita/lib/turing/multi_universal/compare.ma b/matita/matita/lib/turing/multi_universal/compare.ma index 501b7bc77..8ad92d1e8 100644 --- a/matita/matita/lib/turing/multi_universal/compare.ma +++ b/matita/matita/lib/turing/multi_universal/compare.ma @@ -189,6 +189,17 @@ qed. definition compare ≝ λi,j,sig,n. whileTM … (compare_step i j sig n) comp1. +(* (∃rs'.rs = rs0@rs' ∧ current ? (nth j ? outt (niltape ?)) = None ?) ∨ + (∃rs0'.rs0 = rs@rs0' ∧ + outt = change_vec ?? + (change_vec ?? int + (mk_tape sig (reverse sig rs@x::ls) (None sig) []) i) + (mk_tape sig (reverse sig rs@x::ls0) (option_hd sig rs0') + (tail sig rs0')) j) ∨ + (∃xs,ci,cj,rs',rs0'.ci ≠ cj ∧ rs = xs@ci::rs' ∧ rs0 = xs@cj::rs0' ∧ + outt = change_vec ?? + (change_vec ?? int (midtape sig (reverse ? xs@x::ls) ci rs') i) + (midtape sig (reverse ? xs@x::ls0) cj rs0') j)).*) definition R_compare ≝ λi,j,sig,n.λint,outt: Vector (tape sig) (S n). ((current ? (nth i ? int (niltape ?)) ≠ current ? (nth j ? int (niltape ?)) ∨ @@ -198,7 +209,11 @@ definition R_compare ≝ (* nth i ? int (niltape ?) = midtape sig ls x (xs@ci::rs) → *) nth i ? int (niltape ?) = midtape sig ls x rs → nth j ? int (niltape ?) = midtape sig ls0 x rs0 → - (∃rs'.rs = rs0@rs' ∧ current ? (nth j ? outt (niltape ?)) = None ?) ∨ + (∃rs'.rs = rs0@rs' ∧ + outt = change_vec ?? + (change_vec ?? int + (mk_tape sig (reverse sig rs0@x::ls) (option_hd sig rs') (tail ? rs')) i) + (mk_tape sig (reverse sig rs0@x::ls0) (None ?) [ ]) j) ∨ (∃rs0'.rs0 = rs@rs0' ∧ outt = change_vec ?? (change_vec ?? int @@ -208,7 +223,7 @@ definition R_compare ≝ (∃xs,ci,cj,rs',rs0'.ci ≠ cj ∧ rs = xs@ci::rs' ∧ rs0 = xs@cj::rs0' ∧ outt = change_vec ?? (change_vec ?? int (midtape sig (reverse ? xs@x::ls) ci rs') i) - (midtape sig (reverse ? xs@x::ls0) cj rs0') j)). + (midtape sig (reverse ? xs@x::ls0) cj rs0') j)). lemma wsem_compare : ∀i,j,sig,n.i ≠ j → i < S n → j < S n → compare i j sig n ⊫ R_compare i j sig n. @@ -242,14 +257,17 @@ lapply (sem_while … (sem_comp_step i j sig n Hneq Hi Hj) … Hloop) // [ -IH2 #Hnthj % % %{(r1::rs1)} % [%] >Hnthj in Hd; #Hd >Hd in IH1; #IH1 >IH1 [| %2 >nth_change_vec // ] - >nth_change_vec // + >Hnthi >Hnthj % | #r2 #rs2 #Hnthj lapply IH2; >Hd in IH1; >Hnthi >Hnthj >nth_change_vec // >nth_change_vec_neq [| @sym_not_eq // ] >nth_change_vec // cases (true_or_false (r1 == r2)) #Hr1r2 [ >(\P Hr1r2) #_ #IH2 cases (IH2 … (refl ??) (refl ??)) [ * [ * #rs' * #Hrs1 #Hcurout_j % % %{rs'} - >Hrs1 >Hcurout_j normalize % // + >Hrs1 % + [ % + | >Hcurout_j >change_vec_commute // >change_vec_change_vec + >change_vec_commute // @sym_not_eq // ] | * #rs0' * #Hrs2 #Hcurout_i % %2 %{rs0'} >Hrs2 >Hcurout_i % // >change_vec_commute // >change_vec_change_vec diff --git a/matita/matita/lib/turing/multi_universal/match.ma b/matita/matita/lib/turing/multi_universal/match.ma index da7481f5e..3417463a4 100644 --- a/matita/matita/lib/turing/multi_universal/match.ma +++ b/matita/matita/lib/turing/multi_universal/match.ma @@ -192,7 +192,9 @@ definition R_match_step_false ≝ ((current sig (nth dst (tape sig) int (niltape sig)) = None ?) ∧ outt = int) ∨ (∃ls0,rs0,xs0. nth dst ? int (niltape ?) = midtape sig ls0 x rs0 ∧ xs = rs0@xs0 ∧ - current sig (nth dst (tape sig) outt (niltape sig)) = None ?) ∨ + outt = change_vec ?? + (change_vec ?? int (mk_tape sig (reverse ? rs0@x::ls) (option_hd ? xs0) (tail ? xs0)) src) + (mk_tape ? (reverse ? rs0@x::ls0) (None ?) [ ]) dst) ∨ (∃ls0,rs0. nth dst ? int (niltape ?) = midtape sig ls0 x (xs@rs0) ∧ (* ∀rsj,c. @@ -257,8 +259,11 @@ lemma sem_match_step : #_ #Hcomp cases (Hcomp ????? (refl ??) (refl ??)) -Hcomp [ * [ * #rs' * #_ #Hcurtc_dst * #td * whd in ⊢ (%→?); * whd in ⊢ (??%?→?); >nth_current_chars >nth_current_chars >Hcurtc_dst - cases (current ? (nth src …)) [| #x ] - normalize in ⊢ (%→?); #H destruct (H) + cases (current ? (nth src …)) + [normalize in ⊢ (%→?); #H destruct (H) + | #x >nth_change_vec // cases (reverse ? rs0) + [ normalize in ⊢ (%→?); #H destruct (H) + | #r1 #rs1 normalize in ⊢ (%→?); #H destruct (H) ] ] | * #rs0' * #_ #Hcurtc_src * #td * whd in ⊢ (%→?); * whd in ⊢ (??%?→?); >(?:nth src ? (current_chars ?? tc) (None ?) = None ?) [|>nth_current_chars >Hcurtc_src >nth_change_vec_neq @@ -317,7 +322,8 @@ lemma sem_match_step : >nth_current_chars >Hta_src >nth_current_chars >Hta_dst whd in ⊢ (??%?→?); #Hfalse destruct (Hfalse) ] -Hcomp1 cases (Hcomp2 … Hta_src Hta_dst) [ * - [ * #rs' * #Hxs #Hcurtc % %2 %{ls0} %{rs0} %{rs'} % // % // + [ * #rs' * #Hxs #Hcurtc % %2 %{ls0} %{rs0} %{rs'} % + [ % // | >Hcurtc % ] | * #rs0' * #Hxs #Htc %2 >Htc %{ls0} %{rs0'} % // ] | * #xs0 * #ci * #cj * #rs' * #rs0' * * * #Hci #Hxs #Hrs0 #Htc @False_ind @@ -379,10 +385,12 @@ lapply (sem_while … (sem_match_step src dst sig n Hneq Hsrc Hdst) … Hloop) / | * #ls0 * #rs0 * #xs0 * * #Htc_dst #Hrs0 #HNone % [ >Htc_dst normalize in ⊢ (%→?); #H destruct (H) | #ls1 #x1 #rs1 >Htc_dst #H destruct (H) - >Hrs0 cases xs0 + >Hrs0 >HNone cases xs0 [ % %{[ ]} %{[ ]} % [ >append_nil >append_nil %] - (* change false case - #cj #ls2 #H destruct (H) *) @daemon + @eq_f3 // + [ >reverse_append % + | >reverse_append >reverse_cons >reverse_append + >associative_append >associative_append % ] | #x2 #xs2 %2 #l #l1 % #Habs lapply (eq_f ?? (length ?) ?? Habs) >length_append whd in ⊢ (??%(??%)→?); >length_append >length_append normalize >commutative_plus whd in ⊢ (???%→?); @@ -474,29 +482,24 @@ lapply (sem_while … (sem_match_step src dst sig n Hneq Hsrc Hdst) … Hloop) / 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. + λsrc,sig,n.λt: Vector (tape sig) (S n). + ∃x,xs. + nth src (tape sig) t (niltape sig) = midtape ? [] x xs. lemma terminate_match_m : - ∀src,dst,sig,n,is_startc,is_endc,t. + ∀src,dst,sig,n,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)) // + Pre_match_m src sig n t → + match_m src dst sig n ↓ t. +#src #dst #sig #n #t #Hneq #Hsrc #Hdst * #start * #xs +#Hmid_src +@(terminate_while … (sem_match_step src dst sig n 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 % + >Hmid_src #HR cases (HR ?? (refl ??)) -HR + >nth_change_vec // >Htape_dst | #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 ⊢ (%→?); -- 2.39.2