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

No more axioms but the paralogisms.

File:
1 edited

Legend:

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

    r350 r351  
    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).
    40 *)
     39
     40notation "hvbox(n break ≲ m)"
     41  non associative with precedence 47
     42  for @{ 'less_than_or_equalb $n $m }.
     43
     44interpretation "Nat less than or equal bool" 'less_than_or_equalb n m = (less_than_or_equal_b n m).
     45
    4146
    4247ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝
     
    5459
    5560interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m).
    56 (*interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m).
    57 *)
     61
     62notation "hvbox(n break ≳ m)"
     63  non associative with precedence 47
     64  for @{ 'greater_than_or_equalb $n $m }.
     65
     66interpretation "Nat greater than or equal bool" 'greater_than_or_equalb n m = (greater_than_or_equal_b n m).
     67
    5868
    5969(* Add Boolean versions.                                                      *)
     
    236246(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    237247
    238 naxiom plus_minus_inverse_left:
     248(*naxiom plus_minus_inverse_left:
    239249  ∀m, n: Nat.
    240250    (m + n) - n = m.
    241    
     251*)
     252 
    242253ntheorem less_than_or_equal_monotone:
    243254  ∀m, n: Nat.
     
    250261nqed.
    251262
    252 ntheorem succ_less_than_or_equal_injective:
     263ntheorem less_than_or_equal_injective:
    253264  ∀m, n: Nat.
    254265    (S m) ≤ (S n) → m ≤ n.
     
    259270nqed.
    260271   
    261 naxiom plus_minus_inverse_right:
    262   ∀m, n: Nat.
    263     (m - n) + n = m.
    264 
    265272ntheorem succ_less_than_injective:
    266273  ∀m, n: Nat.
     
    279286 #m; @; #H; nlapply (not_less_than_S_Z m Z H); /2/;
    280287nqed.
     288
    281289   
    282290(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    294302nqed.
    295303
    296 naxiom less_than_or_equal_injective:
    297   ∀m, n: Nat.
    298     S m ≤ S n → m ≤ n.
    299 
    300304(*
    301305nlemma less_than_or_equal_zero_equal_zero:
     
    548552nqed.
    549553
     554
     555nlemma succ_injective:
     556  ∀m, n: Nat.
     557    S m = S n → m = n.
     558  #m n H;
     559  napply (match H return λy.λ_.m = match y with [Z ⇒ Z | S z ⇒ z] with
     560           [refl ⇒ ? ]);
     561  @;
     562nqed.
     563
     564ntheorem eq_f: ∀A,B:Type[0].∀f:A→B.∀a,a'. a=a' → f a = f a'.
     565 //;
     566nqed.
     567
     568ntheorem plus_minus_inverse_right:
     569  ∀m, n: Nat.
     570   n ≤ m → (m - n) + n = m.
     571 #m; nelim m
     572  [ #n; nelim n; //; #H1 H2 H3; ncases (nothing_less_than_Z H1);
     573    #K; ncases (K H3)
     574  | #y H1 x H2; nnormalize; ngeneralize in match H2; ncases x; nnormalize; /2/;
     575    #w; nrewrite < succ_plus; /4/. ##]
     576nqed.
     577
    550578(*
    551 nlemma succ_injective:
    552   ∀m, n: Nat.
    553     S m = S n → m = n.
    554   #m n.
    555   nelim m.
    556   #H.
    557   ninversion H.
    558   #H.
    559   ndestruct
    560579
    561580nlemma plus_minus_associate:
     
    578597  #N H.
    579598*)
     599
     600ntheorem less_than_or_equal_b_correct: ∀m,n. less_than_or_equal_b m n = true → m ≤ n.
     601 #m; nelim m; //; #y H1 z; ncases z; nnormalize
     602  [ #H; ndestruct | /3/ ]
     603nqed.
     604
     605ntheorem less_than_or_equal_b_complete: ∀m,n. less_than_or_equal_b m n = false → ¬(m ≤ n).
     606 #m; nelim m; nnormalize
     607  [ #n H; ndestruct | #y H1 z; ncases z; nnormalize
     608    [ #H; ndestruct | /3/ ] /2/.
     609nqed.
     610
     611ndefinition less_than_or_equal_b_elim:
     612 ∀m,n. ∀P: Bool → Type[0]. (m ≤ n → P true) → (¬(m ≤ n) → P false) →
     613  P (less_than_or_equal_b m n).
     614 #m n P H1 H2; nlapply (less_than_or_equal_b_correct m n);
     615 nlapply (less_than_or_equal_b_complete m n);
     616 ncases (less_than_or_equal_b m n); /3/.
     617nqed.
     618
     619ndefinition greater_than_or_equal_b_elim:
     620 ∀m,n. ∀P: Bool → Type[0]. (m ≥ n → P true) → (¬(m ≥ n) → P false) →
     621  P (greater_than_or_equal_b m n).
     622 #m n; napply less_than_or_equal_b_elim;
     623nqed.
     624
     625ntheorem less_than_b_correct: ∀m,n. less_than_b m n = true → m < n.
     626 #m; nelim m
     627  [ #n; ncases n [ #H; nnormalize in H; ndestruct | #z H; /2/ ]
     628##| #y H z; ncases z [ nnormalize; #K; ndestruct | #o K;
     629    napply less_than_or_equal_monotone; napply H; napply K ]
     630nqed.
     631
     632ntheorem less_than_b_complete: ∀m,n. less_than_b m n = false → ¬(m < n).
     633 #m; nelim m
     634  [ #n; ncases n; //; #y H1; nnormalize in H1; ndestruct
     635  | #y H z; ncases z; //; #o H2; nlapply (H … H2); /3/.
     636nqed.
     637
     638ndefinition less_than_b_elim:
     639 ∀m,n. ∀P: Bool → Type[0]. (m < n → P true) → (¬(m < n) → P false) →
     640  P (less_than_b m n).
     641 #m n; nlapply (less_than_b_correct m n); nlapply (less_than_b_complete m n);
     642 ncases (less_than_b m n); /3/.
     643nqed.
     644
     645ndefinition greater_than_b_elim:
     646 ∀m,n. ∀P: Bool → Type[0]. (m > n → P true) → (¬(m > n) → P false) →
     647  P (greater_than_b m n).
     648 #m n; napply less_than_b_elim.
     649nqed.
Note: See TracChangeset for help on using the changeset viewer.