Changeset 3552 for LTS/Vm.ma


Ignore:
Timestamp:
Apr 9, 2015, 11:04:21 PM (5 years ago)
Author:
piccolo
Message:

closed all daemons

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3549 r3552  
    821821  |*: #tl #IH #lbl whd in match (get_costlabels_of_trace ????); * // @IH
    822822]
    823 qed.
    824 
    825 let rec dependent_map (A,B : Type[0]) (l : list A) (f : ∀a : A.mem … a l → B) on l : list B ≝
    826 (match l return λx.l=x → ? with
    827 [ nil ⇒ λ_.nil ?
    828 | cons x xs ⇒ λprf.(f x ?) :: dependent_map A B xs (λx,prf1.f x ?)
    829 ])(refl …).
    830 [ >prf %% | >prf %2 assumption]
    831 qed.
    832 
    833 lemma dependent_map_append : ∀A,B,l1,l2,f.
    834 dependent_map A B (l1 @ l2) (λa,prf.f a prf) =
    835 (dependent_map A B l1 (λa,prf.f a ?)) @ (dependent_map A B l2 (λa,prf.f a ?)).
    836 [2: @hide_prf /2/ | 3: @hide_prf /2/]
    837 #A #B #l1 elim l1 normalize /2/
    838 qed.
    839 
    840 lemma rewrite_in_dependent_map : ∀A,B,l1,l2,f.
    841         ∀EQ:l1 = l2.
    842          dependent_map A B l1 (λa,prf.f a prf) =
    843          dependent_map A B l2 (λa,prf.f a ?).
    844 [2: >EQ // | #A #B #l1 #l2 #f #EQ >EQ in f; #f % ]
    845823qed.
    846824
Note: See TracChangeset for help on using the changeset viewer.