include "turing/mono.ma".
+lemma le_to_eq : ∀m,n.m ≤ n → ∃k. n = m + k. /3 by plus_minus, ex_intro/
+qed.
+
+lemma minus_tech : ∀a,b.a + b - a = b. // qed.
+
+lemma loop_incr2 : ∀sig,M,m,n,cfg,cfg'.m ≤ n →
+ loopM sig M m cfg = Some ? cfg' → loopM sig M n cfg = Some ? cfg'.
+#sig #M #m #n #cfg #cfg' #H cases (le_to_eq … H) #k #Hk >Hk
+>commutative_plus @loop_incr
+qed.
+
(* given a FinSet F:
- get its cardinality
- return its nth element
- return the index of a given element
*)
-axiom FS_crd : FinSet → nat.
-axiom FS_nth : ∀F:FinSet.nat → option F.
-axiom index_of_FS : ∀F:FinSet.F → nat.
+definition FS_crd ≝ λF:FinSet.|enum F|.
+definition FS_nth ≝ λF:FinSet.λn.nth_opt ? n (enum F).
+definition index_of_FS_aux ≝ λF:FinSet.λf.position_of ? (λx.x==f) (enum F).
+
+lemma index_of_FS_aux_None :
+ ∀F,f.index_of_FS_aux F f = None ? → False.
+#F #f #e cut (memb ? f (enum F) = false)
+[ generalize in match e; -e normalize in ⊢ (%→?); generalize in match O;
+ elim (enum F) //
+ #hd #tl #IH #n whd in ⊢ (??%?→?); cases (true_or_false (hd==f))
+ #Hbool >Hbool normalize
+ [ #H destruct (H)
+ | #H >(\bf ?) [| @sym_not_eq @(\Pf Hbool) ] @IH // ]
+| >enum_complete #H destruct (H) ]
+qed.
+
+definition index_of_FS : ∀F:FinSet.F → nat ≝ λF,f.
+match index_of_FS_aux F f
+return (λx:option nat.index_of_FS_aux F f = x → nat) with
+[ None ⇒ λe.?
+| Some n ⇒ λe.n ] (refl ??).cases (index_of_FS_aux_None … e)
+qed.
(* unary bit representation (with a given length) of a certain number *)
-axiom unary_of_nat : nat → nat → (list bool).
+let rec unary_of_nat n k on n ≝
+ match n with [ O ⇒ [ ] | S q ⇒ (eqb q k)::unary_of_nat q k].
+
+lemma lt_FS_index_crd_aux : ∀sig,c,n.index_of_FS_aux sig c = Some ? n → n < FS_crd sig.
+#sig #c #n whd in ⊢ (??%?→?); >(?:FS_crd sig = O + FS_crd sig) //
+generalize in match O; normalize in match (FS_crd sig); elim (enum sig)
+normalize [ #n0 #H destruct (H) ]
+#hd #tl #IH #n0 cases (hd==c) normalize
+[ #H destruct (H) //
+| #H lapply (IH ? H) // ]
+qed.
-axiom FinVector : Type[0] → nat → FinSet.
+lemma index_of_FS_def : ∀sig,c,n.index_of_FS sig c = n → index_of_FS_aux sig c = Some ? n.
+#sig #c #n whd in ⊢ (??%?→?); lapply (refl ? (index_of_FS_aux sig c))
+cases (index_of_FS_aux sig c) in ⊢ (???%→??(match % return ? with [ _ ⇒ ? | _ ⇒ ? ] ?)?→%);
+[ #e cases (index_of_FS_aux_None ?? e)
+| normalize // ]
+qed.
+
+lemma index_of_FS_def2 : ∀sig,c.index_of_FS_aux sig c = Some ? (index_of_FS sig c)./2/
+qed.
+
+lemma lt_FS_index_crd: ∀sig,c.index_of_FS sig c < FS_crd sig.
+#sig #c @(lt_FS_index_crd_aux sig c ? (index_of_FS_def2 …))
+qed.
+
+lemma le_position_of_aux : ∀T,f,l,k,n.position_of_aux T f l k = Some ? n → k ≤ n.
+#T #f #l elim l normalize
+[ #k #n #H destruct (H)
+| #hd #tl #IH #k #n cases (f hd) normalize
+ [ #H destruct (H) %
+ | #H lapply (IH … H) /2 by lt_to_le/ ]
+]
+qed.
+
+lemma nth_index_of_FS_aux :
+∀sig,a,n.index_of_FS_aux sig a = Some ? n → FS_nth sig n = Some ? a.
+#sig #a #n normalize >(?:n = O + n) in ⊢ (%→?); //
+lapply O lapply n -n elim (enum sig) normalize
+[ #n #k #H destruct (H)
+| #hd #tl #IH #n #k cases (true_or_false (hd==a)) #Ha >Ha normalize
+ [ #H destruct (H) >(?:n = O) // >(\P Ha) //
+ | cases n
+ [ <plus_n_O #H @False_ind lapply (le_position_of_aux … H) #H1
+ cases (not_le_Sn_n k) /2/
+ | #n0 #Hrec @(IH ? (S k)) >Hrec /2 by eq_f/ ]
+ ]
+]
+qed.
+
+lemma nth_index_of_FS : ∀sig,a.FS_nth sig (index_of_FS ? a) = Some ? a.
+#sig #a @nth_index_of_FS_aux >index_of_FS_def2 %
+qed.
+
+definition bin_char ≝ λsig,ch.unary_of_nat (FS_crd sig) (index_of_FS sig ch).
+
+definition opt_bin_char ≝ λsig,c.match c with
+[ None ⇒ [ ] | Some c0 ⇒ bin_char sig c0 ].
+
+lemma eq_length_bin_char_FS_crd : ∀sig,c.|bin_char sig c| = FS_crd sig.
+#sig #c whd in ⊢ (??(??%)?); elim (FS_crd sig) //
+#n #IH <IH in ⊢ (???%); %
+qed.
+
+lemma bin_char_FS_nth_tech :
+ ∀sig,c,l1,b,l2.bin_char sig c = l1@b::l2 → b = (((|l2|):DeqNat) == index_of_FS sig c).
+#sig #c #l1 #b #l2 #Hbin lapply (eq_length_bin_char_FS_crd sig c)
+>Hbin #Hlen lapply Hbin lapply Hlen -Hlen -Hbin
+whd in match (bin_char ??); lapply l2 lapply c lapply l1 -l2 -c -l1
+elim (FS_crd sig)
+[ #l1 #b #l2 normalize in ⊢ (??%?→?); cases l1
+ [ normalize #H destruct (H) | #hd #tl normalize #H destruct (H) ]
+| #n #IH #l1 #b #l2 whd in ⊢ (?→??%?→?); cases l1
+ [ whd in ⊢ (??%?→???%→?); #Hlen destruct (Hlen)
+ #H <(cons_injective_l ????? H) @eq_f2 //
+ | #b0 #l10 #Hlen #H lapply (cons_injective_r ????? H) -H #H @(IH … H)
+ normalize in Hlen; destruct (Hlen) % ]
+]
+qed.
+
+lemma nth_opt_memb : ∀T:DeqSet.∀l,n,t.nth_opt T n l = Some ? t → memb T t l = true.
+#T #l elim l normalize [ #n #t #H destruct (H) ]
+#hd #tl #IH #n #t cases n normalize
+[ #Ht destruct (Ht) >(\b (refl ? t)) %
+| #n0 #Ht cases (t==hd) // @(IH … Ht) ]
+qed.
+
+lemma FS_nth_neq :
+∀sig,m,n. m ≠ n →
+∀s1,s2.FS_nth sig m = Some ? s1 → FS_nth sig n = Some ? s2 → s1 ≠ s2.
+#sig #m #n #Hneq #s1 #s2 lapply (enum_unique sig) lapply Hneq
+lapply n lapply m -n -m normalize elim (enum sig)
+[ #m #n #_ #_ normalize #H destruct (H)
+| #hd #tl #IH #m #n #Hneq whd in ⊢ (??%?→?);
+ cases (true_or_false (hd ∈ tl)) #Hbool >Hbool normalize in ⊢ (%→?);
+ [ #H destruct (H)
+ | #H cases m in Hneq;
+ [ #Hneq whd in ⊢ (??%?→?); #H1 destruct (H1) cases n in Hneq;
+ [ * #H cases (H (refl ??))
+ | #n0 #_ whd in ⊢ (??%?→?); #Htl % #Heq destruct (Heq)
+ >(nth_opt_memb … Htl) in Hbool; #Hfalse destruct (Hfalse)
+ ]
+ | #m0 #Hneq whd in ⊢ (??%?→?); #H1
+ whd in ⊢ (??%?→?); cases n in Hneq;
+ [ #_ whd in ⊢ (??%?→?); #H2 destruct (H2) % #Heq destruct (Heq)
+ >(nth_opt_memb … H1) in Hbool; #Hfalse destruct (Hfalse)
+ | #n0 #Hneq whd in ⊢ (??%?→?); @(IH m0 n0 ? H … H1)
+ % #Heq cases Hneq /2/
+ ]
+ ]
+ ]
+]
+qed.
+
+lemma nth_opt_Some : ∀T,l,n.n < |l| → ∃t.nth_opt T n l = Some ? t.
+#T #l elim l
+[ normalize #n #H @False_ind cases (not_le_Sn_O n) /2/
+| #hd #tl #IH #n normalize cases n
+ [ #_ %{hd} //
+ | #n0 #Hlt cases (IH n0 ?) [| @le_S_S_to_le // ]
+ #t #Ht normalize %{t} // ]
+]
+qed.
+
+corollary FS_nth_Some : ∀sig,n.n < FS_crd sig → ∃s.FS_nth sig n = Some ? s.
+#sig #n @nth_opt_Some
+qed.
+
+lemma bin_char_FS_nth :
+ ∀sig,c,l1,b,l2.bin_char sig c = l1@b::l2 → b = (FS_nth sig (|l2|) == Some ? c).
+#sig #c #l1 #b #l2 #H >(bin_char_FS_nth_tech … H)
+cases (true_or_false (((|l2|):DeqNat)==index_of_FS sig c)) #Hbool >Hbool
+[ >(?:(|l2|)=index_of_FS sig c) [|change with ((|l2|):DeqNat) in ⊢ (??%?); @(\P Hbool) ]
+ @sym_eq @(\b ?) @nth_index_of_FS
+| <nth_index_of_FS @sym_eq @(\bf ?) % #Hfalse
+ cases (FS_nth_Some sig (|l2|) ?) [| <(eq_length_bin_char_FS_crd sig c) >H >length_append normalize // ]
+ #s1 #H1
+ cases (FS_nth_Some sig (index_of_FS sig c) ?) [|//]
+ #s2 #H2
+ cases (FS_nth_neq … H1 H2) [| @(\Pf Hbool) ]
+ #Hfalse2 @Hfalse2 <Hfalse in H2; >H1 #HSome destruct (HSome) %
+]
+qed.
+
+corollary binary_to_bin_char :∀sig,csl,csr,a.
+ csl@true::csr=bin_char sig a → FS_nth ? (length ? csr) = Some ? a.
+#sig #csl #csr #a #H @(\P ?) @sym_eq @bin_char_FS_nth //
+qed.
+
+(* axiom FinVector : Type[0] → nat → FinSet.*)
definition binary_base_states ≝ initN 6.
FinProd (FinProd states binary_base_states)
(FinProd (FinOption sig) (initN (S (S (2 * (FS_crd sig)))))).
-axiom daemon : ∀T:Type[0].T.
-
definition to_initN : ∀n,m.n < m → initN m ≝ λn,m,Hn.mk_Sig … n ….// qed.
definition initN_pred : ∀n.∀m:initN n.initN n ≝ λn,m.mk_Sig … (pred (pi1 … m)) ….
(〈start sig M,bin0,None ?,FS_crd sig〉) (halt_binaryTM sig M).
/2 by lt_S_to_lt/ qed.
-definition bin_char ≝ λsig,ch.unary_of_nat (FS_crd sig) (index_of_FS sig ch).
-
-definition opt_bin_char ≝ λsig,c.match c with
-[ None ⇒ [ ] | Some c0 ⇒ bin_char sig c0 ].
-
definition bin_list ≝ λsig,l.flatten ? (map ?? (bin_char sig) l).
definition rev_bin_list ≝ λsig,l.flatten ? (map ?? (λc.reverse ? (bin_char sig c)) l).
>Hcur %
qed.
-(* to be checked *)
-axiom binary_to_bin_char :∀sig,csl,csr,a.
- csl@true::csr=bin_char sig a → FS_nth ? (length ? csr) = Some ? a.
-
lemma binaryTM_phase0_midtape_aux :
∀sig,M,q,ls,a,rs,k.
halt sig M q=false →
t = mk_tape ? (reverse ? csl@ls) (option_hd ? (csr@rs)) (tail ? (csr@rs)) →
csl@csr = bin_char sig a →
|csl@csr| = FS_crd sig →
- (index_of_FS ? a < |csl| → ch = Some ? a) →
+ (|csr| ≤ index_of_FS ? a → ch = Some ? a) →
loopM ? (mk_binaryTM sig M) (S (length ? csr) + k)
(mk_config ?? (〈q,bin0,ch,length ? csr〉) t)
= loopM ? (mk_binaryTM sig M) k
(mk_tape ? (reverse ? (bin_char ? a)@ls) (option_hd ? rs) (tail ? rs))). [2,3:@le_S /2 by O/]
#sig #M #q #ls #a #rs #k #Hhalt #csr elim csr
[ #csl #t #ch #Hlen #Ht >append_nil #Hcsl #Hlencsl #Hch >loopM_unfold >loop_S_false [|normalize //]
- >Hch [| >Hlencsl (* lemmatize *) @daemon]
+ >Hch [| >Hlencsl // ]
<loopM_unfold @eq_f >binaryTM_bin0_bin1 @eq_f >Ht
whd in match (step ???); whd in match (trans ???); <Hcsl %
| #c cases c
| #c1 #csr1 normalize >rev_append_def >rev_append_def >reverse_append % ]
| /2 by lt_S_to_lt/
|]
- #H whd in match (plus ??); >H @eq_f @eq_f2 %
+ #H whd in match (plus ??); >Ha >H @eq_f @eq_f2 %
| #csr0 #IH #csl #t #ch #Hlen #Ht #Heq #Hcrd #Hch >loopM_unfold >loop_S_false [|normalize //]
<loopM_unfold >binaryTM_bin0_false [| >Ht % ]
lapply (IH (csl@[false]) (tape_move FinBool t R) ??????)
[6: @ch
- | (* by cases: if index < |csl|, then Hch, else False *)
- @daemon
+ | #Hle cases (le_to_or_lt_eq … Hle) [ @Hch ]
+ #Hindex lapply (bin_char_FS_nth … (sym_eq … Heq)) >Hindex
+ >(nth_index_of_FS sig a) >(\b (refl ? (Some sig a))) #H destruct (H)
| >associative_append @Hcrd
| >associative_append @Heq
| >Ht whd in match (option_hd ??) in ⊢ (??%?); whd in match (tail ??) in ⊢ (??%?);
]
qed.
-lemma le_to_eq : ∀m,n.m ≤ n → ∃k. n = m + k. /3 by plus_minus, ex_intro/
-qed.
-
-lemma minus_tech : ∀a,b.a + b - a = b. // qed.
-
lemma binaryTM_phase0_midtape :
∀sig,M,t,q,ls,a,rs,ch.
+ O < FS_crd sig →
halt sig M q=false →
t = mk_tape ? ls (option_hd ? (bin_char ? a)) (tail ? (bin_char sig a)@rs) →
∀k.S (FS_crd sig) ≤ k →
= loopM ? (mk_binaryTM sig M) (k - S (FS_crd sig))
(mk_config ?? (〈q,bin1,Some ? a,FS_crd sig〉)
(mk_tape ? (reverse ? (bin_char ? a)@ls) (option_hd ? rs) (tail ? rs))). [|*:@le_S //]
-#sig #M #t #q #ls #a #rs #ch #Hhalt #Ht #k #Hk
+#sig #M #t #q #ls #a #rs #ch #Hcrd #Hhalt #Ht #k #Hk
cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >(minus_tech (S (FS_crd sig)))
-cut (∃c,cl.bin_char sig a = c::cl) [@daemon] * #c * #cl #Ha >Ha
-cut (FS_crd sig = |bin_char sig a|) [@daemon] #Hlen
+cut (∃c,cl.bin_char sig a = c::cl)
+[ lapply (refl ? (|bin_char ? a|)) >eq_length_bin_char_FS_crd in ⊢ (???%→?);
+ cases (bin_char ? a) [|/3 by ex_intro/] normalize in ⊢ (??%?→?); #H
+ <H in Hcrd; -H #H cases (not_le_Sn_O O) #Hfalse cases (Hfalse H) ]
+* #c * #cl #Ha >Ha
+cut (FS_crd sig = |bin_char sig a|) [/2 by plus_minus_m_m/] #Hlen
@(trans_eq ?? (loopM ? (mk_binaryTM ? M) (S (|c::cl|) + k0)
(mk_config ?? 〈q,bin0,〈ch,|c::cl|〉〉 t)))
-[ /2 by O/ | @eq_f2 // @eq_f2 // @eq_f <Ha >Hlen % ]
+[ @le_S_S <Ha <Hlen // | @eq_f2 // @eq_f2 // @eq_f <Ha >Hlen % ]
>(binaryTM_phase0_midtape_aux ? M q ls a rs ? ? (c::cl) [ ] t ch) //
-[| normalize #Hfalse @False_ind cases (not_le_Sn_O ?) /2/
-| <Ha (* |bin_char sig ?| = FS_crd sig *) @daemon
+[| <Ha <Hlen lapply (lt_FS_index_crd sig a) #Hlt #Hle
+ lapply (transitive_le ??? Hlt Hle) #H cases (not_le_Sn_n (index_of_FS ? a))
+ #H1 @False_ind /2/
+| <Ha >Hlen %
| >Ha %
| >Ht >Ha %
| <Ha <Hlen // ]
[ #csl #Hcount #Hcrd * #fs #Hfs >loopM_unfold >loop_S_false // <loopM_unfold
cut (fs = [ ])
[ cases fs in Hfs; // #f0 #fs0 #H lapply (eq_f ?? (length ?) … H)
- >length_append >(?:|bin_char sig chn| = FS_crd sig) [|@daemon]
+ >length_append >(?:|bin_char sig chn| = FS_crd sig) [|//]
<Hcrd >length_reverse #H1 cut (O = |f0::fs0|) [ /2/ ]
normalize #H1 destruct (H1) ]
#H destruct (H) >append_nil in Hfs; #Hfs
[| cases csl // cases ls // ]
cases fs in Hfs;
[ #Hfalse cut (|bin_char ? chn| = |csl|) [ >Hfalse >length_append >length_reverse // ]
- -Hfalse >(?:|bin_char sig chn| = FS_crd sig) [|@daemon]
+ -Hfalse >(?:|bin_char sig chn| = FS_crd sig) [|//]
<Hcrd in ⊢ (%→?); >(?:|csl| = |csl|+ O) in ⊢ (???%→?); //
#Hfalse cut (S n0 = O) /2 by injective_plus_r/ #H destruct (H)
| #f0 #fs0 #Hbinchar
- cut (bin_char ? chn = reverse ? csl@(FS_nth ? n0 == Some ? chn)::fs0) [@daemon]
+ cut (bin_char ? chn = reverse ? csl@(FS_nth ? n0 == Some ? chn)::fs0)
+ [ >Hbinchar >(bin_char_FS_nth … Hbinchar) >(?:|fs0|=n0) //
+ <(eq_length_bin_char_FS_crd sig chn) in Hcrd; >Hbinchar
+ >length_append >length_reverse whd in ⊢ (???(??%)→?); /2 by injective_S/ ]
-Hbinchar #Hbinchar >Hbinchar @(trans_eq ???? (IH …)) //
[ %{fs0} >reverse_cons >associative_append @Hbinchar
| whd in ⊢ (??%?); <Hcrd // ]
(mk_tape ? (csl@ls) (option_hd ? (csr@rs)) (tail ? (csr@rs))))
= loopM ? (mk_binaryTM sig M) k
(mk_config ?? (〈qn,bin3,ch,displ_of_move sig mv〉)
- (mk_tape ? (reverse ? (bin_char sig chn)@ls) (option_hd ? rs) (tail ? rs)))) [1,2: @le_S_S /2 by le_S/]
+ (mk_tape ? (reverse ? (bin_char sig chn)@ls) (option_hd ? rs) (tail ? rs)))) [1,2: @le_S_S [/2 by lt_to_le/|/2 by le_S/] ]
[ #sig #M #q #ch #qn #chn #mv #ls #rs #k #csr #Htrans elim csr
[ #csl #Hcount #Hcrd * #fs #Hfs >loopM_unfold >loop_S_false // normalize in match (length ? [ ]);
>(binaryTM_bin2_O … Htrans) <loopM_unfold @eq_f @eq_f @eq_f3 //
cases fs in Hfs; // #f0 #fs0 #H lapply (eq_f ?? (length ?) … H)
- >length_append >(?:|bin_char sig chn| = FS_crd sig) [|@daemon]
- <Hcrd >length_reverse #H1 cut (O = |f0::fs0|) [ /2/ ]
+ >length_append >(?:|bin_char sig chn| = FS_crd sig) [|//]
+ <Hcrd >length_reverse >length_append whd in match (|[]|); #H1 cut (O = |f0::fs0|) [ /2 by plus_to_minus/ ]
normalize #H1 destruct (H1)
| #b0 #bs0 #IH #csl #Hcount #Hcrd * #fs #Hfs
>loopM_unfold >loop_S_false // >(binaryTM_bin2_S_Some … Htrans)
(option_hd ? (bs0@rs)) (tail ? (bs0@rs)))
in match (tape_move ? (tape_write ???) ?);
[| cases bs0 // cases rs // ] @IH
- [ whd in Hcount:(?%?); /2 by lt_S_to_lt/
- | <Hcrd >length_append >length_append normalize //
+ [ <Hcrd >length_append >length_append normalize //
| cases fs in Hfs;
- [ #Hfalse cut (|bin_char ? chn| = |csl|) [ >Hfalse >length_append >length_reverse // ] -Hfalse >(?:|bin_char sig chn| = FS_crd sig) [|@daemon]
+ [ #Hfalse cut (|bin_char ? chn| = |csl|) [ >Hfalse >length_append >length_reverse // ] -Hfalse >(?:|bin_char sig chn| = FS_crd sig) [|//]
<Hcrd >length_append normalize >(?:|csl| = |csl|+ O) in ⊢ (???%→?); //
#Hfalse cut (S (|bs0|) = O) /2 by injective_plus_r/ #H destruct (H)
| #f0 #fs0 #Hbinchar
- cut (bin_char ? chn = reverse ? csl@(FS_nth ? (|bs0|) == Some ? chn)::fs0) [@daemon]
+ cut (bin_char ? chn = reverse ? csl@(FS_nth ? (|bs0|) == Some ? chn)::fs0)
+ [ >Hbinchar >(bin_char_FS_nth … Hbinchar) >(?:|fs0|=|bs0|) //
+ <(eq_length_bin_char_FS_crd sig chn) in Hcrd; >Hbinchar
+ >length_append >length_append >length_reverse
+ whd in ⊢ (??(??%)(??%)→?); /2 by injective_S/ ]
-Hbinchar #Hbinchar >Hbinchar %{fs0} >reverse_cons >associative_append %
]
]
]
| #Hcut #sig #M #q #ch #qn #chn #mv #ls #cs #rs #Htrans #Hcrd #k #Hk
- cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech @trans_eq
+ cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >(?:S (FS_crd sig) +k0-S (FS_crd sig) = k0) [|@minus_tech]
+ @trans_eq
[3: @(trans_eq ???? (Hcut ??????? ls ?? cs Htrans [ ] …)) //
[ normalize % // | normalize @Hcrd | >Hcrd // ]
|| @eq_f2 [ >Hcrd % | @eq_f2 // @eq_f cases Hcrd // ] ] ]
]
qed.
-axiom loop_increase : ∀sig,M,m,n,cfg,cfg'.m < n →
- loopM sig M m cfg = Some ? cfg' → loopM sig M n cfg = Some ? cfg'.
+lemma tape_move_niltape :
+ ∀sig,mv.tape_move sig (niltape ?) mv = niltape ?. #sig * // qed.
+
+lemma iter_tape_move_niltape :
+ ∀sig,mv,n.iter … (λt.tape_move sig t mv) n (niltape ?) = niltape ?.
+#sig #mv #n elim n // -n #n #IH whd in ⊢ (??%?); >tape_move_niltape //
+qed.
+
+lemma tape_move_R_left :
+ ∀sig,rs.tape_move sig (mk_tape ? [ ] (None ?) rs) R =
+ mk_tape ? [ ] (option_hd ? rs) (tail ? rs). #sig * //
+qed.
lemma binaryTM_loop :
∀sig,M,i,tf,qf. O < FS_crd sig →
[|cases t in Hcur;
[4: #ls #c #rs normalize in ⊢ (%→?); #H destruct (H)
| #_ whd in match (tape_bin_lift ??);
- (* TODO *)
- (* ∀mv.tape_move ? (niltape ?) mv = niltape ? *)
- (* ∀n.iter ? (λt.tape_move ? t ?) n (niltape ?) = niltape ? *)
- @daemon
+ >tape_move_niltape >iter_tape_move_niltape >tape_move_niltape %
| #r0 #rs0 #_ cases mv
[ >tape_bin_lift_unfold whd in match (mv_tech L); whd in match (displ2_of_move sig L);
whd in match (rev_bin_list ??); whd in match (option_hd ??);
whd in match (right ??); >(?: []@bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
- (* TODO *)
- (* tape_move (mk_tape [ ] (None ?) rs R = ... *)
- (* use iter_tape_move_R *)
- @daemon
+ >tape_move_R_left >hd_tech [| >eq_length_bin_char_FS_crd // ]
+ >tail_tech [| >eq_length_bin_char_FS_crd // ]
+ >iter_tape_move_L_left //
| >tape_bin_lift_unfold whd in match (mv_tech R); whd in match (displ2_of_move sig R);
whd in match (rev_bin_list ??); whd in match (option_hd ??);
whd in match (right ??); >(?: []@bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
whd in match (tape_move ? (leftof ???) R);
>tape_bin_lift_unfold >left_midtape >opt_bin_char_Some >right_midtape
- >iter_O
- (* TODO *)
- (* tape_move (mk_tape [ ] (None ?) rs R = ... *)
- @daemon
+ >iter_O >tape_move_R_left >hd_tech [| >eq_length_bin_char_FS_crd // ]
+ >tail_tech [| >eq_length_bin_char_FS_crd // ] //
| >tape_bin_lift_unfold % ]
| #l0 #ls0 #_ cases mv
[ >tape_bin_lift_unfold whd in match (mv_tech L); whd in match (displ2_of_move sig L);
whd in match (left ??); whd in match (tail ??);
whd in match (tape_move ? (rightof ???) L);
>(?: rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
- (* TODO *)
- (* tape_move (mk_tape ls (None ?) [ ] R = ... *)
- (* use iter_tape_move_L *)
- @daemon
+ >(?:tape_move ? (mk_tape ? ? (None ?) [ ]) R =
+ mk_tape ? (reverse ? (bin_char ? l0)@rev_bin_list ? ls0) (None ?) [ ])
+ [| cases (reverse ? (bin_char ? l0)@rev_bin_list ? ls0) //]
+ >(?:None ? = option_hd ? [ ]) // >iter_tape_move_L [|@eq_length_bin_char_FS_crd]
+ >append_nil >tape_bin_lift_unfold >left_midtape >current_midtape >right_midtape
+ >opt_bin_char_Some >append_nil %
| >tape_bin_lift_unfold whd in match (mv_tech R); whd in match (displ2_of_move sig R);
whd in match (bin_list ??); >append_nil whd in match (option_hd ??);
whd in match (left ??); whd in match (tail ??); >iter_O cases (rev_bin_list ??) //
lapply (binaryTM_phase0_None_Some … (None ?) (FS_crd sig) … Hhalt Hcur' Htrans) // [/2 by monotonic_lt_plus_l/]
cases t in Hcur;
[ 4: #ls #c #rs normalize in ⊢ (%→?); #H destruct (H)
- | 2: #r0 #rs0 #_ cut (∃b,bs.bin_char ? r0 = b::bs) [ @daemon ] * #b * #bs #Hbs
+ | 2: #r0 #rs0 #_ cut (∃b,bs.bin_char ? r0 = b::bs)
+ [ <(eq_length_bin_char_FS_crd sig r0) in Hcrd; cases (bin_char ? r0)
+ [ cases (not_le_Sn_O O) #H #H1 cases (H H1) |/3 by ex_intro/] ]
+ * #b * #bs #Hbs
lapply (binaryTM_phase4_extend ???? (tape_move ? (tape_bin_lift ? (leftof ? r0 rs0)) R) b … Htrans)
[ >tape_bin_lift_unfold whd in match (option_hd ??); whd in match (tail ??);
whd in match (right ??);
[ @eq_f @eq_f
>tape_bin_lift_unfold whd in match (rev_bin_list ??);
whd in match (right ??); whd in match (bin_list ??);
- cases (bin_char ? r0) // (* bin_char can't be nil *) @daemon
+ <(eq_length_bin_char_FS_crd sig r0) in Hcrd; cases (bin_char ? r0) //
+ cases (not_le_Sn_O O) #H #H1 cases (H H1)
| @le_S_S >associative_plus >associative_plus >commutative_plus @(le_plus O) //
|]]
- >phase2 [| (*arith*) @daemon ]
- >phase3 [| (*arith*) @daemon ]
+ >phase2
+ [|<plus_minus [|//] <plus_minus [|//] <plus_minus [|//] // ]
+ >phase3 [|<plus_minus [|//] <plus_minus [|//] // ]
>(?: 1+1+S (FS_crd sig)+S (FS_crd sig)+S (displ_of_move sig mv)+k0-1-1
-S (FS_crd sig)-S (FS_crd sig) -S (displ_of_move sig mv) = k0)
- [| (*arith*) @daemon ]
+ [|<plus_minus [|//] <plus_minus [|//] // ]
-phase0 -phase2 -phase3 -phase4 -phase5 <state_bin_lift_unfold
>(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
(mk_tape ? (reverse ? (bin_char sig chn)@[])
| >(?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
cases mv
[ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
- >iter_split >iter_tape_move_L [| @daemon ]
- >hd_tech [|@daemon] >tail_tech [|@daemon] >iter_tape_move_L_left [|//]
+ >iter_split >iter_tape_move_L [|@eq_length_bin_char_FS_crd]
+ >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [|>eq_length_bin_char_FS_crd // ] >iter_tape_move_L_left [|//]
whd in match (tape_move ???); >tape_bin_lift_unfold %
| normalize in match (displ_of_move ??); >iter_O
normalize in match (tape_move ???);
>tape_bin_lift_unfold >opt_bin_char_Some
- >hd_tech [|@daemon] >tail_tech [| @daemon ] %
+ >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [| >eq_length_bin_char_FS_crd // ] %
| normalize in match (displ_of_move ??);
- >iter_tape_move_L [|@daemon]
+ >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
normalize in match (tape_move ???); >tape_bin_lift_unfold
- >opt_bin_char_Some >hd_tech [|@daemon] >tail_tech [|@daemon] % ]
+ >opt_bin_char_Some >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [|>eq_length_bin_char_FS_crd // ] % ]
]
| #_ lapply (binaryTM_phase4_write ? M q (None ?) (niltape ?) (refl ??))
lapply (binaryTM_phase2_Some_of ?? q (None ?) … [ ] Htrans)
[ @le_S_S @(le_plus O) // ]
>state_bin_lift_unfold >phase0 [|//]
>phase4 [|//]
- >phase2 [|(*arith *) @daemon]
- >phase3 [| (*arith*) @daemon ]
+ >phase2 [| <plus_minus [|//] // ]
+ >phase3 [| <plus_minus [|//] <plus_minus [|//] // ]
>(?: 1+1+S (FS_crd sig) + S (displ_of_move sig mv)+k0-1-1
-S (FS_crd sig)-S (displ_of_move sig mv) = k0)
- [| (*arith*) @daemon ]
+ [| <plus_minus [|//] <plus_minus [|//] // ]
-phase0 -phase2 -phase3 -phase4 <state_bin_lift_unfold
>(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
(mk_tape ? (reverse ? (bin_char sig chn)@[]) (None ?) [ ])
| cases mv
[ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
>iter_split change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????(????%))?);
- >iter_tape_move_L [| @daemon ]
- >append_nil in ⊢ (??(????(???%?))?); >tail_tech [|@daemon]
+ >iter_tape_move_L [| >eq_length_bin_char_FS_crd // ]
+ >append_nil in ⊢ (??(????(???%?))?);
+ >tail_tech [| >eq_length_bin_char_FS_crd // ]
>iter_tape_move_L_left [|//]
normalize in match (tape_move ???);
>tape_bin_lift_unfold %
>tape_bin_lift_unfold %
| normalize in match (displ_of_move ??);
change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????%)?);
- >iter_tape_move_L [|@daemon]
+ >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
normalize in match (tape_move ???); >tape_bin_lift_unfold
- >opt_bin_char_Some >hd_tech [|@daemon] >tail_tech [|@daemon] % ]
+ >opt_bin_char_Some >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [|>eq_length_bin_char_FS_crd // ] % ]
]
| #l0 #ls0 #_ lapply (binaryTM_phase4_write ? M q (None ?) (tape_bin_lift ? (rightof ? l0 ls0)) ?)
[ >tape_bin_lift_unfold >current_mk_tape % ]
>(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
cases (reverse ? (bin_char ? l0)) // cases (rev_bin_list ? ls0) // ]
>phase4 [|//]
- >phase2 [|(*arith *) @daemon]
- >phase3 [| (*arith*) @daemon]
+ >phase2 [|<plus_minus [|//] // ]
+ >phase3 [|<plus_minus [|//] <plus_minus [|//] // ]
>(?: 1+1+S (FS_crd sig) + S (displ_of_move sig mv)+k0-1-1
-S (FS_crd sig)-S (displ_of_move sig mv) = k0)
- [| (*arith*) @daemon ]
+ [| <plus_minus [|//] <plus_minus [|//] // ]
-phase0 -phase2 -phase3 -phase4 <state_bin_lift_unfold
>(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
(mk_tape ? (reverse ? (bin_char sig chn)@rev_bin_list ? (l0::ls0)) (None ?) [ ])
| cases mv
[ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
>iter_split change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????(????%))?);
- >iter_tape_move_L [| @daemon ]
- >append_nil in ⊢ (??(????(???%?))?); >tail_tech [|@daemon]
+ >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
+ >append_nil in ⊢ (??(????(???%?))?); >tail_tech [|>eq_length_bin_char_FS_crd // ]
>(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
- >append_nil >iter_tape_move_L [|@daemon]
+ >append_nil >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
normalize in match (tape_move ???);
>tape_bin_lift_unfold @eq_f2
- [ >hd_tech [|@daemon] %
- | >tail_tech [|@daemon] >opt_bin_char_Some normalize in match (bin_list ??); >append_nil %]
+ [ >hd_tech [|>eq_length_bin_char_FS_crd // ] %
+ | >tail_tech [|>eq_length_bin_char_FS_crd // ] >opt_bin_char_Some
+ normalize in match (bin_list ??); >append_nil %]
| normalize in match (displ_of_move ??); >iter_O
normalize in match (tape_move ???);
>tape_bin_lift_unfold %
| normalize in match (displ_of_move ??);
change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????%)?);
- >iter_tape_move_L [|@daemon]
+ >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
normalize in match (tape_move ???); >tape_bin_lift_unfold
- >opt_bin_char_Some >hd_tech [|@daemon] >tail_tech [|@daemon] % ]
+ >opt_bin_char_Some >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [|>eq_length_bin_char_FS_crd // ] % ]
]
]
]
* #qn * #chn * #mv #Htrans
cut (tape_bin_lift ? t = ?) [| >tape_bin_lift_unfold % ]
>Ht in ⊢ (???%→?); >opt_bin_char_Some >left_midtape >right_midtape #Ht'
- lapply (binaryTM_phase0_midtape ?? (tape_bin_lift ? t) q … (None ?) Hhalt Ht')
+ lapply (binaryTM_phase0_midtape ?? (tape_bin_lift ? t) q … (None ?) Hcrd Hhalt Ht')
lapply (binaryTM_phase1 ?? q (reverse ? (bin_char ? c)) (rev_bin_list ? ls)
(option_hd ? (bin_list ? rs)) (tail ? (bin_list ? rs)) (Some ? c) ??)
- [ cases (bin_list ? rs) // @daemon | >length_reverse @daemon |]
+ [ cases (bin_list ? rs) // #r0 #rs0 normalize in ⊢ (%→?); #H destruct (H)
+ | >length_reverse >eq_length_bin_char_FS_crd // |]
>opt_cons_hd_tl >reverse_reverse
cases chn in Htrans; -chn
[ #Htrans
>state_bin_lift_unfold <Ht >phase0 [|//]
>phase1 [|/2 by monotonic_le_minus_l/]
>phase2 [|/2 by monotonic_le_minus_l/]
- >iter_tape_move_R [|@daemon]
+ >iter_tape_move_R [|>eq_length_bin_char_FS_crd // ]
>phase3 [|/2 by monotonic_le_minus_l/]
-phase0 -phase1 -phase2 -phase3
>(?: S (FS_crd sig) + S (FS_crd sig) + S (FS_crd sig) + S (displ_of_move sig mv) + k0
- S (FS_crd sig) - S (FS_crd sig) - S (FS_crd sig) - S (displ_of_move sig mv)
- = k0) [| (*arith*) @daemon]
+ = k0) [| <plus_minus [|//] <plus_minus [|//] <plus_minus [|//] // ]
<state_bin_lift_unfold
>(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
(mk_tape ? (reverse ? (bin_char sig c)@rev_bin_list ? ls)
| @IHNone <Hloop @eq_f whd in ⊢ (???%); >Ht <Htrans % ]
| normalize in match (tape_write ???); cases mv in Htrans; #Htrans
[ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
- >iter_split >iter_tape_move_L [| @daemon ]
+ >iter_split >iter_tape_move_L [| >eq_length_bin_char_FS_crd // ]
cases ls
- [ >hd_tech [|@daemon] >tail_tech [|@daemon] >iter_tape_move_L_left [|//]
+ [ >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [|>eq_length_bin_char_FS_crd // ]
+ >iter_tape_move_L_left [|//]
>tape_bin_lift_unfold %
| #l0 #ls0 >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
normalize in match (tape_move ???);
- >iter_tape_move_L [|@daemon]
- >hd_tech [|@daemon] >tail_tech [|@daemon]
+ >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
+ >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [|>eq_length_bin_char_FS_crd // ]
>tape_bin_lift_unfold % ]
| normalize in match (displ_of_move ??); >iter_O cases rs
[ normalize in match (tape_move ???); >tape_bin_lift_unfold %
>tape_bin_lift_unfold >opt_bin_char_Some
>left_midtape >right_midtape
>(?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
- >hd_tech [|@daemon] >tail_tech [|@daemon] %
+ >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [|>eq_length_bin_char_FS_crd // ] %
]
- | normalize in match (displ_of_move ??); >iter_tape_move_L [|@daemon]
- >hd_tech [|@daemon] >tail_tech [|@daemon] >tape_bin_lift_unfold %
+ | normalize in match (displ_of_move ??); >iter_tape_move_L
+ [|>eq_length_bin_char_FS_crd // ]
+ >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [|>eq_length_bin_char_FS_crd // ] >tape_bin_lift_unfold %
]
]
| #chn #Htrans
lapply (binaryTM_phase2_Some_ow ?? q (Some ? c) ??? (rev_bin_list ? ls) (bin_char ? c) (bin_list ? rs) Htrans ?)
- [@daemon]
+ [>eq_length_bin_char_FS_crd // ]
lapply (binaryTM_phase3 ? M qn (Some ? c) (displ_of_move sig mv) ?
(mk_tape FinBool (reverse bool (bin_char sig chn)@rev_bin_list ? ls)
(option_hd FinBool (bin_list sig rs)) (tail FinBool (bin_list sig rs)))) [//]
-phase0 -phase1 -phase2 -phase3
>(?: S (FS_crd sig) + S (FS_crd sig) + S (FS_crd sig) + S (displ_of_move sig mv) + k0
- S (FS_crd sig) - S (FS_crd sig) - S (FS_crd sig) - S (displ_of_move sig mv)
- = k0) [| (*arith*) @daemon]
+ = k0)
+ [| <plus_minus [|//] <plus_minus [|//] <plus_minus [|//] // ]
<state_bin_lift_unfold
>(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
(mk_tape ? (reverse ? (bin_char sig chn)@rev_bin_list ? ls)
| @IHNone <Hloop @eq_f whd in ⊢ (???%); >Ht <Htrans % ]
| normalize in match (tape_write ???); cases mv in Htrans; #Htrans
[ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
- >iter_split >iter_tape_move_L [| @daemon ]
+ >iter_split >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
cases ls
- [ >hd_tech [|@daemon] >tail_tech [|@daemon] >iter_tape_move_L_left [|//]
+ [ >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [|>eq_length_bin_char_FS_crd // ] >iter_tape_move_L_left [|//]
>tape_bin_lift_unfold %
| #l0 #ls0 >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
normalize in match (tape_move ???);
- >iter_tape_move_L [|@daemon]
- >hd_tech [|@daemon] >tail_tech [|@daemon]
+ >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
+ >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [|>eq_length_bin_char_FS_crd // ]
>tape_bin_lift_unfold % ]
| normalize in match (displ_of_move ??); >iter_O cases rs
[ normalize in match (tape_move ???); >tape_bin_lift_unfold %
>tape_bin_lift_unfold >opt_bin_char_Some
>left_midtape >right_midtape
>(?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
- >hd_tech [|@daemon] >tail_tech [|@daemon] %
+ >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [|>eq_length_bin_char_FS_crd // ] %
]
- | normalize in match (displ_of_move ??); >iter_tape_move_L [|@daemon]
- >hd_tech [|@daemon] >tail_tech [|@daemon] >tape_bin_lift_unfold %
+ | normalize in match (displ_of_move ??); >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
+ >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [|>eq_length_bin_char_FS_crd // ] >tape_bin_lift_unfold %
]
]
]
∀u1.t1 = tape_bin_lift sig u1 →
∃u2.t2 = tape_bin_lift sig u2 ∧ R u1 u2.
-(*
-∀sig,M,i,tf,qf. O < FS_crd sig →
- ∀t,q.∃k.i ≤ k ∧
- ((loopM sig M i (mk_config ?? q t) = Some ? (mk_config ?? qf tf) →
- loopM ? (mk_binaryTM sig M) k
- (mk_config ?? (state_bin_lift ? M q) (tape_bin_lift ? t)) =
- Some ? (mk_config ?? (state_bin_lift ? M qf) (tape_bin_lift ? tf))) ∧
- (loopM sig M i (mk_config ?? q t) = None ? →
- loopM ? (mk_binaryTM sig M) k
- (mk_config ?? (state_bin_lift ? M q) (tape_bin_lift ? t)) = None ?)).
- *)
-axiom loop_incr : ∀sig,M,m,n,cfg,cfg'.m ≤ n →
- loopM sig M m cfg = Some ? cfg' → loopM sig M n cfg = Some ? cfg'.
-
theorem sem_binaryTM :
∀sig,M,R.O < FS_crd sig → M ⊫ R → mk_binaryTM sig M ⊫ R_bin_lift ? R.
#sig #M #R #Hcrd #HM #t #k #outc #Hloopbin #u #Ht
[ #H cases (binaryTM_loop ? M k u (start ? M) Hcrd u (start ? M))
#k0 * #Hlt * #_ #H1 lapply (H1 H) -H -H1 <Ht
whd in match (initc ???) in Hloopbin; whd in match (start ??) in Hloopbin;
- >state_bin_lift_unfold >(loop_incr … Hlt Hloopbin) #H destruct (H)
+ >state_bin_lift_unfold >(loop_incr2 … Hlt Hloopbin) #H destruct (H)
| * #qf #tf #H cases (binaryTM_loop ? M k tf qf Hcrd u (start ? M))
#k0 * #Hlt * #H1 #_ lapply (H1 H) -H1 <Ht
whd in match (initc ???) in Hloopbin; whd in match (start ??) in Hloopbin;
- >state_bin_lift_unfold >(loop_incr … Hlt Hloopbin) #Heq destruct (Heq)
+ >state_bin_lift_unfold >(loop_incr2 … Hlt Hloopbin) #Heq destruct (Heq)
% [| % [%]] @(HM … H)
qed.
\ No newline at end of file