]
qed.
+lemma memb_reverse: ∀S:DeqSet.∀a:S.∀l.
+ memb ? a l = true → memb ? a (reverse ? l) = true.
+#S #a #l elim l [normalize //]
+#b #tl #Hind #memba change with ([b]@tl) in match (b::tl);
+>reverse_append cases (orb_true_l … memba) #Hcase
+ [@memb_append_l2 >(\P Hcase) whd in match (reverse ??); @memb_hd
+ |@memb_append_l1 /2/
+ ]
+qed.
+
lemma mem_to_memb: ∀S:DeqSet.∀a,l. mem S a l → memb S a l = true.
#S #a #l elim l normalize
[@False_ind
(******************************** semantics ***********************************)
lemma sem_if: ∀sig.∀M1,M2,M3:TM sig.∀Rtrue,Rfalse,R2,R3,acc.
- M1 â\8a§ [acc: Rtrue,Rfalse] → M2 ⊨ R2 → M3 ⊨ R3 →
+ M1 â\8a¨ [acc: Rtrue,Rfalse] → M2 ⊨ R2 → M3 ⊨ R3 →
ifTM sig M1 M2 M3 acc ⊨ (Rtrue ∘ R2) ∪ (Rfalse ∘ R3).
#sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HR3 #t
cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse
definition loopM ≝ λsig,M,i,cin.
loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) cin.
+lemma loopM_unfold : ∀sig,M,i,cin.
+ loopM sig M i cin = loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) cin.
+// qed.
+
definition initc ≝ λsig.λM:TM sig.λt.
mk_config sig (states sig M) (start sig M) t.
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).
-
definition copy_step_subcase ≝
λalpha,c,elseM.ifTM ? (test_char ? (λx.x == 〈c,true〉))
(seq (FinProd alpha FinBool) (adv_mark_r …)
(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
*)
-include "turing/while_machine.ma".
include "turing/if_machine.ma".
+include "turing/basic_machines.ma".
include "turing/universal/alphabet.ma".
-include "turing/universal/tests.ma".
(* ADVANCE TO MARK (right)
@ex_intro [| % [ % | #ls0 #c0 #b0 #rs0 #H1 destruct (H1) % ] ] ]
qed.
-(* MOVE RIGHT
-
- moves the head one step to the right
-
-*)
-
-definition move_states ≝ initN 2.
-definition move0 : move_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
-definition move1 : move_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
-
-definition move_r ≝
- λalpha:FinSet.mk_TM alpha move_states
- (λp.let 〈q,a〉 ≝ p in
- match a with
- [ None ⇒ 〈move1,None ?〉
- | Some a' ⇒ match (pi1 … q) with
- [ O ⇒ 〈move1,Some ? 〈a',R〉〉
- | S q ⇒ 〈move1,None ?〉 ] ])
- move0 (λq.q == move1).
-
-definition R_move_r ≝ λalpha,t1,t2.
- ∀ls,c,rs.
- t1 = midtape alpha ls c rs →
- t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
-
-lemma sem_move_r :
- ∀alpha.Realize ? (move_r alpha) (R_move_r alpha).
-#alpha #intape @(ex_intro ?? 2) cases intape
-[ @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-|#a #al @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-|#a #al @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-| #ls #c #rs
- @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
- cases rs0 // ] ] ]
-qed.
-
-(* MOVE LEFT
-
- moves the head one step to the right
-
-*)
-
-definition move_l ≝
- λalpha:FinSet.mk_TM alpha move_states
- (λp.let 〈q,a〉 ≝ p in
- match a with
- [ None ⇒ 〈move1,None ?〉
- | Some a' ⇒ match pi1 … q with
- [ O ⇒ 〈move1,Some ? 〈a',L〉〉
- | S q ⇒ 〈move1,None ?〉 ] ])
- move0 (λq.q == move1).
-
-definition R_move_l ≝ λalpha,t1,t2.
- ∀ls,c,rs.
- t1 = midtape alpha ls c rs →
- t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
-
-lemma sem_move_l :
- ∀alpha.Realize ? (move_l alpha) (R_move_l alpha).
-#alpha #intape @(ex_intro ?? 2) cases intape
-[ @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-|#a #al @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-|#a #al @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-| #ls #c #rs
- @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
- cases ls0 // ] ] ]
-qed.
(* MOVE RIGHT AND MARK machine
| * #Hx0 #Houtc %2
% [ <(\P Hx) in Hx0; #Hx0 lapply (\Pf Hx0) @not_to_not #Hx' >Hx' %
| >Houtc % ]
- | (* members of lists are invariant under reverse *) @daemon ]
+ | #x #membx @Hl1 <(reverse_reverse …l1) @memb_reverse @membx ]
| %2 % [ @(\Pf Hc) ]
>Hintape in Hta; #Hta cases (Hta ? (refl ??)) -Hta #Hx #Hta
>Hx in Hc;#Hc destruct (Hc) ]
[ @(ex_intro ?? 2)
@(ex_intro ?? (mk_config ?? 〈mcl4,sep〉 (midtape ? lt c rt)))
% [ %
- [ >(\P Hc) >loop_S_false // >loop_S_true
+ [ >(\P Hc) >loopM_unfold >loop_S_false // >loop_S_true
[ @eq_f whd in ⊢ (??%?); >mcl_trans_init_sep %
|>(\P Hc) whd in ⊢(??(???(???%))?); >mcl_trans_init_sep % ]
|@Hfalse]
|@(ex_intro ?? 4) cases rt
[ @ex_intro
[|% [ %
- [ >loop_S_false // >mcl_q0_q1 //
+ [ >loopM_unfold >loop_S_false // >mcl_q0_q1 //
| normalize in ⊢ (%→?); @Hfalse]
| normalize in ⊢ (%→?); #_ #H1 @False_ind @(absurd ?? H1) % ] ]
| #r0 #rt0 @ex_intro
[| % [ %
- [ >loop_S_false // >mcl_q0_q1 //
+ [ >loopM_unfold >loop_S_false // >mcl_q0_q1 //
| #_ #a #b #ls #rs #Hb destruct (Hb) %
[ @(\Pf Hc)
| >mcl_q1_q2 >mcl_q2_q3 cases ls normalize // ] ]
\ / GNU General Public License Version 2
V_____________________________________________________________*)
-include "turing/universal/move_char_c.ma".
+(* include "turing/universal/move_char_c.ma". *)
include "turing/universal/move_char_l.ma".
include "turing/universal/tuples.ma".
[ #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) %
- |@daemon ]
+ |@(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 :
∨
(no_bars rs1 ∧ t2 = midtape ? (reverse ? rs1@c::ls) 〈grid,false〉 rs2).
+axiom daemon :∀P:Prop.P.
+
axiom tech_split :
∀A:DeqSet.∀f,l.
(∀x.memb A x l = true → f x = false) ∨
[whd in ⊢ (??%?); >q_low_head_false in Hq_low;
whd in ⊢ ((???%)→?); generalize in match (h qin);
#x #H destruct (H) %
- |>Ht2 whd in match (step ???);
+ |>Ht2 whd in match (step FinBool ??);
whd in match (trans ???);
>(eq_pair_fst_snd … (t ?))
@is_low_config // >Hlift
#q #Htd #tape1 #Htb
lapply (IH (\fst (trans ? M 〈q,current ? tape1〉)) Htd) -IH
#IH cases (Htc … Htb); -Htc #Hhaltq
- whd in match (step ???); >(eq_pair_fst_snd ?? (trans ???))
+ whd in match (step FinBool ??); >(eq_pair_fst_snd ?? (trans ???))
#Htc change with (mk_config ????) in Htc:(???(??%));
cases (IH ? Htc) #q1 * #tape2 * * #HRTM #Hhaltq1 #Houtc
@(ex_intro … q1) @(ex_intro … tape2) %
[%
[cases HRTM #k * #outc1 * #Hloop #Houtc1
@(ex_intro … (S k)) @(ex_intro … outc1) %
- [>loop_S_false [2://] whd in match (step ???);
+ [>loop_S_false [2://] whd in match (step FinBool ??);
>(eq_pair_fst_snd ?? (trans ???)) @Hloop
|@Houtc1
]
projects / helm.git / commitdiff