Changeset 24 for C-semantics/Coqlib.ma


Ignore:
Timestamp:
Aug 27, 2010, 1:21:50 PM (10 years ago)
Author:
campbell
Message:

Separate out IOMonad from the rest of the executable semantics.
Start adding simulation results.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Coqlib.ma

    r10 r24  
    794794  induction l; simpl; congruence.
    795795Qed.
    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*)
     797nlemma 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(*
    809812Lemma list_append_map:
    810813  forall (A B: Type) (f: A -> B) (l1 l2: list A),
Note: See TracChangeset for help on using the changeset viewer.