-lemma sem_match_tuple_step:
- accRealize ? match_tuple_step (inr … (inl … (inr … 0)))
- R_match_tuple_step_true R_match_tuple_step_false.
-@(acc_sem_if_app … (sem_test_char ? (λc:STape.¬ is_grid (\fst c))) …
- (sem_seq … sem_compare
- (sem_if … (sem_test_char ? (λc:STape.is_grid (\fst c)))
- (sem_nop …)
- (sem_seq … sem_mark_next_tuple
- (sem_if … (sem_test_char ? (λc:STape.is_grid (\fst c)))
- (sem_mark ?) (sem_seq … (sem_move_l …) (sem_init_current …))))))
- (sem_nop ?) …)
-[(* is_grid: termination case *)
- 2:#t1 #t2 #t3 whd in ⊢ (%→?); #H #H1 whd #ls #c #rs #Ht1
- cases (H c ?) [2: >Ht1 %] #Hgrid #Heq %
- [@injective_notb @Hgrid | <Heq @H1]
-|#tapea #tapeout #tapeb whd in ⊢ (%→?); #Htapea
- * #tapec * #Hcompare #Hor
- #ls #c #l1 #l2 #c1 #l3 #l4 #rs #n #Hc #Hl1bars #Hl1marks #Hc1 #Hl3 #eqn
- #eqlen #Htable #Htapea1 cases (Htapea 〈c,true〉 ?) >Htapea1 [2:%]
- #notgridc -Htapea -Htapea1 -tapea #Htapeb
- cases (Hcompare … Htapeb) -Hcompare -Htapeb * #_ #_ #Hcompare
- cases (Hcompare c c1 l1 l3 (l2@[〈bar,false〉]) (l4@〈grid,false〉::rs) eqlen Hl1bars Hl3 Hl1marks … (refl …) Hc ?)
- -Hcompare
- [* #Htemp destruct (Htemp) #Htapec %1 % [%]
- >Htapec in Hor; -Htapec *
- [2: * #t3 * whd in ⊢ (%→?); #H @False_ind
- cases (H … (refl …)) whd in ⊢ ((??%?)→?); #H destruct (H)
- |* #taped * whd in ⊢ (%→?); #Htaped cases (Htaped ? (refl …)) -Htaped *
- #Htaped whd in ⊢ (%→?); #Htapeout >Htapeout >Htaped >associative_append
- %
- ]
- |* #la * #c' * #d' * #lb * #lc * * * #H1 #H2 #H3 #Htapec
- cut (〈c,false〉::l1 ≠ 〈c1,false〉::l3)
- [>H2 >H3 elim la
- [@(not_to_not …H1) normalize #H destruct %
- |#x #tl @not_to_not normalize #H destruct //
- ]
- ] #Hnoteq %2
- cut (is_bit d' = true)
- [cases la in H3;
- [normalize in ⊢ (%→?); #H destruct //
- |#x #tl #H @(Hl3 〈d',false〉)
- normalize in H; destruct @memb_append_l2 @memb_hd
- ]
- ] #Hd'
- >Htapec in Hor; -Htapec *
- [* #taped * whd in ⊢ (%→?); #H @False_ind
- cases (H … (refl …)) >(bit_not_grid ? Hd') #Htemp destruct (Htemp)
- |* #taped * whd in ⊢ (%→?); #H cases (H … (refl …)) -H #_
- #Htaped * #tapee * whd in ⊢ (%→?); #Htapee
- <(associative_append ? lc (〈comma,false〉::l4)) in Htaped; #Htaped
- cases (Htapee … Htaped ???) -Htaped -Htapee
- [* #rs3 * * (* we proceed by cases on rs4 *)
- [(* rs4 is empty : the case is absurd since the tape
- cannot end with a bar *)
- * #d * #b * * * #Heq1 @False_ind
- cut (∀A,l1,l2.∀a:A. a::l1@l2=(a::l1)@l2) [//] #Hcut
- >Hcut in Htable; >H3 >associative_append
- normalize >Heq1 >Hcut <associative_append >Hcut
- <associative_append #Htable @(absurd … Htable)
- @last_of_table
- |(* rs4 not empty *)
- * #d2 #b2 #rs3' * #d * #b * * * #Heq1 #Hnobars
- cut (is_grid d2 = false)
- [@(no_grids_in_table … Htable … 〈d2,b2〉)
- @daemon (* no grids in table *)] #Hd2
- whd in ⊢ ((???%)→?); #Htemp destruct (Htemp) #Htapee >Htapee -Htapee *
- [(* we know current is not grid *)
- * #tapef * whd in ⊢ (%→?); #Htapef
- cases (Htapef … (refl …)) >Hd2 #Htemp destruct (Htemp)
- |* #tapef * whd in ⊢ (%→?); #Htapef
- cases (Htapef … (refl …)) #_ -Htapef #Htapef
- * #tapeg >Htapef -Htapef *
- (* move_l *)
- whd in ⊢ (%→?);
- #H lapply (H … (refl …)) whd in ⊢ (???%→?); -H #Htapeg
- >Htapeg -Htapeg
- (* init_current *)
- whd in ⊢ (%→?); #Htapeout
- %1 cases (some_option_hd ? (reverse ? (reverse ? la)) 〈c',true〉)
- * #c00 #b00 #Hoption
- (* cut
- ((reverse ? rs3 @〈d',false〉::reverse ? la@reverse ? (l2@[〈bar,false〉])@(〈grid,false〉::reverse ? lb))
- = *)
- lapply
- (Htapeout (reverse ? rs3 @〈d',false〉::reverse ? la@reverse ? (l2@[〈bar,false〉])@(〈grid,false〉::reverse ? lb))
- c' (reverse ? la) false ls bar (〈d2,true〉::rs3'@〈grid,false〉::rs) c00 b00 ?????) -Htapeout
- [whd in ⊢ (??(??%??)?); @eq_f3 [2:%|3: %]
- >associative_append
- generalize in match (〈c',true〉::reverse ? la@〈grid,false〉::ls); #l
- whd in ⊢ (???(???%)); >associative_append >associative_append %
- |>reverse_cons @Hoption
- |cases la in H2;
- [normalize in ⊢ (%→?); #Htemp destruct (Htemp)
- @injective_notb @notgridc
- |#x #tl normalize in ⊢ (%→?); #Htemp destruct (Htemp)
- @bit_not_grid @(Hl1bars 〈c',false〉) @memb_append_l2 @memb_hd
- ]
- |cut (only_bits (la@(〈c',false〉::lb)))
- [<H2 whd #c0 #Hmemb cases (orb_true_l … Hmemb)
- [#eqc0 >(\P eqc0) @Hc |@Hl1bars]
- |#Hl1' #x #Hx @bit_not_grid @Hl1'
- @memb_append_l1 @daemon
- ]
- |@daemon
- |>reverse_append >reverse_cons >reverse_reverse
- >reverse_append >reverse_reverse
- >reverse_cons >reverse_append >reverse_reverse
- >reverse_append >reverse_cons >reverse_reverse
- >reverse_reverse
- #Htapeout % [@Hnoteq]
- @(ex_intro … d2)
- cut (∃rs31,rs32.rs3 = rs31@〈comma,false〉::rs32)
- [@daemon] * #rs31 * #rs32 #Hrs3
- (* cut
- (〈c1,false〉::l3@〈comma,false〉::l4= la@〈d',false〉::rs3@〈bar,false〉::〈d2,b2〉::rs3')
- [@daemon] #Hcut *)
- @(ex_intro … rs32) @(ex_intro … rs3') %
- [>Hrs3 in Heq1; @daemon
- |>Htapeout @eq_f2
- [@daemon
- |<associative_append <associative_append
- <associative_append <associative_append <associative_append
- <associative_append >(associative_append …la) <H2
- normalize in ⊢ (??%?);
- >associative_append >associative_append
- >associative_append >associative_append >associative_append
- >associative_append normalize @eq_f @eq_f @eq_f @eq_f
- cut (true = b2) [@daemon] #Hcut >Hcut
- cut (∀A,l1,l2,l3. l1 = l2 → l1@l3 =
- <Heq1 >(associative_append …la)
- cut (true = b2
-
-
- ]
- ]
- ]
- |* #Hnobars #Htapee >Htapee -Htapee *
- [whd in ⊢ (%→?); * #tapef * whd in ⊢ (%→?); #Htapef
- cases (Htapef … (refl …)) -Htapef #_ #Htapef >Htapef -Htapef
- whd in ⊢ (%→?); #Htapeout %2
- >(Htapeout … (refl …)) %
- [ %
- [ @Hnoteq
- | whd #x #Hx @Hnobars @memb_append_l2 @memb_cons //
- ]
- | %
- ]
- |whd in ⊢ (%→?); * #tapef * whd in ⊢ (%→?); #Htapef
- cases (Htapef … (refl …)) -Htapef
- whd in ⊢ ((??%?)→?); #Htemp destruct (Htemp)
- ]
- |(* no marks in table *)
- #x #membx @(no_marks_in_table … Htable)
- @memb_append_l2 @memb_cons
- cut (∀A,l1,l2.∀a:A. a::l1@l2=(a::l1)@l2) [//] #Hcut >Hcut
- >H3 >associative_append @memb_append_l2 @memb_cons @membx
- |(* no grids in table *)
- #x #membx @(no_grids_in_table … Htable)
- @memb_append_l2 @memb_cons
- cut (∀A,l1,l2.∀a:A. a::l1@l2=(a::l1)@l2) [//] #Hcut >Hcut
- >H3 >associative_append @memb_append_l2 @memb_cons @membx
- |whd in ⊢ (??%?); >(bit_not_grid … Hd') >(bit_not_bar … Hd') %
- ]
- ]
- |#x #membx @(no_marks_in_table … Htable)
- @memb_append_l2 @memb_cons @memb_cons @memb_append_l1 @membx
- |#x #membx @(no_marks_in_table … Htable)
- cases (memb_append … membx) -membx #membx
- [@memb_append_l1 @membx | @memb_append_l2 >(memb_single … membx) @memb_hd]
- |>associative_append %
- ]
- ]