lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
// qed.
+theorem times_n_1 : ∀n:nat. n = n * 1.
+#n // qed.
+
(* ci servono questi risultati?
theorem times_O_to_O: ∀n,m:nat.n*m=O → n=O ∨ m=O.
napply nat_elim2 /2/
#n (elim n) // #abs @False_ind /2/
qed.
+theorem S_pred: ∀n. 0 < n → S(pred n) = n.
+#n #posn (cases posn) //
+qed.
+
(*
theorem lt_pred: \forall n,m.
O < n \to n < m \to pred n < pred m.
]
qed.
-theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
-intro.elim n.apply False_ind.exact (not_le_Sn_O O H).
-apply eq_f.apply pred_Sn.
-qed.
-
theorem le_pred_to_le:
∀n,m. O < m → pred n ≤ pred m → n ≤ m.
intros 2
qed.
(* some properties of functions *)
-(*
-definition increasing \def \lambda f:nat \to nat.
-\forall n:nat. f n < f (S n).
-
-theorem increasing_to_monotonic: \forall f:nat \to nat.
-increasing f \to monotonic nat lt f.
-unfold monotonic.unfold lt.unfold increasing.unfold lt.intros.elim H1.apply H.
-apply (trans_le ? (f n1)).
-assumption.apply (trans_le ? (S (f n1))).
-apply le_n_Sn.
-apply H.
+
+definition increasing ≝ λf:nat → nat. ∀n:nat. f n < f (S n).
+
+theorem increasing_to_monotonic: ∀f:nat → nat.
+ increasing f → monotonic nat lt f.
+#f #incr #n #m #ltnm (elim ltnm) /2/
qed.
-theorem le_n_fn: \forall f:nat \to nat. (increasing f)
-\to \forall n:nat. n \le (f n).
-intros.elim n.
-apply le_O_n.
-apply (trans_le ? (S (f n1))).
-apply le_S_S.apply H1.
-simplify in H. unfold increasing in H.unfold lt in H.apply H.
+theorem le_n_fn: ∀f:nat → nat.
+ increasing f → ∀n:nat. n ≤ f n.
+#f #incr #n (elim n) /2/
qed.
-theorem increasing_to_le: \forall f:nat \to nat. (increasing f)
-\to \forall m:nat. \exists i. m \le (f i).
-intros.elim m.
-apply (ex_intro ? ? O).apply le_O_n.
-elim H1.
-apply (ex_intro ? ? (S a)).
-apply (trans_le ? (S (f a))).
-apply le_S_S.assumption.
-simplify in H.unfold increasing in H.unfold lt in H.
-apply H.
+theorem increasing_to_le: ∀f:nat → nat.
+ increasing f → ∀m:nat.∃i.m ≤ f i.
+#f #incr #m (elim m) /2/#n * #a #lenfa
+@(ex_intro ?? (S a)) /2/
qed.
-theorem increasing_to_le2: \forall f:nat \to nat. (increasing f)
-\to \forall m:nat. (f O) \le m \to
-\exists i. (f i) \le m \land m <(f (S i)).
-intros.elim H1.
-apply (ex_intro ? ? O).
-split.apply le_n.apply H.
-elim H3.elim H4.
-cut ((S n1) < (f (S a)) \lor (S n1) = (f (S a))).
-elim Hcut.
-apply (ex_intro ? ? a).
-split.apply le_S. assumption.assumption.
-apply (ex_intro ? ? (S a)).
-split.rewrite < H7.apply le_n.
-rewrite > H7.
-apply H.
-apply le_to_or_lt_eq.apply H6.
+theorem increasing_to_le2: ∀f:nat → nat. increasing f →
+ ∀m:nat. f 0 ≤ m → ∃i. f i ≤ m ∧ m < f (S i).
+#f #incr #m #lem (elim lem)
+ [@(ex_intro ? ? O) /2/
+ |#n #len * #a * #len #ltnr (cases(le_to_or_lt_eq … ltnr)) #H
+ [@(ex_intro ? ? a) % /2/
+ |@(ex_intro ? ? (S a)) % //
+ ]
+ ]
+qed.
+
+theorem increasing_to_injective: ∀f:nat → nat.
+ increasing f → injective nat nat f.
+#f #incr #n #m cases(decidable_le n m)
+ [#lenm cases(le_to_or_lt_eq … lenm) //
+ #lenm #eqf @False_ind @(absurd … eqf) @lt_to_not_eq
+ @increasing_to_monotonic //
+ |#nlenm #eqf @False_ind @(absurd … eqf) @sym_not_eq
+ @lt_to_not_eq @increasing_to_monotonic /2/
+ ]
qed.
-*)
(*********************** monotonicity ***************************)
theorem monotonic_le_plus_r:
apply lt_plus.assumption.assumption.
qed. *)
-theorem monotonic_lt_times_l:
- ∀c:nat. O < c → monotonic nat lt (λt.(t*c)).
+theorem monotonic_lt_times_r:
+ ∀c:nat. O < c → monotonic nat lt (λt.(c*t)).
#c #posc #n #m #ltnm
(elim ltnm) normalize
[/2/
]
qed.
-theorem monotonic_lt_times_r:
- ∀c:nat. O < c → monotonic nat lt (λt.(c*t)).
-/2/ qed.
+theorem monotonic_lt_times_l:
+ ∀c:nat. O < c → monotonic nat lt (λt.(t*c)).
+/2/
+qed.
theorem lt_to_le_to_lt_times:
∀n,m,p,q:nat. n < m → p ≤ q → O < q → n*p < m*q.
#n #m #posn #posm @(lt_O_n_elim n posn) @(lt_O_n_elim m posm) //.
qed.
+
(*
theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
[|@le_plus_minus_m_m | @monotonic_le_plus_l // ]
qed.
+theorem le_minus_to_plus_r: ∀a,b,c. c ≤ b → a ≤ b - c → a + c ≤ b.
+#a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2/
+qed.
+
theorem le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p.
#n #m #p #lep /2/ qed.
+theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b.
+#a #b #c #H @(le_plus_to_le_r … b) /2/
+qed.
+
+theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b.
+#a #b #c #H @not_le_to_lt
+@(not_to_not … (lt_to_not_le …H)) /2/
+qed.
+
+theorem lt_minus_to_plus_r: ∀a,b,c. a < b - c → a + c < b.
+#a #b #c #H @not_le_to_lt @(not_to_not … (le_plus_to_minus …))
+@lt_to_not_le //
+qed.
+
+theorem lt_plus_to_minus: ∀n,m,p. m ≤ n → n < p+m → n-m < p.
+#n #m #p #lenm #H normalize <minus_Sn_m // @le_plus_to_minus //
+qed.
+
+theorem lt_plus_to_minus_r: ∀a,b,c. a + b < c → a < c - b.
+#a #b #c #H @le_plus_to_minus_r //
+qed.
+
theorem monotonic_le_minus_r:
∀p,q,n:nat. q ≤ p → n-p ≤ n-q.
#p #q #n #lepq @le_plus_to_minus
theorem distributive_times_minus: distributive ? times minus.
#a #b #c
(cases (decidable_lt b c)) #Hbc
- [>(eq_minus_O …) /2/ >(eq_minus_O …) //
+ [> eq_minus_O /2/ >eq_minus_O //
@monotonic_le_times_r /2/
- |@sym_eq (applyS plus_to_minus) <(distributive_times_plus …)
- (* STRANO *)
- @(eq_f …b) (applyS plus_minus_m_m) /2/
+ |@sym_eq (applyS plus_to_minus) <distributive_times_plus
+ @eq_f (applyS plus_minus_m_m) /2/
+qed.
+
+theorem minus_plus: ∀n,m,p. n-m-p = n -(m+p).
+#n #m #p
+cases (decidable_le (m+p) n) #Hlt
+ [@plus_to_minus @plus_to_minus <associative_plus
+ @minus_to_plus //
+ |cut (n ≤ m+p) [@(transitive_le … (le_n_Sn …)) @not_le_to_lt //]
+ #H >eq_minus_O /2/ >eq_minus_O //
+ ]
+qed.
+
+(*
+theorem plus_minus: ∀n,m,p. p ≤ m → (n+m)-p = n +(m-p).
+#n #m #p #lepm @plus_to_minus >(commutative_plus p)
+>associative_plus <plus_minus_m_m //
+qed. *)
+
+theorem minus_minus: ∀n,m,p:nat. p ≤ m → m ≤ n →
+ p+(n-m) = n-(m-p).
+#n #m #p #lepm #lemn
+@sym_eq @plus_to_minus <associative_plus <plus_minus_m_m //
+<commutative_plus <plus_minus_m_m //
qed.
(*********************** boolean arithmetics ********************)
projects / helm.git / blobdiff