Changeset 3574 for LTS/utils.ma


Ignore:
Timestamp:
Jun 18, 2015, 6:33:00 PM (4 years ago)
Author:
piccolo
Message:

assembly pass in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/utils.ma

    r3563 r3574  
    1717include "../src/ASM/Util.ma".
    1818include "../src/utilities/option.ma".
     19
     20definition 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.
    1922
    2023lemma bind_inversion : ∀A,B : Type[0].∀m : option A.
     
    360363@eq_f2 // @IH //
    361364qed.
     365
     366(* nth_opt*)
     367
     368lemma 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/
     370qed.
     371
     372lemma 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/
     374qed.
Note: See TracChangeset for help on using the changeset viewer.