include "turing/multi_universal/par_test.ma".
include "turing/multi_universal/moves_2.ma".
+lemma eq_vec_change_vec : ∀sig,n.∀v1,v2:Vector sig n.∀i,t,d.
+ nth i ? v2 d = t →
+ (∀j.i ≠ j → nth j ? v1 d = nth j ? v2 d) →
+ v2 = change_vec ?? v1 t i.
+#sig #n #v1 #v2 #i #t #d #H1 #H2 @(eq_vec … d)
+#i0 #Hlt cases (decidable_eq_nat i0 i) #Hii0
+[ >Hii0 >nth_change_vec //
+| >nth_change_vec_neq [|@sym_not_eq //] @sym_eq @H2 @sym_not_eq // ]
+qed.
+
+lemma right_mk_tape :
+ ∀sig,ls,c,rs.(c = None ? → ls = [ ] ∨ rs = [ ]) → right ? (mk_tape sig ls c rs) = rs.
+#sig #ls #c #rs cases c // cases ls
+[ cases rs //
+| #l0 #ls0 #H normalize cases (H (refl ??)) #H1 [ destruct (H1) | >H1 % ] ]
+qed.
+
+lemma left_mk_tape : ∀sig,ls,c,rs.left ? (mk_tape sig ls c rs) = ls.
+#sig #ls #c #rs cases c // cases ls // cases rs //
+qed.
+
+lemma current_mk_tape : ∀sig,ls,c,rs.current ? (mk_tape sig ls c rs) = c.
+#sig #ls #c #rs cases c // cases ls // cases rs //
+qed.
+
+lemma length_tail : ∀A,l.0 < |l| → |tail A l| < |l|.
+#A * normalize //
+qed.
+
+(*
+[ ] → [ ], l2, 1
+a::al →
+ [ ] → [ ], l1, 2
+ b::bl → match rec(al,bl)
+ x, y, 1 → b::x, y, 1
+ x, y, 2 → a::x, y, 2
+*)
+
+lemma lists_length_split :
+ ∀A.∀l1,l2:list A.(∃la,lb.(|la| = |l1| ∧ l2 = la@lb) ∨ (|la| = |l2| ∧ l1 = la@lb)).
+#A #l1 elim l1
+[ #l2 %{[ ]} %{l2} % % %
+| #hd1 #tl1 #IH *
+ [ %{[ ]} %{(hd1::tl1)} %2 % %
+ | #hd2 #tl2 cases (IH tl2) #x * #y *
+ [ * #IH1 #IH2 %{(hd2::x)} %{y} % normalize % //
+ | * #IH1 #IH2 %{(hd1::x)} %{y} %2 normalize % // ]
+ ]
+]
+qed.
+
+definition option_cons ≝ λsig.λc:option sig.λl.
+ match c with [ None ⇒ l | Some c0 ⇒ c0::l ].
+
+lemma opt_cons_tail_expand : ∀A,l.l = option_cons A (option_hd ? l) (tail ? l).
+#A * //
+qed.
+
definition match_test ≝ λsrc,dst.λsig:DeqSet.λn.λv:Vector ? n.
match (nth src (option sig) v (None ?)) with
[ None ⇒ false
]
qed.
-axiom daemon : ∀P:Prop.P.
-
-(* XXX: move to turing (or mono) *)
-definition option_cons ≝ λsig.λc:option sig.λl.
- match c with [ None ⇒ l | Some c0 ⇒ c0::l ].
-
definition R_match_step_true_naive ≝
λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
|left ? (nth src ? outt (niltape ?))| +
|left ? (nth src ? int (niltape ?))| +
|option_cons ? (current ? (nth dst ? int (niltape ?))) (right ? (nth dst ? int (niltape ?)))|.
-axiom right_mk_tape : ∀sig,ls,c,rs.right ? (mk_tape sig ls c rs) = rs.
-axiom left_mk_tape : ∀sig,ls,c,rs.left ? (mk_tape sig ls c rs) = ls.
-axiom current_mk_tape : ∀sig,ls,c,rs.current ? (mk_tape sig ls c rs) = c.
-axiom length_tail : ∀A,l.0 < |l| → |tail A l| < |l|.
-axiom lists_length_split :
- ∀A.∀l1,l2:list A.(∃la,lb.(|la| = |l1| ∧ l2 = la@lb) ∨ (|la| = |l2| ∧ l1 = la@lb)).
-axiom opt_cons_tail_expand : ∀A,l.l = option_cons A (option_hd ? l) (tail ? l).
-
lemma sem_match_step_termination :
∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
match_step src dst sig n ⊨
>nth_current_chars >nth_current_chars >Hcurtc_dst
cases (current ? (nth src …))
[normalize in ⊢ (%→?); #H destruct (H)
- | #x >nth_change_vec // cases (reverse ? rs0)
+ | #x >nth_change_vec [|@Hdst] cases (reverse ? rs0)
[ normalize in ⊢ (%→?); #H destruct (H)
| #r1 #rs1 normalize in ⊢ (%→?); #H destruct (H) ] ]
| * #rs0' * #_ #Hcurtc_src * #td * whd in ⊢ (%→?); * whd in ⊢ (??%?→?);
normalize in ⊢ (%→?); #H destruct (H) ]
| * #xs * #ci * #cj * #rs'' * #rs0' * * * #Hcicj #Hrs #Hrs0
#Htc * #td * * #Hmatch #Htd destruct (Htd) * #te * * *
- >Htc >change_vec_commute // >nth_change_vec //
- >change_vec_commute [|@sym_not_eq //] >nth_change_vec //
+ >Htc >change_vec_commute [|//] >nth_change_vec [|//]
+ >change_vec_commute [|@sym_not_eq //] >nth_change_vec [|//]
cases (lists_length_split ? ls ls0) #lsa * #lsb * * #Hlen #Hlsalsb
destruct (Hlsalsb) *
[ #Hte #_ #_ <(reverse_reverse … ls) in Hte; <(reverse_reverse … lsa)
@(list_cases2 … Hlen')
[ #H1 #H2 >H1 >H2 -H1 -H2 normalize in match (reverse ? [ ]); #Hte #_
lapply (Hte … (refl ??) … (refl ??) (refl ??)) -Hte
- >change_vec_commute // >change_vec_change_vec
+ >change_vec_commute [|//] >change_vec_change_vec
>change_vec_commute [|@sym_not_eq //] >change_vec_change_vec #Hte
- >Hte * * #_ >nth_change_vec // >reverse_reverse
+ >Hte * * #_ >nth_change_vec [|//] >reverse_reverse
#H lapply (H … (refl ??)) -H #Htb1 #Htb2
- cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (midtape sig [] s0 (xs@ci::rs'')) src) (mk_tape sig (s0::lsb) (option_hd sig (xs@cj::rs0')) (tail sig (xs@cj::rs0'))) dst)
- [@daemon] -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec //
- >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
- >right_mk_tape normalize in match (left ??);
+ cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (midtape sig [ ] s0 (xs@ci::rs'')) src) (mk_tape sig (s0::lsb) (option_hd sig (xs@cj::rs0')) (tail sig (xs@cj::rs0'))) dst)
+ [ @(eq_vec_change_vec … (niltape ?))
+ [@Htb1| #j #Hj <Htb2 // >(nth_change_vec_neq ??????? Hj) % ] ]
+ -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec [|//]
+ >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec [|//]
+ >right_mk_tape [|cases xs [|#x0 #xs0] normalize in ⊢ (??%?→?); #H destruct (H)]
+ normalize in match (left ??);
>Hmidta_src >Hmidta_dst >current_mk_tape <opt_cons_tail_expand
whd in match (option_cons ???); >Hrs0
normalize in ⊢ (?(?%)%); //
>H1 in Hlen'; >H2 whd in ⊢ (??%%→?); #Hlen'
>length_reverse >length_reverse destruct (Hlen') //
| /2 by refl, trans_eq/ ] -Hte
- #Hte #_ * * #_ >Hte >nth_change_vec // #Htb1 #Htb2
+ #Hte #_ * * #_ >Hte >nth_change_vec [|//] #Htb1 #Htb2
cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta
(mk_tape sig (hda::lsb) (option_hd ? (reverse sig (reverse sig xs@s0::reverse sig tla)@cj::rs0')) (tail ? (reverse sig (reverse sig xs@s0::reverse sig tla)@cj::rs0'))) dst)
(midtape ? [ ] hdb (reverse sig (reverse sig xs@s0::reverse sig tlb)@ci::rs'')) src)
- [@daemon] -Htb1 -Htb2 #Htb >Htb whd
- >nth_change_vec // >nth_change_vec_neq // >nth_change_vec //
- >right_mk_tape >Hmidta_src >Hmidta_dst
+ [ >change_vec_commute [|@sym_not_eq //] @(eq_vec_change_vec … (niltape ?))
+ [ @Htb1 %
+ | #j #Hj <Htb2 // >change_vec_commute // >change_vec_change_vec
+ >change_vec_commute [|@sym_not_eq //] >change_vec_change_vec
+ >nth_change_vec_neq in ⊢ (???%); // ] ]
+ -Htb1 -Htb2 #Htb >Htb whd
+ >nth_change_vec [|//] >nth_change_vec_neq [|//] >nth_change_vec [|//]
+ >right_mk_tape
+ [| cases (reverse sig (reverse sig xs@s0::reverse sig tla))
+ [|#x0 #xs0] normalize in ⊢ (??%?→?); #H destruct (H) ]
+ >Hmidta_src >Hmidta_dst
whd in match (left ??); whd in match (left ??); whd in match (right ??);
>current_mk_tape <opt_cons_tail_expand whd in match (option_cons ???);
>Hrs0 >length_append whd in ⊢ (??(??%)); >length_append >length_reverse
lapply (Hte … (refl ??) … (refl ??) (refl ??)) -Hte
>change_vec_change_vec >change_vec_commute [|@sym_not_eq //]
>change_vec_change_vec #Hte #_
- >Hte * * #_ >nth_change_vec // >reverse_reverse
+ >Hte * * #_ >nth_change_vec [|//] >reverse_reverse
#H lapply (H … (refl ??)) -H #Htb1 #Htb2
cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (mk_tape ? [s0] (option_hd ? (xs@cj::rs0')) (tail ? (xs@cj::rs0'))) dst)
(midtape ? lsb s0 (xs@ci::rs'')) src)
- [@daemon] -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec //
- >nth_change_vec_neq // >nth_change_vec //
- >right_mk_tape normalize in match (left ??);
+ [ >change_vec_commute [|@sym_not_eq //] @(eq_vec_change_vec … (niltape ?))
+ [ @Htb1
+ | #j #Hj <Htb2 // >nth_change_vec_neq in ⊢ (???%); // ] ]
+ -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec [|//]
+ >nth_change_vec_neq [|//] >nth_change_vec [|//]
+ >right_mk_tape
+ [| cases xs [|#x0 #xs0] normalize in ⊢ (??%?→?); #H destruct (H) ]
+ normalize in match (left ??);
>Hmidta_src >Hmidta_dst >current_mk_tape <opt_cons_tail_expand >Hrs0
>length_append normalize >length_append >length_append
<(reverse_reverse ? lsa) >H1 normalize //
>H1 in Hlen'; >H2 whd in ⊢ (??%%→?); #Hlen'
>length_reverse >length_reverse destruct (Hlen') //
| /2 by refl, trans_eq/ ] -Hte
- #Hte #_ * * #_ >Hte >nth_change_vec_neq // >nth_change_vec // #Htb1 #Htb2
+ #Hte #_ * * #_ >Hte >nth_change_vec_neq [|//] >nth_change_vec [|//] #Htb1 #Htb2
cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta
(mk_tape sig [hdb] (option_hd ? (reverse sig (reverse sig xs@s0::reverse sig tlb)@cj::rs0')) (tail ? (reverse sig (reverse sig xs@s0::reverse sig tlb)@cj::rs0'))) dst)
(midtape ? lsb hda (reverse sig (reverse sig xs@s0::reverse sig tla)@ci::rs'')) src)
- [@daemon] -Htb1 -Htb2 #Htb >Htb whd
- >nth_change_vec // >nth_change_vec_neq // >nth_change_vec //
- >right_mk_tape >Hmidta_src >Hmidta_dst
+ [ >change_vec_commute [|@sym_not_eq //] @(eq_vec_change_vec … (niltape ?))
+ [ @Htb1 %
+ | #j #Hj <Htb2 [|//] >change_vec_change_vec
+ >change_vec_commute [|@sym_not_eq //]
+ >change_vec_change_vec >nth_change_vec_neq in ⊢ (???%); // ] ]
+ -Htb1 -Htb2 #Htb >Htb whd
+ >nth_change_vec [|//] >nth_change_vec_neq [|//] >nth_change_vec [|//]
+ >right_mk_tape
+ [| cases (reverse sig (reverse sig xs@s0::reverse sig tlb))
+ [|#x0 #xs0] normalize in ⊢ (??%?→?); #H destruct (H) ]
+ >Hmidta_src >Hmidta_dst
whd in match (left ??); whd in match (left ??); whd in match (right ??);
>current_mk_tape <opt_cons_tail_expand
whd in match (option_cons ???);
lapply (Hte … (refl ??) … (refl ??)) -Hte #Hte destruct (Hte) * * #_
>Hmidta_dst #Htb1 lapply (Htb1 … (refl ??)) -Htb1 #Htb1 #Htb2
cut (tb = change_vec ?? ta (mk_tape ? (s0::lsa@lsb) (option_hd ? rs0) (tail ? rs0)) dst)
- [@daemon] -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec //
+ [@(eq_vec_change_vec … (niltape ?)) [@Htb1|@Htb2] ]
+ -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec [|//]
>nth_change_vec_neq [|@sym_not_eq //] >Hmidta_src >Hmidta_dst
- >right_mk_tape normalize in match (left ??); normalize in match (right ??);
+ >right_mk_tape
+ [| cases rs0 [ #_ %2 % | #x0 #xs0 normalize in ⊢ (??%?→?); #H destruct (H)] ]
+ normalize in match (left ??); normalize in match (right ??);
>Hmidta_src >Hmidta_dst >current_mk_tape <opt_cons_tail_expand
normalize //
| #hda #hdb #tla #tlb #H1 #H2 >H1 >H2
lapply (Hte ???? (refl ??) ? s0 ? (reverse ? tla) ?? (refl ??))
[ >length_reverse >length_reverse cut (|hda::tla| = |hdb::tlb|) //
normalize #H destruct (H) // ] #Hte #_ #_ #_
- * * #_ >Hte >nth_change_vec // #Htb1 #Htb2
+ * * #_ >Hte >nth_change_vec [|//] #Htb1 #Htb2
cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta
(mk_tape sig (hda::lsb) (option_hd ? (reverse sig (reverse sig tla)@s0::rs0)) (tail ? (reverse sig (reverse sig tla)@s0::rs0))) dst)
(midtape ? [ ] hdb (reverse sig (reverse sig tlb)@s::rs)) src)
- [@daemon] -Htb1 -Htb2 #Htb >Htb whd
- >nth_change_vec // >nth_change_vec_neq // >nth_change_vec //
- >right_mk_tape >Hmidta_src >Hmidta_dst
+ [ >change_vec_commute [|@sym_not_eq //] @(eq_vec_change_vec … (niltape ?))
+ [ @Htb1 //
+ | #j #Hj <Htb2 // >nth_change_vec_neq in ⊢ (???%); // ]]
+ -Htb1 -Htb2 #Htb >Htb whd
+ >nth_change_vec [|//] >nth_change_vec_neq [|//] >nth_change_vec [|//]
+ >right_mk_tape
+ [| cases (reverse sig (reverse sig tla))
+ [|#x0 #xs0] normalize in ⊢ (??%?→?); #H destruct (H) ]
+ >Hmidta_src >Hmidta_dst
whd in match (left ??); whd in match (left ??); whd in match (right ??);
>current_mk_tape <opt_cons_tail_expand >length_append
>length_reverse >length_reverse <(length_reverse ? ls) <Hlen'
lapply (Hte … (refl ??) … (refl ??)) -Hte #Hte destruct (Hte)
* * #_ >Hmidta_dst #Htb1 lapply (Htb1 … (refl ??)) -Htb1 #Htb1 #Htb2
cut (tb = change_vec (tape sig) (S n) ta (mk_tape ? (s0::ls0) (option_hd ? rs0) (tail ? rs0)) dst)
- [@daemon] -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec //
+ [ @(eq_vec_change_vec … (niltape ?)) // @Htb2 ]
+ -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec [|//]
>nth_change_vec_neq [|@sym_not_eq //] >Hmidta_src >Hmidta_dst
- >current_mk_tape >right_mk_tape normalize in ⊢ (??%); <opt_cons_tail_expand
+ >current_mk_tape >right_mk_tape
+ [| cases rs0 [ #_ %2 % | #x0 #xs0 normalize in ⊢ (??%?→?); #H destruct (H) ]]
+ normalize in ⊢ (??%); <opt_cons_tail_expand
normalize //
| #hda #hdb #tla #tlb #H1 #H2 >H1 >H2
>reverse_cons >reverse_cons #Hte #_ #_
| >length_reverse >length_reverse cut (|hda::tla| = |hdb::tlb|) //
normalize #H destruct (H) //
| /2 by refl, trans_eq/ ] -Hte
- #Hte * * #_ >Hte >nth_change_vec_neq // >nth_change_vec // #Htb1 #Htb2
+ #Hte * * #_ >Hte >nth_change_vec_neq [|//] >nth_change_vec [|//] #Htb1 #Htb2
cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta
(mk_tape sig [hdb] (option_hd ? (reverse sig (reverse sig tlb)@s0::rs0)) (tail ? (reverse sig (reverse sig tlb)@s0::rs0))) dst)
(midtape ? lsb hda (reverse sig (reverse sig tla)@s::rs)) src)
- [@daemon] -Htb1 -Htb2 #Htb >Htb whd
- >nth_change_vec // >nth_change_vec_neq // >nth_change_vec //
- >right_mk_tape >Hmidta_src >Hmidta_dst
+ [ >change_vec_commute [|@sym_not_eq //] @(eq_vec_change_vec … (niltape ?))
+ [ @Htb1 %
+ | #j #Hj <Htb2 // >change_vec_commute [|@sym_not_eq //]
+ >nth_change_vec_neq in ⊢ (???%); // ]]
+ -Htb1 -Htb2 #Htb >Htb whd
+ >nth_change_vec [|//] >nth_change_vec_neq [|//] >nth_change_vec [|//]
+ >right_mk_tape
+ [| cases (reverse ? (reverse ? tlb)) [|#x0 #xs0] normalize in ⊢ (??%?→?); #H destruct (H) ]
+ >Hmidta_src >Hmidta_dst
whd in match (left ??); whd in match (left ??); whd in match (right ??);
>current_mk_tape <opt_cons_tail_expand >length_append
normalize in ⊢ (??%); >length_append >reverse_reverse
projects / helm.git / blobdiff