# source:src/utilities/extranat.ma

Last change on this file was 3081, checked in by campbell, 8 years ago

Tidy up recent work a little.

File size: 5.2 KB
Line
1include "basics/types.ma".
2include "arithmetics/nat.ma".
3include "utilities/option.ma".
4
5(* JHM: here, for definiteness; used in ASM/ASM.ma *)
6let rec nat_bound_opt (N:nat) (n:nat) : option (n < N) ≝
7match N return λy. option (n < y) with
8[ O ⇒ None ?
9| S N' ⇒
10    match n return λx. option (x < S N') with
11    [ O ⇒ (return (lt_O_S ?))
12    | S n' ⇒ (! prf ← nat_bound_opt N' n' ; return (le_S_S ?? prf))
13    ]
14].
15
16lemma plus_split : ∀x,y:nat. ∃z. x = y + z ∨ y = x + z.
17#x0 elim x0
18[ #y %{y} %2 %
19| #x #IH *
20  [ %{(S x)} %1 %
21  | #y cases (IH y) #z *
22    [ #H %{z} %1 >H //
23    | #H %{z} %2 >H //
24    ]
25  ]
26] qed.
27
28inductive nat_compared : nat → nat → Type[0] ≝
29| nat_lt : ∀n,m:nat. nat_compared n (n+S m)
30| nat_eq : ∀n:nat.   nat_compared n n
31| nat_gt : ∀n,m:nat. nat_compared (m+S n) m.
32
33let rec nat_compare (n:nat) (m:nat) : nat_compared n m ≝
34match n return λx. nat_compared x m with
35[ O ⇒ match m return λy. nat_compared O y with [ O ⇒ nat_eq ? | S m' ⇒ nat_lt ?? ]
36| S n' ⇒
37    match m return λy. nat_compared (S n') y with
38    [ O ⇒ nat_gt n' O
39    | S m' ⇒ match nat_compare n' m' return λx,y.λ_. nat_compared (S x) (S y) with
40             [ nat_lt x y ⇒ nat_lt ??
41             | nat_eq x ⇒ nat_eq ?
42             | nat_gt x y ⇒ nat_gt ? (S y)
43             ]
44    ]
45].
46
47lemma nat_compare_eq : ∀n. nat_compare n n = nat_eq n.
48#n elim n
49[ @refl
50| #m #IH whd in ⊢ (??%?); >IH @refl
51] qed.
52
53lemma nat_compare_lt : ∀n,m. nat_compare n (n+S m) = nat_lt n m.
54#n #m elim n
55[ //
56| #n' #IH whd in ⊢ (??%?); >IH @refl
57] qed.
58
59lemma nat_compare_gt : ∀n,m. nat_compare (m+S n) m = nat_gt n m.
60#n #m elim m
61[ //
62| #m' #IH whd in ⊢ (??%?); >IH @refl
63] qed.
64
65
66let rec eq_nat_dec (n:nat) (m:nat) : Sum (n=m) (n≠m) ≝
67match n return λn.Sum (n=m) (n≠m) with
68[ O ⇒ match m return λm.Sum (O=m) (O≠m) with [O ⇒ inl ?? (refl ??) | S m' ⇒ inr ??? ]
69| S n' ⇒ match m return λm.Sum (S n'=m) (S n'≠m) with [O ⇒ inr ??? | S m' ⇒
70           match eq_nat_dec n' m' with [ inl E ⇒ inl ??? | inr NE ⇒ inr ??? ] ]
71].
72[ 1,2: % #E destruct
73| >E @refl
74| % #E destruct cases NE /2/
75] qed.
76
77lemma max_l : ∀m,n,o:nat. o ≤ m → o ≤ max m n.
78#m #n #o #H whd in ⊢ (??%); @leb_elim #H'
79[ @(transitive_le ? m ? H H')
80| @H
81] qed.
82
83lemma max_r : ∀m,n,o:nat. o ≤ n → o ≤ max m n.
84#m #n #o #H whd in ⊢ (??%); @leb_elim #H'
85[ @H
86| @(transitive_le … H) @(transitive_le … (not_le_to_lt … H')) //
87] qed.
88
89lemma max_O_n : ∀n. max O n = n.
90* //
91qed.
92
93lemma max_n_O : ∀n. max n O = n.
94* //
95qed.
96
97lemma associative_max : associative nat max.
98#n #m #o normalize
99@(leb_elim n m)
100[ normalize @(leb_elim m o) normalize #H1 #H2
101  [ >(le_to_leb_true n o) /2/
102  | >(le_to_leb_true n m) //
103  ]
104| normalize @(leb_elim m o) normalize #H1 #H2
105  [ %
106  | >(not_le_to_leb_false … H2)
107    >(not_le_to_leb_false n o) // @lt_to_not_le @(transitive_lt … m) /2/
108  ]
109] qed.
110
111lemma le_S_to_le: ∀n,m:ℕ.S n ≤ m → n ≤ m.
112 /2/ qed.
113
114lemma le_plus_k:
115  ∀n,m:ℕ.n ≤ m → ∃k:ℕ.m = n + k.
116 #n #m elim m -m;
117 [ #Hn % [ @O | <(le_n_O_to_eq n Hn) // ]
118 | #m #Hind #Hn cases (le_to_or_lt_eq … Hn) -Hn; #Hn
119   [ elim (Hind (le_S_S_to_le … Hn)) #k #Hk % [ @(S k) | >Hk // ]
120   | % [ @O | <Hn // ]
121   ]
122 ]
123qed.
124
125lemma eq_plus_S_to_lt:
126  ∀n,m,p:ℕ.n = m + (S p) → m < n.
127 #n #m #p /2 by lt_plus_to_lt_l/
128qed.
129
130(* "Fast" proofs:  some proofs get reduced during normalization (in particular,
131   some functions which use a proof for rewriting are applied to constants and
132   get reduced during a proof or while matita is searching for a term;
133   they may also be normalized during testing), and so here are some more
134   efficient versions.  Perhaps they could be replaced using some kind of proof
135   irrelevance? *)
136
137let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝
138match n return λn'.∀m.S(n'+m) = n'+S m with
139[ O ⇒ λm.refl ??
140| S n' ⇒ λm. ?
141]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed.
142
143let rec plus_n_O_faster (n:nat) : n = n + O ≝
144match n return λn.n=n+O with
145[ O ⇒ refl ??
146| S n' ⇒ match plus_n_O_faster n' return λx.λ_.S n'=S x with [ refl ⇒ refl ?? ]
147].
148
149let rec commutative_plus_faster (n,m:nat) : n+m = m+n ≝
150match n return λn.n+m = m+n with
151[ O ⇒ plus_n_O_faster ?
152| S n' ⇒ ?
153]. @(match plus_n_Sm_fast m n' return λx.λ_. ? = x with [ refl ⇒ ? ])
154@(match commutative_plus_faster n' m return λx.λ_.? = S x with [refl ⇒ ?]) @refl qed.
155
156lemma distributive_times_plus_fast : distributive ? times plus.
157#n elim n [ #m #p % ]
158#n' #IH #m #p normalize
159>IH
160>associative_plus in ⊢ (???%);
161<(associative_plus ? p) in ⊢ (???%);
162>(commutative_plus_faster ? p) in ⊢ (???%);
163>(associative_plus p)
164@associative_plus
165qed.
166
167lemma times_n_Sm_fast : ∀n,m.n + n * m = n * S m.
168#n elim n -n
169[ #m % ]
170#n #IH #m normalize <IH
171<associative_plus >(commutative_plus_faster n)
172>associative_plus >IH %
173qed.
174
175lemma commutative_times_fast : commutative ? times.
176#n elim n -n
177[ #m <times_n_O % ]
178#n #IH #m normalize <times_n_Sm_fast >IH %
179qed.
180
181(* notation for sum *)
182notation > "Σ_{ ident i ∈ l } f"
183  with precedence 20
184  for @{'fold plus 0 (λ\${ident i}.true) (λ\${ident i}. \$f) \$l}.
185notation < "hvbox(Σ_{ ident i break ∈ l } break f)"
186  with precedence 20
187for @{'fold plus 0 (λ\${ident i}:\$X.true) (λ\${ident i}:\$Y. \$f) \$l}.
188
Note: See TracBrowser for help on using the repository browser.