Changeset 1515 for src/utilities


Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (9 years ago)
Author:
campbell
Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
Location:
src/utilities
Files:
3 edited

Legend:

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

    r1330 r1515  
    656656definition minus ≝ λn,m. match partial_minus n m with [ MinusPos p ⇒ p | _ ⇒ one ].
    657657
    658 interpretation "natural minus" 'minus x y = (minus x y).
     658interpretation "positive minus" 'minus x y = (minus x y).
    659659
    660660lemma partialminus_S: ∀n,m:Pos.
     
    942942  ].
    943943
    944 theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Prop.
     944theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Type[0].
    945945(n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)).
    946946#n elim n;
     
    11591159
    11601160definition two_power_pos : Pos → Pos ≝ λp.two_power_nat (nat_of_pos p).
     1161
     1162
     1163
     1164definition max : Pos → Pos → Pos ≝
     1165λn,m. match leb n m with [ true ⇒ m | _ ⇒ n].
  • src/utilities/extralib.ma

    r1350 r1515  
    389389definition mod ≝ λm,n. snd ?? (divide m n).
    390390
    391 lemma pred_minus: ∀n,m. pred n - m = pred (n-m).
     391lemma pred_minus: ∀n,m:Pos. pred n - m = pred (n-m).
    392392@pos_elim /3/;
    393393qed.
  • src/utilities/extranat.ma

    r961 r1515  
     1include "basics/types.ma".
    12include "arithmetics/nat.ma".
    23
     
    3637[ //
    3738| #m' #IH whd in ⊢ (??%?) > IH @refl
     39] qed.
     40
     41
     42let rec eq_nat_dec (n:nat) (m:nat) : Sum (n=m) (n≠m) ≝
     43match n return λn.Sum (n=m) (n≠m) with
     44[ O ⇒ match m return λm.Sum (O=m) (O≠m) with [O ⇒ inl ?? (refl ??) | S m' ⇒ inr ??? ]
     45| S n' ⇒ match m return λm.Sum (S n'=m) (S n'≠m) with [O ⇒ inr ??? | S m' ⇒
     46           match eq_nat_dec n' m' with [ inl E ⇒ inl ??? | inr NE ⇒ inr ??? ] ]
     47].
     48[ 1,2: % #E destruct
     49| >E @refl
     50| % #E destruct cases NE /2/
    3851] qed.
    3952
Note: See TracChangeset for help on using the changeset viewer.