Ignore:
Timestamp:
Dec 1, 2010, 1:10:53 PM (10 years ago)
Author:
mulligan
Message:

less axioms

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Nat.ma

    r349 r350  
    3737 
    3838interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m).
    39 interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m).
     39(*interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m).
     40*)
    4041
    4142ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝
     
    4546ndefinition greater_than_or_equal_b: ∀m, n: Nat. Bool ≝
    4647  λm, n: Nat.
    47     n ≤ m.
     48    less_than_or_equal_b n m.
    4849   
    4950notation "hvbox(n break ≥ m)"
     
    5354
    5455interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m).
    55 interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m).
     56(*interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m).
     57*)
    5658
    5759(* Add Boolean versions.                                                      *)
     
    7678 
    7779interpretation "Nat greater than prop" 'greater_than n m = (greater_than_p n m).
     80
     81nlet rec less_than_b (m: Nat) (n: Nat) on m ≝
     82  match m with
     83    [ Z ⇒
     84      match n with
     85        [ Z ⇒ false
     86        | S o ⇒ true
     87        ]
     88    | S o ⇒
     89      match n with
     90        [ Z ⇒ false
     91        | S p ⇒ less_than_b o p
     92        ]
     93    ].
     94
     95(* interpretation "Nat less than bool" 'less_than n m = (less_than_b n m). *)
     96
     97ndefinition greater_than_b ≝
     98  λm, n: Nat.
     99    less_than_b n m.
     100   
     101(* interpretation "Nat greater than bool" 'greater_than n m = (greater_than_b n m). *)
    78102
    79103(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    125149
    126150nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝
    127   match n ≤ p with
     151  match less_than_or_equal_b n p with
    128152    [ true ⇒ Z
    129153    | false ⇒
     
    148172     
    149173nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝
    150   match n ≤ p with
     174  match less_than_or_equal_b n p with
    151175    [ true ⇒ n
    152176    | false ⇒
     
    216240    (m + n) - n = m.
    217241   
    218 naxiom less_than_or_equal_monotone:
     242ntheorem less_than_or_equal_monotone:
    219243  ∀m, n: Nat.
    220244    m ≤ n → (S m) ≤ (S n).
    221    
    222 naxiom succ_less_than_or_equal_injective:
     245 #m n H; nelim H; /2/.
     246nqed.
     247
     248nlemma trans_le: ∀n,m,l. n ≤ m → m ≤ l → n ≤ l.
     249 #n m l H H1; nelim H1; /2/.
     250nqed.
     251
     252ntheorem succ_less_than_or_equal_injective:
    223253  ∀m, n: Nat.
    224254    (S m) ≤ (S n) → m ≤ n.
     255 #m n H;
     256 nchange with (match S m with [ Z ⇒ Z | S x ⇒ x] ≤ match S n with [ Z ⇒ Z | S x ⇒ x]);
     257 napply (match H return λx.λ_. m ≤ match x with [Z ⇒ Z | S x ⇒ x] with [ ltoe_refl ⇒ ? | ltoe_step y H ⇒ ? ]);
     258 nnormalize; /3/.
     259nqed.
    225260   
    226261naxiom plus_minus_inverse_right:
     
    228263    (m - n) + n = m.
    229264
    230 naxiom greater_than_b: Nat → Nat → Bool.
    231 naxiom less_than_b: Nat → Nat → Bool.
    232 
    233 naxiom succ_less_than_injective:
     265ntheorem succ_less_than_injective:
    234266  ∀m, n: Nat.
    235267    less_than_p (S m) (S n) → m < n.
    236    
    237 naxiom nothing_less_than_Z:
     268 /2/.
     269nqed.
     270
     271nlemma not_less_than_S_Z:
     272 ∀m,n: Nat. S m ≤ n → ¬ (n = Z).
     273 #m n H; nelim H [ @; #K; ndestruct | #y H1 H2; @; #K; ndestruct ]
     274nqed.
     275
     276ntheorem nothing_less_than_Z:
    238277  ∀m: Nat.
    239278    ¬(m < Z).
     279 #m; @; #H; nlapply (not_less_than_S_Z m Z H); /2/;
     280nqed.
    240281   
    241282(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.