From: Wilmer Ricciotti Date: Tue, 22 Jan 2013 09:57:18 +0000 (+0000) Subject: Removed all axioms in unistep_aux X-Git-Tag: make_still_working~1319 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9971fb3f00ed1d0749622afa8d0523e3e923a1a3;p=helm.git Removed all axioms in unistep_aux --- diff --git a/matita/matita/lib/turing/multi_universal/moves_2.ma b/matita/matita/lib/turing/multi_universal/moves_2.ma index d86b89a6a..807823f74 100644 --- a/matita/matita/lib/turing/multi_universal/moves_2.ma +++ b/matita/matita/lib/turing/multi_universal/moves_2.ma @@ -321,6 +321,23 @@ lapply (sem_while … (sem_mte_step sig R) … Hloop) // | #ls1 #c1 #rs1 #H destruct (H) >reverse_cons >associative_append @IH % ] ] ] qed. +lemma terminate_move_to_end_r : ∀sig,t.move_to_end sig R ↓ t. +#sig #t @(terminate_while … (sem_mte_step sig R …)) // +cases t +[ % #t1 * #ls * #c * #rs * #H destruct +|2,3: #a0 #al0 % #t1 * #ls * #c * #rs * #H destruct +| #ls #c #rs lapply c -c lapply ls -ls elim rs + [ #ls #c % #t1 * #ls0 * #c0 * #rs0 * #Hmid #Ht1 destruct % + #t2 * #ls1 * #c1 * #rs1 * normalize in ⊢ (%→?); #H destruct + | #r0 #rs0 #IH #ls #c % #t1 * #ls1 * #c1 * #rs1 * #Hmid #Ht1 destruct @IH + ] +] +qed. + +lemma sem_move_to_end_r : ∀sig. move_to_end sig R ⊨ R_move_to_end_r sig. +#sig @WRealize_to_Realize // +qed. + definition R_move_to_end_l ≝ λsig,int,outt. (current ? int = None ? → outt = int) ∧ @@ -340,4 +357,21 @@ lapply (sem_while … (sem_mte_step sig L) … Hloop) // lapply (IH Hfalse) -IH * #_ #IH % [ normalize in ⊢ (%→?); #H destruct (H) | #ls1 #c1 #rs1 #H destruct (H) >reverse_cons >associative_append @IH % ] ] ] -qed. \ No newline at end of file +qed. + +lemma terminate_move_to_end_l : ∀sig,t.move_to_end sig L ↓ t. +#sig #t @(terminate_while … (sem_mte_step sig L …)) // +cases t +[ % #t1 * #ls * #c * #rs * #H destruct +|2,3: #a0 #al0 % #t1 * #ls * #c * #rs * #H destruct +| #ls elim ls + [ #c #rs % #t1 * #ls0 * #c0 * #rs0 * #Hmid #Ht1 destruct % + #t2 * #ls1 * #c1 * #rs1 * normalize in ⊢ (%→?); #H destruct + | #l0 #ls0 #IH #c #rs % #t1 * #ls1 * #c1 * #rs1 * #Hmid #Ht1 destruct @IH + ] +] +qed. + +lemma sem_move_to_end_l : ∀sig. move_to_end sig L ⊨ R_move_to_end_l sig. +#sig @WRealize_to_Realize // +qed. diff --git a/matita/matita/lib/turing/multi_universal/unistep_aux.ma b/matita/matita/lib/turing/multi_universal/unistep_aux.ma index b1f111409..4f37564c0 100644 --- a/matita/matita/lib/turing/multi_universal/unistep_aux.ma +++ b/matita/matita/lib/turing/multi_universal/unistep_aux.ma @@ -52,6 +52,60 @@ include "turing/multi_universal/tuples.ma". cfg_to_obj *) +definition copy_char_states ≝ initN 3. + +definition cc0 : copy_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)). +definition cc1 : copy_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)). + +definition trans_copy_char ≝ + λsrc,dst.λsig:FinSet.λn. + λp:copy_char_states × (Vector (option sig) (S n)). + let 〈q,a〉 ≝ p in + match pi1 … q with + [ O ⇒ 〈cc1,change_vec ? (S n) + (change_vec ? (S n) (null_action ? n) (〈None ?,R〉) src) + (〈nth src ? a (None ?),R〉) dst〉 + | S _ ⇒ 〈cc1,null_action ? n〉 ]. + +definition copy_char ≝ + λsrc,dst,sig,n. + mk_mTM sig n copy_char_states (trans_copy_char src dst sig n) + cc0 (λq.q == cc1). + +definition R_copy_char ≝ + λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n). + outt = change_vec ?? + (change_vec ?? int + (tape_move_mono ? (nth src ? int (niltape ?)) 〈None ?, R〉) src) + (tape_move_mono ? (nth dst ? int (niltape ?)) + 〈current ? (nth src ? int (niltape ?)), R〉) dst. + +lemma copy_char_q0_q1 : + ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n → + step sig n (copy_char src dst sig n) (mk_mconfig ??? cc0 v) = + mk_mconfig ??? cc1 + (change_vec ? (S n) + (change_vec ?? v + (tape_move_mono ? (nth src ? v (niltape ?)) 〈None ?, R〉) src) + (tape_move_mono ? (nth dst ? v (niltape ?)) 〈current ? (nth src ? v (niltape ?)), R〉) dst). +#src #dst #sig #n #v #Heq #Hsrc #Hdst +whd in ⊢ (??%?); +<(change_vec_same … v dst (niltape ?)) in ⊢ (??%?); +<(change_vec_same … v src (niltape ?)) in ⊢ (??%?); +>tape_move_multi_def @eq_f2 // +>pmap_change >pmap_change tape_move_null_action @eq_f2 // @eq_f2 +[ >change_vec_same % +| >change_vec_same >change_vec_same // ] +qed. + +lemma sem_copy_char: + ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n → + copy_char src dst sig n ⊨ R_copy_char src dst sig n. +#src #dst #sig #n #Hneq #Hsrc #Hdst #int +%{2} % [| % [ % | whd >copy_char_q0_q1 // ]] +qed. + definition obj ≝ (0:DeqNat). definition cfg ≝ (1:DeqNat). definition prg ≝ (2:DeqNat). @@ -59,7 +113,7 @@ definition prg ≝ (2:DeqNat). definition obj_to_cfg ≝ mmove cfg FSUnialpha 2 L · (ifTM ?? (inject_TM ? (test_null ?) 2 obj) - (copy_step obj cfg FSUnialpha 2 · + (copy_char obj cfg FSUnialpha 2 · mmove cfg FSUnialpha 2 L · mmove obj FSUnialpha 2 L) (inject_TM ? (write FSUnialpha null) 2 cfg) @@ -78,7 +132,6 @@ definition R_obj_to_cfg ≝ λt1,t2:Vector (tape FSUnialpha) 3. (mk_tape ? [ ] (option_hd FSUnialpha (reverse ? (null::ls))) (tail ? (reverse ? (null::ls)))) cfg). -axiom sem_move_to_end_l : ∀sig. move_to_end sig L ⊨ R_move_to_end_l sig. axiom accRealize_to_Realize : ∀sig,n.∀M:mTM sig n.∀Rtrue,Rfalse,acc. M ⊨ [ acc: Rtrue, Rfalse ] → M ⊨ Rtrue ∪ Rfalse. @@ -116,7 +169,7 @@ lemma sem_obj_to_cfg : obj_to_cfg ⊨ R_obj_to_cfg. (sem_seq ?????? (sem_if ?????????? (sem_test_null_multi ?? obj ?) - (sem_seq ?????? (accRealize_to_Realize … (sem_copy_step …)) + (sem_seq ?????? (sem_copy_char …) (sem_seq ?????? (sem_move_multi ? 2 cfg L ?) (sem_move_multi ? 2 obj L ?))) (sem_inject ???? cfg ? (sem_write FSUnialpha null))) @@ -126,8 +179,11 @@ lemma sem_obj_to_cfg : obj_to_cfg ⊨ R_obj_to_cfg. #tc * whd in ⊢ (%→?); #Htc * #td * * [ * #te * * #Hcurtc #Hte - * destruct (Hte) #te * * - [ whd in ⊢ (%→%→?); * #x * #y * * -Hcurtc #Hcurtc1 #Hcurtc2 #Hte + * destruct (Hte) #te * whd in ⊢ (%→?); #Hte + cut (∃x.current ? (nth obj ? tc (niltape ?)) = Some ? x) + [ cases (current ? (nth obj ? tc (niltape ?))) in Hcurtc; + [ * #H @False_ind /2/ | #x #_ %{x} % ] ] * #x #Hcurtc' +(* [ whd in ⊢ (%→%→?); * #x * #y * * -Hcurtc #Hcurtc1 #Hcurtc2 #Hte *) * #tf * whd in ⊢ (%→%→?); #Htf #Htd * #tg * * * whd in ⊢ (%→%→%→%→?); #Htg1 #Htg2 #Htg3 #Htb #c #ls #Hta1 % @@ -136,8 +192,8 @@ lemma sem_obj_to_cfg : obj_to_cfg ⊨ R_obj_to_cfg. cut (tg = change_vec ?? td (mk_tape ? [ ] (None ?) (reverse ? ls@[x])) cfg) [ lapply (eq_vec_change_vec ??????? (Htg2 ls x [ ] ?) Htg3) // >Htd >nth_change_vec_neq // >Htf >nth_change_vec // - >Hte >nth_change_vec // >Htc >nth_change_vec // ] -Htg1 -Htg2 -Htg3 #Htg - destruct + >Hte >Hcurtc' >nth_change_vec // >Htc >nth_change_vec // ] + -Htg1 -Htg2 -Htg3 #Htg destruct >change_vec_change_vec >change_vec_change_vec >change_vec_commute // >change_vec_change_vec >change_vec_commute [|@sym_not_eq //] >change_vec_change_vec @@ -149,18 +205,12 @@ lemma sem_obj_to_cfg : obj_to_cfg ⊨ R_obj_to_cfg. [ #Hta2 whd in match (tape_move ???); tape_move_mk_tape_R [| #_ % %] >reverse_cons - >nth_change_vec_neq in Hcurtc1; [|@sym_not_eq //] >Hta2 + >nth_change_vec_neq in Hcurtc'; [|@sym_not_eq //] >Hta2 normalize in ⊢ (%→?); #H destruct (H) % ] - | #Hta2 >Htc in Hcurtc1; >nth_change_vec_neq [| @sym_not_eq //] + | #Hta2 >Htc in Hcurtc'; >nth_change_vec_neq [| @sym_not_eq //] >Hta2 #H destruct (H) ] - | * #Hcurtc0 #Hte #_ #_ #c #ls #Hta1 >Hta1 in Htc; >eq_mk_tape_rightof - whd in match (tape_move ???); #Htc >Htc in Hcurtc0; * - [ >Htc in Hcurtc; >nth_change_vec_neq [|@sym_not_eq //] - #Hcurtc #Hcurtc0 >Hcurtc0 in Hcurtc; * #H @False_ind @H % - | >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H) ] - ] | * #te * * #Hcurtc #Hte * whd in ⊢ (%→%→?); #Htd1 #Htd2 * #tf * * * #Htf1 #Htf2 #Htf3 whd in ⊢ (%→?); #Htb @@ -203,60 +253,6 @@ lemma sem_test_null_char : | tape_move_multi_def @eq_f2 // ->pmap_change >pmap_change tape_move_null_action @eq_f2 // @eq_f2 -[ >change_vec_same % -| >change_vec_same >change_vec_same // ] -qed. - -lemma sem_copy_char: - ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n → - copy_char src dst sig n ⊨ R_copy_char src dst sig n. -#src #dst #sig #n #Hneq #Hsrc #Hdst #int -%{2} % [| % [ % | whd >copy_char_q0_q1 // ]] -qed. - definition cfg_to_obj ≝ mmove cfg FSUnialpha 2 L · (ifTM ?? (inject_TM ? test_null_char 2 cfg)