From: Claudio Sacerdoti Coen Date: Sun, 14 Oct 2007 15:56:00 +0000 (+0000) Subject: Some lemmas moves to the file they belong to. X-Git-Tag: 0.4.95@7852~130 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0b69be40774bf7f75c8ed8a75c02998437ebbdbb;p=helm.git Some lemmas moves to the file they belong to. Broken references to renamed errors fixed. --- diff --git a/matita/library/Q/Qaxioms.ma b/matita/library/Q/Qaxioms.ma index 6cf6b6994..da8e9e7a6 100644 --- a/matita/library/Q/Qaxioms.ma +++ b/matita/library/Q/Qaxioms.ma @@ -65,7 +65,7 @@ axiom frac_Qinv1: \forall a,b:nat.Qinv(frac a b) = frac b a. axiom frac_Qinv2: \forall a,b:nat.Qinv(frac (Zopp a) b) = frac (Zopp b) a. definition sigma_Q \def \lambda n,p,f.iter_p_gen n p Q f QO Qplus. - +(* theorem geometric: \forall q.\exists k. Qlt q (sigma_Q k (\lambda x.true) (\lambda x. frac (S O) x)). - \ No newline at end of file +*) \ No newline at end of file diff --git a/matita/library/algebra/finite_groups.ma b/matita/library/algebra/finite_groups.ma index 7f76ae0c8..0c7bd0b64 100644 --- a/matita/library/algebra/finite_groups.ma +++ b/matita/library/algebra/finite_groups.ma @@ -60,140 +60,6 @@ interpretation "Index_of_finite_enumerable representation" (* several definitions/theorems to be moved somewhere else *) -definition ltb ≝λn,m. leb n m ∧ notb (eqb n m). - -theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n (S_pred m); - [ apply le_S_S; - assumption - | assumption - ] -]. -qed. - -theorem le_to_le_pred: - ∀n,m. n ≤ m → pred n ≤ pred m. -intros 2; -elim n; -[ simplify; - apply le_O_n -| simplify; - generalize in match H1; - clear H1; - elim m; - [ elim (not_le_Sn_O ? H1) - | simplify; - apply le_S_S_to_le; - assumption - ] -]. -qed. - -theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n. -intros; -unfold Not; -intro; -unfold lt in H; -unfold lt in H1; -generalize in match (le_S_S ? ? H); -intro; -generalize in match (transitive_le ? ? ? H2 H1); -intro; -apply (not_le_Sn_n ? H3). -qed. - - - -(* moved to nat/order.ma -theorem lt_O_S: ∀n. O < S n. -intro; -unfold lt; -apply le_S_S; -apply le_O_n. -qed. *) - -theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m. -intros; -unfold lt in H1; -generalize in match (le_S_S_to_le ? ? H1); -intro; -apply cic:/matita/nat/orders/antisym_le.con; -assumption. -qed. - theorem pigeonhole: ∀n:nat.∀f:nat→nat. (∀x,y.x≤n → y≤n → f x = f y → x=y) → @@ -307,7 +173,7 @@ elim n; apply (ltb_elim (f (S n1)) (f a)); [ simplify; intros; - generalize in match (lt_S_S ? ? H5); + generalize in match (lt_to_lt_S_S ? ? H5); intro; rewrite < S_pred in H6; [ elim (lt_n_m_to_not_lt_m_Sn ? ? H4 H6) @@ -385,7 +251,8 @@ elim n; [ apply (H1 ? ? ? ? Hcut); apply le_S; assumption - | apply eq_pred_to_eq; + | alias id "eq_pred_to_eq" = "cic:/matita/nat/relevant_equations/eq_pred_to_eq.con". +apply eq_pred_to_eq; [ apply (ltn_to_ltO ? ? H7) | apply (ltn_to_ltO ? ? H6) | assumption diff --git a/matita/library/assembly/byte.ma b/matita/library/assembly/byte.ma index f2d1dc156..2bf233ec1 100644 --- a/matita/library/assembly/byte.ma +++ b/matita/library/assembly/byte.ma @@ -283,9 +283,9 @@ lemma eq_bpred_S_a_a: rewrite > nat_of_exadecimal_exadecimal_of_nat in Hletin1; elim (eq_mod_O_to_exists ? ? Hletin1); clear Hletin1; rewrite > H1; - rewrite > div_times_ltO; [2: autobatch | ] + rewrite > lt_O_to_div_times; [2: autobatch | ] lapply (eq_f ? ? (λx.x/16) ? ? H1); - rewrite > div_times_ltO in Hletin; [2: autobatch | ] + rewrite > lt_O_to_div_times in Hletin; [2: autobatch | ] lapply (eq_f ? ? (λx.x \mod 16) ? ? H1); rewrite > eq_mod_times_n_m_m_O in Hletin1; elim daemon diff --git a/matita/library/assembly/exadecimal.ma b/matita/library/assembly/exadecimal.ma index 761c06c94..c059b43fa 100644 --- a/matita/library/assembly/exadecimal.ma +++ b/matita/library/assembly/exadecimal.ma @@ -768,8 +768,7 @@ lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16. elim b; simplify; [ - |*: alias id "lt_S_S" = "cic:/matita/algebra/finite_groups/lt_S_S.con". - repeat (apply lt_S_S) + |*: repeat (apply lt_to_lt_S_S) ]; autobatch. qed. diff --git a/matita/library/demo/propositional_sequent_calculus.ma b/matita/library/demo/propositional_sequent_calculus.ma index 9bd89394d..4498676a3 100644 --- a/matita/library/demo/propositional_sequent_calculus.ma +++ b/matita/library/demo/propositional_sequent_calculus.ma @@ -157,13 +157,13 @@ inductive derive: sequent → Prop ≝ | NotL: ∀l1,l2,f. derive 〈l1,f::l2〉 → derive 〈FNot f :: l1,l2〉. -alias id "Nil" = "cic:/matita/list/list.ind#xpointer(1/1/1)". let rec and_of_list l ≝ match l with - [ Nil ⇒ FTrue - | Cons F l' ⇒ FAnd F (and_of_list l') + [ nil ⇒ FTrue + | cons F l' ⇒ FAnd F (and_of_list l') ]. +alias id "Nil" = "cic:/matita/list/list.ind#xpointer(1/1/1)". let rec or_of_list l ≝ match l with [ Nil ⇒ FFalse @@ -276,7 +276,6 @@ theorem soundness: ∀F. derive F → is_tautology (formula_of_sequent F). qed. alias num (instance 0) = "natural number". -alias symbol "plus" = "natural plus". let rec size F ≝ match F with [ FTrue ⇒ 0 @@ -289,8 +288,8 @@ let rec size F ≝ let rec sizel l ≝ match l with - [ Nil ⇒ 0 - | Cons F l' ⇒ size F + sizel l' + [ nil ⇒ 0 + | cons F l' ⇒ size F + sizel l' ]. definition size_of_sequent ≝ @@ -311,8 +310,7 @@ definition same_atom : Formula → Formula → bool. qed. definition symmetricb ≝ - λA:Type.λeq:A → A → bool. - ∀x,y. eq x y = eq y x. + λA:Type.λeq:A → A → bool. ∀x,y. eq x y = eq y x. theorem symmetricb_eqb: symmetricb ? eqb. intro; @@ -918,4 +916,3 @@ qed. | apply NotR; simplify in H1; *) -*) diff --git a/matita/library/nat/compare.ma b/matita/library/nat/compare.ma index c701cd2e7..78dc50318 100644 --- a/matita/library/nat/compare.ma +++ b/matita/library/nat/compare.ma @@ -181,6 +181,50 @@ apply ((H1 H2)). qed. *) +definition ltb ≝λn,m. leb n m ∧ notb (eqb n m). + +theorem ltb_to_Prop : + ∀n,m. + match ltb n m with + [ true ⇒ n < m + | false ⇒ n ≮ m + ]. +intros; +unfold ltb; +apply leb_elim; +apply eqb_elim; +intros; +simplify; +[ rewrite < H; + apply le_to_not_lt; + constructor 1 +| apply (not_eq_to_le_to_lt ? ? H H1) +| rewrite < H; + apply le_to_not_lt; + constructor 1 +| apply le_to_not_lt; + generalize in match (not_le_to_lt ? ? H1); + clear H1; + intro; + apply lt_to_le; + assumption +]. +qed. + +theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop. +(n < m → (P true)) → (n ≮ m → (P false)) → +P (ltb n m). +intros. +cut +(match (ltb n m) with +[ true ⇒ n < m +| false ⇒ n ≮ m] → (P (ltb n m))). +apply Hcut.apply ltb_to_Prop. +elim (ltb n m). +apply ((H H2)). +apply ((H1 H2)). +qed. + let rec nat_compare n m: compare \def match n with [ O \Rightarrow @@ -203,11 +247,6 @@ nat_compare n m = nat_compare (S n) (S m). intros.simplify.reflexivity. 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 nat_compare_pred_pred: \forall n,m:nat.lt O n \to lt O m \to eq compare (nat_compare n m) (nat_compare (pred n) (pred m)). diff --git a/matita/library/nat/ord.ma b/matita/library/nat/ord.ma index 5895b3bcd..340e33a86 100644 --- a/matita/library/nat/ord.ma +++ b/matita/library/nat/ord.ma @@ -166,8 +166,7 @@ apply p_ord_exp apply le_times_l. assumption. apply le_times_r.assumption. -alias id "not_eq_to_le_to_lt" = "cic:/matita/algebra/finite_groups/not_eq_to_le_to_lt.con". -apply not_eq_to_le_to_lt. + apply not_eq_to_le_to_lt. unfold.intro.apply H1. rewrite < H3. apply (witness ? r r ?).simplify.apply plus_n_O. @@ -456,4 +455,4 @@ theorem mod_p_ord_inv: intros.rewrite > eq_p_ord_inv. apply mod_plus_times. assumption. -qed. \ No newline at end of file +qed. diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma index 42454393c..caecbe063 100644 --- a/matita/library/nat/orders.ma +++ b/matita/library/nat/orders.ma @@ -130,6 +130,43 @@ apply nat_elim2 ] 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; +elim n; +[ apply le_O_n +| simplify in H2; + rewrite > (S_pred m); + [ apply le_S_S; + assumption + | assumption + ] +]. +qed. + +theorem le_to_le_pred: + ∀n,m. n ≤ m → pred n ≤ pred m. +intros 2; +elim n; +[ simplify; + apply le_O_n +| simplify; + generalize in match H1; + clear H1; + elim m; + [ elim (not_le_Sn_O ? H1) + | simplify; + apply le_S_S_to_le; + assumption + ] +]. +qed. + (* le to lt or eq *) theorem le_to_or_lt_eq : \forall n,m:nat. n \leq m \to n < m \lor n = m. @@ -138,6 +175,14 @@ right.reflexivity. left.unfold lt.apply le_S_S.assumption. qed. +theorem Not_lt_n_n: ∀n. n ≮ n. +intro; +unfold Not; +intro; +unfold lt in H; +apply (not_le_Sn_n ? H). +qed. + (* not eq *) theorem lt_to_not_eq : \forall n,m:nat. n distr_times_plus. rewrite > distr_times_plus. rewrite < assoc_plus.reflexivity. qed. + +theorem eq_pred_to_eq: + ∀n,m. O < n → O < m → pred n = pred m → n = m. +intros; +generalize in match (eq_f ? ? S ? ? H2); +intro; +rewrite < S_pred in H3; +rewrite < S_pred in H3; +assumption. +qed.