--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "logic/pts.ma".
+
+ninductive bool: Type[0] ≝
+ true: bool
+ | false: bool.
\ No newline at end of file
sets/sets.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma
logic/cprop.ma sets/setoids1.ma
+datatypes/bool.ma logic/pts.ma
sets/setoids1.ma properties/relations1.ma sets/setoids.ma
sets/setoids.ma logic/connectives.ma properties/relations.ma
logic/equality.ma logic/connectives.ma properties/relations.ma
logic/connectives.ma logic/pts.ma
algebra/abelian_magmas.ma algebra/magmas.ma
-nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/nat.ma
+nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma
+nat/minus.ma nat/order.ma
algebra/magmas.ma sets/sets.ma
nat/nat.ma logic/equality.ma sets/setoids.ma
+nat/big_ops.ma algebra/magmas.ma nat/order.ma
properties/relations1.ma logic/pts.ma
+nat/compare.ma datatypes/bool.ma nat/order.ma
properties/relations.ma logic/pts.ma
+nat/order.ma nat/nat.ma
algebra/unital_magmas.ma algebra/magmas.ma
logic/pts.ma
+sets/partitions.ma nat/compare.ma nat/minus.ma nat/plus.ma sets/sets.ma
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "nat/order.ma".
+include "algebra/magmas.ma".
+
+alias symbol "eq" = "leibnitz's equality".
+alias id "refl" = "cic:/matita/ng/logic/equality/eq.con(0,1,2)".
+nlet rec big_op (M: magma_type) (n: nat) (f: ∀m. lt m n → M) (v: M) on n : M ≝
+ (match n return λx.∀p:n=x.? with
+ [ O ⇒ λ_.v
+ | S n' ⇒ λp.op ? (f n' ?) (big_op M n' ? v) ]) (refl ? n).
+##[ nrewrite > p; napply le_n
+ | #m; #H; napply (f n'); nrewrite > p; napply le_n]
+nqed.
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "nat/order.ma".
+include "datatypes/bool.ma".
+
+naxiom decompose1: ¬(lt O O).
+naxiom decompose2: ∀n. ¬(lt (S n) O).
+
+ndefinition ltb: ∀n,m:nat. lt n m ∨ ¬(lt n m).
+ #n; nelim n
+ [ #m; ncases m
+ [ napply or_intror; #H; napply (decompose1 H)
+ | #m'; napply or_introl; napply lt_O_Sn ]
+##| #n'; #Hn'; #m; ncases m
+ [ napply or_intror; #H; napply (decompose2 … H)
+ | #m'; ncases (Hn' m')
+ [ #H; napply or_introl; napply le_S_S; napply H
+ | #H; napply or_intror; #K; napply H; napply le_S_S_to_le; napply K]##]
+nqed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "nat/order.ma".
+
+nlet rec minus (n:nat) (m:nat) on m : nat ≝
+ match m with
+ [ O ⇒ n
+ | S m' ⇒
+ match n with
+ [ O ⇒ O
+ | S n' ⇒ minus n' m']].
+
+naxiom le_minus: ∀n,m,p. le n m → le (minus n p) m.
+naxiom lt_minus: ∀n,m,p. lt n m → lt (minus n p) m.
\ No newline at end of file
napply mk_setoid [ napply nat | napply EQ]
nqed.
-unification hint 0 ((λx,y.True) (carr NAT) nat).
\ No newline at end of file
+unification hint 0 ((λx,y.True) (carr NAT) nat).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "nat/nat.ma".
+
+ninductive le (n: nat) : nat → CProp[0] ≝
+ le_n: le n n
+ | le_S: ∀m. le n m → le n (S m).
+
+ndefinition lt ≝ λn,m. le (S n) m.
+
+nlemma le_O_n: ∀n. le O n.
+ #n; nelim n [ napply le_n | #n'; #H; napply le_S; nassumption ]
+nqed.
+
+(* needs decompose *)
+naxiom le_S_S: ∀n,m. le n m → le (S n) (S m).
+naxiom le_S_S_to_le: ∀n,m. le (S n) (S m) → le n m.
+naxiom lt_Sn_m: ∀n,m. lt (S n) m → lt n m.
+
+nlemma lt_O_Sn: ∀n. lt O (S n).
+ #n; napply le_S_S; napply le_O_n.
+nqed.
(* *)
(**************************************************************************)
-include "nat/nat.ma".
+include "nat/big_ops.ma".
include "algebra/unital_magmas.ma".
include "algebra/abelian_magmas.ma".
| napply O
| #x; napply refl
| #x; (* qua manca ancora l'hint *) napply (symm plus_abelian_magma_type) ]
-nqed.
\ No newline at end of file
+nqed.
+
+ndefinition big_plus ≝ λn.λf.big_op plus_magma_type n f O.
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "sets/sets.ma".
+include "nat/plus.ma".
+include "nat/compare.ma".
+include "nat/minus.ma".
+
+(* sbaglia a fare le proiezioni *)
+nrecord finite_partition (A: Type[0]) : Type[1] ≝
+ { card: nat;
+ class: ∀n. lt n card → Ω \sup A;
+ inhabited: ∀i,p. class i p ≬ class i p(*;
+ disjoint: ∀i,j,p,p'. class i p ≬ class j p' → i=j;
+ covers: big_union ?? class = full_set A*)
+ }.
+
+nrecord has_card (A: Type[0]) (S: Ω \sup A) (n: nat) : CProp[0] ≝
+ { f: ∀m:nat. lt m n → A;
+ in_S: ∀m.∀p:lt m n. f ? p ∈ S (*;
+ f_inj: injective ?? f;
+ f_sur: surjective ?? f*)
+ }.
+
+(*
+nlemma subset_of_finite:
+ ∀A. ∃n. has_card ? (full_subset A) n → ∀S. ∃m. has_card ? S m.
+nqed.
+*)
+
+nlet rec partition_splits_card_map
+ A (P: finite_partition A) (s: ∀i. lt i (card ? P) → nat)
+ (H:∀i.∀p: lt i (card ? P). has_card ? (class ? P i p) (s i p))
+ m (H1: lt m (big_plus ? s)) index (p: lt index (card ? P)) on index : A ≝
+ match index return λx. lt x (card ? P) → ? with
+ [ O ⇒ λp'.f ??? (H O p') m ?
+ | S index' ⇒ λp'.
+ match ltb m (s index p) with
+ [ or_introl K ⇒ f ??? (H index p) m K
+ | or_intror _ ⇒ partition_splits_card_map A P s H (minus m (s index p)) ? index' ? ]] p.
+##[##2: napply lt_minus; nassumption
+ |##3: napply lt_Sn_m; nassumption
+ |
+nqed.
+
+nlemma partition_splits_card:
+ ∀A. ∀P: finite_partition A. ∀s: ∀i. lt i (card ? P) → nat.
+ (∀i.∀p: lt i (card ? P). has_card ? (class ? P i p) (s i p)) →
+ has_card A (full_set A) (big_plus (card ? P) s).
+ #A; #P; #s; #H; napply mk_has_card
+ [ #m; #H1; napply partition_splits_card_map A P s H m H1 (pred (card ? P))
+ |
+ ]
+nqed.
\ No newline at end of file
∀A,B.∀f: unary_morphism A B. injective ?? (quotiented_mor ?? f).
#A; #B; #f; nwhd; #x; #x'; #H; nassumption.
nqed.
-
-(************************** partitions ****************************)
-
-nrecord partition (A: Type[0]) : Type[1] ≝
- { index_set: setoid;
- class: index_set → Ω \sup A;
- disjoint: ∀i,j. ¬ (i = j) → ¬(class i ≬ class j);
- covers: big_union ?? class = full_set A
- }.
-
-(*
-nrecord has_card (A: Type[0]) (S: Ω \sup A) (n: nat) : Prop ≝
- { f: ∀m:nat. m < n → S;
- f_inj: injective ?? f;
- f_sur: surjective ?? f
- }.
-
-nlemma subset_of_finite:
- ∀A. ∃n. has_card ? (full_subset A) n → ∀S. ∃m. has_card ? S m.
-nqed.
-
-nlemma partition_splits_card:
- ∀A. ∀P: partition A. ∀s: index_set P → nat.
- (∀i. has_card ? (class i) = s i) →
- has_card ? (full_subset A) (big_plus ? (λi. s i)).
-nqed.
-*)
\ No newline at end of file
projects / helm.git / commitdiff