From ca41435a6021292ccba239aa173651c0be705b45 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 24 Jun 2008 14:47:16 +0000 Subject: [PATCH] notation factored, coercion commant taking terms and not only URI --- .../components/binaries/transcript/grafite.ml | 2 +- .../software/components/grafite/grafiteAst.ml | 4 +- .../components/grafite/grafiteAstPp.ml | 8 +-- .../components/grafite/grafiteMarshal.ml | 2 +- .../grafite_engine/grafiteEngine.ml | 8 ++- .../grafite_parser/grafiteDisambiguate.ml | 7 ++- .../grafite_parser/grafiteParser.ml | 8 +-- .../matita/contribs/dama/dama/bishop_set.ma | 6 +-- .../contribs/dama/dama/cprop_connectives.ma | 51 +++++-------------- .../matita/contribs/dama/dama/lebesgue.ma | 4 +- .../dama/dama/models/discrete_uniformity.ma | 6 +-- .../models/nat_dedekind_sigma_complete.ma | 39 +++++++------- .../dama/dama/models/nat_ordered_uniform.ma | 2 +- .../contribs/dama/dama/models/q_function.ma | 49 +++++++++--------- .../matita/contribs/dama/dama/ordered_set.ma | 2 +- .../contribs/dama/dama/ordered_uniform.ma | 28 +++++----- .../dama/dama/property_exhaustivity.ma | 24 ++++----- .../contribs/dama/dama/property_sigma.ma | 2 +- .../matita/contribs/dama/dama/supremum.ma | 18 +++---- .../matita/contribs/dama/dama/uniform.ma | 10 ++-- helm/software/matita/core_notation.moo | 15 ++++++ helm/software/matita/help/C/sec_commands.xml | 25 ++++++--- helm/software/matita/library/Q/frac.ma | 7 +++ helm/software/matita/library/Q/inv.ma | 5 ++ helm/software/matita/library/Q/q.ma | 4 ++ helm/software/matita/library/Z/z.ma | 2 +- .../matita/library/datatypes/constructors.ma | 25 +++------ .../matita/library/decidable_kit/eqtype.ma | 6 +-- .../matita/library/demo/power_derivative.ma | 4 +- .../software/matita/library/logic/equality.ma | 4 +- 30 files changed, 198 insertions(+), 179 deletions(-) diff --git a/helm/software/components/binaries/transcript/grafite.ml b/helm/software/components/binaries/transcript/grafite.ml index e88406b58..1616c18a9 100644 --- a/helm/software/components/binaries/transcript/grafite.ml +++ b/helm/software/components/binaries/transcript/grafite.ml @@ -95,7 +95,7 @@ let commit och items = | T.Line line -> out_line_comment och line | T.BaseUri uri -> out_command och (set "baseuri" uri) | T.Include script -> out_command och (require script) - | T.Coercion specs -> out_command och (coercion (snd specs)) + | T.Coercion specs -> out_unexported och "COERCION" (snd specs) | T.Notation specs -> out_unexported och "NOTATION" (snd specs) (**) | T.Inline (_, T.Var, src, _) -> out_alias och (UriManager.name_of_uri (UriManager.uri_of_string src)) src | T.Inline specs -> out_command och (inline (trd_rth specs)) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 2290c4d0b..d2e2f6f5f 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -147,11 +147,11 @@ type 'term macro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 12 +let magic = 13 type ('term,'obj) command = | Index of loc * 'term option (* key *) * UriManager.uri (* value *) - | Coercion of loc * UriManager.uri * bool (* add_obj *) * + | Coercion of loc * 'term * bool (* add_obj *) * int (* arity *) * int (* saturations *) | Default of loc * string * UriManager.uri list | Drop of loc diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 84facde66..ae9aa5027 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -288,15 +288,15 @@ let pp_default what uris = Printf.sprintf "default \"%s\" %s" what (String.concat " " (List.map UriManager.string_of_uri uris)) -let pp_coercion uri do_composites arity saturations= +let pp_coercion ~term_pp t do_composites arity saturations= Printf.sprintf "coercion %s %d %d %s" - (UriManager.string_of_uri uri) arity saturations + (term_pp t) arity saturations (if do_composites then "" else "nocomposites") let pp_command ~term_pp ~obj_pp = function | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri - | Coercion (_, uri, do_composites, i, j) -> - pp_coercion uri do_composites i j + | Coercion (_, t, do_composites, i, j) -> + pp_coercion ~term_pp t do_composites i j | Default (_,what,uris) -> pp_default what uris | Drop _ -> "drop" | Include (_,path) -> "include \"" ^ path ^ "\"" diff --git a/helm/software/components/grafite/grafiteMarshal.ml b/helm/software/components/grafite/grafiteMarshal.ml index 7731902b4..836f592b0 100644 --- a/helm/software/components/grafite/grafiteMarshal.ml +++ b/helm/software/components/grafite/grafiteMarshal.ml @@ -45,7 +45,7 @@ let rehash_cmd_uris = let uris = List.map rehash_uri uris in GrafiteAst.Default (loc, name, uris) | GrafiteAst.Coercion (loc, uri, close, arity, saturations) -> - GrafiteAst.Coercion (loc, rehash_uri uri, close, arity, saturations) + GrafiteAst.Coercion (loc, CicUtil.rehash_term uri, close, arity, saturations) | GrafiteAst.Index (loc, key, uri) -> GrafiteAst.Index (loc, HExtlib.map_option CicUtil.rehash_term key, rehash_uri uri) | cmd -> diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 8813e498b..b3a628463 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -455,7 +455,8 @@ type 'a eval_from_moo = { efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status } let coercion_moo_statement_of (uri,arity, saturations) = - GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity, saturations) + GrafiteAst.Coercion + (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations) let refinement_toolkit = { RefinementTool.type_of_aux' = @@ -481,6 +482,11 @@ let refinement_toolkit = { } let eval_coercion status ~add_composites uri arity saturations = + let uri = + try CicUtil.uri_of_term uri + with Invalid_argument _ -> + raise (Invalid_argument "coercion can only be constants/constructors") + in let status,compounds = GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity saturations (GrafiteTypes.get_baseuri status) diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 71460415a..318b38f61 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -470,7 +470,12 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)= in let metasenv,key = disambiguate_term_option metasenv key in !lexicon_status_ref, metasenv,GrafiteAst.Index(loc,key,uri) - | GrafiteAst.Coercion _ + | GrafiteAst.Coercion (loc,t,b,a,s) -> + let lexicon_status_ref = ref lexicon_status in + let disambiguate_term = + disambiguate_term text prefix_len lexicon_status_ref [] in + let metasenv,t = disambiguate_term metasenv t in + !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s) | GrafiteAst.Default _ | GrafiteAst.Drop _ | GrafiteAst.Include _ diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 7b119ab11..721cb0eff 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -657,13 +657,15 @@ EXTEND ind_types in GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) - | IDENT "coercion" ; suri = URI ; arity = OPT int ; - saturations = OPT int; composites = OPT (IDENT "nocomposites") -> + | IDENT "coercion" ; + t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ; + arity = OPT int ; saturations = OPT int; + composites = OPT (IDENT "nocomposites") -> let arity = match arity with None -> 0 | Some x -> x in let saturations = match saturations with None -> 0 | Some x -> x in let composites = match composites with None -> true | Some _ -> false in GrafiteAst.Coercion - (loc, UriManager.uri_of_string suri, composites, arity, saturations) + (loc, t, composites, arity, saturations) | IDENT "record" ; (params,name,ty,fields) = record_spec -> GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields)) | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> diff --git a/helm/software/matita/contribs/dama/dama/bishop_set.ma b/helm/software/matita/contribs/dama/dama/bishop_set.ma index 9fee3d9fd..8cb77ec24 100644 --- a/helm/software/matita/contribs/dama/dama/bishop_set.ma +++ b/helm/software/matita/contribs/dama/dama/bishop_set.ma @@ -101,12 +101,12 @@ interpretation "bishop set subset" 'subset a b = (bs_subset _ a b). definition square_bishop_set : bishop_set → bishop_set. intro S; apply (mk_bishop_set (S × S)); -[1: intros (x y); apply ((fst x # fst y) ∨ (snd x # snd y)); +[1: intros (x y); apply ((\fst x # \fst y) ∨ (\snd x # \snd y)); |2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X); |3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X); |4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H; - [1: cases (bs_cotransitive ??? (fst z) X); [left;left|right;left]assumption; - |2: cases (bs_cotransitive ??? (snd z) X); [left;right|right;right]assumption;]] + [1: cases (bs_cotransitive ??? (\fst z) X); [left;left|right;left]assumption; + |2: cases (bs_cotransitive ??? (\snd z) X); [left;right|right;right]assumption;]] qed. notation "s 2 \atop \neq" non associative with precedence 90 diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma index a0a701694..b8b33f8e6 100644 --- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma +++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "logic/equality.ma". +include "datatypes/constructors.ma". inductive Or (A,B:CProp) : CProp ≝ | Left : A → Or A B @@ -39,48 +40,22 @@ notation < "a ∧ b ∧ c ∧ d" with precedence 35 for @{'and4 $a $b $c $d}. interpretation "constructive quaternary and" 'and4 x y z t = (Conj4 x y z t). -coinductive product (A,B:Type) : Type ≝ pair : ∀a:A.∀b:B.product A B. - -notation "a \times b" left associative with precedence 70 for @{'product $a $b}. -interpretation "prod" 'product a b = (product a b). - -definition first : ∀A.∀P.A × P → A ≝ λA,P,s.match s with [pair x _ ⇒ x]. -definition second : ∀A.∀P.A × P → P ≝ λA,P,s.match s with [pair _ y ⇒ y]. - -interpretation "pair pi1" 'pi1 = (first _ _). -interpretation "pair pi2" 'pi2 = (second _ _). -interpretation "pair pi1" 'pi1a x = (first _ _ x). -interpretation "pair pi2" 'pi2a x = (second _ _ x). -interpretation "pair pi1" 'pi1b x y = (first _ _ x y). -interpretation "pair pi2" 'pi2b x y = (second _ _ x y). - -notation "hvbox(\langle term 19 a, break term 19 b\rangle)" -with precedence 90 for @{ 'pair $a $b}. -interpretation "pair" 'pair a b = (pair _ _ a b). - inductive exT (A:Type) (P:A→CProp) : CProp ≝ ex_introT: ∀w:A. P w → exT A P. interpretation "CProp exists" 'exists \eta.x = (exT _ x). interpretation "dependent pair" 'pair a b = (ex_introT _ _ a b). -notation < "'fst' \nbsp x" non associative with precedence 90 for @{'pi1a $x}. -notation < "'snd' \nbsp x" non associative with precedence 90 for @{'pi2a $x}. -notation < "'fst' \nbsp x \nbsp y" non associative with precedence 90 for @{'pi1b $x $y}. -notation < "'snd' \nbsp x \nbsp y" non associative with precedence 90 for @{'pi2b $x $y}. -notation > "'fst'" non associative with precedence 90 for @{'pi1}. -notation > "'snd'" non associative with precedence 90 for @{'pi2}. - 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). +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. @@ -90,12 +65,12 @@ definition pi1exT23 ≝ 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). +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. diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma index af0a11453..c5a256a00 100644 --- a/helm/software/matita/contribs/dama/dama/lebesgue.ma +++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma @@ -72,10 +72,10 @@ split; [1: intro j; cases (Hxy j); cases H3; cases H4; split; [apply (H5 0);|apply (H7 0)] |2: cases (H l u Xi 〈?,h〉) (Ux Uy); apply Ux; cases Hx; split; [apply H3;] - cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy]; + cases H4; split; [apply H5] intros (y Hy);cases (H6 (\fst y));[2:apply Hy]; exists [apply w] apply H7; |3: cases (H l u Yi 〈?,h〉) (Ux Uy); apply Uy; cases Hy; split; [apply H3;] - cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy]; + cases H4; split; [apply H5] intros (y Hy);cases (H6 (\fst y));[2:apply Hy]; exists [apply w] apply H7;]] qed. diff --git a/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma b/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma index 8063ea0bf..412b5407d 100644 --- a/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma +++ b/helm/software/matita/contribs/dama/dama/models/discrete_uniformity.ma @@ -21,7 +21,7 @@ intro C; apply (mk_uniform_space C); alias symbol "pi2" = "pair pi2". alias symbol "pi1" = "pair pi1". alias symbol "and" = "logical and". - apply (∃_:unit.∀n:C square.(fst n ≈ snd n → P n) ∧ (P n → fst n ≈ snd n)); + apply (∃_:unit.∀n:C square.(\fst n ≈ \snd n → P n) ∧ (P n → \fst n ≈ \snd n)); |2: intros 4 (U H x Hx); simplify in Hx; cases H (_ H1); cases (H1 x); apply H2; apply Hx; |3: intros; cases H (_ PU); cases H1 (_ PV); @@ -34,8 +34,8 @@ intro C; apply (mk_uniform_space C); [1: exists [apply something] intro n; cases (PU n); split; intros; try split;[apply H1;|apply H2] assumption; |2: intros 2 (x Hx); cases Hx; cases H1; clear H1; - cases (PU 〈(fst x),x1〉); lapply (H4 H2) as H5; simplify in H5; - cases (PU 〈x1,(snd x)〉); lapply (H7 H3) as H8; simplify in H8; + cases (PU 〈(\fst x),x1〉); lapply (H4 H2) as H5; simplify in H5; + cases (PU 〈x1,(\snd x)〉); lapply (H7 H3) as H8; simplify in H8; generalize in match H5; generalize in match H8; generalize in match (PU x); clear H6 H7 H1 H4 H2 H3 H5 H8; cases x; simplify; intros; cases H1; clear H1; apply H4; diff --git a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma index 0908b6f70..bc009b5c6 100644 --- a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma +++ b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma @@ -28,14 +28,16 @@ cases (nat_compare n m); intros; [constructor 1|constructor 2|constructor 3] assumption; qed. -alias symbol "pi1" = "exT fst". +alias symbol "pi1" = "exT \fst". alias symbol "leq" = "natural 'less or equal to'". 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). + ∀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〉); fold normalize X; intros; cases H1; -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 "plus" = "natural plus". +alias symbol "nat" = "Uniform space N". +letin spec ≝ (λi,j:ℕ.(u≤i ∧ s = \fst (a j)) ∨ (i < u ∧ s+i ≤ u + \fst (a j))); (* s - aj <= max 0 (u - i) *) letin m ≝ (hide ? ( let rec aux i ≝ match i with @@ -43,10 +45,10 @@ letin m ≝ (hide ? ( | S m ⇒ let pred ≝ aux m in let apred ≝ a pred in - match cmp_nat (fst apred) s with + match cmp_nat (\fst apred) s with [ cmp_eq _ ⇒ pred | cmp_gt nP ⇒ match ? in False return λ_.nat with [] - | cmp_lt nP ⇒ fst (H3 apred nP)]] + | cmp_lt nP ⇒ \fst (H3 apred nP)]] in aux : ∀i:nat.∃j:nat.spec i j));unfold spec in aux ⊢ %; @@ -59,7 +61,7 @@ letin m ≝ (hide ? ( rewrite > (?:s = O); [2: cases Hs; lapply (os_le_to_nat_le ?? H1); apply (symmetric_eq nat O s ?).apply (le_n_O_to_eq s ?).apply (Hletin). - |1: intros; lapply (os_le_to_nat_le (fst (a O)) O (H2 O)); + |1: intros; lapply (os_le_to_nat_le (\fst (a O)) O (H2 O)); lapply (le_n_O_to_eq ? Hletin); assumption;] |2: right; cases Hs; rewrite > (sym_plus s O); split; [apply le_S_S; apply le_O_n]; apply (trans_le ??? (os_le_to_nat_le ?? H1)); @@ -79,21 +81,21 @@ letin m ≝ (hide ? ( [1,3: left; split; [1,3: assumption |2: symmetry; assumption] cut (u = S n1); [2: apply le_to_le_to_eq; assumption ] clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut; - cut (s = S (fst (a w))); + cut (s = S (\fst (a w))); [2: apply le_to_le_to_eq; [2: assumption] - change in H8 with (s + n1 ≤ S (n1 + fst (a w))); + change in H8 with (s + n1 ≤ S (n1 + \fst (a w))); rewrite > plus_n_Sm in H8; rewrite > sym_plus in H8; apply (le_plus_to_le ??? H8);] cases (H3 (a w) H6); - change with (s = fst (a w1)); - change in H4 with (fst (a w) < fst (a w1)); + change with (s = \fst (a w1)); + change in H4 with (\fst (a w) < \fst (a w1)); apply le_to_le_to_eq; [ rewrite > Hcut; assumption ] - apply (os_le_to_nat_le (fst (a w1)) s (H2 w1)); + apply (os_le_to_nat_le (\fst (a w1)) s (H2 w1)); |*: right; split; try assumption; [1: rewrite > sym_plus in ⊢ (? ? %); rewrite < H6; apply le_plus_r; assumption; |2: cases (H3 (a w) H6); - change with (s + S n1 ≤ u + fst (a w1));rewrite < plus_n_Sm; + change with (s + S n1 ≤ u + \fst (a w1));rewrite < plus_n_Sm; apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm; apply (le_plus ???? (le_n ?) H9);]]]]] clearbody m; unfold spec in m; clear spec; @@ -101,20 +103,20 @@ letin find ≝ ( let rec find i u on u : nat ≝ match u with [ O ⇒ (m i:nat) - | S w ⇒ match eqb (fst (a (m i))) s with + | S w ⇒ match eqb (\fst (a (m i))) s with [ true ⇒ (m i:nat) | false ⇒ find (S i) w]] in find : - ∀i,bound.∃j.i + bound = u → s = fst (a j)); -[1: cases (find (S n) n2); intro; change with (s = fst (a w)); + ∀i,bound.∃j.i + bound = u → s = \fst (a j)); +[1: cases (find (S n) n2); intro; change with (s = \fst (a w)); apply H6; rewrite < H7; simplify; apply plus_n_Sm; |2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity |3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1; cases (m u); cases H4; clear H4; cases H5; clear H5; [assumption] cases (not_le_Sn_n ? H4)] clearbody find; cases (find O u); -exists [apply w]; intros; change with (s = fst (a j)); +exists [apply w]; intros; change with (s = \fst (a j)); rewrite > (H4 ?); [2: reflexivity] apply le_to_le_to_eq; [1: apply os_le_to_nat_le; @@ -123,8 +125,9 @@ apply le_to_le_to_eq; rewrite < (H4 ?); [2: reflexivity] apply le_n;] qed. -alias symbol "pi1" = "exT fst". +alias symbol "pi1" = "exT \fst". alias symbol "leq" = "natural 'less or equal to'". +alias symbol "nat" = "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). + ∀x.x is_infimum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j). diff --git a/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma index d1ea3e46b..5291a23fd 100644 --- a/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma +++ b/helm/software/matita/contribs/dama/dama/models/nat_ordered_uniform.ma @@ -22,7 +22,7 @@ simplify; intros 7; cases H3; cases H (_); cases (H8 y); apply H9; cases (H8 p); lapply (H12 H1) as H13; apply (le_le_eq); [1: apply (le_transitive ???? H4); apply (Le≪ ? H13); assumption; -|2: apply (le_transitive ????? H5); apply (Le≫ (snd p) H13); assumption;] +|2: apply (le_transitive ????? H5); apply (Le≫ (\snd p) H13); assumption;] qed. interpretation "Ordered uniform space N" 'nat = nat_ordered_uniform_space. diff --git a/helm/software/matita/contribs/dama/dama/models/q_function.ma b/helm/software/matita/contribs/dama/dama/models/q_function.ma index a1ed8fa00..8f0f472a9 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_function.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma @@ -54,7 +54,7 @@ interpretation "list nth" 'nth = (cic:/matita/list/list/nth.con _). interpretation "list nth" 'nth_appl l d i = (cic:/matita/list/list/nth.con _ l d i). notation < "\rationals \sup 2" non associative with precedence 90 for @{'q2}. -interpretation "Q x Q" 'q2 = (product Q Q). +interpretation "Q x Q" 'q2 = (Prod Q Q). let rec make_list (A:Type) (def:nat→A) (n:nat) on n ≝ match n with @@ -67,15 +67,14 @@ notation < "'mk_list' \nbsp f \nbsp n" with precedence 71 for @{'mk_list_appl $f $n}. interpretation "'mk_list' appl" 'mk_list_appl f n = (make_list _ f n). -alias symbol "pair" = "pair". definition q0 : ℚ × ℚ ≝ 〈OQ,OQ〉. notation < "0 \sub \rationals" with precedence 90 for @{'q0}. interpretation "q0" 'q0 = q0. notation < "[ \rationals \sup 2]" with precedence 90 for @{'lq2}. -interpretation "lq2" 'lq2 = (list (product Q Q)). +interpretation "lq2" 'lq2 = (list (Prod Q Q)). notation < "[ \rationals \sup 2] \sup 2" with precedence 90 for @{'lq22}. -interpretation "lq22" 'lq22 = (product (list (product Q Q)) (list (product Q Q))). +interpretation "lq22" 'lq22 = (Prod (list (Prod Q Q)) (list (Prod Q Q))). notation "'len'" with precedence 90 for @{'len}. @@ -83,56 +82,54 @@ interpretation "len" 'len = length. notation < "'len' \nbsp l" with precedence 70 for @{'len_appl $l}. interpretation "len appl" 'len_appl l = (length _ l). -alias symbol "pi1" = "exT fst". definition eject ≝ λP.λp:∃x:(list (ℚ × ℚ)) × (list (ℚ × ℚ)).P x.match p with [ex_introT p _ ⇒ p]. coercion cic:/matita/dama/models/q_function/eject.con. definition inject ≝ λP.λp:(list (ℚ × ℚ)) × (list (ℚ × ℚ)).λh:P p. ex_introT ? P p h. +(*coercion inject with 0 1 nocomposites.*) coercion cic:/matita/dama/models/q_function/inject.con 0 1 nocomposites. +definition cb0h ≝ (λl.mk_list (λi.〈\fst (nth l q0 i),OQ〉) (length ? l)). + alias symbol "pi2" = "pair pi2". alias symbol "pi1" = "pair pi1". -alias symbol "pair" = "pair". definition rebase: q_f → q_f → ∃p:q_f × q_f.∀i. - fst (nth (bars (fst p)) q0 i) = - fst (nth (bars (snd p)) q0 i). + \fst (nth (bars (\fst p)) q0 i) = + \fst (nth (bars (\snd p)) q0 i). intros (f1 f2); cases f1 (s1 l1); cases f2 (s2 l2); clear f1 f2; -letin aux ≝ ( +letin spec ≝ (λl1,l2:list (ℚ × ℚ).λm:nat.λz:(list (ℚ × ℚ)) × (list (ℚ × ℚ)).True); +letin aux ≝ ( let rec aux (l1,l2:list (ℚ × ℚ)) (n:nat) on n : (list (ℚ × ℚ)) × (list (ℚ × ℚ)) ≝ match n with [ O ⇒ 〈[],[]〉 | S m ⇒ match l1 with - [ nil ⇒ - let copy_l2_with_0 ≝ mk_list (λi.〈fst (nth l2 q0 i),OQ〉) (length ? l2) in - 〈copy_l2_with_0, l2〉 - | cons he1 tl1 ⇒〈[],[]〉 (* + [ nil ⇒ 〈cb0h l2, l2〉 + | cons he1 tl1 ⇒ match l2 with - [ nil ⇒ - let copy_l1_with_0 ≝ mk_list (λi.〈fst (nth l1 q0 i),OQ〉) (length ? l1) in - 〈l1, copy_l1_with_0〉 - | cons he2 tl2 ⇒ - let base1 ≝ fst he1 in - let base2 ≝ fst he2 in - let height1 ≝ snd he1 in - let height2 ≝ snd he2 in + [ nil ⇒ 〈l1, cb0h l1〉 + | cons he2 tl2 ⇒ + let base1 ≝ (\fst he1) in + let base2 ≝ (\fst he2) in + let height1 ≝ (\snd he1) in + let height2 ≝ (\snd he2) in match q_cmp base1 base2 with [ q_eq _ ⇒ let rc ≝ aux tl1 tl2 m in - 〈he1 :: fst rc,he2 :: snd rc〉 + 〈he1 :: \fst rc,he2 :: \snd rc〉 | q_lt _ ⇒ let rest ≝ base2 - base1 in let rc ≝ aux tl1 (〈rest,height2〉 :: tl2) m in - 〈〈base1,height1〉 :: fst rc,〈base1,height2〉 :: snd rc〉 + 〈〈base1,height1〉 :: \fst rc,〈base1,height2〉 :: \snd rc〉 | q_gt _ ⇒ let rest ≝ base1 - base2 in let rc ≝ aux (〈rest,height1〉 :: tl1) tl2 m in - 〈〈base2,height1〉 :: fst rc,〈base2,height2〉 :: snd rc〉 -]]*)]] -in aux : ∀l1,l2,m.∃p.True); + 〈〈base2,height1〉 :: \fst rc,〈base2,height2〉 :: \snd rc〉 +]]]] +in aux); : ∀l1,l2,m.∃z.spec l1 l2 m z); cases (q_cmp s1 s2); [1: apply (mk_q_f s1); diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma index a820eff54..a227af3c1 100644 --- a/helm/software/matita/contribs/dama/dama/ordered_set.ma +++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma @@ -52,7 +52,7 @@ qed. lemma square_ordered_set: ordered_set → ordered_set. intro O; apply (mk_ordered_set (O × O)); -[1: intros (x y); apply (fst x ≰ fst y ∨ snd x ≰ snd y); +[1: intros (x y); apply (\fst x ≰ \fst y ∨ \snd x ≰ \snd y); |2: intro x0; cases x0 (x y); clear x0; simplify; intro H; cases H (X X); apply (os_coreflexive ?? X); |3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2); diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma index 326681b26..7d80f7081 100644 --- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma +++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma @@ -39,7 +39,7 @@ record ordered_uniform_space : Type ≝ { definition invert_os_relation ≝ λC:ordered_set.λU:C square → Prop. - λx:C square. U 〈snd x,fst x〉. + λx:C square. U 〈\snd x,\fst x〉. interpretation "relation invertion" 'invert a = (invert_os_relation _ a). interpretation "relation invertion" 'invert_symbol = (invert_os_relation _). @@ -47,17 +47,17 @@ interpretation "relation invertion" 'invert_appl a x = (invert_os_relation _ a x lemma segment_square_of_ordered_set_square: ∀O:ordered_set.∀u,v:O.∀x:O square. - fst x ∈ [u,v] → snd x ∈ [u,v] → {[u,v]} square. -intros; split; exists; [1: apply (fst x) |3: apply (snd x)] assumption; + \fst x ∈ [u,v] → \snd x ∈ [u,v] → {[u,v]} square. +intros; split; exists; [1: apply (\fst x) |3: apply (\snd x)] assumption; qed. coercion cic:/matita/dama/ordered_uniform/segment_square_of_ordered_set_square.con 0 2. -alias symbol "pi1" (instance 4) = "exT fst". -alias symbol "pi1" (instance 2) = "exT fst". +alias symbol "pi1" (instance 4) = "exT \fst". +alias symbol "pi1" (instance 2) = "exT \fst". lemma ordered_set_square_of_segment_square : ∀O:ordered_set.∀u,v:O.{[u,v]} square → O square ≝ - λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉. + λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈\fst(\fst b),\fst(\snd b)〉. coercion cic:/matita/dama/ordered_uniform/ordered_set_square_of_segment_square.con. @@ -87,14 +87,14 @@ lemma invert_restriction_agreement: restriction_agreement ? l r U 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);] +[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);] qed. alias symbol "square" (instance 8) = "bishop set square". lemma bs_of_ss: ∀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)〉. + λ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). @@ -104,9 +104,9 @@ alias symbol "pair" (instance 4) = "dependent pair". alias symbol "pair" (instance 2) = "dependent pair". lemma ss_of_bs: ∀O:ordered_set.∀u,v:O. - ∀b:O square.fst b ∈ [u,v] → snd b ∈ [u,v] → {[u,v]} square ≝ + ∀b:O square.\fst b ∈ [u,v] → \snd b ∈ [u,v] → {[u,v]} square ≝ λO:ordered_set.λu,v:O. - λb:(O:bishop_set) square.λH1,H2.〈〈fst b,H1〉,〈snd b,H2〉〉. + λ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 _ _). @@ -140,7 +140,7 @@ intros (O l r); apply mk_ordered_uniform_space; unfold segment_square_of_ordered_set_square; cases b; intros; split; intro; assumption; |2: intros 2 (x Hx); apply (restrict ?????? HuU); apply Hwu; - cases Hx (m Hm); exists[apply (fst m)] apply Hm;] + cases Hx (m Hm); exists[apply (\fst m)] apply Hm;] |4: intros (U HU x); cases HU (u Hu); cases Hu (Gu HuU); clear HU Hu; cases (us_phi4 ?? Gu x) (Hul Hur); split; intros; @@ -161,12 +161,12 @@ interpretation "Ordered uniform space segment" 'segment_set a b = (segment_ordered_uniform_space _ a b). (* Lemma 3.2 *) -alias symbol "pi1" = "exT fst". +alias symbol "pi1" = "exT \fst". lemma restric_uniform_convergence: ∀O:ordered_uniform_space.∀l,u:O. ∀x:{[l,u]}. ∀a:sequence {[l,u]}. - ⌊n,fst (a n)⌋ uniform_converges (fst x) → + ⌊n,\fst (a n)⌋ uniform_converges (\fst x) → a uniform_converges x. intros 8; cases H1; cases H2; clear H2 H1; cases (H ? H3) (m Hm); exists [apply m]; intros; diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma index 58de86885..d04ec1acc 100644 --- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma +++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma @@ -23,39 +23,39 @@ definition exhaustive ≝ (b is_decreasing → b is_lower_located → b is_cauchy). lemma segment_upperbound: - ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.u is_upper_bound ⌊n,fst (a n)⌋. -intros 5; change with (fst (a n) ≤ u); cases (a n); cases H; assumption; + ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.u is_upper_bound ⌊n,\fst (a n)⌋. +intros 5; change with (\fst (a n) ≤ u); cases (a n); cases H; assumption; qed. lemma segment_lowerbound: - ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.l is_lower_bound ⌊n,fst (a n)⌋. -intros 5; change with (l ≤ fst (a n)); cases (a n); cases H; assumption; + ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.l is_lower_bound ⌊n,\fst (a n)⌋. +intros 5; change with (l ≤ \fst (a n)); cases (a n); cases H; assumption; qed. lemma segment_preserves_uparrow: ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.∀x,h. - ⌊n,fst (a n)⌋ ↑ x → a ↑ 〈x,h〉. + ⌊n,\fst (a n)⌋ ↑ x → a ↑ 〈x,h〉. intros; cases H (Ha Hx); split [apply Ha] cases Hx; split; [apply H1] intros; -cases (H2 (fst y)); [2: apply H3;] exists [apply w] assumption; +cases (H2 (\fst y)); [2: apply H3;] exists [apply w] assumption; qed. lemma segment_preserves_downarrow: ∀C:ordered_set.∀l,u:C.∀a:sequence {[l,u]}.∀x,h. - ⌊n,fst (a n)⌋ ↓ x → a ↓ 〈x,h〉. + ⌊n,\fst (a n)⌋ ↓ x → a ↓ 〈x,h〉. intros; cases H (Ha Hx); split [apply Ha] cases Hx; split; [apply H1] intros; -cases (H2 (fst y));[2:apply H3]; exists [apply w] assumption; +cases (H2 (\fst y));[2:apply H3]; exists [apply w] assumption; qed. (* Fact 2.18 *) lemma segment_cauchy: ∀C:ordered_uniform_space.∀l,u:C.∀a:sequence {[l,u]}. - a is_cauchy → ⌊n,fst (a n)⌋ is_cauchy. + a is_cauchy → ⌊n,\fst (a n)⌋ is_cauchy. intros 7; alias symbol "pi1" (instance 3) = "pair pi1". alias symbol "pi2" = "pair pi2". -apply (H (λx:{[l,u]} square.U 〈fst (fst x),fst (snd x)〉)); +apply (H (λx:{[l,u]} square.U 〈\fst (\fst x),\fst (\snd x)〉)); (unfold segment_ordered_uniform_space; simplify); exists [apply U] split; [assumption;] intro; cases b; intros; simplify; split; intros; assumption; @@ -65,7 +65,7 @@ qed. lemma restrict_uniform_convergence_uparrow: ∀C:ordered_uniform_space.property_sigma C → ∀l,u:C.exhaustive {[l,u]} → - ∀a:sequence {[l,u]}.∀x:C. ⌊n,fst (a n)⌋ ↑ x → + ∀a:sequence {[l,u]}.∀x:C. ⌊n,\fst (a n)⌋ ↑ x → x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges 〈x,h〉. intros; cases H2 (Ha Hx); clear H2; cases Hx; split; [1: split; @@ -87,7 +87,7 @@ qed. lemma restrict_uniform_convergence_downarrow: ∀C:ordered_uniform_space.property_sigma C → ∀l,u:C.exhaustive {[l,u]} → - ∀a:sequence {[l,u]}.∀x:C. ⌊n,fst (a n)⌋ ↓ x → + ∀a:sequence {[l,u]}.∀x:C. ⌊n,\fst (a n)⌋ ↓ x → x∈[l,u] ∧ ∀h:x ∈ [l,u].a uniform_converges 〈x,h〉. intros; cases H2 (Ha Hx); clear H2; cases Hx; split; [1: split; diff --git a/helm/software/matita/contribs/dama/dama/property_sigma.ma b/helm/software/matita/contribs/dama/dama/property_sigma.ma index 672099281..2e0e73bc6 100644 --- a/helm/software/matita/contribs/dama/dama/property_sigma.ma +++ b/helm/software/matita/contribs/dama/dama/property_sigma.ma @@ -63,7 +63,7 @@ lemma sigma_cauchy: ∀C:ordered_uniform_space.property_sigma C → ∀a:sequence C.∀l:C.(a ↑ l ∨ a ↓ l) → a is_cauchy → a uniform_converges l. intros 8; cases (H ? H3) (w H5); cases H5 (H8 H9); clear H5; -alias symbol "pair" = "pair". +alias symbol "pair" = "Pair construction". letin spec ≝ (λz,k:nat.∀i,j,l:nat.k ≤ i → k ≤ j → l ≤ z → w l 〈a i,a j〉); letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝ match i with diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma index f53cdc458..a48eb164a 100644 --- a/helm/software/matita/contribs/dama/dama/supremum.ma +++ b/helm/software/matita/contribs/dama/dama/supremum.ma @@ -240,7 +240,7 @@ interpretation "Ordered set sergment in" 'segment_in a b x= (segment _ a b x). lemma segment_ordered_set: ∀O:ordered_set.∀u,v:O.ordered_set. intros (O u v); apply (mk_ordered_set (∃x.x ∈ [u,v])); -[1: intros (x y); apply (fst x ≰ fst y); +[1: intros (x y); apply (\fst x ≰ \fst y); |2: intro x; cases x; simplify; apply os_coreflexive; |3: intros 3 (x y z); cases x; cases y ; cases z; simplify; apply os_cotransitive] qed. @@ -253,24 +253,24 @@ interpretation "Ordered set segment" 'segment_set a b = (* Lemma 2.9 *) lemma segment_preserves_supremum: ∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}. - ⌊n,fst (a n)⌋ is_increasing ∧ - (fst x) is_supremum ⌊n,fst (a n)⌋ → a ↑ x. + ⌊n,\fst (a n)⌋ is_increasing ∧ + (\fst x) is_supremum ⌊n,\fst (a n)⌋ → a ↑ x. intros; split; cases H; clear H; [1: apply H1; |2: cases H2; split; clear H2; [1: apply H; - |2: clear H; intro y0; apply (H3 (fst y0));]] + |2: clear H; intro y0; apply (H3 (\fst y0));]] qed. lemma segment_preserves_infimum: ∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}. - ⌊n,fst (a n)⌋ is_decreasing ∧ - (fst x) is_infimum ⌊n,fst (a n)⌋ → a ↓ x. + ⌊n,\fst (a n)⌋ is_decreasing ∧ + (\fst x) is_infimum ⌊n,\fst (a n)⌋ → a ↓ x. intros; split; cases H; clear H; [1: apply H1; |2: cases H2; split; clear H2; [1: apply H; - |2: clear H; intro y0; apply (H3 (fst y0));]] + |2: clear H; intro y0; apply (H3 (\fst y0));]] qed. (* Definition 2.10 *) @@ -279,11 +279,11 @@ alias symbol "pi2" = "pair pi2". alias symbol "pi1" = "pair pi1". definition square_segment ≝ λO:ordered_set.λa,b:O.λx:O square. - And4 (fst x ≤ b) (a ≤ fst x) (snd x ≤ b) (a ≤ snd x). + And4 (\fst x ≤ b) (a ≤ \fst x) (\snd x ≤ b) (a ≤ \snd x). definition convex ≝ λO:ordered_set.λU:O square → Prop. - ∀p.U p → fst p ≤ snd p → ∀y. square_segment ? (fst p) (snd p) y → U y. + ∀p.U p → \fst p ≤ \snd p → ∀y. square_segment ? (\fst p) (\snd p) y → U y. (* Definition 2.11 *) definition upper_located ≝ diff --git a/helm/software/matita/contribs/dama/dama/uniform.ma b/helm/software/matita/contribs/dama/dama/uniform.ma index ed9e6fe5d..82278eb08 100644 --- a/helm/software/matita/contribs/dama/dama/uniform.ma +++ b/helm/software/matita/contribs/dama/dama/uniform.ma @@ -17,23 +17,23 @@ include "supremum.ma". (* Definition 2.13 *) alias symbol "square" = "bishop set square". -alias symbol "pair" = "pair". +alias symbol "pair" = "Pair construction". alias symbol "exists" = "exists". alias symbol "and" = "logical and". definition compose_bs_relations ≝ λC:bishop_set.λU,V:C square → Prop. - λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉. + λx:C square.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉. definition compose_os_relations ≝ λC:ordered_set.λU,V:C square → Prop. - λx:C square.∃y:C. U 〈fst x,y〉 ∧ V 〈y,snd x〉. + λx:C square.∃y:C. U 〈\fst x,y〉 ∧ V 〈y,\snd x〉. interpretation "bishop set relations composition" 'compose a b = (compose_bs_relations _ a b). interpretation "ordered set relations composition" 'compose a b = (compose_os_relations _ a b). definition invert_bs_relation ≝ λC:bishop_set.λU:C square → Prop. - λx:C square. U 〈snd x,fst x〉. + λ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 @@ -52,7 +52,7 @@ record uniform_space : Type ≝ { us_carr:> bishop_set; us_unifbase: (us_carr square → Prop) → CProp; us_phi1: ∀U:us_carr square → Prop. us_unifbase U → - (λx:us_carr square.fst x ≈ snd x) ⊆ U; + (λx:us_carr square.\fst x ≈ \snd x) ⊆ U; us_phi2: ∀U,V:us_carr square → Prop. us_unifbase U → us_unifbase V → ∃W:us_carr square → Prop.us_unifbase W ∧ (W ⊆ (λx.U x ∧ V x)); us_phi3: ∀U:us_carr square → Prop. us_unifbase U → diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo index 15912d264..c6e3d6015 100644 --- a/helm/software/matita/core_notation.moo +++ b/helm/software/matita/core_notation.moo @@ -4,6 +4,21 @@ for @{ 'exists ${default @{\lambda ${ident i} : $ty. $p} @{\lambda ${ident i} . $p}}}. +notation "hvbox(\langle term 19 a, break term 19 b\rangle)" +with precedence 90 for @{ 'pair $a $b}. + +notation "hvbox(x break \times y)" with precedence 70 +for @{ 'product $x $y}. + +notation < "\fst \nbsp x" non associative with precedence 69 for @{'pi1a $x}. +notation < "\snd \nbsp x" non associative with precedence 69 for @{'pi2a $x}. + +notation < "\fst \nbsp x \nbsp y" non associative with precedence 69 for @{'pi1b $x $y}. +notation < "\snd \nbsp x \nbsp y" non associative with precedence 69 for @{'pi2b $x $y}. + +notation > "\fst" non associative with precedence 90 for @{'pi1}. +notation > "\snd" non associative with precedence 90 for @{'pi2}. + notation "hvbox(a break \to b)" right associative with precedence 20 for @{ \forall $_:$a.$b }. diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml index 4fe77d7b7..4d788f39a 100644 --- a/helm/software/matita/help/C/sec_commands.xml +++ b/helm/software/matita/help/C/sec_commands.xml @@ -76,24 +76,34 @@ coercion - coercion u + coercion u with ariety saturation nocomposites Synopsis: - coercion &uri; + + coercion + (&uri; | &term; with) + [ &nat; [&nat;]] + [ nocomposites ] + Action: - Declares u as an implicit coercion - from the type of its last argument (source) - to its codomain (target). Every time a term x + Declares u as an implicit coercion. + If the type of u is + ∀x1:T1. … ∀x(n-1):T(n-1).Tn the coercion target is + T(n - ariety) while its source is + T(n - ariety - saturation - 1). + Every time a term x of type source is used with expected type target, Matita automatically replaces x with - (u ? … ? x) to avoid a typing error. + (u ? … ? x ? … ?) to avoid a typing error. + Note that the number of ? added after + x is saturation. Implicit coercions are not displayed to the user: (u ? … ? x) is rendered simply as x. @@ -102,7 +112,8 @@ and there is already a coercion u' of target s or source t, a composite implicit coercion is automatically computed - by Matita. + by Matita unless nocomposites + is specified. diff --git a/helm/software/matita/library/Q/frac.ma b/helm/software/matita/library/Q/frac.ma index e4a2fc566..9ce493604 100644 --- a/helm/software/matita/library/Q/frac.ma +++ b/helm/software/matita/library/Q/frac.ma @@ -62,9 +62,14 @@ match q with ]. *) +alias id "numeratorQ" = "cic:/matita/Q/q/q/numeratorQ.con". +alias id "nat" = "cic:/matita/nat/nat/nat.ind#xpointer(1/1)". +alias id "defactorize" = "cic:/matita/nat/factorization/defactorize.con". +alias id "Q" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1)". definition numQ:Q \to nat \def \lambda q. defactorize (numeratorQ q). +alias id "Qinv" = "cic:/matita/Q/q/qinv/Qinv.con". definition denomQ:Q \to nat \def \lambda q. defactorize (numeratorQ (Qinv q)). @@ -104,6 +109,8 @@ elim r ] qed.*) +alias id "Qpos" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/2)". +alias id "OQ" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/1)". definition Qabs:Q \to Q \def \lambda q. match q with [OQ \Rightarrow OQ diff --git a/helm/software/matita/library/Q/inv.ma b/helm/software/matita/library/Q/inv.ma index 31b2d8bc0..9cc2fc3b4 100644 --- a/helm/software/matita/library/Q/inv.ma +++ b/helm/software/matita/library/Q/inv.ma @@ -14,6 +14,7 @@ include "Q/q.ma". +alias id "finv" = "cic:/matita/Q/fraction/finv/finv.con". theorem denominator_integral_factor_finv: ∀f. enumerator_integral_fraction f = denominator_integral_fraction (finv f). intro; @@ -24,6 +25,7 @@ theorem denominator_integral_factor_finv: elim z; simplify; reflexivity] qed. +alias id "Qpos" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/2)". definition is_positive ≝ λq. match q with @@ -31,6 +33,7 @@ definition is_positive ≝ | _ ⇒ False ]. +alias id "Qneg" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/3)". definition is_negative ≝ λq. match q with @@ -38,6 +41,7 @@ definition is_negative ≝ | _ ⇒ False ]. +(* theorem is_positive_denominator_Qinv: ∀q. is_positive q → enumerator q = denominator (Qinv q). intro; @@ -87,3 +91,4 @@ theorem is_negative_enumerator_Qinv: assumption | elim q in H ⊢ %; assumption] qed. +*) \ No newline at end of file diff --git a/helm/software/matita/library/Q/q.ma b/helm/software/matita/library/Q/q.ma index 683ddeb88..51b66cacc 100644 --- a/helm/software/matita/library/Q/q.ma +++ b/helm/software/matita/library/Q/q.ma @@ -16,6 +16,8 @@ include "Z/compare.ma". include "Z/plus.ma". include "nat/factorization.ma". +alias id "pp" = "cic:/matita/Q/fraction/fraction/fraction.ind#xpointer(1/1/1)". +alias id "cons" = "cic:/matita/Q/fraction/fraction/fraction.ind#xpointer(1/1/3)". let rec enumerator_integral_fraction l ≝ match l with [ pp n ⇒ Some ? l @@ -57,6 +59,7 @@ let rec denominator_integral_fraction l ≝ ] ]. +(* definition enumerator_of_fraction ≝ λq. match q with @@ -94,3 +97,4 @@ definition denominator ≝ | Qpos r ⇒ denominator_of_fraction r | Qneg r ⇒ denominator_of_fraction r ]. +*) \ No newline at end of file diff --git a/helm/software/matita/library/Z/z.ma b/helm/software/matita/library/Z/z.ma index 6b750c44c..d598b7de8 100644 --- a/helm/software/matita/library/Z/z.ma +++ b/helm/software/matita/library/Z/z.ma @@ -25,7 +25,7 @@ definition Z_of_nat \def [ O \Rightarrow OZ | (S n)\Rightarrow pos n]. -coercion cic:/matita/Z/z/Z_of_nat.con. +coercion Z_of_nat. definition neg_Z_of_nat \def \lambda n. match n with diff --git a/helm/software/matita/library/datatypes/constructors.ma b/helm/software/matita/library/datatypes/constructors.ma index 926dd35fc..d8130d714 100644 --- a/helm/software/matita/library/datatypes/constructors.ma +++ b/helm/software/matita/library/datatypes/constructors.ma @@ -24,15 +24,9 @@ pair : A \to B \to Prod A B. interpretation "Pair construction" 'pair x y = (cic:/matita/datatypes/constructors/Prod.ind#xpointer(1/1/1) _ _ x y). -notation "hvbox(\langle x break , y \rangle )" with precedence 89 -for @{ 'pair $x $y}. - interpretation "Product" 'product x y = (cic:/matita/datatypes/constructors/Prod.ind#xpointer(1/1) x y). -notation "hvbox(x break \times y)" with precedence 89 -for @{ 'product $x $y}. - definition fst \def \lambda A,B:Type.\lambda p: Prod A B. match p with [(pair a b) \Rightarrow a]. @@ -41,20 +35,15 @@ definition snd \def \lambda A,B:Type.\lambda p: Prod A B. match p with [(pair a b) \Rightarrow b]. -interpretation "First projection" 'fst x = - (cic:/matita/datatypes/constructors/fst.con _ _ x). - -notation "\fst x" with precedence 89 -for @{ 'fst $x}. - -interpretation "Second projection" 'snd x = - (cic:/matita/datatypes/constructors/snd.con _ _ x). - -notation "\snd x" with precedence 89 -for @{ 'snd $x}. +interpretation "pair pi1" 'pi1 = (fst _ _). +interpretation "pair pi2" 'pi2 = (snd _ _). +interpretation "pair pi1" 'pi1a x = (fst _ _ x). +interpretation "pair pi2" 'pi2a x = (snd _ _ x). +interpretation "pair pi1" 'pi1b x y = (fst _ _ x y). +interpretation "pair pi2" 'pi2b x y = (snd _ _ x y). theorem eq_pair_fst_snd: \forall A,B:Type.\forall p:Prod A B. -p = 〈 (\fst p), (\snd p) 〉. +p = 〈 \fst p, \snd p 〉. intros.elim p.simplify.reflexivity. qed. diff --git a/helm/software/matita/library/decidable_kit/eqtype.ma b/helm/software/matita/library/decidable_kit/eqtype.ma index 4b248a97e..fe3964c65 100644 --- a/helm/software/matita/library/decidable_kit/eqtype.ma +++ b/helm/software/matita/library/decidable_kit/eqtype.ma @@ -50,7 +50,7 @@ definition nat_eqType : eqType ≝ mk_eqType ? ? eqbP. (* XXX le coercion nel cast non vengono inserite *) definition nat_canonical_eqType : nat → nat_eqType := λn : nat.(n : sort nat_eqType). -coercion cic:/matita/decidable_kit/eqtype/nat_canonical_eqType.con. +coercion nat_canonical_eqType. definition bcmp ≝ λx,y:bool. match x with [ true ⇒ y | false => notb y ]. @@ -68,7 +68,7 @@ qed. definition bool_eqType : eqType ≝ mk_eqType ? ? bcmpP. definition bool_canonical_eqType : bool → bool_eqType := λb : bool.(b : sort bool_eqType). -coercion cic:/matita/decidable_kit/eqtype/bool_canonical_eqType.con. +coercion bool_canonical_eqType. (* ### subtype of an eqType ### *) @@ -136,7 +136,7 @@ qed. definition option_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (ocmpP d). definition option_canonical_eqType : ∀d:eqType.d → option_eqType d ≝ λd:eqType.λx:d.(Some ? x : sort (option_eqType d)). -coercion cic:/matita/decidable_kit/eqtype/option_canonical_eqType.con. +coercion option_canonical_eqType. (* belle le coercions! *) definition test_canonical_option_eqType ≝ diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma index 9e360caab..e8ab55c35 100644 --- a/helm/software/matita/library/demo/power_derivative.ma +++ b/helm/software/matita/library/demo/power_derivative.ma @@ -88,7 +88,7 @@ let rec inj (n:nat) on n : R ≝ ] ]. -coercion cic:/matita/demo/power_derivative/inj.con. +coercion inj. axiom Rplus_Rzero_x: ∀x:R.0+x=x. axiom Rplus_comm: symmetric ? Rplus. @@ -108,7 +108,7 @@ definition monomio ≝ definition costante : nat → R → R ≝ λa:nat.λx:R.inj a. -coercion cic:/matita/demo/power_derivative/costante.con 1. +coercion costante with 1. axiom f_eq_extensional: ∀f,g:R→R.(∀x:R.f x = g x) → f=g. diff --git a/helm/software/matita/library/logic/equality.ma b/helm/software/matita/library/logic/equality.ma index 308652d7d..cc181dfbf 100644 --- a/helm/software/matita/library/logic/equality.ma +++ b/helm/software/matita/library/logic/equality.ma @@ -81,8 +81,8 @@ intros.elim H.apply refl_eq. qed. (* *) -coercion cic:/matita/logic/equality/sym_eq.con. -coercion cic:/matita/logic/equality/eq_f.con. +coercion sym_eq. +coercion eq_f. (* *) default "equality" -- 2.39.2