source: src/utilities/extranat.ma @ 1445

Last change on this file since 1445 was 961, checked in by campbell, 10 years ago

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File size: 2.5 KB
Line 
1include "arithmetics/nat.ma".
2
3inductive nat_compared : nat → nat → Type[0] ≝
4| nat_lt : ∀n,m:nat. nat_compared n (n+S m)
5| nat_eq : ∀n:nat.   nat_compared n n
6| nat_gt : ∀n,m:nat. nat_compared (m+S n) m.
7
8let rec nat_compare (n:nat) (m:nat) : nat_compared n m ≝
9match n return λx. nat_compared x m with
10[ O ⇒ match m return λy. nat_compared O y with [ O ⇒ nat_eq ? | S m' ⇒ nat_lt ?? ]
11| S n' ⇒
12    match m return λy. nat_compared (S n') y with
13    [ O ⇒ nat_gt n' O
14    | S m' ⇒ match nat_compare n' m' return λx,y.λ_. nat_compared (S x) (S y) with
15             [ nat_lt x y ⇒ nat_lt ??
16             | nat_eq x ⇒ nat_eq ?
17             | nat_gt x y ⇒ nat_gt ? (S y)
18             ]
19    ]
20].
21
22lemma nat_compare_eq : ∀n. nat_compare n n = nat_eq n.
23#n elim n
24[ @refl
25| #m #IH whd in ⊢ (??%?) > IH @refl
26] qed.
27
28lemma nat_compare_lt : ∀n,m. nat_compare n (n+S m) = nat_lt n m.
29#n #m elim n
30[ //
31| #n' #IH whd in ⊢ (??%?) > IH @refl
32] qed.
33
34lemma nat_compare_gt : ∀n,m. nat_compare (m+S n) m = nat_gt n m.
35#n #m elim m
36[ //
37| #m' #IH whd in ⊢ (??%?) > IH @refl
38] qed.
39
40lemma max_l : ∀m,n,o:nat. o ≤ m → o ≤ max m n.
41#m #n #o #H whd in ⊢ (??%) @leb_elim #H'
42[ @(transitive_le ? m ? H H')
43| @H
44] qed.
45
46lemma max_r : ∀m,n,o:nat. o ≤ n → o ≤ max m n.
47#m #n #o #H whd in ⊢ (??%) @leb_elim #H'
48[ @H
49| @(transitive_le … H) @(transitive_le … (not_le_to_lt … H')) //
50] qed.
51
52
53(* "Fast" proofs:  some proofs get reduced during normalization (in particular,
54   some functions which use a proof for rewriting are applied to constants and
55   get reduced during a proof or while matita is searching for a term;
56   they may also be normalized during testing), and so here are some more
57   efficient versions.  Perhaps they could be replaced using some kind of proof
58   irrelevance? *)
59
60let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝
61match n return λn'.∀m.S(n'+m) = n'+S m with
62[ O ⇒ λm.refl ??
63| S n' ⇒ λm. ?
64]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed.
65
66let rec plus_n_O_faster (n:nat) : n = n + O ≝
67match n return λn.n=n+O with
68[ O ⇒ refl ??
69| S n' ⇒ match plus_n_O_faster n' return λx.λ_.S n'=S x with [ refl ⇒ refl ?? ]
70].
71
72let rec commutative_plus_faster (n,m:nat) : n+m = m+n ≝
73match n return λn.n+m = m+n with
74[ O ⇒ plus_n_O_faster ?
75| S n' ⇒ ?
76]. @(match plus_n_Sm_fast m n' return λx.λ_. ? = x with [ refl ⇒ ? ])
77@(match commutative_plus_faster n' m return λx.λ_.? = S x with [refl ⇒ ?]) @refl qed.
78
Note: See TracBrowser for help on using the repository browser.