From: Wilmer Ricciotti Date: Thu, 17 May 2012 16:33:59 +0000 (+0000) Subject: Progress X-Git-Tag: make_still_working~1714 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=64a59f1d6a60237ad78234f2bf90c0e5eb8c89ce;p=helm.git Progress --- diff --git a/matita/matita/lib/turing/universal/copy.ma b/matita/matita/lib/turing/universal/copy.ma index 467055248..3403d5555 100644 --- a/matita/matita/lib/turing/universal/copy.ma +++ b/matita/matita/lib/turing/universal/copy.ma @@ -130,21 +130,23 @@ definition copy_step ≝ definition R_copy_step_true ≝ λt1,t2. - ∀a,l1,x0,a0,l2,c,l3. - t1 = midtape STape (l1@〈a0,false〉::〈x0,true〉::l2) - 〈c,true〉 (〈a,false〉::l3) → - (∀c.memb ? c l1 = true → is_marked ? c = false) → - (∃x. c = bit x ∧ - t2 = midtape STape (〈bit x,false〉::l1@〈a0,true〉::〈bit x,false〉::l2) 〈a,true〉 l3) ∨ - (c = null ∧ - t2 = midtape ? (〈null,false〉::l1@〈a0,true〉::〈x0,false〉::l2) 〈a,true〉 l3). + ∀ls,c,rs. t1 = midtape STape ls 〈c,true〉 rs → + bit_or_null c = true ∧ + (∀a,l1,x0,a0,l2,l3. + ls = (l1@〈a0,false〉::〈x0,true〉::l2) → + rs = (〈a,false〉::l3) → + no_marks l1 → + ((∃x. c = bit x ∧ + t2 = midtape STape (〈bit x,false〉::l1@〈a0,true〉::〈bit x,false〉::l2) 〈a,true〉 l3) ∨ + (c = null ∧ + t2 = midtape ? (〈null,false〉::l1@〈a0,true〉::〈x0,false〉::l2) 〈a,true〉 l3))). definition R_copy_step_false ≝ λt1,t2. ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs → bit_or_null (\fst c) = false ∧ t2 = t1. -axiom sem_comp_step : +axiom sem_copy_step : accRealize ? copy_step (inr … (inl … (inr … 0))) R_copy_step_true R_copy_step_false. (* @@ -171,16 +173,83 @@ definition R_copy0 ≝ λt1,t2. t1 = midtape STape (l3@l4@〈c0,true〉::ls) 〈c,true〉 (l1@rs) → no_marks l1 → no_marks (l3@l4) → |l1| = |l4| → ∀l1',bv.〈c,false〉::l1 = l1'@[〈comma,bv〉] → only_bits_or_nulls l1' → - ∀l4',bg.l4@[〈c0,true〉] = 〈grid,bg〉::l4' → only_bits_or_nulls l4' → + ∀l4',bg.l4@[〈c0,false〉] = 〈grid,bg〉::l4' → only_bits_or_nulls l4' → (c = comma ∧ t2 = t1) ∨ (c ≠ comma ∧ t2 = midtape ? (reverse ? l1'@l3@〈grid,true〉:: merge_config l4' (reverse ? l1')@ls) 〈comma,true〉 rs). -axiom sem_copy0 : Realize ? copy0 R_copy0. +lemma wsem_copy0 : WRealize ? copy0 R_copy0. +#intape #k #outc #Hloop +lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop +* #ta * #Hstar @(star_ind_l ??????? Hstar) +[ #tb whd in ⊢ (%→?); #Hleft + #ls #c #c0 #rs #l1 #l3 #l4 #Htb #Hl1nomarks #Hl3l4nomarks #Hlen #l1' #bv + #Hl1 #Hl1bits #l4' #bg #Hl4 #Hl4bits + cases (Hleft … Htb) -Hleft #Hc #Houtc % % + [ generalize in match Hl1bits; -Hl1bits cases l1' in Hl1; + [ normalize #Hl1 #c1 destruct (Hl1) % + | * #c' #b' #l0 #Heq normalize in Heq; destruct (Heq) + #Hl1bits lapply (Hl1bits 〈c',false〉 ?) [ @memb_hd ] + >Hc #Hfalse destruct ] + | @Houtc ] +| #tb #tc #td whd in ⊢ (%→?→(?→%)→%→?); #Htc #Hstar1 #Hind #Htd + lapply (Hind Htd) -Hind #Hind + #ls #c #c0 #rs #l1 #l3 #l4 #Htb #Hl1nomarks #Hl3l4nomarks #Hlen #l1' #bv + #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 + @(list_cases_2 … Hlen1) + [ #Hl1nil @False_ind >Hl1nil in Hl1; cases l1' normalize + [ #Hl1 destruct normalize in Hcbitnull; destruct (Hcbitnull) + | #p0 #l0 normalize #Hfalse destruct (Hfalse) cases l0 in e0; + [ normalize #Hfalse1 destruct (Hfalse1) + | #p0' #l0' normalize #Hfalse1 destruct (Hfalse1) ] ] + | * #a #ba * #a0 #ba0 #l1'' #l4'' #Hl1cons #Hl4cons + lapply (eq_f ?? (reverse ?) ?? Hl4cons) >reverse_reverse >reverse_cons -Hl4cons #Hl4cons + cut (ba = false) [ @daemon ] #Hba + cut (ba0 = false) [ @daemon ] #Hba0 + >Hba0 in Hl4cons; >Hba in Hl1cons; -Hba0 -Hba #Hl1cons #Hl4cons + >Hl4cons in Htc; >Hl1cons #Htc + lapply (Htc a (l3@reverse ? l4'') c0 a0 ls (l1''@rs) ? (refl ??) ?) + [ #x #Hx @Hl3l4nomarks >Hl4cons associative_append >associative_append % + | -Htc * + [ * #x * #Hx #Htc + lapply (Hind (〈bit x,false〉::ls) a a0 rs l1'' + (〈bit x,false〉::l3) (reverse ? l4'') ????) + [ >Hl1cons in Hlen; >Hl4cons >length_append >commutative_plus + normalize #Hlen destruct (Hlen) // + | #x0 #Hx0 cases (orb_true_l … Hx0) + [ #Hx0eq >(\P Hx0eq) % + | -Hx0 #Hx0 @Hl3l4nomarks >Hl4cons + Hl1cons @memb_cons // + | >Htc >associative_append % + | -Hind + cut (∃la.l1' = 〈c,false〉::la) + [ >Hl1cons in Hl1; cases l1' + [normalize #Hfalse destruct (Hfalse) + | #p #la normalize #Hla destruct (Hla) @(ex_intro ?? la) % ] ] + * #la #Hla + cut (∃lb.l4' = lb@[〈c0,false〉]) + [ >Hl4cons in Hl4; + @(list_elim_left … l4') + (* si usa l'iniettività del "cons destro" + [ normalize + | #p #lb + cases l4' + [normalize + | #p #lb *) + + @(list_elim_left … l4') +