Changeset 2111 for src/ASM/Util.ma
 Timestamp:
 Jun 26, 2012, 5:30:41 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r2055 r2111 253 253 qed. 254 254 255 (*CSC: practically equal to shift_nth_safe but for commutation 256 of addition. One of the two lemmas should disappear. *) 257 lemma nth_safe_prepend: 258 ∀A,l1,l2,j.∀H:j<l2.∀K:l1+j<(l1@l2). 259 nth_safe A j l2 H =nth_safe A (l1+j) (l1@l2) K. 260 #A #l1 #l2 #j #H >commutative_plus @shift_nth_safe 261 qed. 262 263 lemma nth_safe_cons: 264 ∀A,hd,tl,l2,j,j_ok,Sj_ok. 265 nth_safe A j (tl@l2) j_ok =nth_safe A (1+j) (hd::tl@l2) Sj_ok. 266 // 267 qed. 268 269 lemma eq_nth_safe_proof_irrelevant: 270 ∀A,l,i,i_ok,i_ok'. 271 nth_safe A l i i_ok = nth_safe A l i i_ok'. 272 #A #l #i #i_ok #i_ok' % 273 qed. 274 275 lemma nth_safe_append: 276 ∀A,l,n,n_ok. 277 ∃pre,suff. 278 (pre @ [nth_safe A n l n_ok]) @ suff = l. 279 #A #l elim l normalize 280 [ #n #abs cases (absurd ? abs (not_le_Sn_O ?)) 281  #hd #tl #IH #n cases n normalize 282 [ #_ %{[]} /2/ 283  #m #m_ok cases (IH m ?) 284 [ #pre * #suff #EQ %{(hd::pre)} %{suff} <EQ in ⊢ (???%); %  skip ]] 285 qed. 255 286 256 287 definition last_safe ≝
Note: See TracChangeset
for help on using the changeset viewer.