nat : type. z : nat. s : {x: nat} nat. list : type. nil : list. cons : {x:nat}{L: list} list. map : {f:{x:nat}nat}{l1:list}{l2:list} type. map-nil : {f:{x:nat}nat} map ([x] f x) nil nil. map-cons : {f:{x:nat}nat}{l1:list}{l2:list}{d:map ([x] f x) l1 l2}{e:nat} map ([x] f x) (cons e l1) (cons (f e) l2). eq-list : {l1:list}{l2:list} type. eq-list-nil : eq-list nil nil. eq-list-cons : {l1:list}{l2:list}{x:nat}{d:eq-list l1 l2} eq-list (cons x l1) (cons x l2). append : {l1:list}{l2:list}{l3:list} type. append-nil : {l2:list} append nil l2 l2. append-cons : {l1:list}{l2:list}{l3:list}{x:nat}{d: append l1 l2 l3} append (cons x l1) l2 (cons x l3).
Click on a command or tactic to see a detailed view of its use.
Specification "map.lf". Theorem map-eq : forall L1 L2 L3 D1 D2 f, {D1: map f L1 L2} => {D2: map f L1 L3} => exists E, {E: eq-list L2 L3}.induction on 1. intros. case H1. % cons case case H2. inst H3 with n = e. apply IH to H6 H11. exists eq-list-cons l2 L4 (f1 e) (E n1 n). search. % nil case case H2. exists eq-list-nil. search.Theorem map-distrib-append : forall L1 L2 L12 f FL12 FL1 FL2 D1 D2 D3 D4 D5 FL12', {D1: append L1 L2 L12} => {D2: map f L12 FL12} => {D3: map f L1 FL1} => {D4: map f L2 FL2} => {D5: append FL1 FL2 FL12'} => exists E, {E: eq-list FL12 FL12'}.