From cd7e658c917c4542b0308acf208aa40f1f7064e4 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 8 Jun 2012 09:52:38 +0000 Subject: [PATCH] Modifications and refactoring --- matita/matita/lib/turing/basic_machines.ma | 2 +- .../matita/lib/turing/universal/alphabet.ma | 40 + matita/matita/lib/turing/universal/marks.ma | 4 - .../lib/turing/universal/move_char_c.ma | 158 --- .../lib/turing/universal/move_char_l.ma | 166 --- .../matita/lib/turing/universal/normalTM.ma | 319 ++++++ .../matita/lib/turing/universal/trans_step.ma | 52 - matita/matita/lib/turing/universal/tuples.ma | 951 ++---------------- 8 files changed, 464 insertions(+), 1228 deletions(-) delete mode 100644 matita/matita/lib/turing/universal/move_char_c.ma delete mode 100644 matita/matita/lib/turing/universal/move_char_l.ma create mode 100644 matita/matita/lib/turing/universal/normalTM.ma delete mode 100644 matita/matita/lib/turing/universal/trans_step.ma diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma index 796992e22..eed6ad1f6 100644 --- a/matita/matita/lib/turing/basic_machines.ma +++ b/matita/matita/lib/turing/basic_machines.ma @@ -199,7 +199,7 @@ definition swap ≝ mk_TM alpha (swap_states alpha) (λp.let 〈q,a〉 ≝ p in let 〈q',b〉 ≝ q in - let q' ≝ pi1 nat (λi.i<4) q' in (* perche' devo passare il predicato ??? *) + let q' ≝ pi1 nat (λi.i<4) q' in match a with [ None ⇒ 〈〈swap3,foo〉,None ?〉 (* if tape is empty then stop *) | Some a' ⇒ diff --git a/matita/matita/lib/turing/universal/alphabet.ma b/matita/matita/lib/turing/universal/alphabet.ma index bf2484f29..4d87907d2 100644 --- a/matita/matita/lib/turing/universal/alphabet.ma +++ b/matita/matita/lib/turing/universal/alphabet.ma @@ -52,6 +52,7 @@ definition FSUnialpha ≝ mk_FinSet DeqUnialpha [bit true;bit false;null;comma;bar;grid] unialpha_unique unialpha_complete. +(*************************** testing characters *******************************) definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ]. definition is_null ≝ λc.match c with [ null ⇒ true | _ ⇒ false ]. @@ -63,3 +64,42 @@ definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ]. definition is_comma ≝ λc.match c with [ comma ⇒ true | _ ⇒ false ]. definition bit_or_null ≝ λc.is_bit c ∨ is_null c. + +lemma bit_not_grid: ∀d. is_bit d = true → is_grid d = false. +* // normalize #H destruct +qed. + +lemma bit_or_null_not_grid: ∀d. bit_or_null d = true → is_grid d = false. +* // normalize #H destruct +qed. + +lemma bit_not_bar: ∀d. is_bit d = true → is_bar d = false. +* // normalize #H destruct +qed. + +lemma bit_or_null_not_bar: ∀d. bit_or_null d = true → is_bar d = false. +* // normalize #H destruct +qed. +(**************************** testing strings *********************************) +definition is_marked ≝ λalpha.λp:FinProd … alpha FinBool. + let 〈x,b〉 ≝ p in b. + +definition STape ≝ FinProd … FSUnialpha FinBool. + +definition only_bits ≝ λl. + ∀c.memb STape c l = true → is_bit (\fst c) = true. + +definition only_bits_or_nulls ≝ λl. + ∀c.memb STape c l = true → bit_or_null (\fst c) = true. + +definition no_grids ≝ λl. + ∀c.memb STape c l = true → is_grid (\fst c) = false. + +definition no_bars ≝ λl. + ∀c.memb STape c l = true → is_bar (\fst c) = false. + +definition no_marks ≝ λl. + ∀c.memb STape c l = true → is_marked ? c = false. + +definition bar_or_grid ≝ λc:STape.is_bar (\fst c) ∨ is_grid (\fst c). + diff --git a/matita/matita/lib/turing/universal/marks.ma b/matita/matita/lib/turing/universal/marks.ma index 13e85c56d..829f56dc5 100644 --- a/matita/matita/lib/turing/universal/marks.ma +++ b/matita/matita/lib/turing/universal/marks.ma @@ -443,10 +443,6 @@ qed. ^ *) -definition is_marked ≝ - λalpha.λp:FinProd … alpha FinBool. - let 〈x,b〉 ≝ p in b. - definition adv_both_marks ≝ λalpha.seq ? (adv_mark_r alpha) (seq ? (move_l ?) diff --git a/matita/matita/lib/turing/universal/move_char_c.ma b/matita/matita/lib/turing/universal/move_char_c.ma deleted file mode 100644 index 6e601ad2b..000000000 --- a/matita/matita/lib/turing/universal/move_char_c.ma +++ /dev/null @@ -1,158 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| - \ / This file is distributed under the terms of the - \ / GNU General Public License Version 2 - V_____________________________________________________________*) - - -(* MOVE_CHAR (variant c) MACHINE - -Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra. - -Input: -(ls,cs,rs can be empty; # is a parameter) - - ls x cs # rs - ^ - H - -Output: - ls cs x # rs - ^ - H - -Initial state = 〈0,#〉 -Final state = 〈4,#〉 - -*) - -include "turing/basic_machines.ma". -include "turing/if_machine.ma". - -definition mcc_step ≝ λalpha:FinSet.λsep:alpha. - ifTM alpha (test_char ? (λc.¬c==sep)) - (single_finalTM … (seq … (swap_r alpha sep) (move_r ?))) (nop ?) tc_true. - -definition Rmcc_step_true ≝ - λalpha,sep,t1,t2. - ∀a,b,ls,rs. - t1 = midtape alpha (a::ls) b rs → - b ≠ sep ∧ - t2 = mk_tape alpha (a::b::ls) (option_hd ? rs) (tail ? rs). - -definition Rmcc_step_false ≝ - λalpha,sep,t1,t2. - left ? t1 ≠ [] → current alpha t1 ≠ None alpha → - current alpha t1 = Some alpha sep ∧ t2 = t1. - -lemma sem_mcc_step : - ∀alpha,sep. - mcc_step alpha sep ⊨ - [inr … (inl … (inr … start_nop)): Rmcc_step_true alpha sep, Rmcc_step_false alpha sep]. -#alpha #sep - @(acc_sem_if_app … - (sem_test_char …) (sem_seq …(sem_swap_r …) (sem_move_r …)) (sem_nop …)) - [#intape #outtape #tapea whd in ⊢ (%→%→%); - #Htapea * #tapeb * whd in ⊢ (%→%→?); - #Htapeb #Houttape #a #b #ls #rs #Hintape - >Hintape in Htapea; #Htapea cases (Htapea ? (refl …)) -Htapea - #Hbsep #Htapea % [@(\Pf (injective_notb ? false Hbsep))] - @Houttape @Htapeb // - |#intape #outtape #tapea whd in ⊢ (%→%→%); - cases (current alpha intape) - [#_ #_ #_ * #Hfalse @False_ind @Hfalse % - |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % // - lapply (injective_notb ? true csep) -csep #csep >(\P csep) // - ] - ] -qed. - -(* the move_char (variant c) machine *) -definition move_char_c ≝ - λalpha,sep.whileTM alpha (mcc_step alpha sep) (inr … (inl … (inr … start_nop))). - -definition R_move_char_c ≝ - λalpha,sep,t1,t2. - ∀b,a,ls,rs. t1 = midtape alpha (a::ls) b rs → - (b = sep → t2 = t1) ∧ - (∀rs1,rs2.rs = rs1@sep::rs2 → - b ≠ sep → memb ? sep rs1 = false → - t2 = midtape alpha (a::reverse ? rs1@b::ls) sep rs2). - -lemma sem_move_char_c : - ∀alpha,sep. - WRealize alpha (move_char_c alpha sep) (R_move_char_c alpha sep). -#alpha #sep #inc #i #outc #Hloop -lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%] --Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar) -[ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea - % - [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??) - [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2)] - | #rs1 #rs2 #Hrs #Hb #Hrs1 - >Htapea in H1; #H1 cases (H1 ??) - [#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct % - |*:% #H2 normalize in H2; destruct (H2) ] - ] -| #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse - lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH - #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea) - #Ha0 #Htapeb % - [ #Hfalse @False_ind @(absurd ?? Ha0) // - | * - [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ (* normalize *) - >Hrs in Htapeb; #Htapeb normalize in Htapeb; - cases (IH … Htapeb) #Houtc #_ >Houtc normalize // - | #r0 #rs0 #rs2 #Hrs #_ #Hrs0 - cut (r0 ≠ sep ∧ memb … sep rs0 = false) - [ % - [ % #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct - | whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse - [ destruct - | @Hfalse ] - ] - ] * - #Hr0 -Hrs0 #Hrs0 >Hrs in Htapeb; - normalize in ⊢ (%→?); #Htapeb - cases (IH … Htapeb) -IH #_ #IH - >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 GOOD: we must stop if current = None too!!! *) - -axiom ssem_move_char_c : - ∀alpha,sep. - Realize alpha (move_char_c alpha sep) (R_move_char_c alpha sep). diff --git a/matita/matita/lib/turing/universal/move_char_l.ma b/matita/matita/lib/turing/universal/move_char_l.ma deleted file mode 100644 index bed0ba596..000000000 --- a/matita/matita/lib/turing/universal/move_char_l.ma +++ /dev/null @@ -1,166 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| - \ / This file is distributed under the terms of the - \ / GNU General Public License Version 2 - V_____________________________________________________________*) - - -(* MOVE_CHAR (left) MACHINE - -Sposta il carattere binario su cui si trova la testina appena prima del primo # -alla sua sinistra. - -Input: -(ls,cs,rs can be empty; # is a parameter) - - ls # cs x rs - ^ - H - -Output: - ls # x cs rs - ^ - H - -Initial state = 〈0,#〉 -Final state = 〈4,#〉 - -*) - -include "turing/basic_machines.ma". -include "turing/if_machine.ma". - -definition mcl_step ≝ λalpha:FinSet.λsep:alpha. - ifTM alpha (test_char ? (λc.¬c==sep)) - (single_finalTM … (seq … (swap alpha sep) (move_l ?))) (nop ?) tc_true. - -definition Rmcl_step_true ≝ - λalpha,sep,t1,t2. - ∀a,b,ls,rs. - t1 = midtape alpha ls b (a::rs) → - b ≠ sep ∧ - t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a::b::rs). - -definition Rmcl_step_false ≝ - λalpha,sep,t1,t2. - right ? t1 ≠ [] → current alpha t1 ≠ None alpha → - current alpha t1 = Some alpha sep ∧ t2 = t1. - -lemma sem_mcl_step : - ∀alpha,sep. - mcl_step alpha sep ⊨ - [inr … (inl … (inr … start_nop)): Rmcl_step_true alpha sep, Rmcl_step_false alpha sep]. -#alpha #sep - @(acc_sem_if_app … - (sem_test_char …) (sem_seq …(sem_swap …) (sem_move_l …)) (sem_nop …)) - [#intape #outtape #tapea whd in ⊢ (%→%→%); - #Htapea * #tapeb * whd in ⊢ (%→%→?); - #Htapeb #Houttape #a #b #ls #rs #Hintape - >Hintape in Htapea; #Htapea cases (Htapea ? (refl …)) -Htapea - #Hbsep #Htapea % [@(\Pf (injective_notb ? false Hbsep))] - @Houttape @Htapeb // - |#intape #outtape #tapea whd in ⊢ (%→%→%); - cases (current alpha intape) - [#_ #_ #_ * #Hfalse @False_ind @Hfalse % - |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % // - lapply (injective_notb ? true csep) -csep #csep >(\P csep) // - ] - ] -qed. - -(* the move_char (variant left) machine *) -definition move_char_l ≝ - λalpha,sep.whileTM alpha (mcl_step alpha sep) (inr … (inl … (inr … start_nop))). - -definition R_move_char_l ≝ - λalpha,sep,t1,t2. - ∀b,a,ls,rs. t1 = midtape alpha ls b (a::rs) → - (b = sep → t2 = t1) ∧ - (∀ls1,ls2.ls = ls1@sep::ls2 → - b ≠ sep → memb ? sep ls1 = false → - t2 = midtape alpha ls2 sep (a::reverse ? ls1@b::rs)). - -lemma sem_move_char_l : - ∀alpha,sep. - WRealize alpha (move_char_l alpha sep) (R_move_char_l alpha sep). -#alpha #sep #inc #i #outc #Hloop -lapply (sem_while … (sem_mcl_step alpha sep) inc i outc Hloop) [%] --Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar) -[ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea - % - [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??) - [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2) ] - | #rs1 #rs2 #Hrs #Hb #Hrs1 - >Htapea in H1; (* normalize in ⊢ (% → ?); *) #H1 cases (H1 ??) - [ #Hfalse normalize in Hfalse; @False_ind @(absurd ?? Hb) destruct % - |*:% normalize #H2 destruct (H2) ] - ] -| #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse - lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH - #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea) - #Ha0 #Htapeb % - [ #Hfalse @False_ind @(absurd ?? Ha0) // - | * - [ #ls2 whd in ⊢ (???%→?); #Hls #_ #_ - >Hls in Htapeb; #Htapeb normalize in Htapeb; - cases (IH … Htapeb) #Houtc #_ >Houtc normalize // - | #l0 #ls0 #ls2 #Hls #_ #Hls0 - cut (l0 ≠ sep ∧ memb … sep ls0 = false) - [ % - [ % #Hl0 >Hl0 in Hls0; >memb_hd #Hfalse destruct - | whd in Hls0:(??%?); cases (sep==l0) in Hls0; normalize #Hfalse - [ destruct - | @Hfalse ] - ] - ] * - #Hl0 -Hls0 #Hls0 >Hls in Htapeb; - normalize in ⊢ (%→?); #Htapeb - cases (IH … Htapeb) -IH #_ #IH - >reverse_cons >associative_append @IH // - ] - ] -qed. - -lemma terminate_move_char_l : - ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha ls b (a::rs) → - (b = sep ∨ memb ? sep ls = true) → Terminate alpha (move_char_l alpha sep) t. -#alpha #sep #t #b #a #ls #rs #Ht #Hsep -@(terminate_while … (sem_mcl_step alpha sep)) - [% - |generalize in match Hsep; -Hsep - generalize in match Ht; -Ht - generalize in match rs; -rs - generalize in match a; -a - generalize in match b; -b - generalize in match t; -t - elim ls - [#t #b #a #rs #Ht #Hsep % #tinit - whd in ⊢ (%→?); #H @False_ind - cases (H … Ht) #Hb #_ cases Hb #eqb @eqb - cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct - |#l0 #ls0 #Hind #t #b #a #rs #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 GOOD: we must stop if current = None too!!! -lemma ssem_move_char_l : - ∀alpha,sep. - Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep). -#alpha #sep * -[ %{5} % [| % [whd in ⊢ (??%?); - @WRealize_to_Realize // @terminate_move_char_l -*) - -axiom ssem_move_char_l : - ∀alpha,sep. - Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep). diff --git a/matita/matita/lib/turing/universal/normalTM.ma b/matita/matita/lib/turing/universal/normalTM.ma new file mode 100644 index 000000000..686b91099 --- /dev/null +++ b/matita/matita/lib/turing/universal/normalTM.ma @@ -0,0 +1,319 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| + \ / This file is distributed under the terms of the + \ / GNU General Public License Version 2 + V_____________________________________________________________*) + +include "turing/universal/alphabet.ma". +include "turing/mono.ma". + +(************************* turning DeqMove into a DeqSet **********************) +definition move_eq ≝ λm1,m2:move. + match m1 with + [R ⇒ match m2 with [R ⇒ true | _ ⇒ false] + |L ⇒ match m2 with [L ⇒ true | _ ⇒ false] + |N ⇒ match m2 with [N ⇒ true | _ ⇒ false]]. + +lemma move_eq_true:∀m1,m2. + move_eq m1 m2 = true ↔ m1 = m2. +* + [* normalize [% #_ % |2,3: % #H destruct ] + |* normalize [1,3: % #H destruct |% #_ % ] + |* normalize [1,2: % #H destruct |% #_ % ] +qed. + +definition DeqMove ≝ mk_DeqSet move move_eq move_eq_true. + +unification hint 0 ≔ ; + X ≟ DeqMove +(* ---------------------------------------- *) ⊢ + move ≡ carr X. + +unification hint 0 ≔ m1,m2; + X ≟ DeqMove +(* ---------------------------------------- *) ⊢ + move_eq m1 m2 ≡ eqb X m1 m2. + + +(************************ turning DeqMove into a FinSet ***********************) +definition move_enum ≝ [L;R;N]. + +lemma move_enum_unique: uniqueb ? [L;R;N] = true. +// qed. + +lemma move_enum_complete: ∀x:move. memb ? x [L;R;N] = true. +* // qed. + +definition FinMove ≝ + mk_FinSet DeqMove [L;R;N] move_enum_unique move_enum_complete. + +unification hint 0 ≔ ; + X ≟ FinMove +(* ---------------------------------------- *) ⊢ + move ≡ FinSetcarr X. + +(*************************** normal Turing Machines ***************************) + +(* A normal turing machine is just an ordinary machine where: + 1. the tape alphabet is bool + 2. the finite state are supposed to be an initial segment of the natural + numbers. + Formally, it is specified by a record with the number n of states, a proof + that n is positive, the transition function and the halting function. +*) + +definition trans_source ≝ λn.FinProd (initN n) (FinOption FinBool). +definition trans_target ≝ λn.FinProd (initN n) (FinOption (FinProd FinBool FinMove)). + +record normalTM : Type[0] ≝ +{ no_states : nat; + pos_no_states : (0 < no_states); + ntrans : trans_source no_states → trans_target no_states; + nhalt : initN no_states → bool +}. + +(* A normal machine is just a special case of Turing Machine. *) + +definition normalTM_to_TM ≝ λM:normalTM. + mk_TM FinBool (initN (no_states M)) + (ntrans M) (mk_Sig ?? 0 (pos_no_states M)) (nhalt M). + +coercion normalTM_to_TM. + +definition nconfig ≝ λn. config FinBool (initN n). + +(******************************** tuples **************************************) + +(* By general results on FinSets we know that there is every function f between +two finite sets A and B can be described by means of a finite graph of pairs +〈a,f a〉. Hence, the transition function of a normal turing machine can be +described by a finite set of tuples 〈i,c〉,〈j,action〉〉 of the following type: + (Nat_to n × (option FinBool)) × (Nat_to n × (option (FinBool × move))). +Unfortunately this description is not suitable for an Universal Machine, since +such a machine must work with a fixed alphabet, while the size on n is unknown. +Hence, we must pass from natural numbers to a representation for them on a +finitary, e.g. binary, alphabet. In general, we shall associate +to a pair 〈〈i,c〉,〈j,action〉〉 a tuples with the following syntactical structure + |w_ix,w_jy,z +where +1. "|" and "," are special characters used as delimiters; +2. w_i and w_j are list of booleans representing the states $i$ and $j$; +3. x is special symbol null if C=None and is a if c=Some a +4. y and z are both null if action = None, and are equal to b,m' if + action = Some b,m; +5. finally, m' = 0 if m = L, m' = 1 if m=R and m' = null if m = N + +As a minor, additional complication, we shall suppose that every characters is +decorated by an additonal bit, normally set to false, to be used as a marker. +*) + +definition mk_tuple ≝ λqin,cin,qout,cout,mv. + 〈bar,false〉::qin@cin::〈comma,false〉::qout@cout::〈comma,false〉::[mv]. + +(* by definition, a tuple is not marked *) +definition tuple_TM : nat → list STape → Prop ≝ + λn,t.∃qin,cin,qout,cout,mv. + no_marks qin ∧ no_marks qout ∧ + only_bits qin ∧ only_bits qout ∧ + bit_or_null cin = true ∧ bit_or_null cout = true ∧ bit_or_null mv = true ∧ + (cout = null → mv = null) ∧ + |qin| = n ∧ |qout| = n ∧ + t = mk_tuple qin 〈cin,false〉 qout 〈cout,false〉 〈mv,false〉. + +(***************************** state encoding *********************************) +(* p < n is represented with a list of bits of lenght n with the p-th bit from +left set to 1. An additional intial bit is set to 1 if the state is final and +to 0 otherwise. *) + +let rec to_bitlist n p: list bool ≝ + match n with [ O ⇒ [ ] | S q ⇒ (eqb p q)::to_bitlist q p]. + +let rec from_bitlist l ≝ + match l with + [ nil ⇒ 0 (* assert false *) + | cons b tl ⇒ if b then |tl| else from_bitlist tl]. + +lemma bitlist_length: ∀n,p.|to_bitlist n p| = n. +#n elim n normalize // +qed. + +lemma bitlist_inv1: ∀n,p.p(not_eq_to_eqb_false … Hpn) normalize @Hind @ltpn + |#Heq >(eq_to_eqb_true … Heq) normalize eqtl @le_n + ] +qed. + +definition nat_of: ∀n. Nat_to n → nat. +#n normalize * #p #_ @p +qed. + +definition bits_of_state ≝ λn.λh:Nat_to n → bool.λs:Nat_to n. + h s::(to_bitlist n (nat_of n s)). + +definition m_bits_of_state ≝ λn.λh.λp. + map ? (unialpha×bool) (λx.〈bit x,false〉) (bits_of_state n h p). + +lemma no_marks_bits_of_state : ∀n,h,p. no_marks (m_bits_of_state n h p). +#n #h #p #x whd in match (m_bits_of_state n h p); +#H cases (orb_true_l … H) -H + [#H >(\P H) % + |elim (to_bitlist n (nat_of n p)) + [whd in ⊢ ((??%?)→?); #H destruct + |#b #l #Hind #H cases (orb_true_l … H) -H #H + [>(\P H) % |@Hind @H] + ] + ] +qed. + +lemma only_bits_bits_of_state : ∀n,h,p. only_bits (m_bits_of_state n h p). +#n #h #p #x whd in match (m_bits_of_state n h p); +#H cases (orb_true_l … H) -H + [#H >(\P H) % + |elim (to_bitlist n (nat_of n p)) + [whd in ⊢ ((??%?)→?); #H destruct + |#b #l #Hind #H cases (orb_true_l … H) -H #H + [>(\P H) % |@Hind @H ] + ] + ] +qed. + +(******************************** action encoding *****************************) +definition low_action ≝ λaction. + match action with + [ None ⇒ 〈null,null〉 + | Some act ⇒ let 〈na,m〉 ≝ act in + match m with + [ R ⇒ 〈bit na,bit true〉 + | L ⇒ 〈bit na,bit false〉 + | N ⇒ 〈bit na,null〉] + ]. + +(******************************** tuple encoding ******************************) +definition tuple_type ≝ λn. + (Nat_to n × (option FinBool)) × (Nat_to n × (option (FinBool × move))). + +definition tuple_encoding ≝ λn.λh:Nat_to n→bool. + λp:tuple_type n. + let 〈inp,outp〉 ≝ p in + let 〈q,a〉 ≝ inp in + let cin ≝ match a with [ None ⇒ null | Some b ⇒ bit b ] in + let 〈qn,action〉 ≝ outp in + let 〈cout,mv〉 ≝ low_action action in + let qin ≝ m_bits_of_state n h q in + let qout ≝ m_bits_of_state n h qn in + mk_tuple qin 〈cin,false〉 qout 〈cout,false〉 〈mv,false〉. + +(* +definition WFTuple_conditions ≝ + λn,qin,cin,qout,cout,mv. + no_marks qin ∧ no_marks qout ∧ (* queste fuori ? *) + only_bits qin ∧ only_bits qout ∧ + bit_or_null cin = true ∧ bit_or_null cout = true ∧ bit_or_null mv = true ∧ + (cout = null → mv = null) ∧ + |qin| = n ∧ |qout| = n. *) + +lemma is_tuple: ∀n,h,p. tuple_TM (S n) (tuple_encoding n h p). +#n #h * * #q #a * #qn #action +@(ex_intro … (m_bits_of_state n h q)) +letin cin ≝ match a with [ None ⇒ null | Some b ⇒ bit b ] +@(ex_intro … cin) +@(ex_intro … (m_bits_of_state n h qn)) +letin cout ≝ + match action with + [ None ⇒ null | Some act ⇒ bit (\fst act)] +@(ex_intro … cout) +letin mv ≝ match action with + [ None ⇒ null + | Some act ⇒ + match \snd act with + [ R ⇒ bit true | L ⇒ bit false | N ⇒ null] + ] +@(ex_intro … mv) +%[%[%[%[%[%[%[% /3/ + |whd in match cin ; cases a //] + |whd in match cout; cases action //] + |whd in match mv; cases action // * #b #m cases m //] + |whd in match cout; whd in match mv; cases action + [// | #act whd in ⊢ ((??%?)→?); #Hfalse destruct ]] + |>length_map normalize @eq_f //] + |>length_map normalize @eq_f //] + |normalize cases a cases action normalize // + [* #c #m cases m % |* #c #m #c1 cases m %] + ] +qed. + +definition tuple_length ≝ λn.2*n+6. + +lemma length_of_tuple: ∀n,t. tuple_TM n t → + |t| = tuple_length n. +#n #t * #qin * #cin * #qout * #cout * #mv *** #_ #Hqin #Hqout #eqt >eqt +whd in match (mk_tuple ?????); normalize >length_append >Hqin -Hqin normalize +>length_append normalize >Hqout -Hqout // +qed. + +definition tuples_list ≝ λn.λh.map … (λp.tuple_encoding n h p). + +(******************* general properties of encoding of tuples *****************) + +lemma no_grids_in_tuple : ∀n,l.tuple_TM n l → no_grids l. +#n #l * #qin * #cin * #qout * #cout * #mv * * * * * * * * * * +#_ #_ #Hqin #Hqout #Hcin #Hcout #Hmv #_ #_ #_ #Hl >Hl +#c #Hc cases (orb_true_l … Hc) -Hc #Hc +[ >(\P Hc) % +| cases (memb_append … Hc) -Hc #Hc +[ @bit_not_grid @(Hqin … Hc) +| cases (orb_true_l … Hc) -Hc #Hc +[ change with (c == 〈cin,false〉 = true) in Hc; >(\P Hc) @bit_or_null_not_grid // +| cases (orb_true_l … Hc) -Hc #Hc +[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) % +| cases (memb_append …Hc) -Hc #Hc +[ @bit_not_grid @(Hqout … Hc) +| cases (orb_true_l … Hc) -Hc #Hc +[ change with (c == 〈cout,false〉 = true) in Hc; >(\P Hc) @bit_or_null_not_grid // +| cases (orb_true_l … Hc) -Hc #Hc +[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) % +| >(memb_single … Hc) @bit_or_null_not_grid @Hmv +]]]]]] +qed. + +lemma no_marks_in_tuple : ∀n,l.tuple_TM n l → no_marks l. +#n #l * #qin * #cin * #qout * #cout * #mv * * * * * * * * * * +#Hqin #Hqout #_ #_ #_ #_ #_ #_ #_ #_ #Hl >Hl +#c #Hc cases (orb_true_l … Hc) -Hc #Hc +[ >(\P Hc) % +| cases (memb_append … Hc) -Hc #Hc +[ @(Hqin … Hc) +| cases (orb_true_l … Hc) -Hc #Hc +[ change with (c == 〈cin,false〉 = true) in Hc; >(\P Hc) % +| cases (orb_true_l … Hc) -Hc #Hc +[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) % +| cases (memb_append … Hc) -Hc #Hc +[ @(Hqout … Hc) +| cases (orb_true_l … Hc) -Hc #Hc +[ change with (c == 〈cout,false〉 = true) in Hc; >(\P Hc) % +| cases (orb_true_l … Hc) -Hc #Hc +[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) % +| >(memb_single … Hc) % +]]]]]] +qed. + + diff --git a/matita/matita/lib/turing/universal/trans_step.ma b/matita/matita/lib/turing/universal/trans_step.ma deleted file mode 100644 index 943045163..000000000 --- a/matita/matita/lib/turing/universal/trans_step.ma +++ /dev/null @@ -1,52 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| - \ / This file is distributed under the terms of the - \ / GNU General Public License Version 2 - V_____________________________________________________________*) - - -include "turing/universal/trans_to_tuples.ma". - -check TM - -(* definition zero : ∀n.initN n ≝ λn.mk_Sig ?? 0 (le_O_n n). *) - -definition normalTM ≝ λn,t,h. - λk:0Hp @mit_hd // + |#H whd in match (tuples_list ???); + cases (is_tuple n h p1) #qin1 * #cin1 * #qout1 * #cout1 * #mv1 + * #_ #Htuplep1 >Htuplep1 @mit_tl // @Hind // + ] + ] +qed. + +axiom match_decomp: ∀n,l,qin,cin,qout,cout,mv. + match_in_table (S n) qin cin qout cout mv l → + ∃l1,l2. l = l1@(mk_tuple qin cin qout cout mv)@l2 ∧ + (∃q.|l1| = (tuple_length (S n))*q) ∧ + tuple_TM (S n) (mk_tuple qin cin qout cout mv). + +axiom daemon: ∀P:Prop. P. + +lemma match_to_tuples_list: ∀n,h,l,qin,cin,qout,cout,mv. + match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_list n h l)) → + ∃p. p = mk_tuple qin cin qout cout mv ∧ mem ? p (tuples_list n h l). +#n #h #l #qin #cin #qout #cout #mv #Hmatch +@(ex_intro … (mk_tuple qin cin qout cout mv)) % // +cases (match_decomp … Hmatch) #l1 * #l2 * * #Hflat #Hlen #Htuple +@(flatten_to_mem … Hflat … Hlen) + [// + |@daemon + |@(length_of_tuple … Htuple) + ] +qed. + +lemma match_to_tuple: ∀n,h,l,qin,cin,qout,cout,mv. + match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_list n h l)) → + ∃p. tuple_encoding n h p = mk_tuple qin cin qout cout mv ∧ mem ? p l. +#n #h #l #qin #cin #qout #cout #mv #Hmatch +cases (match_to_tuples_list … Hmatch) +#p * #eqp #memb +cases(mem_map … (λp.tuple_encoding n h p) … memb) +#p1 * #Hmem #H @(ex_intro … p1) % /2/ +qed. + +lemma match_to_trans: + ∀n.∀trans: trans_source n → trans_target n. + ∀h,qin,cin,qout,cout,mv. + match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_list n h (graph_enum ?? trans))) → + ∃s,t. tuple_encoding n h 〈s,t〉 = mk_tuple qin cin qout cout mv + ∧ trans s = t. +#n #trans #h #qin #cin #qout #cout #mv #Hmatch +cases (match_to_tuple … Hmatch) -Hmatch * #s #t * #Heq #Hmem +@(ex_intro … s) @(ex_intro … t) % // @graph_enum_correct +@mem_to_memb @Hmem +qed. + +lemma trans_to_match: + ∀n.∀h.∀trans: trans_source n → trans_target n. + ∀inp,outp,qin,cin,qout,cout,mv. trans inp = outp → + tuple_encoding n h 〈inp,outp〉 = mk_tuple qin cin qout cout mv → + match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_list n h (graph_enum ?? trans))). +#n #h #trans #inp #outp #qin #cin #qout #cout #mv #Htrans #Htuple +@(tuple_to_match … (refl…)) (tuple_len … Htuple) >(tuple_len … Htuple0) % ] + [ >(length_of_tuple … Htuple) >(length_of_tuple … Htuple0) % ] -Heq #Heq destruct (Heq) // ] qed. @@ -127,9 +177,9 @@ lemma match_in_table_append : t = mk_tuple qin cin qout cout mv ∨ match_in_table n qin cin qout cout mv T. #n #T #qin #cin #qout #cout #mv #t #Ht #Hmatch inversion Hmatch [ #T0 #H #H1 % >(append_l1_injective … H1) // - >(tuple_len … Ht) >(tuple_len … H) % + >(length_of_tuple … Ht) >(length_of_tuple … H) % | #qin0 #cin0 #qout0 #cout0 #mv0 #T0 #H #H1 #_ #H2 %2 - >(append_l2_injective … H2) // >(tuple_len … Ht) >(tuple_len … H) % + >(append_l2_injective … H2) // >(length_of_tuple … Ht) >(length_of_tuple … H) % ] qed. @@ -224,796 +274,3 @@ elim Htable ] qed. -(* -lemma table_invert_l : ∀n,T0,qin,cin,qout,cout,mv. - table_TM n (mk_tuple qin cin qout cout mv@〈bar,false〉::T0) → - tuple_TM n (mk_tuple qin cin qout cout mv). -#n #T #qin #cin #qout #cout #mv #HT inversion HT -[ change with (append ???) in ⊢ (??(??%?)?→?);cases qin [ #Hfalse | #t0 #ts0 #Hfalse] normalize in Hfalse; destruct (Hfalse) -| #t0 #T0 #Ht0 #HT0 #_ - - -lemma table_invert_r : ∀n,T0,qin,cin,qout,cout,mv. - table n (mk_tuple qin cin qout cout mv@〈bar,false〉::T0) → table n T0. -*) - -lemma no_grids_in_tuple : ∀n,l.tuple_TM n l → no_grids l. -#n #l * #qin * #cin * #qout * #cout * #mv * * * * * * * * * * -#_ #_ #Hqin #Hqout #Hcin #Hcout #Hmv #_ #_ #_ #Hl >Hl -#c #Hc cases (orb_true_l … Hc) -Hc #Hc -[ >(\P Hc) % -| cases (memb_append … Hc) -Hc #Hc -[ @bit_not_grid @(Hqin … Hc) -| cases (orb_true_l … Hc) -Hc #Hc -[ change with (c == 〈cin,false〉 = true) in Hc; >(\P Hc) @bit_or_null_not_grid // -| cases (orb_true_l … Hc) -Hc #Hc -[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) % -| cases (memb_append …Hc) -Hc #Hc -[ @bit_not_grid @(Hqout … Hc) -| cases (orb_true_l … Hc) -Hc #Hc -[ change with (c == 〈cout,false〉 = true) in Hc; >(\P Hc) @bit_or_null_not_grid // -| cases (orb_true_l … Hc) -Hc #Hc -[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) % -| >(memb_single … Hc) @bit_or_null_not_grid @Hmv -]]]]]] -qed. - -lemma no_marks_in_tuple : ∀n,l.tuple_TM n l → no_marks l. -#n #l * #qin * #cin * #qout * #cout * #mv * * * * * * * * * * -#Hqin #Hqout #_ #_ #_ #_ #_ #_ #_ #_ #Hl >Hl -#c #Hc cases (orb_true_l … Hc) -Hc #Hc -[ >(\P Hc) % -| cases (memb_append … Hc) -Hc #Hc -[ @(Hqin … Hc) -| cases (orb_true_l … Hc) -Hc #Hc -[ change with (c == 〈cin,false〉 = true) in Hc; >(\P Hc) % -| cases (orb_true_l … Hc) -Hc #Hc -[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) % -| cases (memb_append … Hc) -Hc #Hc -[ @(Hqout … Hc) -| cases (orb_true_l … Hc) -Hc #Hc -[ change with (c == 〈cout,false〉 = true) in Hc; >(\P Hc) % -| cases (orb_true_l … Hc) -Hc #Hc -[ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) % -| >(memb_single … Hc) % -]]]]]] -qed. - -lemma no_grids_in_table: ∀n.∀l.table_TM n l → no_grids l. -#n #l #t elim t - [normalize #c #H destruct - |#t1 #t2 #Ht1 #Ht2 #IH lapply (no_grids_in_tuple … Ht1) -Ht1 #Ht1 #x #Hx - cases (memb_append … Hx) -Hx #Hx - [ @(Ht1 … Hx) - | @(IH … Hx) ] ] -qed. - -lemma no_marks_in_table: ∀n.∀l.table_TM n l → no_marks l. -#n #l #t elim t - [normalize #c #H destruct - |#t1 #t2 #Ht1 #Ht2 #IH lapply (no_marks_in_tuple … Ht1) -Ht1 #Ht1 #x #Hx - cases (memb_append … Hx) -Hx #Hx - [ @(Ht1 … Hx) - | @(IH … Hx) ] ] -qed. - -axiom last_of_table: ∀n,l,b.¬ table_TM n (l@[〈bar,b〉]). - -(* -l0 x* a l1 x0* a0 l2 ------> l0 x a* l1 x0 a0* l2 - ^ ^ - -if current (* x *) = # - then - else if x = 0 - then move_right; ---- - adv_to_mark_r; - if current (* x0 *) = 0 - then advance_mark ---- - adv_to_mark_l; - advance_mark - else STOP - else x = 1 (* analogo *) - -*) - - -(* - MARK NEXT TUPLE machine - (partially axiomatized) - - marks the first character after the first bar (rightwards) - *) - -definition bar_or_grid ≝ λc:STape.is_bar (\fst c) ∨ is_grid (\fst c). - -definition mark_next_tuple ≝ - seq ? (adv_to_mark_r ? bar_or_grid) - (ifTM ? (test_char ? (λc:STape.is_bar (\fst c))) - (move_right_and_mark ?) (nop ?) tc_true). - -definition R_mark_next_tuple ≝ - λt1,t2. - ∀ls,c,rs1,rs2. - (* c non può essere un separatore ... speriamo *) - t1 = midtape STape ls c (rs1@〈grid,false〉::rs2) → - no_marks rs1 → no_grids rs1 → bar_or_grid c = false → - (∃rs3,rs4,d,b.rs1 = rs3 @ 〈bar,false〉 :: rs4 ∧ - no_bars rs3 ∧ - Some ? 〈d,b〉 = option_hd ? (rs4@〈grid,false〉::rs2) ∧ - t2 = midtape STape (〈bar,false〉::reverse ? rs3@c::ls) 〈d,true〉 (tail ? (rs4@〈grid,false〉::rs2))) - ∨ - (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) ∨ - (∃l1,c,l2.f c = true ∧ l = l1@c::l2 ∧ ∀x.memb ? x l1 = true → f x = false). -(*#A #f #l elim l -[ % #x normalize #Hfalse *) - -theorem sem_mark_next_tuple : - Realize ? mark_next_tuple R_mark_next_tuple. -#intape -lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid) - (ifTM ? (test_char ? (λc:STape.is_bar (\fst c))) (move_right_and_mark ?) (nop ?) tc_true) ????) -[@sem_if [5: // |6: @sem_move_right_and_mark |7: // |*:skip] -| // -|||#Hif cases (Hif intape) -Hif - #j * #outc * #Hloop * #ta * #Hleft #Hright - @(ex_intro ?? j) @ex_intro [|% [@Hloop] ] - -Hloop - #ls #c #rs1 #rs2 #Hrs #Hrs1 #Hrs1' #Hc - cases (Hleft … Hrs) - [ * #Hfalse >Hfalse in Hc; #Htf destruct (Htf) - | * #_ #Hta cases (tech_split STape (λc.is_bar (\fst c)) rs1) - [ #H1 lapply (Hta rs1 〈grid,false〉 rs2 (refl ??) ? ?) - [ * #x #b #Hx whd in ⊢ (??%?); >(Hrs1' … Hx) >(H1 … Hx) % - | % - | -Hta #Hta cases Hright - [ * #tb * whd in ⊢ (%→?); #Hcurrent - @False_ind cases (Hcurrent 〈grid,false〉 ?) - [ normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) - | >Hta % ] - | * #tb * whd in ⊢ (%→?); #Hcurrent - cases (Hcurrent 〈grid,false〉 ?) - [ #_ #Htb whd in ⊢ (%→?); #Houtc - %2 % - [ @H1 - | >Houtc >Htb >Hta % ] - | >Hta % ] - ] - ] - | * #rs3 * #c0 * #rs4 * * #Hc0 #Hsplit #Hrs3 - % @(ex_intro ?? rs3) @(ex_intro ?? rs4) - lapply (Hta rs3 c0 (rs4@〈grid,false〉::rs2) ???) - [ #x #Hrs3' whd in ⊢ (??%?); >Hsplit in Hrs1;>Hsplit in Hrs3; - #Hrs3 #Hrs1 >(Hrs1 …) [| @memb_append_l1 @Hrs3'|] - >(Hrs3 … Hrs3') @Hrs1' >Hsplit @memb_append_l1 // - | whd in ⊢ (??%?); >Hc0 % - | >Hsplit >associative_append % ] -Hta #Hta - cases Hright - [ * #tb * whd in ⊢ (%→?); #Hta' - whd in ⊢ (%→?); #Htb - cases (Hta' c0 ?) - [ #_ #Htb' >Htb' in Htb; #Htb - generalize in match Hsplit; -Hsplit - cases rs4 in Hta; - [ #Hta #Hsplit >(Htb … Hta) - >(?:c0 = 〈bar,false〉) - [ @(ex_intro ?? grid) @(ex_intro ?? false) - % [ % [ % - [(* Hsplit *) @daemon |(*Hrs3*) @daemon ] | % ] | % ] - | (* Hc0 *) @daemon ] - | #r5 #rs5 >(eq_pair_fst_snd … r5) - #Hta #Hsplit >(Htb … Hta) - >(?:c0 = 〈bar,false〉) - [ @(ex_intro ?? (\fst r5)) @(ex_intro ?? (\snd r5)) - % [ % [ % [ (* Hc0, Hsplit *) @daemon | (*Hrs3*) @daemon ] | % ] - | % ] | (* Hc0 *) @daemon ] ] | >Hta % ] - | * #tb * whd in ⊢ (%→?); #Hta' - whd in ⊢ (%→?); #Htb - cases (Hta' c0 ?) - [ #Hfalse @False_ind >Hfalse in Hc0; - #Hc0 destruct (Hc0) - | >Hta % ] -]]]] -qed. - -definition init_current_on_match ≝ - (seq ? (move_l ?) - (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c))) - (seq ? (move_r ?) (mark ?)))). - -definition R_init_current_on_match ≝ λt1,t2. - ∀l1,l2,c,rs. no_grids l1 → is_grid c = false → - t1 = midtape STape (l1@〈c,false〉::〈grid,false〉::l2) 〈grid,false〉 rs → - t2 = midtape STape (〈grid,false〉::l2) 〈c,true〉 ((reverse ? l1)@〈grid,false〉::rs). - -lemma sem_init_current_on_match : - Realize ? init_current_on_match R_init_current_on_match. -#intape -cases (sem_seq ????? (sem_move_l ?) - (sem_seq ????? (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c))) - (sem_seq ????? (sem_move_r ?) (sem_mark ?))) intape) -#k * #outc * #Hloop #HR -@(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop -#l1 #l2 #c #rs #Hl1 #Hc #Hintape -cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta -Hintape -generalize in match Hl1; cases l1 - [#Hl1 whd in ⊢ ((???(??%%%))→?); #Hta - * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Hta - [* >Hc #Htemp destruct (Htemp) ] - * #_ #Htc lapply (Htc [ ] 〈grid,false〉 ? (refl ??) (refl …) Hl1) - whd in ⊢ ((???(??%%%))→?); -Htc #Htc - * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htc -Htd - whd in ⊢ ((???(??%%%))→?); #Htd - whd in ⊢ (%→?); #Houtc lapply (Houtc … Htd) -Houtc #Houtc - >Houtc % - |#d #tl #Htl whd in ⊢ ((???(??%%%))→?); #Hta - * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Htb - [* >(Htl … (memb_hd …)) #Htemp destruct (Htemp)] - * #Hd >append_cons #Htb lapply (Htb … (refl ??) (refl …) ?) - [#x #membx cases (memb_append … membx) -membx #membx - [@Htl @memb_cons @membx | >(memb_single … membx) @Hc]]-Htb #Htb - * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htb -Htc - >reverse_append >associative_append whd in ⊢ ((???(??%%%))→?); #Htc - whd in ⊢ (%→?); #Houtc lapply (Houtc … Htc) -Houtc #Houtc - >Houtc >reverse_cons >associative_append % - ] -qed. - -(* -definition init_current_gen ≝ - seq ? (adv_to_mark_l ? (is_marked ?)) - (seq ? (clear_mark ?) - (seq ? (move_l ?) - (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c))) - (seq ? (move_r ?) (mark ?))))). - -definition R_init_current_gen ≝ λt1,t2. - ∀l1,c,l2,b,l3,c1,rs,c0,b0. no_marks l1 → no_grids l2 → - Some ? 〈c0,b0〉 = option_hd ? (reverse ? (〈c,true〉::l2)) → - t1 = midtape STape (l1@〈c,true〉::l2@〈grid,b〉::l3) 〈c1,false〉 rs → - t2 = midtape STape (〈grid,b〉::l3) 〈c0,true〉 - ((tail ? (reverse ? (l1@〈c,false〉::l2))@〈c1,false〉::rs)). - -lemma sem_init_current_gen : Realize ? init_current_gen R_init_current_gen. -#intape -cases (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?)) - (sem_seq ????? (sem_clear_mark ?) - (sem_seq ????? (sem_move_l ?) - (sem_seq ????? (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c))) - (sem_seq ????? (sem_move_r ?) (sem_mark ?))))) intape) -#k * #outc * #Hloop #HR -@(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop -#l1 #c #l2 #b #l3 #c1 #rs #c0 #b0 #Hl1 #Hl2 #Hc #Hintape -cases HR -HR #ta * whd in ⊢ (%→?); #Hta cases (Hta … Hintape) -Hta -Hintape - [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ] -* #_ #Hta lapply (Hta l1 〈c,true〉 ? (refl ??) ??) [@Hl1|%] -Hta #Hta -* #tb * whd in ⊢ (%→?); #Htb lapply (Htb … Hta) -Htb -Hta #Htb -* #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc -Htb -generalize in match Hc; generalize in match Hl2; cases l2 - [#_ whd in ⊢ ((???%)→?); #Htemp destruct (Htemp) - whd in ⊢ ((???(??%%%))→?); #Htc - * #td * whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd - [2: * whd in ⊢ (??%?→?); #Htemp destruct (Htemp) ] - * #_ #Htd >Htd in Htc; -Htd #Htd - * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Htd - >reverse_append >reverse_cons - whd in ⊢ ((???(??%%%))→?); #Hte - whd in ⊢ (%→?); #Houtc lapply (Houtc … Hte) -Houtc -Hte #Houtc - >Houtc % - |#d #tl #Htl #Hc0 whd in ⊢ ((???(??%%%))→?); #Htc - * #td * whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd - [* >(Htl … (memb_hd …)) whd in ⊢ (??%?→?); #Htemp destruct (Htemp)] - * #Hd #Htd lapply (Htd … (refl ??) (refl ??) ?) - [#x #membx @Htl @memb_cons @membx] -Htd #Htd - * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Htd - >reverse_append >reverse_cons >reverse_cons - >reverse_cons in Hc0; >reverse_cons cases (reverse ? tl) - [normalize in ⊢ (%→?); #Hc0 destruct (Hc0) #Hte - whd in ⊢ (%→?); #Houtc lapply (Houtc … Hte) -Houtc -Hte #Houtc - >Houtc % - |* #c2 #b2 #tl2 normalize in ⊢ (%→?); #Hc0 destruct (Hc0) - whd in ⊢ ((???(??%%%))→?); #Hte - whd in ⊢ (%→?); #Houtc lapply (Houtc … Hte) -Houtc -Hte #Houtc - >Houtc >associative_append >associative_append >associative_append % - ] - ] -qed. -*) - -definition init_current ≝ - seq ? (adv_to_mark_l ? (is_marked ?)) - (seq ? (clear_mark ?) - (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c))) - (seq ? (move_r ?) (mark ?)))). - -definition R_init_current ≝ λt1,t2. - ∀l1,c,l2,b,l3,c1,rs,c0,b0. no_marks l1 → no_grids l2 → is_grid c = false → - Some ? 〈c0,b0〉 = option_hd ? (reverse ? (〈c,true〉::l2)) → - t1 = midtape STape (l1@〈c,true〉::l2@〈grid,b〉::l3) 〈c1,false〉 rs → - t2 = midtape STape (〈grid,b〉::l3) 〈c0,true〉 - ((tail ? (reverse ? (l1@〈c,false〉::l2))@〈c1,false〉::rs)). - -lemma sem_init_current : Realize ? init_current R_init_current. -#intape -cases (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?)) - (sem_seq ????? (sem_clear_mark ?) - (sem_seq ????? (sem_adv_to_mark_l ? (λc:STape.is_grid (\fst c))) - (sem_seq ????? (sem_move_r ?) (sem_mark ?)))) intape) -#k * #outc * #Hloop #HR -@(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -cases HR -HR #ta * whd in ⊢ (%→?); #Hta -* #tb * whd in ⊢ (%→?); #Htb -* #tc * whd in ⊢ (%→?); #Htc -* #td * whd in ⊢ (%→%→?); #Htd #Houtc -#l1 #c #l2 #b #l3 #c1 #rs #c0 #b0 #Hl1 #Hl2 #Hc #Hc0 #Hintape -cases (Hta … Hintape) [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ] --Hta * #_ #Hta lapply (Hta l1 〈c,true〉 ? (refl ??) ??) [@Hl1|%] --Hta #Hta lapply (Htb … Hta) -Htb #Htb cases (Htc … Htb) [ >Hc -Hc * #Hc destruct (Hc) ] --Htc * #_ #Htc lapply (Htc … (refl ??) (refl ??) ?) [@Hl2] --Htc #Htc lapply (Htd … Htc) -Htd ->reverse_append >reverse_cons ->reverse_cons in Hc0; cases (reverse … l2) -[ normalize in ⊢ (%→?); #Hc0 destruct (Hc0) - #Htd >(Houtc … Htd) % -| * #c2 #b2 #tl2 normalize in ⊢ (%→?); - #Hc0 #Htd >(Houtc … Htd) - whd in ⊢ (???%); destruct (Hc0) - >associative_append >associative_append % -] -qed. - -definition match_tuple_step ≝ - ifTM ? (test_char ? (λc:STape.¬ is_grid (\fst c))) - (single_finalTM ? - (seq ? compare - (ifTM ? (test_char ? (λc:STape.is_grid (\fst c))) - (nop ?) - (seq ? mark_next_tuple - (ifTM ? (test_char ? (λc:STape.is_grid (\fst c))) - (mark ?) (seq ? (move_l ?) init_current) tc_true)) tc_true))) - (nop ?) tc_true. - -definition R_match_tuple_step_true ≝ λt1,t2. - ∀ls,cur,rs.t1 = midtape STape ls cur rs → - \fst cur ≠ grid ∧ - (∀ls0,c,l1,l2,c1,l3,l4,rs0,n. - only_bits_or_nulls l1 → no_marks l1 (* → no_grids l2 *) → - bit_or_null c = true → bit_or_null c1 = true → - only_bits_or_nulls l3 → S n = |l1| → |l1| = |l3| → - table_TM (S n) (l2@〈c1,false〉::l3@〈comma,false〉::l4) → - ls = 〈grid,false〉::ls0 → cur = 〈c,true〉 → - rs = l1@〈grid,false〉::l2@〈c1,true〉::l3@〈comma,false〉::l4@〈grid,false〉::rs0 → - (* facciamo match *) - (〈c,false〉::l1 = 〈c1,false〉::l3 ∧ - t2 = midtape ? (reverse ? l1@〈c,false〉::〈grid,false〉::ls0) 〈grid,false〉 - (l2@〈c1,false〉::l3@〈comma,true〉::l4@〈grid,false〉::rs0)) - ∨ - (* non facciamo match e marchiamo la prossima tupla *) - (〈c,false〉::l1 ≠ 〈c1,false〉::l3 ∧ - ∃c2,l5,l6.l4 = l5@〈bar,false〉::〈c2,false〉::l6 ∧ - (* condizioni su l5 l6 l7 *) - t2 = midtape STape (〈grid,false〉::ls0) 〈c,true〉 - (l1@〈grid,false〉::l2@〈c1,false〉::l3@〈comma,false〉:: - l5@〈bar,false〉::〈c2,true〉::l6@〈grid,false〉::rs0)) - ∨ - (* non facciamo match e non c'è una prossima tupla: - non specifichiamo condizioni sul nastro di output, perché - non eseguiremo altre operazioni, quindi il suo formato non ci interessa *) - (〈c,false〉::l1 ≠ 〈c1,false〉::l3 ∧ no_bars l4 ∧ current ? t2 = Some ? 〈grid,true〉)). - -definition R_match_tuple_step_false ≝ λt1,t2. - ∀ls,c,rs.t1 = midtape STape ls c rs → is_grid (\fst c) = true ∧ t2 = t1. - -include alias "basics/logic.ma". - -(* -lemma eq_f4: ∀A1,A2,A3,A4,B.∀f:A1 → A2 →A3 →A4 →B. - ∀x1,x2,x3,x4,y1,y2,y3,y4. x1 = y1 → x2 = y2 →x3=y3 →x4 = y4 → - f x1 x2 x3 x4 = f y1 y2 y3 y4. -// -qed-. *) - -lemma some_option_hd: ∀A.∀l:list A.∀a.∃b. - Some ? b = option_hd ? (l@[a]) . -#A #l #a cases l normalize /2/ -qed. - -axiom tech_split2 : ∀A,l1,l2,l3,l4,x. - memb A x l1 = false → memb ? x l3 = false → - l1@x::l2 = l3@x::l4 → l1 = l3 ∧ l2 = l4. - -axiom injective_append : ∀A,l.injective … (λx.append A x l). - -lemma sem_match_tuple_step: - accRealize ? match_tuple_step (inr … (inl … (inr … start_nop))) - R_match_tuple_step_true R_match_tuple_step_false. -@(acc_sem_if_app … (sem_test_char ? (λc:STape.¬ is_grid (\fst c))) … - (sem_seq … sem_compare - (sem_if … (sem_test_char ? (λc:STape.is_grid (\fst c))) - (sem_nop …) - (sem_seq … sem_mark_next_tuple - (sem_if … (sem_test_char ? (λc:STape.is_grid (\fst c))) - (sem_mark ?) (sem_seq … (sem_move_l …) (sem_init_current …)))))) - (sem_nop ?) …) -[(* is_grid: termination case *) - 2:#t1 #t2 #t3 whd in ⊢ (%→?); #H #H1 whd #ls #c #rs #Ht1 - cases (H c ?) [2: >Ht1 %] #Hgrid #Heq % - [@injective_notb @Hgrid | Htapea in Hcur; #Hcur cases (Hcur ? (refl ??)) - -Hcur #Hcur #Htapeb % - [ % #Hfalse >Hfalse in Hcur; normalize #Hfalse1 destruct (Hfalse1)] - #ls0 #c #l1 #l2 #c1 #l3 #l4 #rs0 #n #Hl1bitnull #Hl1marks #Hc #Hc1 #Hl3 #eqn - #eqlen #Htable #Hls #Hcur #Hrs -Htapea >Hls in Htapeb; >Hcur >Hrs #Htapeb - cases (Hcompare … Htapeb) -Hcompare -Htapeb * #_ #_ #Hcompare - cases (Hcompare c c1 l1 l3 l2 (l4@〈grid,false〉::rs0) eqlen Hl1bitnull Hl3 Hl1marks … (refl …) Hc ?) - -Hcompare - [* #Htemp destruct (Htemp) #Htapec %1 % % [%] - >Htapec in Hor; -Htapec * - [2: * #t3 * whd in ⊢ (%→?); #H @False_ind - cases (H … (refl …)) whd in ⊢ ((??%?)→?); #H destruct (H) - |* #taped * whd in ⊢ (%→?); #Htaped cases (Htaped ? (refl …)) -Htaped * - #Htaped whd in ⊢ (%→?); #Htapeout >Htapeout >Htaped - % - ] - |* #la * #c' * #d' * #lb * #lc * * * #H1 #H2 #H3 #Htapec - cut (〈c,false〉::l1 ≠ 〈c1,false〉::l3) - [>H2 >H3 elim la - [@(not_to_not …H1) normalize #H destruct % - |#x #tl @not_to_not normalize #H destruct // - ] - ] #Hnoteq - cut (bit_or_null d' = true) - [cases la in H3; - [normalize in ⊢ (%→?); #H destruct // - |#x #tl #H @(Hl3 〈d',false〉) - normalize in H; destruct @memb_append_l2 @memb_hd - ] - ] #Hd' - >Htapec in Hor; -Htapec * - [* #taped * whd in ⊢ (%→?); #H @False_ind - cases (H … (refl …)) >(bit_or_null_not_grid ? Hd') #Htemp destruct (Htemp) - |* #taped * whd in ⊢ (%→?); #H cases (H … (refl …)) -H #_ - #Htaped * #tapee * whd in ⊢ (%→?); #Htapee - <(associative_append ? lc (〈comma,false〉::l4)) in Htaped; #Htaped - cases (Htapee … Htaped ???) -Htaped -Htapee - [* #rs3 * * (* we proceed by cases on rs4 *) - [(* rs4 is empty : the case is absurd since the tape - cannot end with a bar *) - * #d * #b * * * #Heq1 @False_ind - cut (∀A,l1,l2.∀a:A. a::l1@l2=(a::l1)@l2) [//] #Hcut - >Hcut in Htable; >H3 >associative_append - normalize >Heq1 Hcut - Hcut >H3 >associative_append @memb_append_l2 - @memb_cons >Heq1 @memb_append_l2 @memb_cons @memb_hd] #d2intable - cut (is_grid d2 = false) - [@(no_grids_in_table … Htable … 〈d2,b2〉 d2intable)] #Hd2 - cut (b2 = false) - [@(no_marks_in_table … Htable … 〈d2,b2〉 d2intable)] #Hb2 - >Hb2 in Heq1; #Heq1 -Hb2 -b2 - whd in ⊢ ((???%)→?); #Htemp destruct (Htemp) #Htapee >Htapee -Htapee * - [(* we know current is not grid *) - * #tapef * whd in ⊢ (%→?); #Htapef - cases (Htapef … (refl …)) >Hd2 #Htemp destruct (Htemp) - |* #tapef * whd in ⊢ (%→?); #Htapef - cases (Htapef … (refl …)) #_ -Htapef #Htapef - * #tapeg >Htapef -Htapef * - (* move_l *) - whd in ⊢ (%→?); - #H lapply (H … (refl …)) whd in ⊢ (???%→?); -H #Htapeg - >Htapeg -Htapeg - (* init_current *) - whd in ⊢ (%→?); #Htapeout - cases (some_option_hd ? (reverse ? (reverse ? la)) 〈c',true〉) - * #c00 #b00 #Hoption - lapply - (Htapeout (reverse ? rs3 @〈d',false〉::reverse ? la@reverse ? l2@(〈grid,false〉::reverse ? lb)) - c' (reverse ? la) false ls0 bar (〈d2,true〉::rs3'@〈grid,false〉::rs0) c00 b00 ?????) -Htapeout - [whd in ⊢ (??(??%??)?); @eq_f3 [2:%|3: %] - >associative_append - generalize in match (〈c',true〉::reverse ? la@〈grid,false〉::ls0); #l - whd in ⊢ (???(???%)); >associative_append >associative_append % - |>reverse_cons @Hoption - |cases la in H2; - [normalize in ⊢ (%→?); #Htemp destruct (Htemp) - @bit_or_null_not_grid @Hc - |#x #tl normalize in ⊢ (%→?); #Htemp destruct (Htemp) - @bit_or_null_not_grid @(Hl1bitnull 〈c',false〉) @memb_append_l2 @memb_hd - ] - |cut (only_bits_or_nulls (la@(〈c',false〉::lb))) - [

(\P eqc0) @Hc |@Hl1bitnull] - |#Hl1' #x #Hx @bit_or_null_not_grid @Hl1' - @memb_append_l1 @daemon - ] - |@daemon] #Htapeout % %2 % // - @(ex_intro … d2) - cut (∃rs32.rs3 = lc@〈comma,false〉::rs32) - [ (*cases (tech_split STape (λc.c == 〈bar,false〉) l4) - [ - | * #l41 * * #cbar #bfalse * #l42 * * #Hbar #Hl4 #Hl41 - @(ex_intro ?? l41) >Hl4 in Heq1; #Heq1 - - cut (sublist … lc l3) - [ #x #Hx cases la in H3; - [ normalize #H3 destruct (H3) @Hx - | #p #la' normalize #Hla' destruct (Hla') - @memb_append_l2 @memb_cons @Hx ] ] #Hsublist*) - @daemon] - * #rs32 #Hrs3 - (* cut - (〈c1,false〉::l3@〈comma,false〉::l4= la@〈d',false〉::rs3@〈bar,false〉::〈d2,b2〉::rs3') - [@daemon] #Hcut *) - cut (l4=rs32@〈bar,false〉::〈d2,false〉::rs3') - [ >Hrs3 in Heq1; @daemon ] #Hl4 - @(ex_intro … rs32) @(ex_intro … rs3') % [@Hl4] - >Htapeout @eq_f2 - [(* by Hoption, H2 *) @daemon - |(*>Hrs3 *)>append_cons - > (?:l1@〈grid,false〉::l2@〈c1,false〉::l3@〈comma,false〉::rs32@〈bar,false〉::〈d2,true〉::rs3'@〈grid,false〉::rs - = (l1@〈grid,false〉::l2@〈c1,false〉::l3@〈comma,false〉::rs32@[〈bar,false〉])@〈d2,true〉::rs3'@〈grid,false〉::rs) - [|>associative_append normalize - >associative_append normalize - >associative_append normalize - >associative_append normalize - % ] - >reverse_append >reverse_append >reverse_cons - >reverse_reverse >reverse_cons >reverse_reverse - >reverse_append >reverse_append >reverse_cons - >reverse_reverse >reverse_reverse >reverse_reverse - >(?:(la@[〈c',false〉])@((((lb@[〈grid,false〉])@l2)@la)@[〈d',false〉])@rs3 - =((la@〈c',false〉::lb)@([〈grid,false〉]@l2@la@[〈d',false〉]@rs3))) - [|>associative_append >associative_append - >associative_append >associative_append >associative_append - >associative_append % ] -

Hrs3 - >associative_append >associative_append normalize - >associative_append >associative_append - @eq_f @eq_f @eq_f - >(?:la@(〈d',false〉::lc@〈comma,false〉::rs32)@〈bar,false〉::〈d2,true〉::rs3'@〈grid,false〉::rs0 = - (la@〈d',false〉::lc)@〈comma,false〉::rs32@〈bar,false〉::〈d2,true〉::rs3'@〈grid,false〉::rs0 ) - [| >associative_append normalize >associative_append % ] -

Htapee -Htapee * - [whd in ⊢ (%→?); * #tapef * whd in ⊢ (%→?); #Htapef - cases (Htapef … (refl …)) -Htapef #_ #Htapef >Htapef -Htapef - whd in ⊢ (%→?); #Htapeout %2 % - [% [//] whd #x #Hx @Hnobars @memb_append_l2 @memb_cons // - | >(Htapeout … (refl …)) % ] - |whd in ⊢ (%→?); * #tapef * whd in ⊢ (%→?); #Htapef - cases (Htapef … (refl …)) -Htapef - whd in ⊢ ((??%?)→?); #Htemp destruct (Htemp) - ] - |(* no marks in table *) - #x #membx @(no_marks_in_table … Htable) - @memb_append_l2 - cut (∀A,l1,l2.∀a:A. a::l1@l2=(a::l1)@l2) [//] #Hcut >Hcut - >H3 >associative_append @memb_append_l2 @memb_cons @membx - |(* no grids in table *) - #x #membx @(no_grids_in_table … Htable) - @memb_append_l2 - cut (∀A,l1,l2.∀a:A. a::l1@l2=(a::l1)@l2) [//] #Hcut >Hcut - >H3 >associative_append @memb_append_l2 @memb_cons @membx - |whd in ⊢ (??%?); >(bit_or_null_not_grid … Hd') >(bit_or_null_not_bar … Hd') % - ] - ] - |#x #membx @(no_marks_in_table … Htable) - @memb_append_l2 @memb_cons @memb_append_l1 @membx - |#x #membx @(no_marks_in_table … Htable) - @memb_append_l1 @membx - |% - ] - ] -qed. - -(* - MATCH TUPLE - - scrolls through the tuples in the transition table until one matching the - current configuration is found -*) - -definition match_tuple ≝ whileTM ? match_tuple_step (inr … (inl … (inr … start_nop))). - -lemma is_grid_true : ∀c.is_grid c = true → c = grid. -* normalize [ #b ] #H // destruct (H) -qed. - -(* possible variante ? -definition weakR_match_tuple ≝ λt1,t2. - (∀ls,cur,rs,b. t1 = midtape STape ls 〈grid,b〉 rs → t2 = t1) ∧ - (∀c,l1,c1,l2,l3,ls0,rs0,n. - t1 = midtape STape (〈grid,false〉::ls0) 〈bit c,true〉 rs - (l1@〈grid,false〉::l2@〈bit c1,true〉::l3@〈grid,false〉::rs0) → - only_bits_or_nulls l1 → no_marks l1 → S n = |l1| → - table_TM (S n) (l2@〈c1,false〉::l3) → - (* facciamo match *) - (∃l4,newc,mv,l5. - 〈c1,false〉::l3 = l4@〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv::l5 ∧ - t2 = midtape ? (reverse ? l1@〈c,false〉::〈grid,false〉::ls0) 〈grid,false〉 - (l2@l4@〈c,false〉::l1@〈comma,true〉::newc@〈comma,false〉::mv::l5@ - 〈grid,false〉::rs0)) - ∨ - (* non facciamo match su nessuna tupla; - non specifichiamo condizioni sul nastro di output, perché - non eseguiremo altre operazioni, quindi il suo formato non ci interessa *) - (current ? t2 = Some ? 〈grid,true〉 ∧ - ∀l4,newc,mv,l5. - 〈c1,false〉::l3 ≠ l4@〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv::l5)). -*) - -definition R_match_tuple0 ≝ λt1,t2. - ∀ls,cur,rs. - t1 = midtape STape ls cur rs → - (is_grid (\fst cur) = true → t2 = t1) ∧ - (∀c,l1,c1,l2,l3,ls0,rs0,n. - ls = 〈grid,false〉::ls0 → - cur = 〈c,true〉 → - rs = l1@〈grid,false〉::l2@〈bar,false〉::〈c1,true〉::l3@〈grid,false〉::rs0 → - is_bit c = true → is_bit c1 = true → - only_bits_or_nulls l1 → no_marks l1 → S n = |l1| → - table_TM (S n) (l2@〈bar,false〉::〈c1,false〉::l3) → - (* facciamo match *) - (∃l4,newc,mv,l5. - 〈bar,false〉::〈c1,false〉::l3 = l4@〈bar,false〉::〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv::l5 ∧ - t2 = midtape ? (reverse ? l1@〈c,false〉::〈grid,false〉::ls0) 〈grid,false〉 - (l2@l4@〈bar,false〉::〈c,false〉::l1@〈comma,true〉::newc@〈comma,false〉::mv::l5@ - 〈grid,false〉::rs0)) - ∨ - (* non facciamo match su nessuna tupla; - non specifichiamo condizioni sul nastro di output, perché - non eseguiremo altre operazioni, quindi il suo formato non ci interessa *) - (current ? t2 = Some ? 〈grid,true〉 ∧ - ∀l4,newc,mv,l5. - 〈bar,false〉::〈c1,false〉::l3 ≠ l4@〈bar,false〉::〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv::l5)). - -axiom table_bit_after_bar : - ∀n,l1,c,l2.table_TM n (l1@〈bar,false〉::〈c,false〉::l2) → is_bit c = true. - -lemma wsem_match_tuple : WRealize ? match_tuple R_match_tuple0. -#intape #k #outc #Hloop -lapply (sem_while … sem_match_tuple_step intape k outc Hloop) [%] -Hloop -* #ta * #Hstar @(star_ind_l ??????? Hstar) -[ #tb whd in ⊢ (%→?); #Hleft - #ls #cur #rs #Htb cases (Hleft … Htb) #Hgrid #Houtc % - [ #_ @Houtc - | #c #l1 #c1 #l2 #l3 #ls0 #rs0 #n #Hls #Hcur #Hrs - >Hcur in Hgrid; #Hgrid >(is_grid_true … Hgrid) normalize in ⊢ (%→?); - #Hc destruct (Hc) - ] -| (* in the interesting case, we execute a true iteration, then we restart the - while cycle, finally we end with a false iteration *) - #tb #tc #td whd in ⊢ (%→?); #Htc - #Hstar1 #IH whd in ⊢ (%→?); #Hright lapply (IH Hright) -IH whd in ⊢ (%→?); #IH - #ls #cur #rs #Htb % - [ (* cur can't be true because we assume at least one iteration *) - #Hcur cases (Htc … Htb) * #Hfalse @False_ind @Hfalse @(is_grid_true … Hcur) - | (* current and a tuple are marked *) - #c #l1 #c1 #l2 #l3 #ls0 #rs0 #n #Hls #Hcur #Hrs #Hc #Hc1 #Hl1bitnull #Hl1marks - #Hl1len #Htable cases (Htc … Htb) -Htc -Htb * #_ #Htc - (* expose the marked tuple in table *) - cut (∃la,lb,mv,lc.l3 = la@〈comma,false〉::lb@〈comma,false〉::mv::lc ∧ - S n = |la| ∧ only_bits_or_nulls la) - [@daemon] * #la * #lb * #mv * #lc * * #Hl3 #Hlalen #Hlabitnull - >Hl3 in Htable; >append_cons #Htable - >(?: l2@〈bar,false〉::〈c1,true〉::l3@〈grid,false〉::rs0 - = (l2@[〈bar,false〉])@〈c1,true〉::la@〈comma,false〉::(lb@〈comma,false〉::mv:: - lc)@〈grid,false〉::rs0) in Hrs; - [| >associative_append normalize >Hl3 - >associative_append normalize % ] #Hrs - cases (Htc ????????? Hl1bitnull Hl1marks ?? Hlabitnull Hl1len ? Htable Hls Hcur Hrs) - [5: Hc1 % - |3: whd in ⊢ (??%?); >Hc % - |-Htc * - [ (* case 1: match successful *) - * #Heq #Htc % %{[]} %{lb} %{mv} %{lc} destruct (Heq) % - [% - | cases (IH … Htc) -IH #Houtc #_ >(Houtc (refl ??)) - >Htc @eq_f normalize >associative_append normalize - >associative_append normalize % - ] - | (* case 2: tuples don't match, we still have other tuples to try *) - * #Hdiff * #c2 * #l5 * #l6 * #Heqlblc #Htc - cases (IH ??? … Htc) -IH #_ #IH - (* by induction hypothesis *) - lapply (IH ? l1 c2 (l2@〈bar,false〉::〈c1,false〉::la@〈comma,false〉::l5) l6 ? rs0 n (refl ??) (refl ??) ???????) - [ generalize in match Htable; - >associative_append normalize - >associative_append normalize >Heqlblc - >associative_append normalize // - | @Hl1len - | @Hl1marks - | @Hl1bitnull - | (*???*) @daemon - | @Hc - | >associative_append normalize - >associative_append normalize - >associative_append % - |-IH * - [ (* the while finally matches a tuple *) - * #l7 * #newc * #mv0 * #l8 * #Hl7l8 #Houtc % - >Heqlblc @(ex_intro ?? (〈bar,false〉::〈c1,false〉::la@〈comma,false〉::l5@l7)) - %{newc} %{mv0} %{l8} % - [ normalize >Hl7l8 >associative_append normalize - >associative_append % - | >Houtc @eq_f >associative_append normalize - >associative_append normalize >associative_append - normalize >associative_append % - ] - | (* the while fails finding a tuple: there are no matches in the whole table *) - * #Houtc #Hdiff1 %2 % - [ @Houtc - | #l50 #newc #mv0 #l51 >Heqlblc - @daemon - ] - ] - ] - ] - | (* match failed and there is no next tuple: the next while cycle will just exit *) - * * #Hdiff #Hnobars generalize in match (refl ? tc); - cases tc in ⊢ (???% → %); - [ #_ normalize in ⊢ (??%?→?); #Hfalse destruct (Hfalse) - |2,3: #x #xs #_ normalize in ⊢ (??%?→?); #Hfalse destruct (Hfalse) ] - #ls1 #cur1 #rs1 #Htc normalize in ⊢ (??%?→?); #Hcur1 - cases (IH … Htc) -IH #IH #_ %2 % - [ destruct (Hcur1) >IH [ >Htc % | % ] - | #l4 #newc #mv0 #l5 - (* no_bars except the first one, where the tuple does not match ⇒ - no match *) - @daemon - ] - ] - ] -qed. - -definition R_match_tuple ≝ λt1,t2. - ∀ls,c,l1,c1,l2,rs,n. - is_bit c = true → is_bit c1 = true → - only_bits_or_nulls l1 → no_marks l1 → S n = |l1| → - table_TM (S n) (〈bar,false〉::〈c1,false〉::l2) → - t1 = midtape STape (〈grid,false〉::ls) 〈c,true〉 - (l1@〈grid,false〉::〈bar,false〉::〈c1,true〉::l2@〈grid,false〉::rs) → - (* facciamo match *) - (∃l3,newc,mv,l4. - 〈bar,false〉::〈c1,false〉::l2 = l3@〈bar,false〉::〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv::l4 ∧ - t2 = midtape ? (reverse ? l1@〈c,false〉::〈grid,false〉::ls) 〈grid,false〉 - (l3@〈bar,false〉::〈c,false〉::l1@〈comma,true〉::newc@〈comma,false〉::mv::l4@〈grid,false〉::rs)) - ∨ - (* non facciamo match su nessuna tupla; - non specifichiamo condizioni sul nastro di output, perché - non eseguiremo altre operazioni, quindi il suo formato non ci interessa *) - (current ? t2 = Some ? 〈grid,true〉 ∧ - ∀l3,newc,mv,l4. - 〈bar,false〉::〈c1,false〉::l2 ≠ l3@〈bar,false〉::〈c,false〉::l1@〈comma,false〉::newc@〈comma,false〉::mv::l4). - -(* we still haven't proved termination *) -axiom sem_match_tuple0 : Realize ? match_tuple R_match_tuple0. - -axiom Realize_to_Realize : - ∀alpha,M,R1,R2.(∀t1,t2.R1 t1 t2 → R2 t1 t2) → Realize alpha M R1 → Realize alpha M R2. - -lemma sem_match_tuple : Realize ? match_tuple R_match_tuple. -generalize in match sem_match_tuple0; @Realize_to_Realize -#t1 #t2 #HR #ls #c #l1 #c1 #l2 #rs #n #Hc #Hc1 #Hl1bitsnulls #Hl1marks #Hl1len #Htable #Ht1 -cases (HR … Ht1) -HR #_ #HR -@(HR ??? [] … (refl ??) (refl ??) (refl ??) Hc Hc1 Hl1bitsnulls Hl1marks - Hl1len Htable) -qed. \ No newline at end of file -- 2.39.2