From 5fc2b08d86038360e588b8fff333a623964efabe Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 28 May 2012 13:33:45 +0000 Subject: [PATCH 1/1] porting of move_char_c --- matita/matita/lib/turing/mono.ma | 1 - matita/matita/lib/turing/universal/copy.ma | 26 +- .../lib/turing/universal/move_char_c.ma | 93 +++--- .../matita/lib/turing/universal/move_tape.ma | 12 +- .../lib/turing/universal/trans_to_tuples.ma | 307 ++++++++++++++++++ 5 files changed, 376 insertions(+), 63 deletions(-) create mode 100644 matita/matita/lib/turing/universal/trans_to_tuples.ma diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma index 7d6bad37f..f041d8b25 100644 --- a/matita/matita/lib/turing/mono.ma +++ b/matita/matita/lib/turing/mono.ma @@ -39,7 +39,6 @@ definition right ≝ | rightof _ _ ⇒ [] | midtape _ _ r ⇒ r ]. - definition current ≝ λsig.λt:tape sig.match t with [ midtape _ c _ ⇒ Some ? c diff --git a/matita/matita/lib/turing/universal/copy.ma b/matita/matita/lib/turing/universal/copy.ma index 019f06540..854b6e158 100644 --- a/matita/matita/lib/turing/universal/copy.ma +++ b/matita/matita/lib/turing/universal/copy.ma @@ -10,21 +10,20 @@ V_____________________________________________________________*) -(* COMPARE BIT - -*) - 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 q with - [ O ⇒ 〈1,Some ? 〈c,N〉〉 - | S _ ⇒ 〈1,None ?〉 ]) - O (λx.x == 1). + 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. @@ -147,7 +146,7 @@ definition R_copy_step_false ≝ bit_or_null (\fst c) = false ∧ t2 = t1. axiom sem_copy_step : - accRealize ? copy_step (inr … (inl … (inr … 0))) R_copy_step_true R_copy_step_false. + accRealize ? copy_step (inr … (inl … (inr … start_nop))) R_copy_step_true R_copy_step_false. (* 1) il primo carattere è marcato @@ -155,7 +154,7 @@ axiom sem_copy_step : 3) il terminatore non è né bit, né null *) -definition copy0 ≝ whileTM ? copy_step (inr … (inl … (inr … 0))). +definition copy0 ≝ whileTM ? copy_step (inr … (inl … (inr … start_nop))). let rec merge_config (l1,l2:list STape) ≝ match l1 with @@ -201,11 +200,6 @@ lemma inj_append_singleton_l2 : >reverse_append >reverse_append normalize #H1 destruct % qed. -lemma length_reverse : ∀A,l.|reverse A l| = |l|. -#A #l elim l // -#a0 #l0 #IH normalize >rev_append_def >length_append >IH normalize // -qed. - lemma wsem_copy0 : WRealize ? copy0 R_copy0. #intape #k #outc #Hloop lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop @@ -272,7 +266,7 @@ lapply (sem_while … sem_copy_step intape k outc Hloop) [%] -Hloop [|normalize in Hl1; destruct (Hl1) %] >(?:l4 = 〈grid,bg〉::lb) [|@(inj_append_singleton_l1 ?? (〈grid,bg〉::lb) ?? Hl4) ] - >length_append >commutative_plus >length_reverse + >length_append >commutative_plus >length_reverse normalize #Hlalb destruct (Hlalb) // ] #Hlen2 * diff --git a/matita/matita/lib/turing/universal/move_char_c.ma b/matita/matita/lib/turing/universal/move_char_c.ma index f970da13e..4d2490ee0 100644 --- a/matita/matita/lib/turing/universal/move_char_c.ma +++ b/matita/matita/lib/turing/universal/move_char_c.ma @@ -35,39 +35,46 @@ include "turing/while_machine.ma". definition mcc_states : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 5) alpha. +definition mcc0 : initN 5 ≝ mk_Sig ?? 0 (leb_true_to_le 1 5 (refl …)). +definition mcc1 : initN 5 ≝ mk_Sig ?? 1 (leb_true_to_le 2 5 (refl …)). +definition mcc2 : initN 5 ≝ mk_Sig ?? 2 (leb_true_to_le 3 5 (refl …)). +definition mcc3 : initN 5 ≝ mk_Sig ?? 3 (leb_true_to_le 4 5 (refl …)). +definition mcc4 : initN 5 ≝ mk_Sig ?? 4 (leb_true_to_le 5 5 (refl …)). + definition mcc_step ≝ λalpha:FinSet.λsep:alpha. mk_TM alpha (mcc_states alpha) (λp.let 〈q,a〉 ≝ p in let 〈q',b〉 ≝ q in + let q' ≝ pi1 nat (λi.i<5) q' in (* perche' devo passare il predicato ??? *) match a with - [ None ⇒ 〈〈4,sep〉,None ?〉 - | Some a' ⇒ + [ None ⇒ 〈〈mcc4,sep〉,None ?〉 + | Some a' ⇒ match q' with [ O ⇒ (* qinit *) match a' == sep with - [ true ⇒ 〈〈4,sep〉,None ?〉 - | false ⇒ 〈〈1,a'〉,Some ? 〈a',L〉〉 ] - | S q' ⇒ match q' with + [ true ⇒ 〈〈mcc4,sep〉,None ?〉 + | false ⇒ 〈〈mcc1,a'〉,Some ? 〈a',L〉〉 ] + | S q' ⇒ match q' with [ O ⇒ (* q1 *) - 〈〈2,a'〉,Some ? 〈b,R〉〉 + 〈〈mcc2,a'〉,Some ? 〈b,R〉〉 | S q' ⇒ match q' with [ O ⇒ (* q2 *) - 〈〈3,sep〉,Some ? 〈b,R〉〉 + 〈〈mcc3,sep〉,Some ? 〈b,R〉〉 | S q' ⇒ match q' with [ O ⇒ (* qacc *) - 〈〈3,sep〉,None ?〉 + 〈〈mcc3,sep〉,None ?〉 | S q' ⇒ (* qfail *) - 〈〈4,sep〉,None ?〉 ] ] ] ] ]) - 〈0,sep〉 - (λq.let 〈q',a〉 ≝ q in q' == 3 ∨ q' == 4). + 〈〈mcc4,sep〉,None ?〉 ] ] ] ] ]) + 〈mcc0,sep〉 + (λq.let 〈q',a〉 ≝ q in q' == mcc3 ∨ q' == mcc4). lemma mcc_q0_q1 : ∀alpha:FinSet.∀sep,a,ls,a0,rs. a0 == sep = false → step alpha (mcc_step alpha sep) - (mk_config ?? 〈0,a〉 (mk_tape … ls (Some ? a0) rs)) = - mk_config alpha (states ? (mcc_step alpha sep)) 〈1,a0〉 + (mk_config ?? 〈mcc0,a〉 (mk_tape … ls (Some ? a0) rs)) = + mk_config alpha (states ? (mcc_step alpha sep)) 〈mcc1,a0〉 (tape_move_left alpha ls a0 rs). #alpha #sep #a * [ #a0 #rs #Ha0 whd in ⊢ (??%?); @@ -80,8 +87,8 @@ qed. lemma mcc_q1_q2 : ∀alpha:FinSet.∀sep,a,ls,a0,rs. step alpha (mcc_step alpha sep) - (mk_config ?? 〈1,a〉 (mk_tape … ls (Some ? a0) rs)) = - mk_config alpha (states ? (mcc_step alpha sep)) 〈2,a0〉 + (mk_config ?? 〈mcc1,a〉 (mk_tape … ls (Some ? a0) rs)) = + mk_config alpha (states ? (mcc_step alpha sep)) 〈mcc2,a0〉 (tape_move_right alpha ls a rs). #alpha #sep #a #ls #a0 * // qed. @@ -89,8 +96,8 @@ qed. lemma mcc_q2_q3 : ∀alpha:FinSet.∀sep,a,ls,a0,rs. step alpha (mcc_step alpha sep) - (mk_config ?? 〈2,a〉 (mk_tape … ls (Some ? a0) rs)) = - mk_config alpha (states ? (mcc_step alpha sep)) 〈3,sep〉 + (mk_config ?? 〈mcc2,a〉 (mk_tape … ls (Some ? a0) rs)) = + mk_config alpha (states ? (mcc_step alpha sep)) 〈mcc3,sep〉 (tape_move_right alpha ls a rs). #alpha #sep #a #ls #a0 * // qed. @@ -109,38 +116,44 @@ definition Rmcc_step_false ≝ lemma mcc_trans_init_sep: ∀alpha,sep,x. - trans ? (mcc_step alpha sep) 〈〈0,x〉,Some ? sep〉 = 〈〈4,sep〉,None ?〉. + trans ? (mcc_step alpha sep) 〈〈mcc0,x〉,Some ? sep〉 = 〈〈mcc4,sep〉,None ?〉. #alpha #sep #x normalize >(\b ?) // qed. lemma mcc_trans_init_not_sep: ∀alpha,sep,x,y.y == sep = false → - trans ? (mcc_step alpha sep) 〈〈0,x〉,Some ? y〉 = 〈〈1,y〉,Some ? 〈y,L〉〉. + trans ? (mcc_step alpha sep) 〈〈mcc0,x〉,Some ? y〉 = 〈〈mcc1,y〉,Some ? 〈y,L〉〉. #alpha #sep #x #y #H1 normalize >H1 // qed. lemma sem_mcc_step : ∀alpha,sep. accRealize alpha (mcc_step alpha sep) - 〈3,sep〉 (Rmcc_step_true alpha sep) (Rmcc_step_false alpha sep). -#alpha #sep * + 〈mcc3,sep〉 (Rmcc_step_true alpha sep) (Rmcc_step_false alpha sep). +#alpha #sep +cut (∀P:Prop.〈mcc4,sep〉=〈mcc3,sep〉→P) + [#P whd in ⊢ ((??(???%?)(???%?))→?); #Hfalse destruct] #Hfalse +* [@(ex_intro ?? 2) - @(ex_intro … (mk_config ?? 〈4,sep〉 (niltape ?))) - % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 @False_ind @(absurd ?? H2) %] + @(ex_intro … (mk_config ?? 〈mcc4,sep〉 (niltape ?))) % + [% [whd in ⊢ (??%?); % | @Hfalse] + |#H1 #H2 @False_ind @(absurd ?? H2) %] |#l0 #lt0 @(ex_intro ?? 2) - @(ex_intro … (mk_config ?? 〈4,sep〉 (leftof ? l0 lt0))) - % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 @False_ind @(absurd ?? H2) %] + @(ex_intro … (mk_config ?? 〈mcc4,sep〉 (leftof ? l0 lt0)))% + [% [whd in ⊢ (??%?);% |@Hfalse] + |#H1 #H2 @False_ind @(absurd ?? H2) %] |#r0 #rt0 @(ex_intro ?? 2) - @(ex_intro … (mk_config ?? 〈4,sep〉 (rightof ? r0 rt0))) - % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 #H3 @False_ind @(absurd ?? H3) %] + @(ex_intro … (mk_config ?? 〈mcc4,sep〉 (rightof ? r0 rt0))) % + [% [whd in ⊢ (??%?);% |@Hfalse] + |#H1 #H2 #H3 @False_ind @(absurd ?? H3) %] | #lt #c #rt cases (true_or_false (c == sep)) #Hc [ @(ex_intro ?? 2) - @(ex_intro ?? (mk_config ?? 〈4,sep〉 (midtape ? lt c rt))) + @(ex_intro ?? (mk_config ?? 〈mcc4,sep〉 (midtape ? lt c rt))) % [ % [ >(\P Hc) >loop_S_false // >loop_S_true [ @eq_f whd in ⊢ (??%?); >mcc_trans_init_sep % |>(\P Hc) whd in ⊢(??(???(???%))?); >mcc_trans_init_sep % ] - | #Hfalse destruct ] + |@Hfalse] |#_ #H1 #H2 % // normalize >(\P Hc) % ] | @(ex_intro ?? 4) cases lt [ @ex_intro @@ -164,7 +177,7 @@ qed. (* the move_char (variant c) machine *) definition move_char_c ≝ - λalpha,sep.whileTM alpha (mcc_step alpha sep) 〈3,sep〉. + λalpha,sep.whileTM alpha (mcc_step alpha sep) 〈mcc3,sep〉. definition R_move_char_c ≝ λalpha,sep,t1,t2. @@ -182,15 +195,12 @@ lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%] -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar) [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea % - [ #Hb >Htapea in H1; >Hb normalize in ⊢ (%→?); #H1 - cases (H1 ??) - [#_ #H2 >H2 % - |*: % #H2 destruct (H2) ] + [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??) + [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2)] | #rs1 #rs2 #Hrs #Hb #Hrs1 - >Htapea in H1; normalize in ⊢ (% → ?); #H1 - cases (H1 ??) - [ #Hfalse @False_ind @(absurd ?? Hb) destruct % - |*:% #H2 destruct (H2) ] + >Htapea in H1; #H1 cases (H1 ??) + [#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct % + |*:% #H2 normalize in H2; destruct (H2) ] ] | #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH @@ -198,10 +208,9 @@ lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%] #Ha0 #Htapeb % [ #Hfalse @False_ind @(absurd ?? Ha0) // | * - [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ normalize - >Hrs in Htapeb; normalize #Htapeb - cases (IH … Htapeb) - #Houtc #_ >Houtc // + [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ (* normalize *) + >Hrs in Htapeb; #Htapeb normalize in Htapeb; + cases (IH … Htapeb) #Houtc #_ >Houtc normalize // | #r0 #rs0 #rs2 #Hrs #_ #Hrs0 cut (r0 ≠ sep ∧ memb … sep rs0 = false) [ % diff --git a/matita/matita/lib/turing/universal/move_tape.ma b/matita/matita/lib/turing/universal/move_tape.ma index 4ec94cbc3..fed33bfa8 100644 --- a/matita/matita/lib/turing/universal/move_tape.ma +++ b/matita/matita/lib/turing/universal/move_tape.ma @@ -15,15 +15,19 @@ include "turing/universal/tuples.ma". definition init_cell_states ≝ initN 2. +definition ics0 : init_cell_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)). +definition ics1 : init_cell_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)). + +d definition init_cell ≝ mk_TM STape init_cell_states (λp.let 〈q,a〉 ≝ p in - match q with + match pi1 … q with [ O ⇒ match a with - [ None ⇒ 〈1, Some ? 〈〈null,false〉,N〉〉 + [ None ⇒ 〈ics1, Some ? 〈〈null,false〉,N〉〉 | Some _ ⇒ 〈1, None ?〉 ] - | S _ ⇒ 〈1,None ?〉 ]) - O (λq.q == 1). + | S _ ⇒ 〈ics1,None ?〉 ]) + ics0 (λq.q == ics1). definition R_init_cell ≝ λt1,t2. (∃c.current STape t1 = Some ? c ∧ t2 = t1) ∨ diff --git a/matita/matita/lib/turing/universal/trans_to_tuples.ma b/matita/matita/lib/turing/universal/trans_to_tuples.ma new file mode 100644 index 000000000..e40a0bbc8 --- /dev/null +++ b/matita/matita/lib/turing/universal/trans_to_tuples.ma @@ -0,0 +1,307 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| + \ / This file is distributed under the terms of the + \ / GNU General Public License Version 2 + V_____________________________________________________________*) + + + +include "turing/universal/tuples.ma". +include "basics/fun_graph.ma". + +(* p < n is represented with a list of bits of lenght n with the + p-th bit from left set to 1 *) + +let rec to_bitlist n p: list bool ≝ + match n with + [ O ⇒ [ ] + | S q ⇒ (eqb p q)::to_bitlist q p]. + +let rec from_bitlist l ≝ + match l with + [ nil ⇒ 0 (* assert false *) + | cons b tl ⇒ if b then |tl| else from_bitlist tl]. + +lemma bitlist_length: ∀n,p.|to_bitlist n p| = n. +#n elim n normalize // +qed. + +lemma bitlist_inv1: ∀n,p.p(not_eq_to_eqb_false … Hpn) normalize @Hind @ltpn + |#Heq >(eq_to_eqb_true … Heq) normalize eqtl @le_n + ] +qed. + +definition nat_of: ∀n. Nat_to n → nat. +#n normalize * #p #_ @p +qed. + +definition bits_of_state ≝ λn.λh:Nat_to n → bool.λs:Nat_to n. + h s::(to_bitlist n (nat_of n s)). + +definition m_bits_of_state ≝ λn.λh.λp. + map ? (unialpha×bool) (λx.〈bit x,false〉) (bits_of_state n h p). + +lemma no_marks_bits_of_state : ∀n,h,p. no_marks (m_bits_of_state n h p). +#n #h #p #x whd in match (m_bits_of_state n h p); +#H cases (orb_true_l … H) -H + [#H >(\P H) % + |elim (to_bitlist n (nat_of n p)) + [whd in ⊢ ((??%?)→?); #H destruct + |#b #l #Hind #H cases (orb_true_l … H) -H #H + [>(\P H) % + |@Hind @H + ] + ] + ] +qed. + +lemma only_bits_bits_of_state : ∀n,h,p. only_bits (m_bits_of_state n h p). +#n #h #p #x whd in match (m_bits_of_state n h p); +#H cases (orb_true_l … H) -H + [#H >(\P H) % + |elim (to_bitlist n (nat_of n p)) + [whd in ⊢ ((??%?)→?); #H destruct + |#b #l #Hind #H cases (orb_true_l … H) -H #H + [>(\P H) % + |@Hind @H + ] + ] + ] +qed. + +definition tuple_type ≝ λn. + (Nat_to n × (option FinBool)) × (Nat_to n × (option (FinBool × move))). + +definition tuple_of_pair ≝ λn.λh:Nat_to n→bool. + λp:tuple_type n. + let 〈inp,outp〉 ≝ p in + let 〈q,a〉 ≝ inp in + let cin ≝ match a with [ None ⇒ null | Some b ⇒ bit b ] in + let 〈qn,action〉 ≝ outp in + let 〈cout,mv〉 ≝ + match action with + [ None ⇒ 〈null,null〉 + | Some act ⇒ let 〈na,m〉 ≝ act in + match m with + [ R ⇒ 〈bit na,bit true〉 + | L ⇒ 〈bit na,bit false〉 + | N ⇒ 〈bit na,null〉] + ] in + let qin ≝ m_bits_of_state n h q in + let qout ≝ m_bits_of_state n h qn in + mk_tuple qin 〈cin,false〉 qout 〈cout,false〉 〈mv,false〉. + +definition WFTuple_conditions ≝ + λn,qin,cin,qout,cout,mv. + no_marks qin ∧ no_marks qout ∧ (* queste fuori ? *) + only_bits qin ∧ only_bits qout ∧ + bit_or_null cin = true ∧ bit_or_null cout = true ∧ bit_or_null mv = true ∧ + (cout = null → mv = null) ∧ + |qin| = n ∧ |qout| = n. + +lemma is_tuple: ∀n,h,p. tuple_TM (S n) (tuple_of_pair n h p). +#n #h * * #q #a * #qn #action +@(ex_intro … (m_bits_of_state n h q)) +letin cin ≝ match a with [ None ⇒ null | Some b ⇒ bit b ] +@(ex_intro … cin) +@(ex_intro … (m_bits_of_state n h qn)) +letin cout ≝ + match action with + [ None ⇒ null | Some act ⇒ bit (\fst act)] +@(ex_intro … cout) +letin mv ≝ match action with + [ None ⇒ null + | Some act ⇒ + match \snd act with + [ R ⇒ bit true | L ⇒ bit false | N ⇒ null] + ] +@(ex_intro … mv) +%[%[%[%[%[%[%[% /3/ + |whd in match cin ; cases a // + ] + |whd in match cout; cases action // + ] + |whd in match mv; cases action // + * #b #m cases m // + ] + |whd in match cout; whd in match mv; cases action + [// | #act whd in ⊢ ((??%?)→?); #Hfalse destruct ] + ] + |>length_map normalize @eq_f // + ] + |>length_map normalize @eq_f // + ] + |normalize cases a cases action normalize // + [* #c #m cases m % + |* #c #m #c1 cases m % + ] + ] +qed. + +definition tuple_length ≝ λn.2*n+3. + +axiom length_of_tuple: ∀n,t. tuple_TM n t → + |t| = tuple_length n. + +definition move_eq ≝ λm1,m2:move. + match m1 with + [R ⇒ match m2 with [R ⇒ true | _ ⇒ false] + |L ⇒ match m2 with [L ⇒ true | _ ⇒ false] + |N ⇒ match m2 with [N ⇒ true | _ ⇒ false]]. + +definition tuples_of_pairs ≝ λn.λh.map … (λp.(tuple_of_pair n h p)@[〈bar,false〉]). + +definition flatten ≝ λA.foldr (list A) (list A) (append A) []. + +lemma wftable: ∀n,h,l.table_TM (S n) (flatten ? (tuples_of_pairs n h l)). +#n #h #l elim l // -l #a #tl #Hind +whd in match (flatten … (tuples_of_pairs …)); +>associative_append @ttm_cons // +qed. + +lemma flatten_to_mem: ∀A,n,l,l1,l2.∀a:list A. 0 < n → + (∀x. mem ? x l → |x| = n) → |a| = n → flatten ? l = l1@a@l2 → + (∃q.|l1| = n*q) → mem ? a l. +#A #n #l elim l + [normalize #l1 #l2 #a #posn #Hlen #Ha #Hnil @False_ind + cut (|a|=0) [@daemon] /2/ + |#hd #tl #Hind #l1 #l2 #a #posn #Hlen #Ha + whd in match (flatten ??); #Hflat * #q cases q + [Hlenl11 @Hlen %1 % + |>Hflat >Heql1 >associative_append % + ] + |@(ex_intro …q1) @(injective_plus_r n) + Hl1 // + ] + ] + ] +qed. + +axiom match_decomp: ∀n,l,qin,cin,qout,cout,mv. + match_in_table (S n) qin cin qout cout mv l → + ∃l1,l2. l = l1@((mk_tuple qin cin qout cout mv)@[〈bar,false〉])@l2 ∧ + (∃q.|l1| = (S (tuple_length (S n)))*q) ∧ tuple_TM (S n) (mk_tuple qin cin qout cout mv). +(* +lemma match_tech: ∀n,l,qin,cin,qout,cout,mv. + (∀t. mem ? t l → |t| = |mk_tuple qin cin qout cout mv|) → + match_in_table (S n) qin cin qout cout mv (flatten ? l) → + ∃p. p = mk_tuple qin cin qout cout mv ∧ mem ? p l. +#n #l #qin #cin #qout #cout #mv #Hlen #Hmatch +@(ex_intro … (mk_tuple qin cin qout cout mv)) % // +@flatten_to_mem *) + +lemma match_to_tuple: ∀n,h,l,qin,cin,qout,cout,mv. + match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h l)) → + ∃p. p = mk_tuple qin cin qout cout mv ∧ mem ? (p@[〈bar,false〉]) (tuples_of_pairs n h l). +#n #h #l #qin #cin #qout #cout #mv #Hmatch +@(ex_intro … (mk_tuple qin cin qout cout mv)) % // +cases (match_decomp … Hmatch) #l1 * #l2 * * #Hflat #Hlen #Htuple +@(flatten_to_mem … Hflat … Hlen) + [// + |@daemon + |>length_append >(length_of_tuple … Htuple) normalize // + ] +qed. + +lemma mem_map: ∀A,B.∀f:A→B.∀l,b. + mem ? b (map … f l) → ∃a. mem ? a l ∧ f a = b. +#A #B #f #l elim l + [#b normalize @False_ind + |#a #tl #Hind #b normalize * + [#eqb @(ex_intro … a) /3/ + |#memb cases (Hind … memb) #a * #mema #eqb + @(ex_intro … a) /3/ + ] + ] +qed. + +lemma match_to_pair: ∀n,h,l,qin,cin,qout,cout,mv. + match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h l)) → + ∃p. tuple_of_pair n h p = mk_tuple qin cin qout cout mv ∧ mem ? p l. +#n #h #l #qin #cin #qout #cout #mv #Hmatch +cases (match_to_tuple … Hmatch) +#p * #eqp #memb +cases(mem_map … (λp.(tuple_of_pair n h p)@[〈bar,false〉]) … memb) +#p1 * #Hmem #H @(ex_intro … p1) % /2/ +qed. + +(* turning DeqMove into a DeqSet *) +lemma move_eq_true:∀m1,m2. + move_eq m1 m2 = true ↔ m1 = m2. +* + [* normalize [% #_ % |2,3: % #H destruct ] + |* normalize [1,3: % #H destruct |% #_ % ] + |* normalize [1,2: % #H destruct |% #_ % ] +qed. + +definition DeqMove ≝ mk_DeqSet move move_eq move_eq_true. + +unification hint 0 ≔ ; + X ≟ DeqMove +(* ---------------------------------------- *) ⊢ + move ≡ carr X. + +unification hint 0 ≔ m1,m2; + X ≟ DeqMove +(* ---------------------------------------- *) ⊢ + move_eq m1 m2 ≡ eqb X m1 m2. + +(* turning DeqMove into a FinSet *) +definition move_enum ≝ [L;R;N]. + +lemma move_enum_unique: uniqueb ? [L;R;N] = true. +// qed. + +lemma move_enum_complete: ∀x:move. memb ? x [L;R;N] = true. +* // qed. + +definition FinMove ≝ + mk_FinSet DeqMove [L;R;N] move_enum_unique move_enum_complete. + +unification hint 0 ≔ ; + X ≟ FinMove +(* ---------------------------------------- *) ⊢ + move ≡ FinSetcarr X. + +definition trans_source ≝ λn.FinProd (initN n) (FinOption FinBool). +definition trans_target ≝ λn.FinProd (initN n) (FinOption (FinProd FinBool FinMove)). + +lemma match_to_trans: + ∀n.∀trans: trans_source n → trans_target n. + ∀h,qin,cin,qout,cout,mv. + match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_of_pairs n h (graph_enum ?? trans))) → + ∃s,t. tuple_of_pair n h 〈s,t〉 = mk_tuple qin cin qout cout mv + ∧ trans s = t. +#n #trans #h #qin #cin #qout #cout #mv #Hmatch +cases (match_to_pair … Hmatch) -Hmatch * #s #t * #Heq #Hmem +@(ex_intro … s) @(ex_intro … t) % // @graph_enum_correct +@mem_to_memb @Hmem +qed. + -- 2.39.2