-lemma cfg_in_table_to_tuple: ∀n,l,h,c. is_config n c →
- ∀ll,lr.table_TM n l h = ll@c@lr →
- ∃out,m,lr0. lr = out@m::lr0 ∧ is_config n (bar::out) ∧ m ≠ bar.
-#n #l #h #c * #qin * #cin * * * #H1 #H2 #H3 #H4
-#ll #lr lapply ll -ll elim l
- [>H4 #ll cases ll normalize [|#hd #tl ] #Habs destruct
- |#t1 #othert #Hind #ll >table_TM_cons #Htuple
- cut (S n < |ll@c@lr|)
- [<Htuple >length_append >(length_of_tuple … (is_tuple … ))
- /2 by transitive_lt, le_n/] #Hsplit lapply Htuple -Htuple
- cases (is_tuple … n h t1) #q1 * #c1 * #q2 * #c2 * #m
- * * * * * * * #Hq1 #Hq2 #Hc1 #Hc2 #Hm #Hlen1 #Hlen2
- whd in ⊢ (???%→?); #Ht1
- (* if ll is empty we match the first tuple t1, otherwise
- we match inside othert *)
- cases ll
- [>H4 >Ht1 normalize in ⊢ (???%→?);
- >associative_append whd in ⊢ (??%?→?); #Heq destruct (Heq) -Heq
- >associative_append in e0; #e0
- lapply (append_l1_injective … e0) [>H3 @Hlen1] #Heq1
- lapply (append_l2_injective … e0) [>H3 @Hlen1]
- normalize in ⊢ (???%→?); whd in ⊢ (??%?→?); #Htemp
- lapply (cons_injective_l ????? Htemp) #Hc1
- lapply (cons_injective_r ????? Htemp) -Htemp #Heq2
- %{(q2@[c2])} %{m} %{(table_TM n othert h)} % // %
- [ <Heq2 >associative_append >associative_append % | %{q2} %{c2} % // % // % // ]
- |(* ll not nil *)
- #b #tl >Ht1 normalize in ⊢ (???%→?);
- whd in ⊢ (??%?→?); #Heq destruct (Heq)
- cases (compare_append … e0) #l *
- [* cases l
- [#_ #Htab cases (Hind [ ] (sym_eq … Htab)) #out * #m0 * #lr0 * * #Hlr #Hcfg #Hm0
- %{out} %{m0} %{lr0} % // % //
- |(* this case is absurd *)
- #al #tll #Heq1 >H4 #Heq2 @False_ind
- lapply (cons_injective_l ? bar … Heq2) #Hbar <Hbar in Heq1; #Heq1
- @(absurd (mem ? bar (q1@(c1::q2@[c2; m]))))
- [>Heq1 @mem_append_l2 %1 //
- |% #Hmembar cases (mem_append ???? Hmembar) -Hmembar
- [#Hmembar lapply(Hq1 bar Hmembar) normalize #Habs destruct (Habs)
- |* [#Habs @absurd //]
- #Hmembar cases (mem_append ???? Hmembar) -Hmembar
- [#Hmembar lapply(Hq2 bar Hmembar) normalize #Habs destruct (Habs)
- |* [#Habs @absurd //] #Hmembar @(absurd ?? Hm) @sym_eq @mem_single //
- ]
- ]
- ]
- ]
- |* #Htl #Htab cases (Hind … Htab) #out * #m0 * #lr0 * * #Hlr #Hcfg #Hm0
- %{out} %{m0} %{lr0} % // % //
- ]
+(*
+lemma tuple_to_config: ∀n,h,t,out,c. is_config n c →
+ tuple_encoding n h t = c@out →
+ ∃outq,outa,m. out = outq@[outa;m] ∧ is_config n (bar::outq@[outa]).
+#n #h * * #q0 #a0 * * #q1 #a1 #m #out #c * #q * #a * * * #Hq #Ha #Hlen #Hc
+whd in ⊢ (??%?→?); #Heq
+%{(bits_of_state n h q1)} %{(low_char a1)} %{(low_mv m)} %
+ [% [ %[ // | cases a1 [|#b] normalize % #H destruct (H)]
+ |whd in ⊢ (??%?); @eq_f //]
+ |@eq_f cut (∀A.∀a:A.∀l1,l2. a::l1@l2 = (a::l1)@l2) [//] #Hcut
+ >append_cons in Heq; >Hcut <associative_append
+ >(append_cons ? (low_char a1)) <associative_append #Heq
+ lapply (append_l1_injective_r ?? (c@out) ??? Heq) [%] -Heq
+ >associative_append #Heq @sym_eq @(append_l2_injective ?????? Heq)
+ >Hc whd in ⊢ (??%%); @eq_f >length_append >length_append
+ @eq_f2 // >length_map >Hlen whd in ⊢ (??%?); @eq_f //
+ ]
+qed.
+*)
+
+lemma tuple_to_config: ∀n,h,t,out,m,c. is_config n c →
+ tuple_encoding n h t = c@out@[m] → is_config n (bar::out).
+#n #h * * #q0 #a0 * * #q1 #a1 #m #out #lowm #c * #q * #a * * * #Hq #Ha #Hlen #Hc
+whd in ⊢ (??%?→?); #Heq %{(bits_of_state n h q1)} %{(low_char a1)} %
+ [% [ %[ // | cases a1 [|#b] normalize % #H destruct (H)]
+ |whd in ⊢ (??%?); @eq_f //]
+ |@eq_f cut (∀A.∀a:A.∀l1,l2. a::l1@l2 = (a::l1)@l2) [//] #Hcut
+ >append_cons in Heq; >Hcut <associative_append
+ >(append_cons ? (low_char a1)) <associative_append #Heq
+ lapply (append_l1_injective_r ?? (c@out) ??? Heq) [%] -Heq
+ >associative_append #Heq @sym_eq @(append_l2_injective ?????? Heq)
+ >Hc whd in ⊢ (??%%); @eq_f >length_append >length_append
+ @eq_f2 // >length_map >Hlen whd in ⊢ (??%?); @eq_f //
+ ]
+qed.
+
+(* da spostare *)
+lemma injective_nat_of: ∀n. injective … (nat_of n).
+#n * #a0 #Ha0 * #b0 #Hb0 normalize #Heq
+generalize in match Ha0; generalize in match Hb0; >Heq //
+qed.
+
+lemma not_of_lt: ∀n,m. nat_of n m < n.
+#n * #a #lta //
+qed.
+
+(* da spostare *)
+lemma injective_map: ∀A,B,f. injective A B f → injective … (map … f).
+#A #B #f #injf #l1 elim l1
+ [* // #a2 #l2 normalize #H destruct
+ |#a1 -l1 #l1 #Hind *
+ [normalize #H destruct
+ |#a2 #l2 normalize #Hmap
+ >(injf … (cons_injective_l ????? Hmap))
+ >(Hind … (cons_injective_r ????? Hmap)) %