Changeset 3574 for LTS/utils.ma
 Timestamp:
 Jun 18, 2015, 6:33:00 PM (4 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/utils.ma
r3563 r3574 17 17 include "../src/ASM/Util.ma". 18 18 include "../src/utilities/option.ma". 19 20 definition update_fun : ∀A : DeqSet.∀B : Type[0].(A → B) → A → B → A → B ≝ 21 λA,B,f,a,b,x.if x == a then b else f x. 19 22 20 23 lemma bind_inversion : ∀A,B : Type[0].∀m : option A. … … 360 363 @eq_f2 // @IH // 361 364 qed. 365 366 (* nth_opt*) 367 368 lemma nth_first : ∀A.∀l1,l2 : list A.∀n : ℕ.l1 > n → nth_opt … n (l1 @ l2) = nth_opt … n l1. 369 #A #l1 elim l1 [ #l2 #n normalize #H @⊥ /2/] #x #xs #IH #l2 * // #n #H @IH normalize in H; /2/ 370 qed. 371 372 lemma nth_second : ∀A.∀l1,l2 : list A.∀n : ℕ.l1 ≤ n → nth_opt … n (l1 @ l2) = nth_opt … (n  l1) l2. 373 #A #l1 elim l1 [normalize //] #x #xs #IH #l2 * [ normalize #H @⊥ /2/] #n #H normalize @IH /2/ 374 qed.
Note: See TracChangeset
for help on using the changeset viewer.