Changeset 1628 for src/utilities


Ignore:
Timestamp:
Dec 19, 2011, 2:48:35 PM (9 years ago)
Author:
campbell
Message:

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

Location:
src/utilities
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/binary/positive.ma

    r1587 r1628  
    11611161λn,m. match leb n m with [ true ⇒ m | _ ⇒ n].
    11621162
     1163lemma commutative_max : commutative Pos max.
     1164#n #m whd in ⊢ (??%%);
     1165lapply (pos_compare_to_Prop n m)
     1166cases (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
     1172lemma max_l : ∀m,n:Pos. m ≤ max m n.
     1173#m #n normalize @leb_elim //
     1174qed.
     1175
     1176lemma max_r : ∀m,n:Pos. n ≤ max m n.
     1177#m #n >commutative_max //
     1178qed.
    11631179
    11641180
  • src/utilities/lists.ma

    r1626 r1628  
    11include "basics/lists/list.ma".
     2
     3(* An alternative form of All that can be easier to use sometimes. *)
     4lemma 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 ⊢ (???% → ?);
     8generalize 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.
    215
    316let 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.