Changeset 1628 for src/utilities
- Timestamp:
- Dec 19, 2011, 2:48:35 PM (9 years ago)
- Location:
- src/utilities
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/utilities/binary/positive.ma
r1587 r1628 1161 1161 λn,m. match leb n m with [ true ⇒ m | _ ⇒ n]. 1162 1162 1163 lemma commutative_max : commutative Pos max. 1164 #n #m whd in ⊢ (??%%); 1165 lapply (pos_compare_to_Prop n m) 1166 cases (pos_compare n m) whd in ⊢ (% → ?); #H 1167 [ >(le_to_leb_true n m) >(not_le_to_leb_false m n) /2/ 1168 | >H @refl 1169 | >(le_to_leb_true m n) >(not_le_to_leb_false n m) /2/ 1170 ] qed. 1171 1172 lemma max_l : ∀m,n:Pos. m ≤ max m n. 1173 #m #n normalize @leb_elim // 1174 qed. 1175 1176 lemma max_r : ∀m,n:Pos. n ≤ max m n. 1177 #m #n >commutative_max // 1178 qed. 1163 1179 1164 1180 -
src/utilities/lists.ma
r1626 r1628 1 1 include "basics/lists/list.ma". 2 3 (* An alternative form of All that can be easier to use sometimes. *) 4 lemma All_alt : ∀A,P,l. 5 (∀a,pre,post. l = pre@a::post → P a) → 6 All A P l. 7 #A #P #l #H lapply (refl ? l) change with ([ ] @ l) in ⊢ (???% → ?); 8 generalize in ⊢ (???(??%?) → ?); elim l in ⊢ (? → ???(???%) → %); 9 [ #pre #E % 10 | #a #tl #IH #pre #E % 11 [ @(H a pre tl E) 12 | @(IH (pre@[a])) >associative_append @E 13 ] 14 ] qed. 2 15 3 16 let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝
Note: See TracChangeset
for help on using the changeset viewer.