Changeset 24 for Csemantics/Coqlib.ma
 Timestamp:
 Aug 27, 2010, 1:21:50 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Coqlib.ma
r10 r24 794 794 induction l; simpl; congruence. 795 795 Qed. 796 797 Lemma list_in_map_inv: 798 forall (A B: Type) (f: A > B) (l: list A) (y: B), 799 In y (List.map f l) > exists x:A, y = f x /\ In x l. 800 Proof. 801 induction l; simpl; intros. 802 contradiction. 803 elim H; intro. 804 exists a; intuition auto. 805 generalize (IHl y H0). intros [x [EQ IN]]. 806 exists x; tauto. 807 Qed. 808 796 *) 797 nlemma list_in_map_inv: 798 ∀A,B: Type. ∀f: A > B. ∀l: list A. ∀y: B. 799 in_list ? y (map ?? f l) → ∃x:A. y = f x ∧ in_list ? x l. 800 #A B f l; nelim l; 801 ##[ nnormalize; #y H; ninversion H; 802 ##[ #x l' e1 e2; ndestruct; 803 ## #x z l' H1 H2 H3 H4; ndestruct; 804 ##] 805 ## #x l' IH y H; ninversion H; 806 ##[ nnormalize; #y' l'' e1 e2; ndestruct; @x; @; //; 807 ## nnormalize; #h h' t H1 H2 H3 H4; ndestruct; 808 nelim (IH h H1); #x'; *; #IH1 IH2; @x'; @; /2/; 809 ##] 810 ##] nqed. 811 (* 809 812 Lemma list_append_map: 810 813 forall (A B: Type) (f: A > B) (l1 l2: list A),
Note: See TracChangeset
for help on using the changeset viewer.