Changeset 487 for Deliverables/D3.1/Csemantics/Coqlib.ma
 Timestamp:
 Feb 9, 2011, 11:49:17 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Coqlib.ma
r473 r487 19 19 20 20 include "binary/Z.ma". 21 include " datatypes/sums.ma".22 include " datatypes/list.ma".21 include "basics/types.ma". 22 include "basics/list.ma". 23 23 24 24 include "extralib.ma". … … 350 350 (* * Properties of powers of two. *) 351 351 352 nlemma two_power_nat_O : two_power_nat O = one.353 // ; nqed.354 355 nlemma two_power_nat_pos : ∀n:nat. Z_two_power_nat n > 0.356 // ; nqed.357 358 nlemma two_power_nat_two_p:352 lemma two_power_nat_O : two_power_nat O = one. 353 // qed. 354 355 lemma two_power_nat_pos : ∀n:nat. Z_two_power_nat n > 0. 356 // qed. 357 358 lemma two_power_nat_two_p: 359 359 ∀x. Z_two_power_nat x = two_p (Z_of_nat x). 360 #x ; ncases x;361 ##[ //; 362 ## nnormalize; #p; nelim p; //; #p' H; nrewrite > (nat_succ_pos …); //; 363 ##] nqed.360 #x cases x 361 [ // 362  normalize #p elim p // #p' #H >(nat_succ_pos …) // 363 ] qed. 364 364 (* 365 365 Lemma two_p_monotone: … … 576 576 (*naxiom align : Z → Z → Z.*) 577 577 578 ndefinition align ≝ λn: Z. λamount: Z.578 definition align ≝ λn: Z. λamount: Z. 579 579 ((n + amount  1) / amount) * amount. 580 580 (* … … 600 600 (* * Mapping a function over an option type. *) 601 601 602 ndefinition option_map ≝ λA,B.λf:A→B.λv:option A.602 definition option_map ≝ λA,B.λf:A→B.λv:option A. 603 603 match v with [ Some v' ⇒ Some ? (f v')  None ⇒ None ? ]. 604 604 … … 794 794 induction l; simpl; congruence. 795 795 Qed. 796 *) 797 nlemma list_in_map_inv:798 ∀A,B: Type . ∀f: A > B. ∀l: list A. ∀y: B.796 *) (* 797 lemma list_in_map_inv: 798 ∀A,B: Type[0]. ∀f: A > B. ∀l: list A. ∀y: B. 799 799 in_list ? y (map ?? f l) → ∃x:A. y = f x ∧ in_list ? x l. 800 800 #A B f l; nelim l; … … 808 808 nelim (IH h H1); #x'; *; #IH1 IH2; @x'; @; /2/; 809 809 ##] 810 ##] nqed. 810 ##] nqed.*) 811 811 (* 812 812 Lemma list_append_map: … … 841 841 (* * [list_disjoint l1 l2] holds iff [l1] and [l2] have no elements 842 842 in common. *) 843 844 ndefinition list_disjoint : ∀A:Type. list A → list A → Prop ≝843 (* 844 definition list_disjoint : ∀A:Type[0]. list A → list A → Prop ≝ 845 845 λA,l1,l2. 846 846 ∀x,y: A. in_list A x l1 → in_list A y l2 → x ≠ y. 847 847 848 nlemma list_disjoint_cons_left:849 ∀A: Type . ∀a: A. ∀l1,l2: list A.848 lemma list_disjoint_cons_left: 849 ∀A: Type[0]. ∀a: A. ∀l1,l2: list A. 850 850 list_disjoint A (a :: l1) l2 → list_disjoint A l1 l2. 851 851 #A;#a;#l1;#l2;nwhd in ⊢ (% → %); #H; … … 874 874 nwhd in ⊢ (% → %); 875 875 #H;#x;#y;#H1;#H2; napply sym_neq; /2/; 876 nqed. 876 nqed.*) 877 877 878 (* 878 879 Lemma list_disjoint_dec: … … 898 899 (* * [list_norepet l] holds iff the list [l] contains no repetitions, 899 900 i.e. no element occurs twice. *) 900 901 ninductive list_norepet (A: Type) : list A → Prop ≝901 (* 902 inductive list_norepet (A: Type[0]) : list A → Prop ≝ 902 903  list_norepet_nil: 903 904 list_norepet A (nil A) 904 905  list_norepet_cons: 905 906 ∀hd,tl. 906 ¬(in_list A hd tl) → list_norepet A tl → list_norepet A (hd :: tl). 907 ¬(in_list A hd tl) → list_norepet A tl → list_norepet A (hd :: tl).*) 907 908 (* 908 909 Lemma list_norepet_dec:
Note: See TracChangeset
for help on using the changeset viewer.