source: src/utilities/extranat.ma @ 961

Last change on this file since 961 was 961, checked in by campbell, 8 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.