Changeset 1628 for src/utilities

Timestamp:

Dec 19, 2011, 2:48:35 PM (8 years ago)

Author:

campbell

Message:

Show that the universe generated by Clight/fresh.ma is good.

Location:

src/utilities

Files:

• binary/positive.ma (modified) (1 diff)
• lists.ma (modified) (1 diff)

src/utilities/binary/positive.ma

@@ -1161 +1161 @@
 λn,m. match leb n m with [ true ⇒ m | _ ⇒ n].
 
+lemma commutative_max : commutative Pos max.
+#n #m whd in ⊢ (??%%);
+lapply (pos_compare_to_Prop n m)
+cases (pos_compare n m) whd in ⊢ (% → ?); #H
+[ >(le_to_leb_true n m) >(not_le_to_leb_false m n) /2/
+| >H @refl
+| >(le_to_leb_true m n) >(not_le_to_leb_false n m) /2/
+] qed.
+
+lemma max_l : ∀m,n:Pos. m ≤ max m n.
+#m #n normalize @leb_elim //
+qed.
+
+lemma max_r : ∀m,n:Pos. n ≤ max m n.
+#m #n >commutative_max //
+qed.
 
 

src/utilities/lists.ma

@@ -1 +1 @@
 include "basics/lists/list.ma".
+
+(* An alternative form of All that can be easier to use sometimes. *)
+lemma All_alt : ∀A,P,l.
+  (∀a,pre,post. l = pre@a::post → P a) →
+  All A P l.
+#A #P #l #H lapply (refl ? l) change with ([ ] @ l) in ⊢ (???% → ?);
+generalize in ⊢ (???(??%?) → ?); elim l in ⊢ (? → ???(???%) → %);
+[ #pre #E %
+| #a #tl #IH #pre #E %
+  [ @(H a pre tl E)
+  | @(IH (pre@[a])) >associative_append @E
+  ]
+] qed.
 
 let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝