include "algebra/groups.ma".
-record finite_enumerable (T:Type) : Type ≝
+record finite_enumerable (T:Type) : Type≝
{ order: nat;
repr: nat → T;
index_of: T → nat;
interpretation "Finite_enumerable order" 'card C =
(cic:/matita/algebra/finite_groups/order.con C _).
-record finite_enumerable_SemiGroup : Type ≝
+record finite_enumerable_SemiGroup : Type≝
{ semigroup:> SemiGroup;
is_finite_enumerable:> finite_enumerable semigroup
}.
(* 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<m.
-intros;
-elim (le_to_or_lt_eq ? ? H1);
-[ assumption
-| elim (H H2)
-].
-qed.
-
-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.
-
-theorem Not_lt_n_n: ∀n. n ≮ n.
-intro;
-unfold Not;
-intro;
-unfold lt in H;
-apply (not_le_Sn_n ? H).
-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.
-
-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.
-
-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.
-
-theorem lt_S_S: ∀n,m. n < m → S n < S m.
-intros;
-unfold lt in H;
-apply (le_S_S ? ? H).
-qed.
-
-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) →
| clear n;
letin f' ≝
(λx.
- let fSn1 ≝ f (S n1) in
- let fx ≝ f x in
+ let fSn1 ≝f (S n1) in
+ let fx ≝f x in
match ltb fSn1 fx with
[ true ⇒ pred fx
| false ⇒ fx
[ simplify in H5;
clear Hcut;
clear Hcut1;
+ unfold f' in H5;
clear f';
elim H5;
clear H5;
[ simplify in H5;
clear Hcut;
clear Hcut1;
+ unfold f' in H5;
clear f';
elim H5;
clear H5;
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)
[ 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
]
].
qed.
-
+(* demo *)
theorem finite_enumerable_SemiGroup_to_left_cancellable_to_right_cancellable_to_isMonoid:
∀G:finite_enumerable_SemiGroup.
left_cancellable ? (op G) →
right_cancellable ? (op G) →
∃e:G. isMonoid (mk_PreMonoid G e).
intros;
-letin f ≝ (λn.ι(G \sub O · G \sub n));
+letin f ≝(λn.ι(G \sub O · G \sub n));
cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
-[ letin EX ≝ (Hcut O ?);
+[ letin EX ≝(Hcut O ?);
[ apply le_O_n
| clearbody EX;
clear Hcut;
unfold f in EX;
elim EX;
clear EX;
- letin HH ≝ (eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
+ letin HH ≝(eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
clearbody HH;
rewrite > (repr_index_of ? (is_finite_enumerable G)) in HH;
apply (ex_intro ? ? (G \sub a));
- letin GOGO ≝ (refl_eq ? (repr ? (is_finite_enumerable G) O));
+ letin GOGO ≝(refl_eq ? (repr ? (is_finite_enumerable G) O));
clearbody GOGO;
rewrite < HH in GOGO;
rewrite < HH in GOGO:(? ? % ?);
rewrite > (op_associative ? G) in GOGO;
- letin GaGa ≝ (H ? ? ? GOGO);
+ letin GaGa ≝(H ? ? ? GOGO);
clearbody GaGa;
clear GOGO;
constructor 1;
[ simplify;
apply (semigroup_properties G)
| unfold is_left_unit; intro;
- letin GaxGax ≝ (refl_eq ? (G \sub a ·x));
- clearbody GaxGax;
+ letin GaxGax ≝(refl_eq ? (G \sub a ·x));
+ clearbody GaxGax; (* demo *)
rewrite < GaGa in GaxGax:(? ? % ?);
rewrite > (op_associative ? (semigroup_properties G)) in GaxGax;
apply (H ? ? ? GaxGax)
| unfold is_right_unit; intro;
- letin GaxGax ≝ (refl_eq ? (x·G \sub a));
+ letin GaxGax ≝(refl_eq ? (x·G \sub a));
clearbody GaxGax;
rewrite < GaGa in GaxGax:(? ? % ?);
rewrite < (op_associative ? (semigroup_properties G)) in GaxGax;
assumption
]
| intros;
+ unfold f;
apply index_of_sur
]
].
projects / helm.git / blobdiff