From 716338697e54d7a7e3602aabdecc2a8a639d683e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 7 Dec 2012 14:30:36 +0000 Subject: [PATCH] - untranslated sections of "formal_topology" commented to make it compile - "tutorial" now compiles --- matita/matita/lib/formal_topology/apply_functor.ma | 3 ++- matita/matita/lib/formal_topology/basic_pairs.ma | 3 ++- .../basic_pairs_to_basic_topologies.ma | 5 +++-- .../formal_topology/basic_pairs_to_o-basic_pairs.ma | 3 ++- .../matita/lib/formal_topology/basic_topologies.ma | 3 ++- .../basic_topologies_to_o-basic_topologies.ma | 3 ++- matita/matita/lib/formal_topology/categories.ma | 3 ++- .../matita/lib/formal_topology/concrete_spaces.ma | 5 +++-- .../concrete_spaces_to_o-concrete_spaces.ma | 5 +++-- .../matita/lib/formal_topology/formal_topologies.ma | 5 +++-- matita/matita/lib/formal_topology/notation.ma | 3 ++- matita/matita/lib/formal_topology/o-algebra.ma | 3 ++- matita/matita/lib/formal_topology/o-basic_pairs.ma | 3 ++- .../o-basic_pairs_to_o-basic_topologies.ma | 3 ++- .../lib/formal_topology/o-basic_topologies.ma | 3 ++- .../matita/lib/formal_topology/o-concrete_spaces.ma | 3 ++- .../lib/formal_topology/o-formal_topologies.ma | 3 ++- matita/matita/lib/formal_topology/o-saturations.ma | 3 ++- .../matita/lib/formal_topology/r-o-basic_pairs.ma | 5 +++-- matita/matita/lib/formal_topology/relations.ma | 5 +++-- .../lib/formal_topology/relations_to_o-algebra.ma | 5 +++-- matita/matita/lib/formal_topology/saturations.ma | 3 ++- .../formal_topology/saturations_to_o-saturations.ma | 3 ++- matita/matita/lib/formal_topology/subsets.ma | 3 ++- matita/matita/lib/tutorial/chapter4.ma | 5 ++++- matita/matita/lib/tutorial/chapter5.ma | 2 +- matita/matita/lib/tutorial/chapter6.ma | 13 ++++++++++--- matita/matita/lib/tutorial/chapter7.ma | 3 +-- 28 files changed, 71 insertions(+), 38 deletions(-) diff --git a/matita/matita/lib/formal_topology/apply_functor.ma b/matita/matita/lib/formal_topology/apply_functor.ma index 55e667540..e08cf5176 100644 --- a/matita/matita/lib/formal_topology/apply_functor.ma +++ b/matita/matita/lib/formal_topology/apply_functor.ma @@ -14,7 +14,7 @@ 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; @@ -120,3 +120,4 @@ qed. +*) diff --git a/matita/matita/lib/formal_topology/basic_pairs.ma b/matita/matita/lib/formal_topology/basic_pairs.ma index ff4085554..ded2eb517 100644 --- a/matita/matita/lib/formal_topology/basic_pairs.ma +++ b/matita/matita/lib/formal_topology/basic_pairs.ma @@ -14,7 +14,7 @@ include "formal_topology/relations.ma". include "formal_topology/notation.ma". - +(* record basic_pair: Type[1] ≝ { concr: REL; form: REL; rel: concr ⇒_\r1 form }. @@ -222,3 +222,4 @@ qed. 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)). *) +*) diff --git a/matita/matita/lib/formal_topology/basic_pairs_to_basic_topologies.ma b/matita/matita/lib/formal_topology/basic_pairs_to_basic_topologies.ma index c236dc6a8..b44a42a86 100644 --- a/matita/matita/lib/formal_topology/basic_pairs_to_basic_topologies.ma +++ b/matita/matita/lib/formal_topology/basic_pairs_to_basic_topologies.ma @@ -16,7 +16,7 @@ include "formal_topology/basic_pairs_to_o-basic_pairs.ma". 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)); @@ -61,4 +61,5 @@ qed. lemma BBBB_faithful : failthful2 ?? VVV FIXME -*) \ No newline at end of file +*) +*) diff --git a/matita/matita/lib/formal_topology/basic_pairs_to_o-basic_pairs.ma b/matita/matita/lib/formal_topology/basic_pairs_to_o-basic_pairs.ma index 2041cec40..d787796b7 100644 --- a/matita/matita/lib/formal_topology/basic_pairs_to_o-basic_pairs.ma +++ b/matita/matita/lib/formal_topology/basic_pairs_to_o-basic_pairs.ma @@ -15,7 +15,7 @@ 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; @@ -142,3 +142,4 @@ theorem BP_to_OBP_full: full2 ?? BP_to_OBP. | change in match or_f_star_ with (λq,w,x.fun12 ?? (or_f_star q w) x);] simplify; apply (†(Hgc‡#)); qed. +*) diff --git a/matita/matita/lib/formal_topology/basic_topologies.ma b/matita/matita/lib/formal_topology/basic_topologies.ma index 3b1e2e577..b61f61916 100644 --- a/matita/matita/lib/formal_topology/basic_topologies.ma +++ b/matita/matita/lib/formal_topology/basic_topologies.ma @@ -14,7 +14,7 @@ include "formal_topology/relations.ma". include "formal_topology/saturations.ma". - +(* record basic_topology: Type[1] ≝ { carrbt:> REL; A: Ω^carrbt ⇒_1 Ω^carrbt; @@ -209,3 +209,4 @@ theorem continuous_relation_eqS: apply Hcut2; assumption. qed. *) +*) diff --git a/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma b/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma index 58b75fb68..6b07dfeb0 100644 --- a/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma +++ b/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma @@ -15,7 +15,7 @@ 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); @@ -89,3 +89,4 @@ theorem BTop_to_OBTop_full: full2 ?? BTop_to_OBTop. unfold image_coercion; cases Hg; whd; simplify; intro; simplify; qed. *) + diff --git a/matita/matita/lib/formal_topology/categories.ma b/matita/matita/lib/formal_topology/categories.ma index f5cad55fe..5643e2f6b 100644 --- a/matita/matita/lib/formal_topology/categories.ma +++ b/matita/matita/lib/formal_topology/categories.ma @@ -363,7 +363,7 @@ record functor2 (C1: category2) (C2: category2) : Type[3] ≝ 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 @@ -525,3 +525,4 @@ notation > "r⎻*" non associative with precedence 90 for @{'OR_f_minus_star $r} 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 diff --git a/matita/matita/lib/formal_topology/concrete_spaces.ma b/matita/matita/lib/formal_topology/concrete_spaces.ma index f9f715dc6..d7006cafb 100644 --- a/matita/matita/lib/formal_topology/concrete_spaces.ma +++ b/matita/matita/lib/formal_topology/concrete_spaces.ma @@ -13,7 +13,7 @@ (**************************************************************************) 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] ≝ @@ -106,4 +106,5 @@ definition CSPA: category1. apply (.= id_neutral_left1 ????); apply refl1] qed. -*) \ No newline at end of file +*) +*) diff --git a/matita/matita/lib/formal_topology/concrete_spaces_to_o-concrete_spaces.ma b/matita/matita/lib/formal_topology/concrete_spaces_to_o-concrete_spaces.ma index 29ff0754a..3e70b4372 100644 --- a/matita/matita/lib/formal_topology/concrete_spaces_to_o-concrete_spaces.ma +++ b/matita/matita/lib/formal_topology/concrete_spaces_to_o-concrete_spaces.ma @@ -15,7 +15,7 @@ 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. @@ -49,4 +49,5 @@ definition o_convergent_relation_pair_of_convergent_relation_pair: apply (orelation_of_relation_preserves_composition ?? (form BP2) (rel BP1) ?); ] qed. -*) \ No newline at end of file +*) +*) diff --git a/matita/matita/lib/formal_topology/formal_topologies.ma b/matita/matita/lib/formal_topology/formal_topologies.ma index 177eb454e..e3af412e3 100644 --- a/matita/matita/lib/formal_topology/formal_topologies.ma +++ b/matita/matita/lib/formal_topology/formal_topologies.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "formal_topology/basic_topologies.ma". - +(* (* definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S). intros; constructor 1; @@ -94,4 +94,5 @@ definition formal_map_composition: apply prop1; assumption] qed. -*) \ No newline at end of file +*) +*) diff --git a/matita/matita/lib/formal_topology/notation.ma b/matita/matita/lib/formal_topology/notation.ma index 87ec0e2dd..150205619 100644 --- a/matita/matita/lib/formal_topology/notation.ma +++ b/matita/matita/lib/formal_topology/notation.ma @@ -11,10 +11,11 @@ (* 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 diff --git a/matita/matita/lib/formal_topology/o-algebra.ma b/matita/matita/lib/formal_topology/o-algebra.ma index 496485975..704737550 100644 --- a/matita/matita/lib/formal_topology/o-algebra.ma +++ b/matita/matita/lib/formal_topology/o-algebra.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "formal_topology/categories.ma". - +(* inductive bool : Type[0] := true : bool | false : bool. lemma BOOL : objs1 SET. @@ -440,3 +440,4 @@ qed. lemma oa_overlap_sym': ∀o:OA.∀U,V:o. (U >< V) = (V >< U). intros; split; intro; apply oa_overlap_sym; assumption. qed. +*) diff --git a/matita/matita/lib/formal_topology/o-basic_pairs.ma b/matita/matita/lib/formal_topology/o-basic_pairs.ma index 02ef2143a..1e01764a7 100644 --- a/matita/matita/lib/formal_topology/o-basic_pairs.ma +++ b/matita/matita/lib/formal_topology/o-basic_pairs.ma @@ -14,7 +14,7 @@ include "formal_topology/o-algebra.ma". include "formal_topology/notation.ma". - +(* record Obasic_pair: Type[2] ≝ { Oconcr: OA; Oform: OA; Orel: arrows2 ? Oconcr Oform }. @@ -249,3 +249,4 @@ interpretation "Universal pre-image ⊩*" 'rest x = (fun12 ? ? (or_f_star ? ?) ( 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)). +*) diff --git a/matita/matita/lib/formal_topology/o-basic_pairs_to_o-basic_topologies.ma b/matita/matita/lib/formal_topology/o-basic_pairs_to_o-basic_topologies.ma index fdd226f0f..f44a9f4af 100644 --- a/matita/matita/lib/formal_topology/o-basic_pairs_to_o-basic_topologies.ma +++ b/matita/matita/lib/formal_topology/o-basic_pairs_to_o-basic_topologies.ma @@ -15,7 +15,7 @@ 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 *) @@ -117,3 +117,4 @@ constructor 1; | intros 6; apply refl1;] qed. +*) diff --git a/matita/matita/lib/formal_topology/o-basic_topologies.ma b/matita/matita/lib/formal_topology/o-basic_topologies.ma index 0e9d8604f..095c43805 100644 --- a/matita/matita/lib/formal_topology/o-basic_topologies.ma +++ b/matita/matita/lib/formal_topology/o-basic_topologies.ma @@ -14,7 +14,7 @@ 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; @@ -188,3 +188,4 @@ theorem continuous_relation_eqS: apply Hcut2; assumption. qed. *) +*) diff --git a/matita/matita/lib/formal_topology/o-concrete_spaces.ma b/matita/matita/lib/formal_topology/o-concrete_spaces.ma index d808b0085..f39b25109 100644 --- a/matita/matita/lib/formal_topology/o-concrete_spaces.ma +++ b/matita/matita/lib/formal_topology/o-concrete_spaces.ma @@ -14,7 +14,7 @@ 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)); @@ -132,3 +132,4 @@ definition Oconvergent_relation_space_setoid_of_arrows2_OCSPA : ∀P,Q. arrows2 OCSPA P Q → Oconvergent_relation_space_setoid P Q ≝ λP,Q,x.x. coercion Oconvergent_relation_space_setoid_of_arrows2_OCSPA. +*) diff --git a/matita/matita/lib/formal_topology/o-formal_topologies.ma b/matita/matita/lib/formal_topology/o-formal_topologies.ma index af9da702a..489aba016 100644 --- a/matita/matita/lib/formal_topology/o-formal_topologies.ma +++ b/matita/matita/lib/formal_topology/o-formal_topologies.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "formal_topology/o-basic_topologies.ma". - +(* (* (* definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S). @@ -97,3 +97,4 @@ definition formal_map_composition: apply prop1; assumption] qed. *) +*) diff --git a/matita/matita/lib/formal_topology/o-saturations.ma b/matita/matita/lib/formal_topology/o-saturations.ma index 20db479a3..8a9befa68 100644 --- a/matita/matita/lib/formal_topology/o-saturations.ma +++ b/matita/matita/lib/formal_topology/o-saturations.ma @@ -13,7 +13,7 @@ (**************************************************************************) 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). @@ -35,3 +35,4 @@ theorem o_saturation_idempotent: ∀C:OA.∀A:C ⇒_1 C. is_o_saturation C A → [ apply (if ?? (i (A U) U)); apply (oa_leq_refl C). | apply o_saturation_expansive; assumption] qed. +*) diff --git a/matita/matita/lib/formal_topology/r-o-basic_pairs.ma b/matita/matita/lib/formal_topology/r-o-basic_pairs.ma index 0218ed835..e598f36cb 100644 --- a/matita/matita/lib/formal_topology/r-o-basic_pairs.ma +++ b/matita/matita/lib/formal_topology/r-o-basic_pairs.ma @@ -14,7 +14,7 @@ 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". @@ -252,4 +252,5 @@ STOP; *) -*) \ No newline at end of file +*) +*) diff --git a/matita/matita/lib/formal_topology/relations.ma b/matita/matita/lib/formal_topology/relations.ma index 2ad35655e..2d5d85a6b 100644 --- a/matita/matita/lib/formal_topology/relations.ma +++ b/matita/matita/lib/formal_topology/relations.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "formal_topology/subsets.ma". - +(* record binary_relation (A,B: SET) : Type[1] ≝ { satisfy:> binary_morphism1 A B CPROP }. @@ -323,4 +323,5 @@ theorem extS_singleton: 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. +*) diff --git a/matita/matita/lib/formal_topology/relations_to_o-algebra.ma b/matita/matita/lib/formal_topology/relations_to_o-algebra.ma index bc5153d5d..8030e28f6 100644 --- a/matita/matita/lib/formal_topology/relations_to_o-algebra.ma +++ b/matita/matita/lib/formal_topology/relations_to_o-algebra.ma @@ -14,7 +14,7 @@ include "formal_topology/relations.ma". include "formal_topology/o-algebra.ma". - +(* definition POW': objs1 SET → OAlgebra. intro A; constructor 1; [ apply (Ω^A); @@ -238,4 +238,5 @@ change with (∀a1.(∃x:carr S. a1 ∈ f {(x):S} ∧ x ∈ a) → a1 ∈ f 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. +*) diff --git a/matita/matita/lib/formal_topology/saturations.ma b/matita/matita/lib/formal_topology/saturations.ma index 02030e7cd..fab775bbe 100644 --- a/matita/matita/lib/formal_topology/saturations.ma +++ b/matita/matita/lib/formal_topology/saturations.ma @@ -13,7 +13,7 @@ (**************************************************************************) 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). @@ -36,3 +36,4 @@ theorem saturation_idempotent: ∀C,A. is_saturation C A → ∀U. A (A U) = A U [ apply (if ?? (i ??)); apply subseteq_refl | apply saturation_expansive; assumption] qed. +*) diff --git a/matita/matita/lib/formal_topology/saturations_to_o-saturations.ma b/matita/matita/lib/formal_topology/saturations_to_o-saturations.ma index 39b4176cb..ebea817d0 100644 --- a/matita/matita/lib/formal_topology/saturations_to_o-saturations.ma +++ b/matita/matita/lib/formal_topology/saturations_to_o-saturations.ma @@ -15,7 +15,7 @@ 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. @@ -27,3 +27,4 @@ intros (C R i); apply i; qed. 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. +*) diff --git a/matita/matita/lib/formal_topology/subsets.ma b/matita/matita/lib/formal_topology/subsets.ma index 8bacd2a55..5cb8455a0 100644 --- a/matita/matita/lib/formal_topology/subsets.ma +++ b/matita/matita/lib/formal_topology/subsets.ma @@ -13,7 +13,7 @@ (**************************************************************************) 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 }. @@ -179,3 +179,4 @@ interpretation "bigcup" 'bigcup f = (fun12 ?? (big_union ??) f). 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 ?)). +*) diff --git a/matita/matita/lib/tutorial/chapter4.ma b/matita/matita/lib/tutorial/chapter4.ma index 30fae3df0..aa2f5b08a 100644 --- a/matita/matita/lib/tutorial/chapter4.ma +++ b/matita/matita/lib/tutorial/chapter4.ma @@ -280,6 +280,8 @@ To make an example, in the previous case, the unification problem is bool = carr 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 (* ---------------------------------------- *) ⊢ @@ -334,4 +336,5 @@ unification hint 0 ≔ T1,T2,p1,p2; 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 diff --git a/matita/matita/lib/tutorial/chapter5.ma b/matita/matita/lib/tutorial/chapter5.ma index 9cd43fd23..b90433657 100644 --- a/matita/matita/lib/tutorial/chapter5.ma +++ b/matita/matita/lib/tutorial/chapter5.ma @@ -7,7 +7,7 @@ effectively searching an element of that set inside a data structure. In this 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, diff --git a/matita/matita/lib/tutorial/chapter6.ma b/matita/matita/lib/tutorial/chapter6.ma index 150b07b76..d243ce5c0 100644 --- a/matita/matita/lib/tutorial/chapter6.ma +++ b/matita/matita/lib/tutorial/chapter6.ma @@ -35,8 +35,9 @@ derivative of a language A w.r.t. a given character a. *) 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). @@ -47,8 +48,13 @@ w1,w2,...wk all belonging to l, such that l = w1w2...wk. 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. *) @@ -60,6 +66,7 @@ match l with [ nil ⇒ True | cons w tl ⇒ r w ∧ conjunct ? tl r ]. 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). @@ -154,7 +161,7 @@ qed. 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. @@ -163,7 +170,7 @@ 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