V_____________________________________________________________*)
-include "turing/universal/tuples.ma".
-
-definition write_states ≝ initN 2.
-
-definition wr0 : write_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
-definition wr1 : write_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
-
-definition write ≝ λalpha,c.
- mk_TM alpha write_states
- (λp.let 〈q,a〉 ≝ p in
- match pi1 … q with
- [ O ⇒ 〈wr1,Some ? 〈c,N〉〉
- | S _ ⇒ 〈wr1,None ?〉 ])
- wr0 (λx.x == wr1).
-
-definition R_write ≝ λalpha,c,t1,t2.
- ∀ls,x,rs.t1 = midtape alpha ls x rs → t2 = midtape alpha ls c rs.
-
-axiom sem_write : ∀alpha,c.Realize ? (write alpha c) (R_write alpha c).
+include "turing/universal/marks.ma".
definition copy_step_subcase ≝
λalpha,c,elseM.ifTM ? (test_char ? (λx.x == 〈c,true〉))
HelseM intape)
#k * #outc * #Hloop #HR %{k} %{outc} % [@Hloop] -Hloop
#a #l1 #x0 #a0 #l2 #x #l3 #Hintape #Hl1marks cases HR -HR
-[ * #ta * whd in ⊢ (%→?); >Hintape #Hta cases (Hta … (refl ??)) -Hta #Hx #Hta
- * #tb * whd in ⊢ (%→?); #Htb lapply (Htb … Hta) -Hta -Htb #Htb
- * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htb -Htc #Htc
- * #td * whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd
- [ >Htc * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
- * #_ #Htd lapply (Htd (l1@[〈a0,false〉]) 〈x0,true〉 l2 ? (refl ??) ?) -Htd
- [ #x1 #Hx1 cases (memb_append … Hx1) -Hx1 #Hx1 [@(Hl1marks ? Hx1)|>(memb_single … Hx1) %]
- | normalize >associative_append % ] #Htd
+[ * #ta * whd in ⊢ (%→?); >Hintape * * #c0 * whd in ⊢ (??%?→?); #Hx #Hc #Hta
+ * #tb * whd in ⊢ (%→?); * #Htb cases (Htb (l1@〈a0,false〉::〈x0,true〉::l2) x) -Htb
+ #Htb lapply (Htb … Hta) -Htb #Htb #_ #_
+ * #tc * whd in ⊢ (%→?); * #_ #Htc lapply (Htc … Htb) -Htb -Htc #Htc
+ * #td * whd in ⊢ (%→?); * #_ #Htd cases (Htd … Htc) -Htd #_ #Htd cases (Htd (refl ??))
+ -Htd #Htd lapply (Htd (l1@[〈a0,false〉]) 〈x0,true〉 l2 ???) //
+ [#x1 #Hx1 cases (memb_append … Hx1) [ @Hl1marks | #Hsingle >(memb_single … Hsingle) % ]
+ |whd in ⊢ (??%?); // ]
+ -Htd #Htd #_
* #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Hte -Htd -Htc #Hte
- * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Hte -Htf >reverse_append #Htf
- * #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf) -Htf -Htg >reverse_single #Htg
- * #th * whd in ⊢ (%→?); #Hth lapply (Hth … Htg) -Htg -Hth
+ * #tf * whd in ⊢ (%→?); * #_ #Htf lapply (Htf … Hte) -Hte -Htf >reverse_append #Htf
+ * #tg * whd in ⊢ (%→?); * #Htg #_ lapply (Htg … Htf) -Htf -Htg >reverse_single #Htg
+ * #th * whd in ⊢ (%→?); * #_ #Hth lapply (Hth … Htg) -Htg -Hth
generalize in match Hl1marks; -Hl1marks @(list_elim_left … l1)
- [ #Hl1marks #Hth whd in ⊢ (%→?); #Houtc cases (Houtc … Hth) -Houtc
+ [ #Hl1marks #Hth whd in ⊢ (%→?); * #_ #Houtc cases (Houtc … Hth) -Houtc
[ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
- * #_ #Houtc lapply (Houtc [] ?? (refl ??) (refl ??) Hl1marks) -Houtc
- #Houtc lapply (\P Hx) -Hx #Hx destruct (Hx) % % [%] @Houtc
+ * * #_ #Houtc #_ lapply (Houtc [] ?? (refl ??) (refl ??) Hl1marks) -Houtc
+ #Houtc % >(\P Hc) in Hx; #Hx destruct (Hx) % // @Houtc
| -l1 #c1 #l1 #_ #Hl1marks >reverse_append >reverse_single
- #Hth whd in ⊢ (%→?); #Houtc cases (Houtc … Hth) -Houtc
+ #Hth whd in ⊢ (%→?); * #_ #Houtc cases (Houtc … Hth) -Houtc
[ * >Hl1marks [ #Hfalse destruct (Hfalse) ] @memb_append_l2 @memb_hd ]
- * #_ #Houtc lapply (Houtc (reverse ? l1@[〈x,false〉]) 〈a,true〉 l3 ? (refl ??) ?) -Houtc
- [ #x1 #Hx1 cases (memb_append … Hx1) -Hx1 #Hx1 [ @Hl1marks @memb_append_l1 @daemon | >(memb_single … Hx1) % ]
+ * * #_ #Houtc lapply (Houtc (reverse ? l1@[〈x,false〉]) 〈a,true〉 l3 ? (refl ??) ?) -Houtc
+ [ #x1 #Hx1 cases (memb_append … Hx1) -Hx1 #Hx1
+ [@Hl1marks @memb_append_l1 <(reverse_reverse … l1) @memb_reverse @Hx1
+ |>(memb_single … Hx1) % ]
| normalize >associative_append % ]
- #Houtc lapply (\P Hx) -Hx #Hx destruct (Hx) % % [%] >Houtc
- >reverse_append >reverse_reverse >associative_append >associative_append % ]
-| * #ta * whd in ⊢ (%→?); >Hintape #Hta cases (Hta ? (refl ??)) -Hta
- #Hxc #Hta >Hta #Houtc %2 % // lapply (\Pf Hxc) @not_to_not #Heq >Heq % ]
+ #Houtc #_ % destruct (Hx) lapply (\P Hc) -Hc #Hc destruct (Hc) % //
+ >Houtc >reverse_append >reverse_reverse >associative_append >associative_append % ]
+| * #ta * whd in ⊢ (%→?); >Hintape * #Hxc #Hta #Helse %2 %
+ [| <Hta @Helse ]
+ % #Hxc0 >Hxc0 in Hxc; #Hxc lapply (Hxc 〈c,true〉 (refl …)) #Hfalse
+ cases (\Pf Hfalse) #Hfalse0 @Hfalse0 %
+]
qed.
(*
(sem_adv_to_mark_r … (is_marked ?))))))) (sem_nop ?) intape)
#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
#a #l1 #x0 #a0 #l2 #x #l3 #Hintape #Hl1marks cases HR -HR
-[ * #ta * whd in ⊢ (%→?); >Hintape #Hta cases (Hta … (refl ??)) -Hta #Hx #Hta
- * #tb * whd in ⊢ (%→?); #Htb lapply (Htb … Hta) -Hta -Htb #Htb
- * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htb -Htc #Htc
- * #td * whd in ⊢ (%→?); #Htd cases (Htd … Htc) -Htd
- [ >Htc * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
- * #_ #Htd lapply (Htd (l1@[〈a0,false〉]) 〈x0,true〉 l2 ? (refl ??) ?) -Htd
- [ #x1 #Hx1 cases (memb_append … Hx1) -Hx1 #Hx1 [@(Hl1marks ? Hx1)|>(memb_single … Hx1) %]
- | normalize >associative_append % ] >reverse_append #Htd
- * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Hte -Htd -Htc #Hte
- * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Hte -Htf
+[ * #ta * whd in ⊢ (%→?); >Hintape * * #c * whd in ⊢ (??%?→?); #Hc destruct (Hc) #Hx #Hta
+ * #tb * whd in ⊢ (%→?); * #Htb #_ cases (Htb (l1@〈a0,false〉::〈x0,true〉::l2) x) -Htb #Htb #_ lapply (Htb … Hta) -Hta -Htb #Htb
+ * #tc * whd in ⊢ (%→?); * #_ #Htc lapply (Htc … Htb) -Htb -Htc #Htc
+ * #td * whd in ⊢ (%→?); * #_ #Htd cases (Htd … Htc) -Htd #_ #Htd cases (Htd (refl …)) -Htd #Htd #_
+ lapply (Htd (l1@[〈a0,false〉]) 〈x0,true〉 l2 ? (refl …) ?)
+ [#x1 #Hx1 cases (memb_append … Hx1) [@Hl1marks| -Hx1 #Hx1 >(memb_single … Hx1) % ]
+ |>associative_append % ] -Htd >reverse_append in ⊢ (???%→?); >associative_append in ⊢ (???%→?); #Htd
+ * #te * whd in ⊢ (%→?); * #Hte cases (Hte l2 x0) -Hte #Hte #_ #_ lapply (Hte … Htd) -Hte -Htd -Htc #Hte
+ * #tf * whd in ⊢ (%→?); * #_ #Htf lapply (Htf … Hte) -Hte -Htf
generalize in match Hl1marks; -Hl1marks @(list_elim_left … l1)
- [ #Hl1marks #Hth whd in ⊢ (%→?); #Houtc cases (Houtc … Hth) -Houtc
+ [ #Hl1marks #Hth whd in ⊢ (%→?); * #_ #Houtc cases (Houtc … Hth) -Houtc
[ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
- * #_ #Houtc lapply (Houtc [] ?? (refl ??) (refl ??) Hl1marks) -Houtc
- #Houtc lapply (\P Hx) -Hx #Hx destruct (Hx) % % [%] @Houtc
+ * * #_ #Houtc lapply (Houtc [] ?? (refl ??) (refl ??) Hl1marks) -Houtc
+ #Houtc lapply (\P Hx) -Hx #Hx destruct (Hx) #_ % % [%] @Houtc
| -l1 #c1 #l1 #_ #Hl1marks >reverse_append >reverse_single
- #Hth whd in ⊢ (%→?); #Houtc cases (Houtc … Hth) -Houtc
+ #Hth whd in ⊢ (%→?); * #_ #Houtc cases (Houtc … Hth) -Houtc
[ * >Hl1marks [ #Hfalse destruct (Hfalse) ] @memb_append_l2 @memb_hd ]
- * #_ #Houtc lapply (Houtc (reverse ? l1@[〈x,false〉]) 〈a,true〉 l3 ? (refl ??) ?) -Houtc
- [ #x1 #Hx1 cases (memb_append … Hx1) -Hx1 #Hx1 [ @Hl1marks @memb_append_l1 @daemon | >(memb_single … Hx1) % ]
+ * * #Hc1 #Houtc #_ lapply (Houtc (reverse ? l1@[〈x,false〉]) 〈a,true〉 l3 ? (refl ??) ?) -Houtc
+ [ #x1 #Hx1 cases (memb_append … Hx1) -Hx1 #Hx1
+ [@Hl1marks @memb_append_l1 <(reverse_reverse … l1) @memb_reverse @Hx1
+ |>(memb_single … Hx1) % ]
| normalize >associative_append % ]
#Houtc lapply (\P Hx) -Hx #Hx destruct (Hx) % % [%] >Houtc
>reverse_append >reverse_reverse >associative_append >associative_append % ]
-| * #ta * whd in ⊢ (%→?); >Hintape #Hta cases (Hta ? (refl ??)) -Hta
- #Hxc #Hta >Hta whd in ⊢ (%→?); #Houtc %2 %
- [ lapply (\Pf Hxc) @not_to_not #Heq >Heq %
- | @Houtc ]
+| * #ta * whd in ⊢ (%→?); >Hintape * #Hxc
+ cut (x ≠ null) [ % #Hx cases (\Pf (Hxc ? (refl …))) #Hfalse @Hfalse >Hx % ] -Hxc #Hxnull
+ #Hta whd in ⊢ (%→?); #Houtc %2 % // <Hta @Houtc ]
qed.
definition copy_step ≝
(sem_copy_step_subcase FSUnialpha (bit false) …
(sem_copy_step_subcase FSUnialpha (bit true) … (sem_nocopy_subcase …)))
(sem_nop …))
-[ #t1 #t2 #t3 whd in ⊢ (%→%→?); #H1 #H2 #ls #c #rs #Ht1 >Ht1 in H1; #H1
- cases (H1 … (refl ??)) #Hc #Ht3 % [ @Hc ]
+[ #t1 #t2 #t3 whd in ⊢ (%→%→?); #H1 #H2 #ls #c #rs #Ht1 >Ht1 in H1;
+ * * #c0 * whd in ⊢ (??%?→?); #Hc0 destruct (Hc0) #Hc #Ht3 % //
#a #l1 #x0 #a0 #l2 #l3 #Hls #Hrs #Hl1marks >Hls in Ht3; >Hrs #Ht3
cases (H2 … Ht3 ?)
[ * #Hc' #Ht2 % %{false} % // <Hc' @Ht2
| @Hl1marks ]
| @Hl1marks ]
| #t1 #t2 #t3 whd in ⊢ (%→%→?); #H1 #H2 #ls #c #rs #Ht1
- >Ht1 in H1; #H1 cases (H1 … (refl ??)) #_ #Ht3 cases (H1 ? (refl ??)) -H1
- #Hc #Ht3 % //
-]
+ >Ht1 in H1; * #Hcur #Ht3 % // @Hcur % ]
qed.
(*
>reverse_append >reverse_append normalize #H1 destruct %
qed.
+axiom daemon : ∀P:Prop.P.
+
lemma wsem_copy0 : WRealize ? copy0 R_copy0.
#intape #k #outc #Hloop
lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop
#Hl1 #Hl1bits #l4' #bg #Hl4 #Hl4bits %2
cases (Htc … Htb) -Htc #Hcbitnull #Htc
% [ % #Hc' >Hc' in Hcbitnull; normalize #Hfalse destruct (Hfalse) ]
- cut (|l1| = |reverse ? l4|) [@daemon] #Hlen1
+ cut (|l1| = |reverse ? l4|) [>length_reverse @Hlen] #Hlen1
@(list_cases2 … Hlen1)
[ (* case l1 = [] is discriminated because l1 contains at least comma *)
#Hl1nil @False_ind >Hl1nil in Hl1; cases l1' normalize
(consequently several lists = []) or not *)
*
[ * #Ha #Houtc1
-(* cut (l1 = [〈a,false〉])
- [ cases l1'' in Hl1cons; // #y #ly #Hly
- >Hly in Hl1; cases l1' in Hl1bits;
- [ #_ normalize #Hfalse destruct (Hfalse)
- | #p #lp #Hl1bits normalize #Heq destruct (Heq)
- @False_ind lapply (Hl1bits 〈a,false〉 ?)
- [ cases lp in e0;
- [ normalize #Hfalse destruct (Hfalse)
- | #p0 #lp0 normalize in ⊢ (%→?); #Heq destruct (Heq)
- @memb_cons @memb_hd ]
- | >Ha normalize #Hfalse destruct (Hfalse) ]
- ]
- ] #Hl1a
- cut (l4 = [〈a0,false〉])
- [ generalize in match Hl4bits; cases l4' in Hl4;
- [ >Hl4cons #Hfalse #_
- lapply (inj_append_singleton_l1 ?? [] ?? Hfalse)
- cases (reverse ? l4'') normalize
- [ #Hfalse1 | #p0 #lp0 #Hfalse1 ] destruct (Hfalse1)
- | #p #lp
-
- cases l4'' in Hl4cons; // #y #ly #Hly
- >Hly in Hl4; cases l4' in Hl4bits;
- [ #_ >reverse_cons #Hfalse
- lapply (inj_append_singleton_l1 ?? [] ?? Hfalse)
- -Hfalse cases ly normalize
- [ #Hfalse | #p #Hp #Hfalse ] destruct (Hfalse)
-
- | #p #lp #Hl1bits normalize #Heq destruct (Heq)
- @False_ind lapply (Hl1bits 〈a,false〉 ?)
- [ cases lp in e0;
- [ normalize #Hfalse destruct (Hfalse)
- | #p0 #lp0 normalize in ⊢ (%→?); #Heq destruct (Heq)
- @memb_cons @memb_hd ]
- | >Ha normalize #Hfalse destruct (Hfalse) ]
- ]
- ] #Hl1a
-
- >Hla normalize #Hl1 destruct (Hl1) lapply (inj_append_ @False_ind
-
- cut (l1'' = [] ∧ l4'' = [])
- [ % [ >Hla in Hl1; normalize #Hl1 destruct (Hl1)
-
- cases l1'' in Hl1bits;
-
- [ #_ normalize #H *)
cut (la = [] ∧ lb = [] ∧ l1'' = [] ∧ l4'' = [])
[ @daemon ] * * * #Hla1 #Hlb1 #Hl1nil #Hl4nil
>Hl1cons in Hl1; >Hla
projects / helm.git / blobdiff