From b0d97cd7e2c50fb1fc2d50c86f3140e226b08a81 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 6 Jun 2012 06:18:43 +0000 Subject: [PATCH] Restructuring --- matita/matita/lib/basics/lists/listb.ma | 10 +++ matita/matita/lib/turing/if_machine.ma | 2 +- matita/matita/lib/turing/mono.ma | 4 + matita/matita/lib/turing/universal/copy.ma | 64 --------------- matita/matita/lib/turing/universal/marks.ma | 78 +------------------ .../lib/turing/universal/move_char_l.ma | 6 +- .../matita/lib/turing/universal/move_tape.ma | 2 +- matita/matita/lib/turing/universal/tuples.ma | 21 ++++- .../matita/lib/turing/universal/universal.ma | 6 +- 9 files changed, 44 insertions(+), 149 deletions(-) diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma index ac72b008b..438f3b497 100644 --- a/matita/matita/lib/basics/lists/listb.ma +++ b/matita/matita/lib/basics/lists/listb.ma @@ -103,6 +103,16 @@ lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2. ] qed. +lemma memb_reverse: ∀S:DeqSet.∀a:S.∀l. + memb ? a l = true → memb ? a (reverse ? l) = true. +#S #a #l elim l [normalize //] +#b #tl #Hind #memba change with ([b]@tl) in match (b::tl); +>reverse_append cases (orb_true_l … memba) #Hcase + [@memb_append_l2 >(\P Hcase) whd in match (reverse ??); @memb_hd + |@memb_append_l1 /2/ + ] +qed. + lemma mem_to_memb: ∀S:DeqSet.∀a,l. mem S a l → memb S a l = true. #S #a #l elim l normalize [@False_ind diff --git a/matita/matita/lib/turing/if_machine.ma b/matita/matita/lib/turing/if_machine.ma index 2bc83c261..6248ab7e7 100644 --- a/matita/matita/lib/turing/if_machine.ma +++ b/matita/matita/lib/turing/if_machine.ma @@ -152,7 +152,7 @@ qed. (******************************** semantics ***********************************) lemma sem_if: ∀sig.∀M1,M2,M3:TM sig.∀Rtrue,Rfalse,R2,R3,acc. - M1 ⊧ [acc: Rtrue,Rfalse] → M2 ⊨ R2 → M3 ⊨ R3 → + M1 ⊨ [acc: Rtrue,Rfalse] → M2 ⊨ R2 → M3 ⊨ R3 → ifTM sig M1 M2 M3 acc ⊨ (Rtrue ∘ R2) ∪ (Rfalse ∘ R3). #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HR3 #t cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma index 8d772af34..e559c88db 100644 --- a/matita/matita/lib/turing/mono.ma +++ b/matita/matita/lib/turing/mono.ma @@ -214,6 +214,10 @@ qed. definition loopM ≝ λsig,M,i,cin. loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) cin. +lemma loopM_unfold : ∀sig,M,i,cin. + loopM sig M i cin = loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) cin. +// qed. + definition initc ≝ λsig.λM:TM sig.λt. mk_config sig (states sig M) (start sig M) t. diff --git a/matita/matita/lib/turing/universal/copy.ma b/matita/matita/lib/turing/universal/copy.ma index c6d7e7911..331bf6881 100644 --- a/matita/matita/lib/turing/universal/copy.ma +++ b/matita/matita/lib/turing/universal/copy.ma @@ -12,24 +12,6 @@ include "turing/universal/tuples.ma". -definition write_states ≝ initN 2. - -definition wr0 : write_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)). -definition wr1 : write_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)). - -definition write ≝ λalpha,c. - mk_TM alpha write_states - (λp.let 〈q,a〉 ≝ p in - match pi1 … q with - [ O ⇒ 〈wr1,Some ? 〈c,N〉〉 - | S _ ⇒ 〈wr1,None ?〉 ]) - wr0 (λx.x == wr1). - -definition R_write ≝ λalpha,c,t1,t2. - ∀ls,x,rs.t1 = midtape alpha ls x rs → t2 = midtape alpha ls c rs. - -axiom sem_write : ∀alpha,c.Realize ? (write alpha c) (R_write alpha c). - definition copy_step_subcase ≝ λalpha,c,elseM.ifTM ? (test_char ? (λx.x == 〈c,true〉)) (seq (FinProd alpha FinBool) (adv_mark_r …) @@ -386,52 +368,6 @@ lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop (consequently several lists = []) or not *) * [ * #Ha #Houtc1 -(* cut (l1 = [〈a,false〉]) - [ cases l1'' in Hl1cons; // #y #ly #Hly - >Hly in Hl1; cases l1' in Hl1bits; - [ #_ normalize #Hfalse destruct (Hfalse) - | #p #lp #Hl1bits normalize #Heq destruct (Heq) - @False_ind lapply (Hl1bits 〈a,false〉 ?) - [ cases lp in e0; - [ normalize #Hfalse destruct (Hfalse) - | #p0 #lp0 normalize in ⊢ (%→?); #Heq destruct (Heq) - @memb_cons @memb_hd ] - | >Ha normalize #Hfalse destruct (Hfalse) ] - ] - ] #Hl1a - cut (l4 = [〈a0,false〉]) - [ generalize in match Hl4bits; cases l4' in Hl4; - [ >Hl4cons #Hfalse #_ - lapply (inj_append_singleton_l1 ?? [] ?? Hfalse) - cases (reverse ? l4'') normalize - [ #Hfalse1 | #p0 #lp0 #Hfalse1 ] destruct (Hfalse1) - | #p #lp - - cases l4'' in Hl4cons; // #y #ly #Hly - >Hly in Hl4; cases l4' in Hl4bits; - [ #_ >reverse_cons #Hfalse - lapply (inj_append_singleton_l1 ?? [] ?? Hfalse) - -Hfalse cases ly normalize - [ #Hfalse | #p #Hp #Hfalse ] destruct (Hfalse) - - | #p #lp #Hl1bits normalize #Heq destruct (Heq) - @False_ind lapply (Hl1bits 〈a,false〉 ?) - [ cases lp in e0; - [ normalize #Hfalse destruct (Hfalse) - | #p0 #lp0 normalize in ⊢ (%→?); #Heq destruct (Heq) - @memb_cons @memb_hd ] - | >Ha normalize #Hfalse destruct (Hfalse) ] - ] - ] #Hl1a - - >Hla normalize #Hl1 destruct (Hl1) lapply (inj_append_ @False_ind - - cut (l1'' = [] ∧ l4'' = []) - [ % [ >Hla in Hl1; normalize #Hl1 destruct (Hl1) - - cases l1'' in Hl1bits; - - [ #_ normalize #H *) cut (la = [] ∧ lb = [] ∧ l1'' = [] ∧ l4'' = []) [ @daemon ] * * * #Hla1 #Hlb1 #Hl1nil #Hl4nil >Hl1cons in Hl1; >Hla diff --git a/matita/matita/lib/turing/universal/marks.ma b/matita/matita/lib/turing/universal/marks.ma index 46de2c4d6..13e85c56d 100644 --- a/matita/matita/lib/turing/universal/marks.ma +++ b/matita/matita/lib/turing/universal/marks.ma @@ -14,10 +14,9 @@ *) -include "turing/while_machine.ma". include "turing/if_machine.ma". +include "turing/basic_machines.ma". include "turing/universal/alphabet.ma". -include "turing/universal/tests.ma". (* ADVANCE TO MARK (right) @@ -225,79 +224,6 @@ lemma sem_mark : @ex_intro [| % [ % | #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ] ] ] qed. -(* MOVE RIGHT - - moves the head one step to the right - -*) - -definition move_states ≝ initN 2. -definition move0 : move_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)). -definition move1 : move_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)). - -definition move_r ≝ - λalpha:FinSet.mk_TM alpha move_states - (λp.let 〈q,a〉 ≝ p in - match a with - [ None ⇒ 〈move1,None ?〉 - | Some a' ⇒ match (pi1 … q) with - [ O ⇒ 〈move1,Some ? 〈a',R〉〉 - | S q ⇒ 〈move1,None ?〉 ] ]) - move0 (λq.q == move1). - -definition R_move_r ≝ λalpha,t1,t2. - ∀ls,c,rs. - t1 = midtape alpha ls c rs → - t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs). - -lemma sem_move_r : - ∀alpha.Realize ? (move_r alpha) (R_move_r alpha). -#alpha #intape @(ex_intro ?? 2) cases intape -[ @ex_intro - [| % [ % | #ls #c #rs #Hfalse destruct ] ] -|#a #al @ex_intro - [| % [ % | #ls #c #rs #Hfalse destruct ] ] -|#a #al @ex_intro - [| % [ % | #ls #c #rs #Hfalse destruct ] ] -| #ls #c #rs - @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1) - cases rs0 // ] ] ] -qed. - -(* MOVE LEFT - - moves the head one step to the right - -*) - -definition move_l ≝ - λalpha:FinSet.mk_TM alpha move_states - (λp.let 〈q,a〉 ≝ p in - match a with - [ None ⇒ 〈move1,None ?〉 - | Some a' ⇒ match pi1 … q with - [ O ⇒ 〈move1,Some ? 〈a',L〉〉 - | S q ⇒ 〈move1,None ?〉 ] ]) - move0 (λq.q == move1). - -definition R_move_l ≝ λalpha,t1,t2. - ∀ls,c,rs. - t1 = midtape alpha ls c rs → - t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs). - -lemma sem_move_l : - ∀alpha.Realize ? (move_l alpha) (R_move_l alpha). -#alpha #intape @(ex_intro ?? 2) cases intape -[ @ex_intro - [| % [ % | #ls #c #rs #Hfalse destruct ] ] -|#a #al @ex_intro - [| % [ % | #ls #c #rs #Hfalse destruct ] ] -|#a #al @ex_intro - [| % [ % | #ls #c #rs #Hfalse destruct ] ] -| #ls #c #rs - @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1) - cases ls0 // ] ] ] -qed. (* MOVE RIGHT AND MARK machine @@ -669,7 +595,7 @@ cases (sem_if ? (test_char ? (λx.x == c)) … tc_true | * #Hx0 #Houtc %2 % [ <(\P Hx) in Hx0; #Hx0 lapply (\Pf Hx0) @not_to_not #Hx' >Hx' % | >Houtc % ] - | (* members of lists are invariant under reverse *) @daemon ] + | #x #membx @Hl1 <(reverse_reverse …l1) @memb_reverse @membx ] | %2 % [ @(\Pf Hc) ] >Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hx #Hta >Hx in Hc;#Hc destruct (Hc) ] diff --git a/matita/matita/lib/turing/universal/move_char_l.ma b/matita/matita/lib/turing/universal/move_char_l.ma index bc6e5c4aa..2fa78ec6a 100644 --- a/matita/matita/lib/turing/universal/move_char_l.ma +++ b/matita/matita/lib/turing/universal/move_char_l.ma @@ -146,7 +146,7 @@ lemma sem_mcl_step : [ @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 〈mcl4,sep〉 (midtape ? lt c rt))) % [ % - [ >(\P Hc) >loop_S_false // >loop_S_true + [ >(\P Hc) >loopM_unfold >loop_S_false // >loop_S_true [ @eq_f whd in ⊢ (??%?); >mcl_trans_init_sep % |>(\P Hc) whd in ⊢(??(???(???%))?); >mcl_trans_init_sep % ] |@Hfalse] @@ -154,12 +154,12 @@ lemma sem_mcl_step : |@(ex_intro ?? 4) cases rt [ @ex_intro [|% [ % - [ >loop_S_false // >mcl_q0_q1 // + [ >loopM_unfold >loop_S_false // >mcl_q0_q1 // | normalize in ⊢ (%→?); @Hfalse] | normalize in ⊢ (%→?); #_ #H1 @False_ind @(absurd ?? H1) % ] ] | #r0 #rt0 @ex_intro [| % [ % - [ >loop_S_false // >mcl_q0_q1 // + [ >loopM_unfold >loop_S_false // >mcl_q0_q1 // | #_ #a #b #ls #rs #Hb destruct (Hb) % [ @(\Pf Hc) | >mcl_q1_q2 >mcl_q2_q3 cases ls normalize // ] ] diff --git a/matita/matita/lib/turing/universal/move_tape.ma b/matita/matita/lib/turing/universal/move_tape.ma index cd8a87c5f..dad01b719 100644 --- a/matita/matita/lib/turing/universal/move_tape.ma +++ b/matita/matita/lib/turing/universal/move_tape.ma @@ -9,7 +9,7 @@ \ / GNU General Public License Version 2 V_____________________________________________________________*) -include "turing/universal/move_char_c.ma". +(* include "turing/universal/move_char_c.ma". *) include "turing/universal/move_char_l.ma". include "turing/universal/tuples.ma". diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma index dc55b13a7..0faa4eece 100644 --- a/matita/matita/lib/turing/universal/tuples.ma +++ b/matita/matita/lib/turing/universal/tuples.ma @@ -146,7 +146,24 @@ lemma generic_match_to_match_in_table_tech : [ #la * #lb * #HT1c #HT0 %{lb} >HT1c @(eq_f2 ??? (append ?) (c::la)) // >HT0 in Ht'; >HT1c >associative_append in ⊢ (???%→?); #Ht' <(append_l1_injective_r … Ht') // <(cons_injective_l ????? Ht) % - |@daemon ] + |@(noteq_to_eqnot ? true) @(not_to_not … not_eq_true_false) #Hbar @sym_eq + cases (memb_append … Hbar) -Hbar #Hbar + [@(Hqin2 … Hbar) + |cases (orb_true_l … Hbar) -Hbar + [#Hbar lapply (\P Hbar) -Hbar #Hbar destruct (Hbar) @Hcin + |whd in ⊢ ((??%?)→?); #Hbar cases (memb_append … Hbar) -Hbar #Hbar + [@(Hqout2 … Hbar) + |cases (orb_true_l … Hbar) -Hbar + [#Hbar lapply (\P Hbar) -Hbar #Hbar destruct (Hbar) @Hcout + |#Hbar cases (orb_true_l … Hbar) -Hbar + [whd in ⊢ ((??%?)→?); #Hbar @Hbar + |#Hbar lapply (memb_single … Hbar) -Hbar #Hbar destruct (Hbar) @Hmv + ] + ] + ] + ] + ] + ] qed. lemma generic_match_to_match_in_table : @@ -328,6 +345,8 @@ definition R_mark_next_tuple ≝ ∨ (no_bars rs1 ∧ t2 = midtape ? (reverse ? rs1@c::ls) 〈grid,false〉 rs2). +axiom daemon :∀P:Prop.P. + axiom tech_split : ∀A:DeqSet.∀f,l. (∀x.memb A x l = true → f x = false) ∨ diff --git a/matita/matita/lib/turing/universal/universal.ma b/matita/matita/lib/turing/universal/universal.ma index 3f8d2910c..5ffbc8d4e 100644 --- a/matita/matita/lib/turing/universal/universal.ma +++ b/matita/matita/lib/turing/universal/universal.ma @@ -331,7 +331,7 @@ lapply (Huni_step n table q_low_hd (\fst qout_low_hd) [whd in ⊢ (??%?); >q_low_head_false in Hq_low; whd in ⊢ ((???%)→?); generalize in match (h qin); #x #H destruct (H) % - |>Ht2 whd in match (step ???); + |>Ht2 whd in match (step FinBool ??); whd in match (trans ???); >(eq_pair_fst_snd … (t ?)) @is_low_config // >Hlift @@ -396,14 +396,14 @@ lapply (sem_while … sem_uni_step intape i outc Hloop) #q #Htd #tape1 #Htb lapply (IH (\fst (trans ? M 〈q,current ? tape1〉)) Htd) -IH #IH cases (Htc … Htb); -Htc #Hhaltq - whd in match (step ???); >(eq_pair_fst_snd ?? (trans ???)) + whd in match (step FinBool ??); >(eq_pair_fst_snd ?? (trans ???)) #Htc change with (mk_config ????) in Htc:(???(??%)); cases (IH ? Htc) #q1 * #tape2 * * #HRTM #Hhaltq1 #Houtc @(ex_intro … q1) @(ex_intro … tape2) % [% [cases HRTM #k * #outc1 * #Hloop #Houtc1 @(ex_intro … (S k)) @(ex_intro … outc1) % - [>loop_S_false [2://] whd in match (step ???); + [>loop_S_false [2://] whd in match (step FinBool ??); >(eq_pair_fst_snd ?? (trans ???)) @Hloop |@Houtc1 ] -- 2.39.2