-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,c,l1,l2,c1,l3,l4,rs,n.
- is_bit c = true → only_bits l1 → no_grids l2 → is_bit c1 = true →
- only_bits l3 → n = |l2| → |l2| = |l3| →
- table_TM (S n) (〈c1,true〉::l3@〈comma,false〉::l4) →
- t1 = midtape STape (〈grid,false〉::ls) 〈c,true〉
- (l1@〈grid,false〉::l2@〈bar,false〉::〈c1,true〉::l3@〈comma,false〉::l4@〈grid,false〉::rs) →
- (* facciamo match *)
- (〈c,true〉::l2 = 〈c1,true〉::l3 ∧
- t2 = midtape ? (reverse ? l2@〈c,false〉::〈grid,false〉::ls) 〈grid,false〉
- (l2@〈bar,false〉::〈c1,false〉::l3@〈comma,true〉::l4@〈grid,false〉::rs))
- ∨
- (* non facciamo match e marchiamo la prossima tupla *)
- (〈c,true〉::l2 ≠ 〈c1,true〉::l3 ∧
- ∃c2,l5,l6,l7.l4 = l5@〈bar,false〉::〈c2,false〉::l6@〈comma,false〉::l7 ∧
- (* condizioni su l5 l6 l7 *)
- t2 = midtape STape (〈grid,false〉::ls) 〈c,true〉
- (l1@〈grid,false〉::l2@〈bar,false〉::〈c1,true〉::l3@〈comma,false〉::
- l5@〈bar,false〉::〈c2,true〉::l6@〈comma,false〉::l7))
- ∨
- (* 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,true〉::l2 ≠ 〈c1,true〉::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.
\ No newline at end of file
+lemma match_in_table_append :
+ ∀n,T,qin,cin,qout,cout,mv,t.
+ tuple_TM n t →
+ match_in_table n qin cin qout cout mv (t@T) →
+ 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) //
+ >(length_of_tuple … Ht) >(length_of_tuple … H) %
+| #qin0 #cin0 #qout0 #cout0 #mv0 #T0 #H #H1 #_ #H2 %2
+ >(append_l2_injective … H2) // >(length_of_tuple … Ht) >(length_of_tuple … H) %
+]
+qed.
+
+lemma generic_match_to_match_in_table_tech :
+ ∀n,t,T0,T1,T2.tuple_TM n t → table_TM n (T1@〈bar,false〉::T2) →
+ t@T0 = T1@〈bar,false〉::T2 → T1 = [] ∨ ∃T3.T1 = t@T3.
+#n #t #T0 #T1 #T2 #Ht cases T1
+[ #_ #_ % %
+| normalize #c #T1c #Htable #Heq %2
+ cases Ht in Heq; #qin * #cin * #qout * #cout * #mv **********
+ #Hqin1 #Hqout1 #Hqin2 #Hqout2 #Hcin #Hcout #Hmv #Hcoutmv #Hqinlen #Hqoutlen
+ #Heqt >Heqt whd in ⊢ (??%%→?); #Ht lapply (cons_injective_r ????? Ht)
+ #Ht' cases (list_decompose_r STape … (sym_eq … Ht') ?)
+ [ #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) %
+ |@(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 :
+ ∀n,T.table_TM n T →
+ ∀qin,cin,qout,cout,mv.|qin| = n → |qout| = n →
+ only_bits qin → only_bits qout →
+ bit_or_null (\fst cin) = true → bit_or_null (\fst cout) = true →
+ bit_or_null (\fst mv) = true →
+ ∀t1,t2.
+ T = (t1@〈bar,false〉::qin@cin::〈comma,false〉::qout@cout::〈comma,false〉::[mv])@t2 →
+ match_in_table n qin cin qout cout mv T.
+#n #T #Htable #qin #cin #qout #cout #mv #Hlenqin #Hlenqout
+#Hqinbits #Hqoutbits #Hcin #Hcout #Hmv
+elim Htable
+[ * [ #t2 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
+ | #c0 #t1 #t2 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
+| #tuple #T0 #H1 #Htable0#IH #t1 #t2 #HT cases H1 #qin0 * #cin0 * #qout0 * #cout0 * #mv0
+ * * * * * * * * * *
+ #Hqin0marks #Hqout0marks #Hqin0bits #Hqout0bits #Hcin0 #Hcout0 #Hmv0 #Hcout0mv0
+ #Hlenqin0 #Hlenqout0 #Htuple
+ lapply (generic_match_to_match_in_table_tech n ? T0 t1
+ (qin@cin::〈comma,false〉::qout@[cout;〈comma,false〉;mv]@t2) H1) #Htmp
+ >Htuple in H1; #H1
+ lapply (ttm_cons … T0 H1 Htable0) <Htuple in ⊢ (%→?); >HT
+ >associative_append normalize >associative_append normalize
+ >associative_append #Htable cases (Htmp Htable ?)
+ [ #Ht1 >Htuple in HT; >Ht1 normalize in ⊢ (??%%→?);
+ >associative_append >associative_append #HT
+ cut (qin0 = qin ∧ (〈cin0,false〉 = cin ∧ (qout0 = qout ∧
+ (〈cout0,false〉 = cout ∧ (〈mv0,false〉 = mv ∧ T0 = t2)))))
+ [ lapply (cons_injective_r ????? HT) -HT #HT
+ lapply (append_l1_injective … HT) [ >Hlenqin @Hlenqin0 ]
+ #Hqin % [ @Hqin ] -Hqin
+ lapply (append_l2_injective … HT) [ >Hlenqin @Hlenqin0 ] -HT #HT
+ lapply (cons_injective_l ????? HT) #Hcin % [ @Hcin ] -Hcin
+ lapply (cons_injective_r ????? HT) -HT #HT
+ lapply (cons_injective_r ????? HT) -HT
+ >associative_append >associative_append #HT
+ lapply (append_l1_injective … HT) [ >Hlenqout @Hlenqout0 ]
+ #Hqout % [ @Hqout ] -Hqout
+ lapply (append_l2_injective … HT) [ >Hlenqout @Hlenqout0 ] -HT normalize #HT
+ lapply (cons_injective_l ????? HT) #Hcout % [ @Hcout ] -Hcout
+ lapply (cons_injective_r ????? HT) -HT #HT
+ lapply (cons_injective_r ????? HT) -HT #HT
+ lapply (cons_injective_l ????? HT) #Hmv % [ @Hmv ] -Hmv
+ @(cons_injective_r ????? HT) ]
+ -HT * #Hqin * #Hcin * #Hqout * #Hcout * #Hmv #HT0
+ >(?:〈bar,false〉::qin0@(〈cin0,false〉::〈comma,false〉::qout0@
+ [〈cout0,false〉;〈comma,false〉;〈mv0,false〉])@T0 = tuple@T0)
+ [ >Htuple >Hqin >Hqout >Hcin >Hcout >Hmv % //
+ | >Htuple normalize >associative_append normalize >associative_append
+ normalize >associative_append % ]
+ | * #T3 #HT3 >HT3 in HT; >associative_append; >associative_append #HT
+ lapply (append_l2_injective … HT) // -HT #HT %2 //
+ @(IH T3 t2) >HT >associative_append %
+ |>HT >associative_append normalize >associative_append normalize
+ >associative_append % ]
+]
+qed.