source: src/utilities/extranat.ma @ 1516

Last change on this file since 1516 was 1516, checked in by sacerdot, 8 years ago

Ported to syntax of Matita 0.99.1.

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