include "formal_topology/categories.ma".
include "formal_topology/notation.ma".
-
+(*
record Fo (C1,C2:CAT2) (F:arrows3 CAT2 C1 C2) : Type[2] ≝ {
F2: C2;
F1: C1;
+*)
include "formal_topology/relations.ma".
include "formal_topology/notation.ma".
-
+(*
record basic_pair: Type[1] ≝ {
concr: REL; form: REL; rel: concr ⇒_\r1 form
}.
interpretation "basic pair relation for subsets" 'Vdash2 x y c = (fun21 (concr ?) ?? (relS c) x y).
interpretation "basic pair relation for subsets (non applied)" 'Vdash c = (fun21 ??? (relS c)).
*)
+*)
include "formal_topology/o-basic_pairs_to_o-basic_topologies.ma".
include "formal_topology/basic_pairs.ma".
include "formal_topology/basic_topologies.ma".
-
+(*
definition basic_topology_of_basic_pair: basic_pair → basic_topology.
intro bp;
letin obt ≝ (OR (BP_to_OBP bp));
lemma BBBB_faithful : failthful2 ?? VVV
FIXME
-*)
\ No newline at end of file
+*)
+*)
include "formal_topology/basic_pairs.ma".
include "formal_topology/o-basic_pairs.ma".
include "formal_topology/relations_to_o-algebra.ma".
-
+(*
definition o_basic_pair_of_basic_pair: basic_pair → Obasic_pair.
intro b;
constructor 1;
| change in match or_f_star_ with (λq,w,x.fun12 ?? (or_f_star q w) x);]
simplify; apply (†(Hgc‡#));
qed.
+*)
include "formal_topology/relations.ma".
include "formal_topology/saturations.ma".
-
+(*
record basic_topology: Type[1] ≝
{ carrbt:> REL;
A: Ω^carrbt ⇒_1 Ω^carrbt;
apply Hcut2; assumption.
qed.
*)
+*)
include "formal_topology/basic_topologies.ma".
include "formal_topology/o-basic_topologies.ma".
include "formal_topology/relations_to_o-algebra.ma".
-
+(*
definition o_basic_topology_of_basic_topology: basic_topology → Obasic_topology.
intros (b); constructor 1;
[ apply (POW' b) | apply (A b) | apply (J b);
unfold image_coercion; cases Hg; whd; simplify; intro; simplify;
qed.
*)
+
notation > "F⎽⇒ x" left associative with precedence 65 for @{'map_arrows2 $F $x}.
notation "F\sub⇒ x" left associative with precedence 65 for @{'map_arrows2 $F $x}.
interpretation "map_arrows2" 'map_arrows2 F x = (fun12 ?? (map_arrows2 ?? F ??) x).
-
+(* BEGIN HERE
definition functor2_setoid: category2 → category2 → setoid3.
#C1 #C2
@mk_setoid3
notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
+*)
\ No newline at end of file
(**************************************************************************)
include "formal_topology/basic_pairs.ma".
-
+(*
(* carr1 e' necessario perche' ci sega via la coercion per gli oggetti di REL!
(confondendola con la coercion per gli oggetti di SET
record concrete_space : Type[1] ≝
apply (.= id_neutral_left1 ????);
apply refl1]
qed.
-*)
\ No newline at end of file
+*)
+*)
include "formal_topology/concrete_spaces.ma".
include "formal_topology/o-concrete_spaces.ma".
include "formal_topology/basic_pairs_to_o-basic_pairs.ma".
-
+(*
(*
(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
definition o_concrete_space_of_concrete_space: cic:/matita/formal_topology/concrete_spaces/concrete_space.ind#xpointer(1/1) → concrete_space.
apply (orelation_of_relation_preserves_composition ?? (form BP2) (rel BP1) ?); ]
qed.
-*)
\ No newline at end of file
+*)
+*)
(**************************************************************************)
include "formal_topology/basic_topologies.ma".
-
+(*
(*
definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
intros; constructor 1;
apply prop1; assumption]
qed.
-*)
\ No newline at end of file
+*)
+*)
(* v GNU General Public License Version 2 *)
(* *)
(**************************************************************************)
-
+(*
notation "hvbox (r \sub \c)" with precedence 90 for @{'concr_rel $r}.
notation "hvbox (r \sub \f)" with precedence 90 for @{'form_rel $r}.
definition hide ≝ λA:Type.λx:A.x.
interpretation "hide" 'hide x = (hide ? x).
+*)
\ No newline at end of file
(**************************************************************************)
include "formal_topology/categories.ma".
-
+(*
inductive bool : Type[0] := true : bool | false : bool.
lemma BOOL : objs1 SET.
lemma oa_overlap_sym': ∀o:OA.∀U,V:o. (U >< V) = (V >< U).
intros; split; intro; apply oa_overlap_sym; assumption.
qed.
+*)
include "formal_topology/o-algebra.ma".
include "formal_topology/notation.ma".
-
+(*
record Obasic_pair: Type[2] ≝ {
Oconcr: OA; Oform: OA; Orel: arrows2 ? Oconcr Oform
}.
notation "'Ext' \sub b" non associative with precedence 90 for @{'ext $b}.
notation > "'Ext'⎽term 90 b" non associative with precedence 90 for @{'ext $b}.
interpretation "Existential pre-image ⊩⎻" 'ext x = (fun12 ? ? (or_f_minus ? ?) (Orel x)).
+*)
include "formal_topology/notation.ma".
include "formal_topology/o-basic_pairs.ma".
include "formal_topology/o-basic_topologies.ma".
-
+(*
alias symbol "eq" = "setoid1 eq".
(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
| intros 6; apply refl1;]
qed.
+*)
include "formal_topology/o-algebra.ma".
include "formal_topology/o-saturations.ma".
-
+(*
record Obasic_topology: Type[2] ≝ {
Ocarrbt:> OA;
oA: Ocarrbt ⇒_2 Ocarrbt; oJ: Ocarrbt ⇒_2 Ocarrbt;
apply Hcut2; assumption.
qed.
*)
+*)
include "formal_topology/o-basic_pairs.ma".
include "formal_topology/o-saturations.ma".
-
+(*
definition A : ∀b:OBP. unary_morphism1 (Oform b) (Oform b).
intros; constructor 1;
[ apply (λx.□⎽b (Ext⎽b x));
∀P,Q. arrows2 OCSPA P Q → Oconvergent_relation_space_setoid P Q ≝ λP,Q,x.x.
coercion Oconvergent_relation_space_setoid_of_arrows2_OCSPA.
+*)
(**************************************************************************)
include "formal_topology/o-basic_topologies.ma".
-
+(*
(*
(*
definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
apply prop1; assumption]
qed.
*)
+*)
(**************************************************************************)
include "formal_topology/o-algebra.ma".
-
+(*
definition is_o_saturation: ∀C:OA. C ⇒_1 C → CProp[1] ≝
λC:OA.λA:C ⇒_1 C.∀U,V. (U ≤ A V) =_1 (A U ≤ A V).
[ apply (if ?? (i (A U) U)); apply (oa_leq_refl C).
| apply o_saturation_expansive; assumption]
qed.
+*)
include "formal_topology/basic_pairs_to_o-basic_pairs.ma".
include "formal_topology/apply_functor.ma".
-
+(*
definition rOBP ≝ Apply (category2_of_category1 BP) OBP BP_to_OBP.
include "formal_topology/o-basic_pairs_to_o-basic_topologies.ma".
*)
-*)
\ No newline at end of file
+*)
+*)
(**************************************************************************)
include "formal_topology/subsets.ma".
-
+(*
record binary_relation (A,B: SET) : Type[1] ≝
{ satisfy:> binary_morphism1 A B CPROP }.
intros; unfold extS; unfold ext; unfold singleton; simplify;
split; intros 2; simplify; simplify in f;
[ cases f; cases e; cases x1; change in f2 with (x =_1 w); apply (. #‡f2); assumption;
- | split; try apply I; exists [apply x] split; try assumption; change with (x = x); apply rule #;] qed.
\ No newline at end of file
+ | split; try apply I; exists [apply x] split; try assumption; change with (x = x); apply rule #;] qed.
+*)
include "formal_topology/relations.ma".
include "formal_topology/o-algebra.ma".
-
+(*
definition POW': objs1 SET → OAlgebra.
intro A; constructor 1;
[ apply (Ω^A);
[ intros 2; change in f3 with (eq1 ? a1 a2); change with (a2 ∈ f* a);
apply (. f3^-1‡#); assumption;
| assumption ]]]
-qed.
\ No newline at end of file
+qed.
+*)
(**************************************************************************)
include "formal_topology/relations.ma".
-
+(*
definition is_saturation: ∀C:REL. Ω^C ⇒_1 Ω^C → CProp[1] ≝
λC:REL.λA:Ω^C ⇒_1 Ω^C. ∀U,V. (U ⊆ A V) =_1 (A U ⊆ A V).
[ apply (if ?? (i ??)); apply subseteq_refl
| apply saturation_expansive; assumption]
qed.
+*)
include "formal_topology/saturations.ma".
include "formal_topology/o-saturations.ma".
include "formal_topology/relations_to_o-algebra.ma".
-
+(*
(* These are only conversions :-) *)
definition o_operator_of_operator: ∀C:REL. (Ω^C ⇒_1 Ω^C) → ((POW C) ⇒_1 (POW C)) ≝ λC,t.t.
definition is_o_reduction_of_is_reduction:
∀C:REL.∀R: Ω^C ⇒_1 Ω^C.is_reduction ? R → is_o_reduction ? (o_operator_of_operator ? R).
intros (C R i); apply i; qed.
+*)
(**************************************************************************)
include "formal_topology/categories.ma".
-
+(*
record powerset_carrier (A: objs1 SET) : Type[1] ≝ { mem_operator: A ⇒_1 CPROP }.
interpretation "powerset low" 'powerset A = (powerset_carrier A).
notation "hvbox(a break ∈. b)" non associative with precedence 45 for @{ 'mem_low $a $b }.
interpretation "bigcap" 'bigcap f = (fun12 ?? (big_intersects ??) f).
interpretation "bigcup mk" 'bigcup_mk f = (fun12 ?? (big_union ??) (mk_unary_morphism2 ?? f ?)).
interpretation "bigcap mk" 'bigcap_mk f = (fun12 ?? (big_intersects ??) (mk_unary_morphism2 ?? f ?)).
+*)
and the hint is to take X= mk_DeqSet bool beqb true. The hint is correct, since
bool is convertible with (carr (mk_DeqSet bool beb true)). *)
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+
unification hint 0 ≔ ;
X ≟ mk_DeqSet bool beqb beqb_true
(* ---------------------------------------- *) ⊢
example hint2: ∀b1,b2.
〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
-#b1 #b2 #H @(\P H).
\ No newline at end of file
+#b1 #b2 #H @(\P H).
+qed-.
\ No newline at end of file
section we shall define several boolean functions acting on lists of elements in
a DeqSet, and prove some of their properties.*)
-include "basics/list.ma".
+include "basics/lists/list.ma".
include "tutorial/chapter4.ma".
(* The first function we define is an effective version of the membership relation,
definition cat : ∀S,l1,l2,w.Prop ≝
λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2.
-
+(*
notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
+*)
interpretation "cat lang" 'middot a b = (cat ? a b).
We need to define the latter operations. The following flatten function takes in
input a list of words and concatenates them together. *)
+(* FG: flatten in list.ma gets in the way:
+alias id "flatten" = "cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)".
+does not work, so we use flatten in lists for now
+
let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝
match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
+*)
(* Given a list of words l and a language r, (conjunct l r) is true if and only if
all words in l are in r, that is for every w in l, r w holds. *)
a word w belongs to l* is and only if there exists a list of strings
lw such that (conjunct lw l) and l = flatten lw. *)
+
definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l.
notation "a ^ *" non associative with precedence 90 for @{ 'star $a}.
interpretation "star lang" 'star l = (star ? l).
lemma cat_to_star:∀S.∀A:word S → Prop.
∀w1,w2. A w1 → A^* w2 → A^* (w1@w2).
#S #A #w1 #w2 #Aw * #l * #H #H1 @(ex_intro … (w1::l))
-% normalize /2/
+% destruct // normalize /2/
qed.
lemma fix_star: ∀S.∀A:word S → Prop.
[* #l generalize in match w; -w cases l [normalize #w * /2/]
#w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
#w1A #cw1 %1 @(ex_intro … w1) @(ex_intro … (flatten S tl))
- % /2/ whd @(ex_intro … tl) /2/
+ % destruct /2/ whd @(ex_intro … tl) /2/
|* [2: whd in ⊢ (%→?); #eqw <eqw //]
* #w1 * #w2 * * #eqw <eqw @cat_to_star
]
| po E1 E2 ⇒ (forget ? E1) + (forget ? E2)
| pk E ⇒ (forget ? E)^* ].
-(* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*)
-interpretation "forget" 'norm a = (forget ? a).
+interpretation "forget" 'card a = (forget ? a).
lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|).
// qed.
projects / helm.git / commitdiff