From 64a752136a679bcab14a9cd01823c18b7cc991de Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 14 Jan 2013 11:46:18 +0000 Subject: [PATCH] Closed some daemons --- .../lib/turing/multi_universal/compare.ma | 12 +++--- .../lib/turing/multi_universal/match.ma | 39 +++++++++++-------- .../lib/turing/multi_universal/moves.ma | 6 --- .../lib/turing/multi_universal/moves_2.ma | 3 -- 4 files changed, 27 insertions(+), 33 deletions(-) diff --git a/matita/matita/lib/turing/multi_universal/compare.ma b/matita/matita/lib/turing/multi_universal/compare.ma index 423a5af33..501b7bc77 100644 --- a/matita/matita/lib/turing/multi_universal/compare.ma +++ b/matita/matita/lib/turing/multi_universal/compare.ma @@ -155,24 +155,21 @@ lapply (refl ? (current ? (nth i ? int (niltape ?)))) cases (current ? (nth i ? int (niltape ?))) in ⊢ (???%→?); [ #Hcuri %{2} % [| % [ % - [ whd in ⊢ (??%?); >comp_q0_q2_null /2/ % comp_q0_q2_null /2/ | normalize in ⊢ (%→?); #H destruct (H) ] | #_ % // % %2 // ] ] | #a #Ha lapply (refl ? (current ? (nth j ? int (niltape ?)))) cases (current ? (nth j ? int (niltape ?))) in ⊢ (???%→?); [ #Hcurj %{2} % [| % [ % - [ whd in ⊢ (??%?); >comp_q0_q2_null /2/ %2 comp_q0_q2_null /2/ %2 | normalize in ⊢ (%→?); #H destruct (H) ] | #_ % // >Ha >Hcurj % % % #H destruct (H) ] ] | #b #Hb %{2} cases (true_or_false (a == b)) #Hab [ % [| % [ % [whd in ⊢ (??%?); >(comp_q0_q1 … a Hneq Hi Hj) // - [>(\P Hab) (\P Hab) (\P Hab) %{b} % // % // <(\P Hab) // ] | * #H @False_ind @H % ] ] @@ -293,5 +290,6 @@ qed. lemma sem_compare : ∀i,j,sig,n. i ≠ j → i < S n → j < S n → compare i j sig n ⊨ R_compare i j sig n. -#i #j #sig #n #Hneq #Hi #Hj @WRealize_to_Realize /2/ +#i #j #sig #n #Hneq #Hi #Hj @WRealize_to_Realize + [/2/| @wsem_compare // ] qed. diff --git a/matita/matita/lib/turing/multi_universal/match.ma b/matita/matita/lib/turing/multi_universal/match.ma index 38dba8d72..da7481f5e 100644 --- a/matita/matita/lib/turing/multi_universal/match.ma +++ b/matita/matita/lib/turing/multi_universal/match.ma @@ -124,6 +124,7 @@ definition R_rewind ≝ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n). ∀ls0,y,rs0.nth dst ? int (niltape ?) = midtape sig ls0 y rs0 → outt = int). +(* theorem accRealize_to_Realize : ∀sig,n.∀M:mTM sig n.∀Rtrue,Rfalse,acc. M ⊨ [ acc: Rtrue, Rfalse ] → M ⊨ Rtrue ∪ Rfalse. @@ -133,6 +134,7 @@ cases (HR t) #k * #outc * * #Hloop cases (true_or_false (cstate sig (states sig n M) n outc == acc)) #Hcase [ % @Htrue @(\P Hcase) | %2 @Hfalse @(\Pf Hcase) ] qed. +*) lemma sem_rewind : ∀src,dst,sig,n. src ≠ dst → src < S n → dst < S n → @@ -239,16 +241,13 @@ lemma sem_match_step : [ #ta #tb #tc * lapply (refl ? (current ? (nth src ? ta (niltape ?)))) cases (current ? (nth src ? ta (niltape ?))) in ⊢ (???%→%); [ #Hcurta_src #Hcomp #_ * #td * >Hcomp [| % %2 %] - whd in ⊢ (%→?); * whd in ⊢ (??%?→?); - >(?:nth src ? (current_chars ?? ta) (None ?) = None ?) - [ normalize in ⊢ (%→?); #H destruct (H) - | @daemon ] + whd in ⊢ (%→?); * whd in ⊢ (??%?→?); + >nth_current_chars >Hcurta_src normalize in ⊢ (%→?); #H destruct (H) | #s #Hs lapply (refl ? (current ? (nth dst ? ta (niltape ?)))) cases (current ? (nth dst ? ta (niltape ?))) in ⊢ (???%→%); [ #Hcurta_dst #Hcomp #_ * #td * >Hcomp [| %2 %] - whd in ⊢ (%→?); * whd in ⊢ (??%?→?); - >(?:nth src ? (current_chars ?? ta) (None ?) = Some ? s) [|@daemon] - >(?:nth dst ? (current_chars ?? ta) (None ?) = None ?) [|@daemon] + whd in ⊢ (%→?); * whd in ⊢ (??%?→?); + >nth_current_chars >nth_current_chars >Hs >Hcurta_dst normalize in ⊢ (%→?); #H destruct (H) | #s0 #Hs0 cases (current_to_midtape … Hs) #ls * #rs #Hmidta_src >Hmidta_src @@ -257,11 +256,15 @@ lemma sem_match_step : [ lapply (\P Hss0) -Hss0 #Hss0 destruct (Hss0) #_ #Hcomp cases (Hcomp ????? (refl ??) (refl ??)) -Hcomp [ * [ * #rs' * #_ #Hcurtc_dst * #td * whd in ⊢ (%→?); * whd in ⊢ (??%?→?); - >(?:nth dst ? (current_chars ?? tc) (None ?) = None ?) [|@daemon] - cases (nth src ? (current_chars ?? tc) (None ?)) - [| #x ] normalize in ⊢ (%→?); #H destruct (H) + >nth_current_chars >nth_current_chars >Hcurtc_dst + cases (current ? (nth src …)) [| #x ] + normalize in ⊢ (%→?); #H destruct (H) | * #rs0' * #_ #Hcurtc_src * #td * whd in ⊢ (%→?); * whd in ⊢ (??%?→?); - >(?:nth src ? (current_chars ?? tc) (None ?) = None ?) [|@daemon] + >(?:nth src ? (current_chars ?? tc) (None ?) = None ?) + [|>nth_current_chars >Hcurtc_src >nth_change_vec_neq + [>nth_change_vec [cases (append ???) // | @Hsrc] + |@(not_to_not … Hneq) // + ]] normalize in ⊢ (%→?); #H destruct (H) ] | * #xs * #ci * #cj * #rs'' * #rs0' * * * #Hcicj #Hrs #Hrs0 #Htc * #td * * #Hmatch #Htd destruct (Htd) * #te * * @@ -310,18 +313,20 @@ lemma sem_match_step : | >(?:tc=ta) in Htest; [|@Hcomp1 % % >Hta_src >Hta_dst @(not_to_not ??? (\Pf Hxx0)) normalize #Hxx0' destruct (Hxx0') % ] - whd in ⊢ (??%?→?); >(?:nth src ? (current_chars ?? ta) (None ?) = Some ? x) - [| @daemon ] - >(?:nth dst ? (current_chars ?? ta) (None ?) = Some ? x0) [|@daemon] + whd in ⊢ (??%?→?); + >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'} % // % // | * #rs0' * #Hxs #Htc %2 >Htc %{ls0} %{rs0'} % // ] | * #xs0 * #ci * #cj * #rs' * #rs0' * * * #Hci #Hxs #Hrs0 #Htc @False_ind - whd in Htest:(??%?); - >(?:nth src ? (current_chars ?? tc) (None ?) = Some ? ci) in Htest; [|@daemon] - >(?:nth dst ? (current_chars ?? tc) (None ?) = Some ? cj) [|@daemon] + whd in Htest:(??%?); + >(?:nth src ? (current_chars ?? tc) (None ?) = Some ? ci) in Htest; + [|>nth_current_chars >Htc >nth_change_vec_neq [|@(not_to_not … Hneq) //] + >nth_change_vec //] + >(?:nth dst ? (current_chars ?? tc) (None ?) = Some ? cj) + [|>nth_current_chars >Htc >nth_change_vec //] normalize #H destruct (H) ] ] ] qed. diff --git a/matita/matita/lib/turing/multi_universal/moves.ma b/matita/matita/lib/turing/multi_universal/moves.ma index df620b352..f725a1940 100644 --- a/matita/matita/lib/turing/multi_universal/moves.ma +++ b/matita/matita/lib/turing/multi_universal/moves.ma @@ -159,14 +159,12 @@ cases (current ? (nth src ? int (niltape ?))) in ⊢ (???%→?); [ #Hcursrc %{2} % [| % [ % [ whd in ⊢ (??%?); >parmove_q0_q2_null_src /2/ - <(nth_vec_map ?? (current …) src ? int (niltape ?)) // | normalize in ⊢ (%→?); #H destruct (H) ] | #_ % // % %2 // ] ] | #a #Ha cases (true_or_false (is_sep a)) #Hsep [ %{2} % [| % [ % [ whd in ⊢ (??%?); >(parmove_q0_q2_sep … Hsep) /2/ - <(nth_vec_map ?? (current …) src ? int (niltape ?)) // | normalize in ⊢ (%→?); #H destruct (H) ] | #_ % // % % %{a} % // ] ] | lapply (refl ? (current ? (nth dst ? int (niltape ?)))) @@ -174,15 +172,11 @@ cases (current ? (nth src ? int (niltape ?))) in ⊢ (???%→?); [ #Hcurdst %{2} % [| % [ % [ whd in ⊢ (??%?); >(parmove_q0_q2_null_dst … Hsep) /2/ - [ <(nth_vec_map ?? (current …) dst ? int (niltape ?)) // - | <(nth_vec_map ?? (current …) src ? int (niltape ?)) // ] | normalize in ⊢ (%→?); #H destruct (H) ] | #_ % // %2 // ] ] | #b #Hb %{2} % [| % [ % [whd in ⊢ (??%?); >(parmove_q0_q1 … Hneq Hsrc Hdst ? b ?? Hsep) // - [ <(nth_vec_map ?? (current …) dst ? int (niltape ?)) // - | <(nth_vec_map ?? (current …) src ? int (niltape ?)) // ] | #_ %{a} %{b} % // % // % // ] | * #H @False_ind @H % ] ]]]] diff --git a/matita/matita/lib/turing/multi_universal/moves_2.ma b/matita/matita/lib/turing/multi_universal/moves_2.ma index 072d3a15a..14f072b4e 100644 --- a/matita/matita/lib/turing/multi_universal/moves_2.ma +++ b/matita/matita/lib/turing/multi_universal/moves_2.ma @@ -137,7 +137,6 @@ cases (current ? (nth src ? int (niltape ?))) in ⊢ (???%→?); [ #Hcursrc %{2} % [| % [ % [ whd in ⊢ (??%?); >parmove_q0_q2_null_src /2/ - <(nth_vec_map ?? (current …) src ? int (niltape ?)) // | normalize in ⊢ (%→?); #H destruct (H) ] | #_ % // % // ] ] | #a #Ha lapply (refl ? (current ? (nth dst ? int (niltape ?)))) @@ -145,8 +144,6 @@ cases (current ? (nth src ? int (niltape ?))) in ⊢ (???%→?); [ #Hcurdst %{2} % [| % [ % [ whd in ⊢ (??%?); >(parmove_q0_q2_null_dst …) /2/ - [ <(nth_vec_map ?? (current …) dst ? int (niltape ?)) // - | <(nth_vec_map ?? (current …) src ? int (niltape ?)) // ] | normalize in ⊢ (%→?); #H destruct (H) ] | #_ % // %2 // ] ] | #b #Hb %{2} % -- 2.39.2