bs_cotransitive: cotransitive ? bs_apart
}.
-notation "hvbox(a break # b)" non associative with precedence 45
- for @{ 'apart $a $b}.
-
interpretation "bishop set apartness" 'apart x y = (bs_apart _ x y).
definition bishop_set_of_ordered_set: ordered_set → bishop_set.
(* Definition 2.2 (2) *)
definition eq ≝ λA:bishop_set.λa,b:A. ¬ (a # b).
-notation "hvbox(a break \approx b)" non associative with precedence 45
- for @{ 'napart $a $b}.
-
interpretation "Bishop set alikeness" 'napart a b = (eq _ a b).
lemma eq_reflexive:∀E:bishop_set. reflexive ? (eq E).
definition bs_subset ≝ λO:bishop_set.λP,Q:O→Prop.∀x:O.P x → Q x.
-interpretation "bishop set subset" 'subset a b = (bs_subset _ a b).
+interpretation "bishop set subset" 'subseteq a b = (bs_subset _ a b).
definition square_bishop_set : bishop_set → bishop_set.
intro S; apply (mk_bishop_set (S × S));
+++ /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/equality.ma".
-include "datatypes/constructors.ma".
-
-inductive Or (A,B:CProp) : CProp ≝
- | Left : A → Or A B
- | Right : B → Or A B.
-
-interpretation "constructive or" 'or x y = (Or x y).
-
-inductive Or3 (A,B,C:CProp) : CProp ≝
- | Left3 : A → Or3 A B C
- | Middle3 : B → Or3 A B C
- | Right3 : C → Or3 A B C.
-
-interpretation "constructive ternary or" 'or3 x y z= (Or3 x y z).
-
-notation < "hvbox(a break ∨ b break ∨ c)" with precedence 35 for @{'or3 $a $b $c}.
-
-inductive Or4 (A,B,C,D:CProp) : CProp ≝
- | Left3 : A → Or4 A B C D
- | Middle3 : B → Or4 A B C D
- | Right3 : C → Or4 A B C D
- | Extra3: D → Or4 A B C D.
-
-interpretation "constructive ternary or" 'or4 x y z t = (Or4 x y z t).
-
-notation < "hvbox(a break ∨ b break ∨ c break ∨ d)" with precedence 35 for @{'or4 $a $b $c $d}.
-
-inductive And (A,B:CProp) : CProp ≝
- | Conj : A → B → And A B.
-
-interpretation "constructive and" 'and x y = (And x y).
-
-inductive And3 (A,B,C:CProp) : CProp ≝
- | Conj3 : A → B → C → And3 A B C.
-
-notation < "hvbox(a break ∧ b break ∧ c)" with precedence 35 for @{'and3 $a $b $c}.
-
-interpretation "constructive ternary and" 'and3 x y z = (And3 x y z).
-
-inductive And4 (A,B,C,D:CProp) : CProp ≝
- | Conj4 : A → B → C → D → And4 A B C D.
-
-notation < "hvbox(a break ∧ b break ∧ c break ∧ d)" with precedence 35 for @{'and4 $a $b $c $d}.
-
-interpretation "constructive quaternary and" 'and4 x y z t = (And4 x y z t).
-
-inductive exT (A:Type) (P:A→CProp) : CProp ≝
- ex_introT: ∀w:A. P w → exT A P.
-
-notation "\ll term 19 a, break term 19 b \gg"
-with precedence 90 for @{'dependent_pair $a $b}.
-interpretation "dependent pair" 'dependent_pair a b =
- (ex_introT _ _ a b).
-
-interpretation "CProp exists" 'exists \eta.x = (exT _ x).
-
-notation "\ll term 19 a, break term 19 b \gg"
-with precedence 90 for @{'dependent_pair $a $b}.
-interpretation "dependent pair" 'dependent_pair a b =
- (ex_introT _ _ a b).
-
-
-definition pi1exT ≝ λA,P.λx:exT A P.match x with [ex_introT x _ ⇒ x].
-definition pi2exT ≝
- λA,P.λx:exT A P.match x return λx.P (pi1exT ?? x) with [ex_introT _ p ⇒ p].
-
-interpretation "exT \fst" 'pi1 = (pi1exT _ _).
-interpretation "exT \fst" 'pi1a x = (pi1exT _ _ x).
-interpretation "exT \fst" 'pi1b x y = (pi1exT _ _ x y).
-interpretation "exT \snd" 'pi2 = (pi2exT _ _).
-interpretation "exT \snd" 'pi2a x = (pi2exT _ _ x).
-interpretation "exT \snd" 'pi2b x y = (pi2exT _ _ x y).
-
-inductive exT23 (A:Type) (P:A→CProp) (Q:A→CProp) (R:A→A→CProp) : CProp ≝
- ex_introT23: ∀w,p:A. P w → Q p → R w p → exT23 A P Q R.
-
-definition pi1exT23 ≝
- λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 x _ _ _ _ ⇒ x].
-definition pi2exT23 ≝
- λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 _ x _ _ _ ⇒ x].
-
-interpretation "exT2 \fst" 'pi1 = (pi1exT23 _ _ _ _).
-interpretation "exT2 \snd" 'pi2 = (pi2exT23 _ _ _ _).
-interpretation "exT2 \fst" 'pi1a x = (pi1exT23 _ _ _ _ x).
-interpretation "exT2 \snd" 'pi2a x = (pi2exT23 _ _ _ _ x).
-interpretation "exT2 \fst" 'pi1b x y = (pi1exT23 _ _ _ _ x y).
-interpretation "exT2 \snd" 'pi2b x y = (pi2exT23 _ _ _ _ x y).
-
-definition Not : CProp → Prop ≝ λx:CProp.x → False.
-
-interpretation "constructive not" 'not x = (Not x).
-
-definition cotransitive ≝
- λC:Type.λlt:C→C→CProp.∀x,y,z:C. lt x y → lt x z ∨ lt z y.
-
-definition coreflexive ≝ λC:Type.λlt:C→C→CProp. ∀x:C. ¬ (lt x x).
-
-definition symmetric ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x.
-
-definition antisymmetric ≝ λA:Type.λR:A→A→CProp.λeq:A→A→Prop.∀x:A.∀y:A.R x y→R y x→eq x y.
-
-definition reflexive ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
-
-definition transitive ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z.
-
ordered_uniform.ma uniform.ma
-cprop_connectives.ma datatypes/constructors.ma logic/equality.ma
-russell_support.ma cprop_connectives.ma nat/nat.ma
+russell_support.ma logic/cprop_connectives.ma nat/nat.ma
lebesgue.ma property_exhaustivity.ma sandwich.ma
-ordered_set.ma cprop_connectives.ma
+ordered_set.ma logic/cprop_connectives.ma
bishop_set.ma ordered_set.ma
bishop_set_rewrite.ma bishop_set.ma
sandwich.ma ordered_uniform.ma
models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma
models/q_function.ma Q/q/qtimes.ma models/q_bars.ma
models/discrete_uniformity.ma bishop_set_rewrite.ma uniform.ma
-models/list_support.ma cprop_connectives.ma list/list.ma nat/le_arith.ma nat/minus.ma
-models/q_bars.ma cprop_connectives.ma models/list_support.ma models/q_support.ma nat_ordered_set.ma
-models/q_support.ma Q/q/qplus.ma Q/q/qtimes.ma cprop_connectives.ma
+models/list_support.ma list/list.ma logic/cprop_connectives.ma nat/le_arith.ma nat/minus.ma
+models/q_bars.ma logic/cprop_connectives.ma models/list_support.ma models/q_support.ma nat_ordered_set.ma
+models/q_support.ma Q/q/qplus.ma Q/q/qtimes.ma logic/cprop_connectives.ma
models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma
models/q_shift.ma
models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma
Q/q/qtimes.ma
datatypes/constructors.ma
list/list.ma
-logic/equality.ma
+logic/cprop_connectives.ma
nat/compare.ma
nat/le_arith.ma
nat/minus.ma
|1: rewrite < H2; rewrite > len_append; rewrite > plus_n_SO; reflexivity]]]
qed.
-include "cprop_connectives.ma".
+include "logic/cprop_connectives.ma".
definition eject_N ≝
λP.λp:∃x:nat.P x.match p with [ex_introT p _ ⇒ p].
lemma nat_dedekind_sigma_complete:
∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing →
∀x.x is_supremum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).
-intros 5; cases x (s Hs); clear x; letin X ≝ (〈s,Hs〉);
+intros 5; cases x (s Hs); clear x; letin X ≝ ≪s,Hs≫;
fold normalize X; intros; cases H1;
alias symbol "plus" = "natural plus".
-alias symbol "nat" = "Uniform space N".
+alias symbol "N" = "Uniform space N".
alias symbol "and" = "logical and".
letin spec ≝ (λi,j:ℕ.(u≤i ∧ s = \fst (a j)) ∨ (i < u ∧ s+i ≤ u + \fst (a j)));
(* s - aj <= max 0 (u - i) *)
alias symbol "pi1" = "exT \fst".
alias symbol "leq" = "natural 'less or equal to'".
-alias symbol "nat" = "ordered set N".
+alias symbol "N" = "ordered set N".
axiom nat_dedekind_sigma_complete_r:
∀l,u:ℕ.∀a:sequence {[l,u]}.a is_decreasing →
∀x.x is_infimum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).
|2: apply (le_transitive ????? H5); apply (Le≫ (\snd p) H13); assumption;]
qed.
-interpretation "Ordered uniform space N" 'nat = nat_ordered_uniform_space.
+interpretation "Ordered uniform space N" 'N = nat_ordered_uniform_space.
apply (discrete_uniform_space_of_bishop_set ℕ);
qed.
-interpretation "Uniform space N" 'nat = nat_uniform_space.
\ No newline at end of file
+interpretation "Uniform space N" 'N = nat_uniform_space.
\ No newline at end of file
include "nat_ordered_set.ma".
include "models/q_support.ma".
include "models/list_support.ma".
-include "cprop_connectives.ma".
+include "logic/cprop_connectives.ma".
definition bar ≝ ℚ × (ℚ × ℚ).
include "Q/q/qtimes.ma".
include "Q/q/qplus.ma".
-include "cprop_connectives.ma".
+include "logic/cprop_connectives.ma".
-notation "\rationals" non associative with precedence 99 for @{'q}.
-interpretation "Q" 'q = Q.
+interpretation "Q" 'Q = Q.
(* group over Q *)
axiom qp : ℚ → ℚ → ℚ.
|2: apply nat_excess_cotransitive]
qed.
-notation "\naturals" non associative with precedence 90 for @{'nat}.
-interpretation "ordered set N" 'nat = nat_ordered_set.
+interpretation "ordered set N" 'N = nat_ordered_set.
alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)".
lemma os_le_to_nat_le:
(* *)
(**************************************************************************)
-include "cprop_connectives.ma".
+include "logic/cprop_connectives.ma".
(* Definition 2.1 *)
record ordered_set: Type ≝ {
definition os_subset ≝ λO:ordered_set.λP,Q:O→Prop.∀x:O.P x → Q x.
-notation "a \subseteq u" left associative with precedence 70
- for @{ 'subset $a $u }.
-interpretation "ordered set subset" 'subset a b = (os_subset _ a b).
+interpretation "ordered set subset" 'subseteq a b = (os_subset _ a b).
∀O:ordered_uniform_space.∀l,r:O.
∀U:{[l,r]} square → Prop.∀u:O square → Prop.
restriction_agreement ? l r U u →
- restriction_agreement ? l r (inv U) (inv u).
+ restriction_agreement ? l r (\inv U) (\inv u).
intros 9; split; intro;
[1: apply (unrestrict ????? (segment_square_of_ordered_set_square ??? 〈\snd b,\fst b〉 H2 H1) H H3);
|2: apply (restrict ????? (segment_square_of_ordered_set_square ??? 〈\snd b,\fst b〉 H2 H1) H H3);]
∀O:ordered_set.∀u,v:O.{[u,v]} square → (bishop_set_of_ordered_set O) square ≝
λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈\fst(\fst b),\fst(\snd b)〉.
+(*
notation < "x \sub \neq" with precedence 91 for @{'bsss $x}.
interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x).
+*)
lemma ss_of_bs:
∀O:ordered_set.∀u,v:O.
λO:ordered_set.λu,v:O.
λb:(O:bishop_set) square.λH1,H2.〈≪\fst b,H1≫,≪\snd b,H2≫〉.
+(*
notation < "x \sub \nleq" with precedence 91 for @{'ssbs $x}.
interpretation "ss_of_bs" 'ssbs x = (ss_of_bs _ _ _ x _ _).
+*)
lemma segment_ordered_uniform_space:
∀O:ordered_uniform_space.∀u,v:O.ordered_uniform_space.
(**************************************************************************)
include "nat/nat.ma".
-include "cprop_connectives.ma".
+include "logic/cprop_connectives.ma".
definition hide ≝ λT:Type.λx:T.x.
definition strictly_decreasing ≝
λC:ordered_set.λa:sequence C.∀n:nat.a n ≰ a (S n).
-notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 50
+notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 45
for @{'strictly_increasing $s}.
-notation > "s 'is_strictly_increasing'" non associative with precedence 50
+notation > "s 'is_strictly_increasing'" non associative with precedence 45
for @{'strictly_increasing $s}.
interpretation "Ordered set strict increasing" 'strictly_increasing s =
(strictly_increasing _ s).
-notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 50
+notation < "s \nbsp 'is_strictly_decreasing'" non associative with precedence 45
for @{'strictly_decreasing $s}.
-notation > "s 'is_strictly_decreasing'" non associative with precedence 50
+notation > "s 'is_strictly_decreasing'" non associative with precedence 45
for @{'strictly_decreasing $s}.
interpretation "Ordered set strict decreasing" 'strictly_decreasing s =
(strictly_decreasing _ s).
(* Definition 2.8 *)
definition segment ≝ λO:ordered_set.λa,b:O.λx:O.(x ≤ b) ∧ (a ≤ x).
-notation "[a,b]" left associative with precedence 70 for @{'segment $a $b}.
+notation "[term 19 a,term 19 b]" non associative with precedence 90 for @{'segment $a $b}.
interpretation "Ordered set sergment" 'segment a b = (segment _ a b).
-notation "hvbox(x \in break [a,b])" non associative with precedence 45
+notation "hvbox(x \in break [term 19 a, term 19 b])" non associative with precedence 45
for @{'segment_in $a $b $x}.
interpretation "Ordered set sergment in" 'segment_in a b x= (segment _ a b x).
include "supremum.ma".
-
(* Definition 2.13 *)
alias symbol "square" = "bishop set square".
alias symbol "pair" = "Pair construction".
definition invert_bs_relation ≝
λC:bishop_set.λU:C square → Prop.
λx:C square. U 〈\snd x,\fst x〉.
-
-notation < "s \sup (-1)" with precedence 70 for @{ 'invert $s }.
-notation < "s \sup (-1) x" with precedence 70
- for @{ 'invert_appl $s $x}.
-notation > "'inv'" with precedence 70 for @{ 'invert_symbol }.
+
+notation > "\inv" with precedence 60 for @{ 'invert_symbol }.
interpretation "relation invertion" 'invert a = (invert_bs_relation _ a).
interpretation "relation invertion" 'invert_symbol = (invert_bs_relation _).
interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation _ a x).
∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ (λx.U x ∧ V x));
us_phi3: ∀U:us_carr square → Prop. us_unifbase U →
∃W:us_carr square → Prop.us_unifbase W ∧ (W ∘ W) ⊆ U;
- us_phi4: ∀U:us_carr square → Prop. us_unifbase U → ∀x.(U x → (inv U) x) ∧ ((inv U) x → U x)
+ us_phi4: ∀U:us_carr square → Prop. us_unifbase U → ∀x.(U x → (\inv U) x) ∧ ((\inv U) x → U x)
}.
(* Definition 2.14 *)
λC:uniform_space.λa:sequence C.∀U.us_unifbase C U →
∃n. ∀i,j. n ≤ i → n ≤ j → U 〈a i,a j〉.
-notation < "a \nbsp 'is_cauchy'" non associative with precedence 50
+notation < "a \nbsp 'is_cauchy'" non associative with precedence 45
for @{'cauchy $a}.
-notation > "a 'is_cauchy'" non associative with precedence 50
+notation > "a 'is_cauchy'" non associative with precedence 45
for @{'cauchy $a}.
interpretation "Cauchy sequence" 'cauchy s = (cauchy _ s).
λC:uniform_space.λa:sequence C.λu:C.
∀U.us_unifbase C U → ∃n. ∀i. n ≤ i → U 〈u,a i〉.
-notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50
+notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45
for @{'uniform_converge $a $x}.
-notation > "a 'uniform_converges' x" non associative with precedence 50
+notation > "a 'uniform_converges' x" non associative with precedence 45
for @{'uniform_converge $a $x}.
interpretation "Uniform convergence" 'uniform_converge s u =
(uniform_converge _ s u).
left associative with precedence 55
for @{ 'times $a $b }.
+notation "hvbox(a break \middot b)"
+ left associative with precedence 55
+ for @{ 'middot $a $b }.
+
notation "hvbox(a break \mod b)"
left associative with precedence 55
for @{ 'module $a $b }.
non associative with precedence 80
for @{ 'fact $a }.
-notation "(a \sup b)"
- right associative with precedence 65
-for @{ 'exp $a $b}.
-
notation "\sqrt a"
non associative with precedence 60
for @{ 'sqrt $a }.
notation "hvbox(\lnot a)"
non associative with precedence 40
for @{ 'not $a }.
+
+notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 70
+for @{ 'powerset $A }.
+
+notation < "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i}. $p)}.
+
+notation "hvbox(a break ∈ b)" non associative with precedence 45
+for @{ 'mem $a $b }.
+
+notation "hvbox(a break ≬ b)" non associative with precedence 45
+for @{ 'overlaps $a $b }. (* \between *)
+
+notation "hvbox(a break ⊆ b)" non associative with precedence 45
+for @{ 'subseteq $a $b }. (* \subseteq *)
+
+notation "hvbox(a break ∩ b)" non associative with precedence 55
+for @{ 'intersects $a $b }. (* \cap *)
+
+notation "hvbox(a break ∪ b)" non associative with precedence 50
+for @{ 'union $a $b }. (* \cup *)
+
+notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
+
+notation "hvbox(a break \approx b)" non associative with precedence 45
+ for @{ 'napart $a $b}.
+
+notation "hvbox(a break # b)" non associative with precedence 45
+ for @{ 'apart $a $b}.
+
+notation "hvbox(a break \circ b)"
+ left associative with precedence 55
+for @{ 'compose $a $b }.
+
+notation "(a \sup b)" left associative with precedence 60 for @{ 'exp $a $b}.
+notation "s \sup (-1)" with precedence 60 for @{ 'invert $s }.
+notation < "s \sup (-1) x" with precedence 60 for @{ 'invert_appl $s $x}.
+
+
+notation "\naturals" non associative with precedence 90 for @{'N}.
+notation "\rationals" non associative with precedence 90 for @{'Q}.
+notation "\reals" non associative with precedence 90 for @{'R}.
+notation "\integers" non associative with precedence 90 for @{'Z}.
+notation "\complexes" non associative with precedence 90 for @{'C}.
+
+notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
group_properties:> isGroup pregroup
}.
-notation "hvbox(x \sup (-1))" with precedence 89
-for @{ 'ginv $x }.
-
-interpretation "Group inverse" 'ginv x =
- (cic:/matita/algebra/groups/inv.con _ x).
+interpretation "Group inverse" 'invert x = (inv _ x).
definition left_cancellable ≝
λT:Type. λop: T -> T -> T.
qed.
theorem eq_opxy_e_to_eq_x_invy:
- ∀G:Group. ∀x,y:G. x·y=1 → x=y \sup -1.
+ ∀G:Group. ∀x,y:G. x·y=ⅇ → x=y \sup -1.
intros;
apply (eq_op_x_y_op_z_y_to_eq ? y);
rewrite > (inv_is_left_inverse ? G);
qed.
theorem eq_opxy_e_to_eq_invx_y:
- ∀G:Group. ∀x,y:G. x·y=1 → x \sup -1=y.
+ ∀G:Group. ∀x,y:G. x·y=ⅇ → x \sup -1=y.
intros;
apply (eq_op_x_y_op_x_z_to_eq ? x);
rewrite > (inv_is_right_inverse ? G);
(* Morphisms *)
record morphism (G,G':Group) : Type ≝
- { image: G → G';
+ { image:1> G → G';
f_morph: ∀x,y:G.image(x·y) = image x · image y
}.
-notation "hvbox(f\tilde x)" with precedence 79
-for @{ 'morimage $f $x }.
-
-interpretation "Morphism image" 'morimage f x =
- (cic:/matita/algebra/groups/image.con _ _ f x).
-
theorem morphism_to_eq_f_1_1:
- ∀G,G'.∀f:morphism G G'.f˜1 = 1.
+ ∀G,G'.∀f:morphism G G'.f ⅇ = ⅇ.
intros;
-apply (eq_op_x_y_op_z_y_to_eq ? (f˜1));
+apply (eq_op_x_y_op_z_y_to_eq ? (f ⅇ));
rewrite > (e_is_left_unit ? G');
rewrite < f_morph;
rewrite > (e_is_left_unit ? G);
theorem eq_image_inv_inv_image:
∀G,G'.∀f:morphism G G'.
- ∀x.f˜(x \sup -1) = (f˜x) \sup -1.
+ ∀x.f (x \sup -1) = (f x) \sup -1.
intros;
-apply (eq_op_x_y_op_z_y_to_eq ? (f˜x));
+apply (eq_op_x_y_op_z_y_to_eq ? (f x));
rewrite > (inv_is_left_inverse ? G');
rewrite < f_morph;
rewrite > (inv_is_left_inverse ? G);
monoid_properties:> isMonoid premonoid
}.
-notation "1" with precedence 89
-for @{ 'munit }.
-
-interpretation "Monoid unit" 'munit =
- (cic:/matita/algebra/monoids/e.con _).
+interpretation "Monoid unit" 'neutral = (e _).
definition is_left_inverse ≝
λM:Monoid.
λopp: M → M.
- ∀x:M. (opp x)·x = 1.
+ ∀x:M. (opp x)·x = ⅇ.
definition is_right_inverse ≝
λM:Monoid.
λopp: M → M.
- ∀x:M. x·(opp x) = 1.
+ ∀x:M. x·(opp x) = ⅇ.
theorem is_left_inverse_to_is_right_inverse_to_eq:
∀M:Monoid. ∀l,r.
op: carrier → carrier → carrier
}.
-notation "hvbox(a break \middot b)"
- left associative with precedence 55
-for @{ 'magma_op $a $b }.
-
-interpretation "magma operation" 'magma_op a b =
- (cic:/matita/algebra/semigroups/op.con _ a b).
+interpretation "magma operation" 'middot a b = (op _ a b).
(* Semigroups *)
--- /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/cprop_connectives.ma".
+
+record powerset (A: Type) : Type ≝ { char: A → CProp }.
+
+interpretation "powerset" 'powerset A = (powerset A).
+
+interpretation "subset construction" 'subset \eta.x = (mk_powerset _ x).
+
+definition mem ≝ λA.λS:Ω \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
+
+interpretation "mem" 'mem a S = (mem _ S a).
+
+definition overlaps ≝ λA:Type.λU,V:Ω \sup A.exT2 ? (λa:A. a ∈ U) (λa.a ∈ V).
+
+interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
+
+definition subseteq ≝ λA:Type.λU,V:Ω \sup A.∀a:A. a ∈ U → a ∈ V.
+
+interpretation "subseteq" 'subseteq U V = (subseteq _ U V).
+
+definition intersects ≝ λA:Type.λU,V:Ω \sup A.{a | a ∈ U ∧ a ∈ V}.
+
+interpretation "intersects" 'intersects U V = (intersects _ U V).
+
+definition union ≝ λA:Type.λU,V:Ω \sup A.{a | a ∈ U ∨ a ∈ V}.
+
+interpretation "union" 'union U V = (union _ U V).
+
+include "logic/equality.ma".
+
+definition singleton ≝ λA:Type.λa:A.{b | a=b}.
+
+interpretation "singleton" 'singl a = (singleton _ a).
(* *)
(**************************************************************************)
-include "logic/equality.ma".
-
-inductive And (A,B:CProp) : CProp ≝
- conj: A → B → And A B.
-
-interpretation "constructive and" 'and x y = (And x y).
-
-inductive Or (A,B:CProp) : CProp ≝
- | or_intro_l: A → Or A B
- | or_intro_r: B → Or A B.
-
-interpretation "constructive or" 'or x y = (Or x y).
-
-inductive exT2 (A:Type) (P,Q:A→CProp) : CProp ≝
- ex_introT2: ∀w:A. P w → Q w → exT2 A P Q.
-
-record powerset (A: Type) : Type ≝ { char: A → CProp }.
-
-notation "hvbox(2 \sup A)" non associative with precedence 45
-for @{ 'powerset $A }.
-
-interpretation "powerset" 'powerset A = (powerset A).
-
-notation < "hvbox({ ident i | term 19 p })" with precedence 90
-for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
-
-notation > "hvbox({ ident i | term 19 p })" with precedence 90
-for @{ 'subset (\lambda ${ident i}. $p)}.
-
-interpretation "subset construction" 'subset \eta.x = (mk_powerset _ x).
-
-definition mem ≝ λA.λS:2 \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
-
-notation "hvbox(a break ∈ b)" non associative with precedence 45
-for @{ 'mem $a $b }.
-
-interpretation "mem" 'mem a S = (mem _ S a).
-
-definition overlaps ≝ λA:Type.λU,V:2 \sup A.exT2 ? (λa:A. a ∈ U) (λa.a ∈ V).
-
-notation "hvbox(a break ≬ b)" non associative with precedence 45
-for @{ 'overlaps $a $b }. (* \between *)
-
-interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
-
-definition subseteq ≝ λA:Type.λU,V:2 \sup A.∀a:A. a ∈ U → a ∈ V.
-
-notation "hvbox(a break ⊆ b)" non associative with precedence 45
-for @{ 'subseteq $a $b }. (* \subseteq *)
-
-interpretation "subseteq" 'subseteq U V = (subseteq _ U V).
-
-definition intersects ≝ λA:Type.λU,V:2 \sup A.{a | a ∈ U ∧ a ∈ V}.
-
-notation "hvbox(a break ∩ b)" non associative with precedence 55
-for @{ 'intersects $a $b }. (* \cap *)
-
-interpretation "intersects" 'intersects U V = (intersects _ U V).
-
-definition union ≝ λA:Type.λU,V:2 \sup A.{a | a ∈ U ∨ a ∈ V}.
-
-notation "hvbox(a break ∪ b)" non associative with precedence 55
-for @{ 'union $a $b }. (* \cup *)
-
-interpretation "union" 'union U V = (union _ U V).
+include "datatypes/subsets.ma".
record axiom_set : Type ≝ {
A:> Type;
i: A → Type;
- C: ∀a:A. i a → 2 \sup A
+ C: ∀a:A. i a → Ω \sup A
}.
-inductive for_all (A: axiom_set) (U,V: 2 \sup A) (covers: A → CProp) : CProp ≝
+inductive for_all (A: axiom_set) (U,V: Ω \sup A) (covers: A → CProp) : CProp ≝
iter: (∀a:A.a ∈ V → covers a) → for_all A U V covers.
-inductive covers (A: axiom_set) (U: 2 \sup A) : A → CProp ≝
+inductive covers (A: axiom_set) (U: \Omega \sup A) : A → CProp ≝
refl: ∀a:A. a ∈ U → covers A U a
| infinity: ∀a:A. ∀j: i ? a. for_all A U (C ? a j) (covers A U) → covers A U a.
interpretation "covers" 'covers a U = (covers _ U a).
definition covers_elim ≝
- λA:axiom_set.λU: 2 \sup A.λP:2 \sup A.
- λH1:∀a:A. a ∈ U → a ∈ P.
+ λA:axiom_set.λU: \Omega \sup A.λP:\Omega \sup A.
+ λH1: U ⊆ P.
λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → C ? a j ⊆ P → a ∈ P.
let rec aux (a:A) (p:a ◃ U) on p : a ∈ P ≝
match p return λaa.λ_:aa ◃ U.aa ∈ P with
in
aux.
-inductive ex_such (A : axiom_set) (U,V : 2 \sup A) (fish: A → CProp) : CProp ≝
+inductive ex_such (A : axiom_set) (U,V : \Omega \sup A) (fish: A → CProp) : CProp ≝
found : ∀a. a ∈ V → fish a → ex_such A U V fish.
-coinductive fish (A:axiom_set) (U: 2 \sup A) : A → CProp ≝
+coinductive fish (A:axiom_set) (U: \Omega \sup A) : A → CProp ≝
mk_fish: ∀a:A. a ∈ U → (∀j: i ? a. ex_such A U (C ? a j) (fish A U)) → fish A U a.
notation "hvbox(a break ⋉ b)" non associative with precedence 45
interpretation "fishl" 'fish A U = (ex_such _ U A (fish _ U)).
interpretation "fish" 'fish a U = (fish _ U a).
-let corec fish_rec (A:axiom_set) (U: 2 \sup A)
- (P: 2 \sup A) (H1: ∀a:A. a ∈ P → a ∈ U)
+let corec fish_rec (A:axiom_set) (U: \Omega \sup A)
+ (P: Ω \sup A) (H1: P ⊆ U)
(H2: ∀a:A. a ∈ P → ∀j: i ? a. C ? a j ≬ P):
∀a:A. ∀p: a ∈ P. a ⋉ U ≝
λa,p.
cases (H1 i); clear H1; apply (H3 a1); assumption]
qed.
-definition singleton ≝ λA:axiom_set.λa:A.{b | a=b}.
-
-notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
-
-interpretation "singleton" 'singl a = (singleton _ a).
-
definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {b}.
interpretation "covered by one" 'leq a b = (leq _ a b).
interpretation "uparrow" 'uparrow a = (uparrow _ a).
-definition downarrow ≝ λA:axiom_set.λU:2 \sup A.mk_powerset ? (λa:A. ↑a ≬ U).
+definition downarrow ≝ λA:axiom_set.λU:Ω \sup A.mk_powerset ? (λa:A. ↑a ≬ U).
notation "↓a" with precedence 80 for @{ 'downarrow $a }.
interpretation "downarrow" 'downarrow a = (downarrow _ a).
-definition fintersects ≝ λA:axiom_set.λU,V:2 \sup A.↓U ∩ ↓V.
+definition fintersects ≝ λA:axiom_set.λU,V:Ω \sup A.↓U ∩ ↓V.
notation "hvbox(U break ↓ V)" non associative with precedence 80 for @{ 'fintersects $U $V }.
record convergent_generated_topology : Type ≝
{ AA:> axiom_set;
- convergence: ∀a:AA.∀U,V:2 \sup AA. a ◃ U → a ◃ V → a ◃ U ↓ V
+ convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ U ↓ V
}.
datatypes/constructors.ma logic/equality.ma
datatypes/compare.ma
datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma
+datatypes/subsets.ma logic/cprop_connectives.ma logic/equality.ma
algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma
algebra/finite_groups.ma algebra/groups.ma nat/relevant_equations.ma
algebra/semigroups.ma higher_order_defs/functions.ma
demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma
demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma
demo/realisability.ma datatypes/constructors.ma logic/connectives.ma
-demo/formal_topology.ma logic/equality.ma
+demo/formal_topology.ma datatypes/subsets.ma
+demo/natural_deduction.ma
list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma
list/list.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma nat/orders.ma nat/plus.ma
list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma
logic/connectives.ma
logic/coimplication.ma logic/connectives.ma
logic/connectives2.ma higher_order_defs/relations.ma
+logic/cprop_connectives.ma datatypes/constructors.ma logic/equality.ma
nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma
nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma
nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma
\lambda A,B,C:Type.\lambda f:(B\to C).\lambda g:(A\to B).\lambda x:A.
f (g x).
-notation "hvbox(a break \circ b)"
- left associative with precedence 70
-for @{ 'compose $a $b }.
-
interpretation "function composition" 'compose f g =
(cic:/matita/higher_order_defs/functions/compose.con _ _ _ f g).
--- /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/equality.ma".
+include "datatypes/constructors.ma".
+
+inductive Or (A,B:CProp) : CProp ≝
+ | Left : A → Or A B
+ | Right : B → Or A B.
+
+interpretation "constructive or" 'or x y = (Or x y).
+
+inductive Or3 (A,B,C:CProp) : CProp ≝
+ | Left3 : A → Or3 A B C
+ | Middle3 : B → Or3 A B C
+ | Right3 : C → Or3 A B C.
+
+interpretation "constructive ternary or" 'or3 x y z= (Or3 x y z).
+
+notation < "hvbox(a break ∨ b break ∨ c)" with precedence 35 for @{'or3 $a $b $c}.
+
+inductive Or4 (A,B,C,D:CProp) : CProp ≝
+ | Left3 : A → Or4 A B C D
+ | Middle3 : B → Or4 A B C D
+ | Right3 : C → Or4 A B C D
+ | Extra3: D → Or4 A B C D.
+
+interpretation "constructive ternary or" 'or4 x y z t = (Or4 x y z t).
+
+notation < "hvbox(a break ∨ b break ∨ c break ∨ d)" with precedence 35 for @{'or4 $a $b $c $d}.
+
+inductive And (A,B:CProp) : CProp ≝
+ | Conj : A → B → And A B.
+
+interpretation "constructive and" 'and x y = (And x y).
+
+inductive And3 (A,B,C:CProp) : CProp ≝
+ | Conj3 : A → B → C → And3 A B C.
+
+notation < "hvbox(a break ∧ b break ∧ c)" with precedence 35 for @{'and3 $a $b $c}.
+
+interpretation "constructive ternary and" 'and3 x y z = (And3 x y z).
+
+inductive And4 (A,B,C,D:CProp) : CProp ≝
+ | Conj4 : A → B → C → D → And4 A B C D.
+
+notation < "hvbox(a break ∧ b break ∧ c break ∧ d)" with precedence 35 for @{'and4 $a $b $c $d}.
+
+interpretation "constructive quaternary and" 'and4 x y z t = (And4 x y z t).
+
+inductive exT (A:Type) (P:A→CProp) : CProp ≝
+ ex_introT: ∀w:A. P w → exT A P.
+
+notation "\ll term 19 a, break term 19 b \gg"
+with precedence 90 for @{'dependent_pair $a $b}.
+interpretation "dependent pair" 'dependent_pair a b =
+ (ex_introT _ _ a b).
+
+interpretation "CProp exists" 'exists \eta.x = (exT _ x).
+
+notation "\ll term 19 a, break term 19 b \gg"
+with precedence 90 for @{'dependent_pair $a $b}.
+interpretation "dependent pair" 'dependent_pair a b =
+ (ex_introT _ _ a b).
+
+
+definition pi1exT ≝ λA,P.λx:exT A P.match x with [ex_introT x _ ⇒ x].
+definition pi2exT ≝
+ λA,P.λx:exT A P.match x return λx.P (pi1exT ?? x) with [ex_introT _ p ⇒ p].
+
+interpretation "exT \fst" 'pi1 = (pi1exT _ _).
+interpretation "exT \fst" 'pi1a x = (pi1exT _ _ x).
+interpretation "exT \fst" 'pi1b x y = (pi1exT _ _ x y).
+interpretation "exT \snd" 'pi2 = (pi2exT _ _).
+interpretation "exT \snd" 'pi2a x = (pi2exT _ _ x).
+interpretation "exT \snd" 'pi2b x y = (pi2exT _ _ x y).
+
+inductive exT23 (A:Type) (P:A→CProp) (Q:A→CProp) (R:A→A→CProp) : CProp ≝
+ ex_introT23: ∀w,p:A. P w → Q p → R w p → exT23 A P Q R.
+
+definition pi1exT23 ≝
+ λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 x _ _ _ _ ⇒ x].
+definition pi2exT23 ≝
+ λA,P,Q,R.λx:exT23 A P Q R.match x with [ex_introT23 _ x _ _ _ ⇒ x].
+
+interpretation "exT2 \fst" 'pi1 = (pi1exT23 _ _ _ _).
+interpretation "exT2 \snd" 'pi2 = (pi2exT23 _ _ _ _).
+interpretation "exT2 \fst" 'pi1a x = (pi1exT23 _ _ _ _ x).
+interpretation "exT2 \snd" 'pi2a x = (pi2exT23 _ _ _ _ x).
+interpretation "exT2 \fst" 'pi1b x y = (pi1exT23 _ _ _ _ x y).
+interpretation "exT2 \snd" 'pi2b x y = (pi2exT23 _ _ _ _ x y).
+
+inductive exT2 (A:Type) (P,Q:A→CProp) : CProp ≝
+ ex_introT2: ∀w:A. P w → Q w → exT2 A P Q.
+
+definition Not : CProp → Prop ≝ λx:CProp.x → False.
+
+interpretation "constructive not" 'not x = (Not x).
+
+definition cotransitive ≝
+ λC:Type.λlt:C→C→CProp.∀x,y,z:C. lt x y → lt x z ∨ lt z y.
+
+definition coreflexive ≝ λC:Type.λlt:C→C→CProp. ∀x:C. ¬ (lt x x).
+
+definition symmetric ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x.
+
+definition antisymmetric ≝ λA:Type.λR:A→A→CProp.λeq:A→A→Prop.∀x:A.∀y:A.R x y→R y x→eq x y.
+
+definition reflexive ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
+
+definition transitive ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z.
+
projects / helm.git / commitdiff
