regular_i sig n l i → regular_i sig n (tail ? l) i.
axiom regular_extend: ∀sig,n,l,i.
- regular_i sig n l i → regular_i sig n (l@[all_blank sig n]) i.
+ regular_i sig n l i → regular_i sig n (l@[all_blanks sig n]) i.
axiom all_blank_after_blank: ∀sig,n,l1,b,l2,i.
nth i ? (vec … b) (blank ?) = blank ? →
lemma regular_trace_extl: ∀sig,n,a,ls,rs,i.
regular_trace sig n a ls rs i →
- regular_trace sig n a (ls@[all_blank sig n]) rs i.
+ regular_trace sig n a (ls@[all_blanks sig n]) rs i.
#sig #n #a #ls #rs #i *
[* #H1 #H2 % % // @(regular_extend … H1)
|* #H1 #H2 %2 % // @(regular_extend … H1)
lemma regular_cons_hd_rs: ∀sig,n.∀a:multi_sig sig n.∀ls,rs1,rs2,i.
regular_trace sig n a ls (rs1@rs2) i →
- regular_trace sig n a ls (rs1@((hd ? rs2 (all_blank …))::(tail ? rs2))) i.
+ regular_trace sig n a ls (rs1@((hd ? rs2 (all_blanks …))::(tail ? rs2))) i.
#sig #n #a #ls #rs1 #rs2 #i cases rs2 [2: #b #tl #H @H]
*[* #H1 >append_nil #H2 %1 %
[@H1 | whd in match (hd ???); @(regular_extend … rs1) //]
improve semantics *)
definition move_to_blank_L ≝ λsig,n,i.
- (move_until ? L (no_blank sig n i)) · extend ? (all_blank sig n).
+ (move_until ? L (not_blank sig n i)) · extend ? (all_blanks sig n).
(*
definition R_move_to_blank_L ≝ λsig,n,i,t1,t2.
definition R_move_to_blank_L ≝ λsig,n,i,t1,t2.
(current ? t1 = None ? →
- t2 = midtape (multi_sig sig n) (left ? t1) (all_blank …) (right ? t1)) ∧
+ t2 = midtape (multi_sig sig n) (left ? t1) (all_blanks …) (right ? t1)) ∧
∀ls,a,rs.
t1 = midtape (multi_sig sig n) ls a rs →
regular_i sig n (a::ls) i →
(∃b,ls1,ls2.
(regular_i sig n (ls1@b::ls2) i) ∧
(∀j. j ≠ i → regular_trace …
- (hd ? (ls1@b::ls2) (all_blank …)) (tail ? (ls1@b::ls2)) rs j) ∧
- (no_blank sig n i b = false) ∧
- (hd (multi_sig sig n) (ls1@[b]) (all_blank …) = a) ∧ (* not implied by the next fact *)
+ (hd ? (ls1@b::ls2) (all_blanks …)) (tail ? (ls1@b::ls2)) rs j) ∧
+ (not_blank sig n i b = false) ∧
+ (hd (multi_sig sig n) (ls1@[b]) (all_blanks …) = a) ∧ (* not implied by the next fact *)
(∀j.j ≤n → to_blank_i ?? j (ls1@b::ls2) = to_blank_i ?? j (a::ls)) ∧
t2 = midtape ? ls2 b ((reverse ? ls1)@rs)).
move_to_blank_L sig n i ⊨ R_move_to_blank_L sig n i.
#sig #n #i
@(sem_seq_app ??????
- (ssem_move_until_L ? (no_blank sig n i)) (sem_extend ? (all_blank sig n)))
+ (ssem_move_until_L ? (not_blank sig n i)) (sem_extend ? (all_blanks sig n)))
#tin #tout * #t1 * * #Ht1a #Ht1b * #Ht2a #Ht2b %
[#Hcur >(Ht1a Hcur) in Ht2a; /2 by /
|#ls #a #rs #Htin #Hreg #Hreg2 -Ht1a cases (Ht1b … Htin)
]
|* #b * #lss * * #H1 #H2 #Ht1 -Ht1b >Ht1 in Ht2a;
whd in match (left ??); whd in match (right ??); #Hout
- %{(all_blank …)} %{(lss@[b])} %{[]}
+ %{(all_blanks …)} %{(lss@[b])} %{[]}
%[%[%[%[%[<H2 @regular_extend //
|<H2 #j #jneqi whd in match (hd ???); whd in match (tail ??);
@regular_trace_extl @Hreg2 //]
- |whd in match (no_blank ????); >blank_all_blank //]
+ |whd in match (not_blank ????); >blank_all_blanks //]
|<H2 //]
|#j #lejn <H2 @sym_eq @to_blank_i_ext]
|>reverse_append >reverse_single @Hout normalize //
(******************************************************************************)
definition shift_i_L ≝ λsig,n,i.
- ncombf_r (multi_sig …) (shift_i sig n i) (all_blank sig n) ·
+ ncombf_r (multi_sig …) (shift_i sig n i) (all_blanks sig n) ·
mti sig n i ·
- extend ? (all_blank sig n).
+ extend ? (all_blanks sig n).
definition R_shift_i_L ≝ λsig,n,i,t1,t2.
(∀a,ls,rs.
(∀x. mem ? x rs → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
shift_l sig n i (a::rs) (rss@[b]) ∧
t2 = midtape (multi_sig sig n)
- ((reverse ? (rss@[b]))@ls) (all_blank sig n) [ ]))).
+ ((reverse ? (rss@[b]))@ls) (all_blanks sig n) [ ]))).
definition R_shift_i_L_new ≝ λsig,n,i,t1,t2.
(∀a,ls,rs.
t1 = midtape ? ls a rs →
∃rs1,b,rs2,rss.
- b = hd ? rs2 (all_blank sig n) ∧
+ b = hd ? rs2 (all_blanks sig n) ∧
nth i ? (vec … b) (blank ?) = (blank ?) ∧
rs = rs1@rs2 ∧
(∀x. mem ? x rs1 → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
theorem sem_shift_i_L: ∀sig,n,i. shift_i_L sig n i ⊨ R_shift_i_L sig n i.
#sig #n #i
@(sem_seq_app ??????
- (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
+ (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blanks sig n))
(sem_seq ????? (ssem_mti sig n i)
- (sem_extend ? (all_blank sig n))))
+ (sem_extend ? (all_blanks sig n))))
#tin #tout * #t1 * * #Ht1a #Ht1b * #t2 * * #Ht2a #Ht2b * #Htout1 #Htout2
#a #ls #rs cases rs
- [#Htin %2 %{(shift_i sig n i a (all_blank sig n))} %{[ ]}
+ [#Htin %2 %{(shift_i sig n i a (all_blanks sig n))} %{[ ]}
%[%[#x @False_ind | @daemon]
|lapply (Ht1a … Htin) -Ht1a -Ht1b #Ht1
lapply (Ht2a … Ht1) -Ht2a -Ht2b #Ht2 >Ht2 in Htout1;
]
|* #b * #rss * * #H1 #H2
#Ht2 %2
- %{(shift_i sig n i b (all_blank sig n))} %{(shift_i sig n i a a1::rss)}
+ %{(shift_i sig n i b (all_blanks sig n))} %{(shift_i sig n i a a1::rss)}
%[%[@H1 |@daemon ]
|>Ht2 in Htout1; #Htout >Htout //
whd in match (left ??); whd in match (right ??);
%{rs1} %{b} %{(b::rs2)} %{(a1::rss)}
%[%[%[%[%[//|@H2]|@H1]|@H3]|@H4] | whd in match (tail ??); @Ht2]
|* #b * #rss * * #H1 #H2 #Ht2
- %{rs} %{(all_blank sig n)} %{[]} %{(rss@[b])}
- %[%[%[%[%[//|@blank_all_blank]|//]|@H1]|@H2] | whd in match (tail ??); @Ht2]
+ %{rs} %{(all_blanks sig n)} %{[]} %{(rss@[b])}
+ %[%[%[%[%[//|@blank_all_blanks]|//]|@H1]|@H2] | whd in match (tail ??); @Ht2]
]
qed.
(*******************************************************************************
-The following machine implements a full move of for a trace: we reach the left
-border, shift the i-th trace and come back to the head position. *)
+The following machine implements a full move for a trace: we reach the left
+border, shift the i-th trace and come back to the head position.
+The head may hold additional information A, so we suppose that the tape alphabet
+is the disjoint sum between A and the alphabet sig of the multi tape machine. *)
+
+definition TA ≝ λA,sig. FinSum A sig.
+definition MTA ≝ λA,sig,n.multi_sig (TA A sig) n.
+
+definition is_head ≝ λA,sig.λc:sig_ext (TA A sig).
+ match c with
+ [ None ⇒ false
+ | Some a ⇒ match a with
+ [ inl _ ⇒ true
+ | inr _ ⇒ false]].
+
+definition is_sig ≝ λA,sig.λc:sig_ext (TA A sig).
+ match c with
+ [ None ⇒ false
+ | Some a ⇒ match a with
+ [ inl _ ⇒ false
+ | inr _ ⇒ true]].
-(* this exclude the possibility that traces do not overlap: the head must
-remain inside all traces *)
+definition not_head ≝ λA,sig,n.λc:multi_sig (TA A sig) n.
+ ¬(is_head A sig (nth n ? (vec … c) (blank ?))).
+
+definition no_head_in ≝ λA,sig,n,l.
+ ∀x. mem ? x (trace (TA A sig) n n l) → is_head … x = false.
+
+(*
+lemma not_head_true: ∀A,sig,n,c. not_head A sig n c = true →
+ is_head … (nth n ? (vec … c) (blank ?)) = false.
+*)
-definition mtiL ≝ λsig,n,i.
- move_to_blank_L sig n i ·
- shift_i_L sig n i ·
- move_until ? L (no_head sig n).
+definition mtiL ≝ λA,sig,n,i.
+ move_to_blank_L (TA A sig) n i ·
+ shift_i_L (TA A sig) n i ·
+ move_until ? L (not_head A sig n).
-definition Rmtil ≝ λsig,n,i,t1,t2.
+definition Rmtil ≝ λA,sig,n,i,t1,t2.
∀ls,a,rs.
- t1 = midtape (multi_sig sig n) ls a rs →
- nth n ? (vec … a) (blank ?) = head ? →
- (∀i.regular_trace sig n a ls rs i) →
+ t1 = midtape (MTA A sig n) ls a rs →
+ is_head A sig (nth n ? (vec … a) (blank ?)) = true →
+ (∀i.regular_trace (TA A sig) n a ls rs i) →
(* next: we cannot be on rightof on trace i *)
(nth i ? (vec … a) (blank ?) = (blank ?)
- → nth i ? (vec … (hd ? rs (all_blank …))) (blank ?) ≠ (blank ?)) →
+ → nth i ? (vec … (hd ? rs (all_blanks …))) (blank ?) ≠ (blank ?)) →
no_head_in … ls →
no_head_in … rs →
(∃ls1,a1,rs1.
- t2 = midtape (multi_sig …) ls1 a1 rs1 ∧
+ t2 = midtape (MTA A sig n) ls1 a1 rs1 ∧
(∀i.regular_trace … a1 ls1 rs1 i) ∧
(∀j. j ≤ n → j ≠ i → to_blank_i ? n j (a1::ls1) = to_blank_i ? n j (a::ls)) ∧
(∀j. j ≤ n → j ≠ i → to_blank_i ? n j rs1 = to_blank_i ? n j rs) ∧
(to_blank_i ? n i ls1 = to_blank_i ? n i (a::ls)) ∧
(to_blank_i ? n i (a1::rs1)) = to_blank_i ? n i rs).
-theorem sem_Rmtil: ∀sig,n,i. i < n → mtiL sig n i ⊨ Rmtil sig n i.
-#sig #n #i #lt_in
+theorem sem_Rmtil: ∀A,sig,n,i. i < n → mtiL A sig n i ⊨ Rmtil A sig n i.
+#A #sig #n #i #lt_in
@(sem_seq_app ??????
(sem_move_to_blank_L … )
(sem_seq ????? (sem_shift_i_L_new …)
- (ssem_move_until_L ? (no_head sig n))))
+ (ssem_move_until_L ? (not_head A sig n))))
#tin #tout * #t1 * * #_ #Ht1 * #t2 * #Ht2 * #_ #Htout
(* we start looking into Rmitl *)
#ls #a #rs #Htin (* tin is a midtape *)
-#Hhead #Hreg #no_rightof #Hnohead_ls #Hnohead_rs
-cut (regular_i sig n (a::ls) i)
+#Hheada #Hreg #no_rightof #Hnohead_ls #Hnohead_rs
+cut (regular_i ? n (a::ls) i)
[cases (Hreg i) * //
cases (true_or_false (nth i ? (vec … a) (blank ?) == (blank ?))) #Htest
[#_ @daemon (* absurd, since hd rs non e' blank *)
[(* the current character on trace i holds the head-mark.
The case is absurd, since b0 is the head of rs2, that is a sublist of rs,
and the head-mark is not in rs *)
- * #H3 @False_ind @(absurd (nth n ? (vec … b0) (blank sig) = head ?))
- [@(\P ?) @injective_notb @H3 ]
- @Hnohead_rs >H2 >trace_append @mem_append_l2
+ * #H3 @False_ind @(absurd (true=false)) [2://] <H3 @sym_eq
+ <(notb_notb true) @(eq_f … notb) @Hnohead_rs >H2 >trace_append @mem_append_l2
lapply Hb0 cases rs2
- [whd in match (hd ???); #H >H in H3; whd in match (no_head ???);
+ [whd in match (hd ???); #H >H in H3; whd in match (not_head ????);
>all_blank_n normalize -H #H destruct (H); @False_ind
|#c #r #H4 %1 >H4 //
]
(* cut (trace sig n j (a1::ls20)=trace sig n j (ls1@b::ls2)) *)
* #ls10 * #a1 * #ls20 * * * #Hls20 #Ha1 #Hnh #Htout
cut (∀j.j ≠ i →
- trace sig n j (reverse (multi_sig sig n) rs1@b::ls2) =
- trace sig n j (ls10@a1::ls20))
+ trace ? n j (reverse (multi_sig (TA A sig) n) rs1@b::ls2) =
+ trace ? n j (ls10@a1::ls20))
[#j #ineqj >append_cons <reverse_cons >trace_def <map_append <reverse_map
lapply (trace_shift_neq …lt_in ? (sym_not_eq … ineqj) … Hrss) [//] #Htr
<(trace_def … (b::rs1)) <Htr >reverse_map >map_append @eq_f @Hls20 ]
#Htracej
- cut (trace sig n i (reverse (multi_sig sig n) (rs1@[b0])@ls2) =
- trace sig n i (ls10@a1::ls20))
+ cut (trace ? n i (reverse (multi_sig (TA A sig) n) (rs1@[b0])@ls2) =
+ trace ? n i (ls10@a1::ls20))
[>trace_def <map_append <reverse_map <map_append <(trace_def … [b0])
- cut (trace sig n i [b0] = [blank ?]) [@daemon] #Hcut >Hcut
+ cut (trace ? n i [b0] = [blank ?]) [@daemon] #Hcut >Hcut
lapply (trace_shift … lt_in … Hrss) [//] whd in match (tail ??); #Htr <Htr
>reverse_map >map_append <trace_def <Hls20 %
]
#Htracei
cut (∀j. j ≠ i →
- (trace sig n j (reverse (multi_sig sig n) rs11) = trace sig n j ls10) ∧
- (trace sig n j (ls1@b::ls2) = trace sig n j (a1::ls20)))
+ (trace ? n j (reverse (MTA A sig n) rs11) = trace ? n j ls10) ∧
+ (trace ? n j (ls1@b::ls2) = trace ? n j (a1::ls20)))
[@daemon (* si fa
#j #ineqj @(first_P_to_eq ? (λx. x ≠ head ?))
[lapply (Htracej … ineqj) >trace_def in ⊢ (%→?); <map_append
>trace_def in ⊢ (%→?); <map_append #H @H
| *) ] #H2
- cut ((trace sig n i (b0::reverse ? rs11) = trace sig n i (ls10@[a1])) ∧
- (trace sig n i (ls1@ls2) = trace sig n i ls20))
+ cut ((trace ? n i (b0::reverse ? rs11) = trace ? n i (ls10@[a1])) ∧
+ (trace ? n i (ls1@ls2) = trace ? n i ls20))
[>H1 in Htracei; >reverse_append >reverse_single >reverse_append
>reverse_reverse >associative_append >associative_append
@daemon
] #H3
cut (∀j. j ≠ i →
- trace sig n j (reverse (multi_sig sig n) ls10@rs2) = trace sig n j rs)
- [#j #jneqi @(injective_append_l … (trace sig n j (reverse ? ls1)))
+ trace ? n j (reverse (MTA A sig n) ls10@rs2) = trace ? n j rs)
+ [#j #jneqi @(injective_append_l … (trace ? n j (reverse ? ls1)))
>map_append >map_append >Hrs1 >H1 >associative_append
<map_append <map_append in ⊢ (???%); @eq_f
<map_append <map_append @eq_f2 // @sym_eq
<(reverse_reverse … rs11) <reverse_map <reverse_map in ⊢ (???%);
@eq_f @(proj1 … (H2 j jneqi))] #Hrs_j
- %{ls20} %{a1} %{(reverse ? (b0::ls10)@tail (multi_sig sig n) rs2)}
+ %{ls20} %{a1} %{(reverse ? (b0::ls10)@tail (MTA A sig n) rs2)}
%[%[%[%[%[@Htout
|#j cases (decidable_eq_nat j i)
[#eqji >eqji (* by cases wether a1 is blank *)
whd in match (to_blank_i ????); <(proj2 … H3)
@daemon ]
|>reverse_cons >associative_append
- cut (to_blank_i sig n i rs = to_blank_i sig n i (rs11@[b0])) [@daemon]
+ cut (to_blank_i ? n i rs = to_blank_i ? n i (rs11@[b0])) [@daemon]
#Hcut >Hcut >(to_blank_i_chop … b0 (a1::reverse …ls10)) [2: @Hb0blank]
>to_blank_i_def >to_blank_i_def @eq_f
>trace_def >trace_def @injective_reverse >reverse_map >reverse_cons
]
|(*we do not find the head: this is absurd *)
* #b1 * #lss * * #H2 @False_ind
- cut (∀x0. mem ? x0 (trace sig n n (b0::reverse ? rss@ls2)) → x0 ≠ head ?)
+ cut (∀x0. mem ? x0 (trace ? n n (b0::reverse ? rss@ls2)) → is_head … x0 = false)
[@daemon] -H2 #H2
- lapply (trace_shift_neq sig n i n … lt_in … Hrss)
+ lapply (trace_shift_neq ? n i n … lt_in … Hrss)
[@lt_to_not_eq @lt_in | // ]
#H3 @(absurd
- (nth n ? (vec … (hd ? (ls1@[b]) (all_blank sig n))) (blank ?) = head ?))
+ (is_head … (nth n ? (vec … (hd ? (ls1@[b]) (all_blanks … n))) (blank ?)) = true))
[>Hhead //
- |@H2 >trace_def %2 <map_append @mem_append_l1 <reverse_map <trace_def
+ |@eqnot_to_noteq @H2 >trace_def %2 <map_append @mem_append_l1 <reverse_map <trace_def
>H3 >H1 >trace_def >reverse_map >reverse_cons >reverse_append
>reverse_reverse >associative_append <map_append @mem_append_l2
cases ls1 [%1 % |#x #ll %1 %]
include "basics/vector_finset.ma".
(* a multi_sig characheter is composed by n+1 sub-characters: n for each tape
-of a multitape machine, and an additional one to mark the position of the head.
-We extend the tape alphabet with two new symbols true and false.
-false is used to pad shorter tapes, and true to mark the head of the tape *)
+of a multitape machine.
+We extend the tape alphabet with a special symbol None to pad shorter tapes.
+For the moment, the actual content of the tape alphabet is left unspecifed,
+but we shall need characters to store states and moves of the multitape
+machines and to mark the head position *)
-definition sig_ext ≝ λsig. FinSum FinBool sig.
-definition blank : ∀sig.sig_ext sig ≝ λsig. inl … false.
-definition head : ∀sig.sig_ext sig ≝ λsig. inl … true.
+definition sig_ext ≝ λsig. FinOption sig.
+definition blank : ∀sig.sig_ext sig ≝ λsig. None sig.
+
+(* definition head : ∀sig.sig_ext sig ≝ λsig. inl … true. *)
definition multi_sig ≝ λsig:FinSet.λn.FinVector (sig_ext sig) n.
(* a character containing blank characters in each trace *)
-let rec all_blank sig n on n : multi_sig sig n ≝
+let rec all_blanks sig n on n : multi_sig sig n ≝
match n with
[ O ⇒ Vector_of_list ? []
- | S m ⇒ vec_cons ? (blank ?) m (all_blank sig m)
+ | S m ⇒ vec_cons ? (blank ?) m (all_blanks sig m)
].
-lemma blank_all_blank: ∀sig,n,i.
- nth i ? (vec … (all_blank sig n)) (blank sig) = blank ?.
+lemma blank_all_blanks: ∀sig,n,i.
+ nth i ? (vec … (all_blanks sig n)) (blank sig) = blank ?.
#sig #n elim n normalize [#i >nth_nil // |#m #Hind #i cases i // #j @Hind ]
qed.
lemma all_blank_n: ∀sig,n.
- nth n ? (vec … (all_blank sig n)) (blank sig) = blank ?.
-#sig #n @blank_all_blank
+ nth n ? (vec … (all_blanks sig n)) (blank sig) = blank ?.
+#sig #n @blank_all_blanks
qed.
(* boolen test functions *)
-definition no_blank ≝ λsig,n,i.λc:multi_sig sig n.
+definition not_blank ≝ λsig,n,i.λc:multi_sig sig n.
¬(nth i ? (vec … c) (blank ?))==blank ?.
+(*
definition no_head ≝ λsig,n.λc:multi_sig sig n.
¬((nth n ? (vec … c) (blank ?))==head ?).
lemma no_head_false: ∀sig,n,a.
nth n ? (vec … n a) (blank sig) = head ? → no_head … a = false.
#sig #n #a #H normalize >H //
-qed.
+qed. *)
(**************************** extract the i-th trace **************************)
definition trace ≝ λsig,n,i,l.
lemma hd_trace: ∀sig,n,i,l.
hd ? (trace sig n i l) (blank ?) =
- nth i ? (hd ? l (all_blank … )) (blank ?).
-#sig #n #i #l elim l // normalize >blank_all_blank %
+ nth i ? (hd ? l (all_blanks … )) (blank ?).
+#sig #n #i #l elim l // normalize >blank_all_blanks %
qed.
lemma tail_trace: ∀sig,n,i,l.
lemma nth_trace : ∀sig,n,i,j,l.
nth j ? (trace sig n i l) (blank ?) =
- nth i ? (nth j ? l (all_blank sig n)) (blank ?).
+ nth i ? (nth j ? l (all_blanks sig n)) (blank ?).
#sig #n #i #j elim j
- [#l cases l normalize // >blank_all_blank //
+ [#l cases l normalize // >blank_all_blanks //
|-j #j #Hind #l whd in match (nth ????); whd in match (nth ????);
cases l
- [normalize >nth_nil >nth_nil >blank_all_blank //
+ [normalize >nth_nil >nth_nil >blank_all_blanks //
|#a #tl normalize @Hind]
]
qed.
+(*
definition no_head_in ≝ λsig,n,l.
∀x. mem ? x (trace sig n n l) → x ≠ head ?.
-
+*)
(* some lemmas over lists, to be moved *)
lemma injective_append_l: ∀A,l. injective ?? (append A l).
definition shift_l ≝ λsig,n,i,v1,v2. (* multi_sig sig n *)
|v1| = |v2| ∧
- ∀j.nth j ? v2 (all_blank sig n) =
- change_vec ? n (nth j ? v1 (all_blank sig n))
- (nth i ? (vec … (nth (S j) ? v1 (all_blank sig n))) (blank ?)) i.
+ ∀j.nth j ? v2 (all_blanks sig n) =
+ change_vec ? n (nth j ? v1 (all_blanks sig n))
+ (nth i ? (vec … (nth (S j) ? v1 (all_blanks sig n))) (blank ?)) i.
(* supposing (shift_l … i v1 v2), the i-th trace of v2 is equal to the tail of
the i-th trace of v1, plus a trailing blank *)
|#b #tl #_ normalize >length_append >length_trace normalize //
]
|#j >nth_trace >Hnth >nth_change_vec // >tail_trace
- cut (trace ? n i [all_blank sig n] = [blank sig])
- [normalize >blank_all_blank //]
+ cut (trace ? n i [all_blanks sig n] = [blank sig])
+ [normalize >blank_all_blanks //]
#Hcut <Hcut <trace_append >nth_trace
<nth_extended //
]
(∀i. i ≤ n → to_blank_i sig n i (a::l1) = to_blank_i sig n i (b::l2)) → a = b.
lemma to_blank_i_ext : ∀sig,n,i,l.
- to_blank_i sig n i l = to_blank_i sig n i (l@[all_blank …]).
+ to_blank_i sig n i l = to_blank_i sig n i (l@[all_blanks …]).
#sig #n #i #l elim l
- [@sym_eq @to_blank_cons_b @blank_all_blank
+ [@sym_eq @to_blank_cons_b @blank_all_blanks
|#a #tl #Hind whd in match (to_blank_i ????); >Hind <to_blank_i_def >Hind %
]
qed.
lemma to_blank_hd_cons : ∀sig,n,i,l1,l2.
to_blank_i sig n i (l1@l2) =
- to_blank_i … i (l1@(hd … l2 (all_blank …))::tail … l2).
+ to_blank_i … i (l1@(hd … l2 (all_blanks …))::tail … l2).
#sig #n #i #l1 #l2 cases l2
[whd in match (hd ???); whd in match (tail ??); >append_nil @to_blank_i_ext
|#a #tl %
projects / helm.git / commitdiff