From 4dc47c9675ffd5fa50296ffaa9b5997501518c98 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 15 Apr 2009 18:48:07 +0000 Subject: [PATCH] - transcript: bugfix - library: we removed most uri's. two still remain :( --- .../components/binaries/transcript/engine.ml | 12 +++-- .../binaries/transcript/grafiteParser.mly | 4 +- .../contribs/procedural/Makefile.common | 4 +- .../procedural/library/library.conf.xml | 1 + helm/software/matita/library/Q/frac.ma | 9 +--- helm/software/matita/library/Q/inv.ma | 5 +- helm/software/matita/library/Q/q.ma | 3 +- helm/software/matita/library/Q/q/qtimes.ma | 2 +- helm/software/matita/library/Z/plus.ma | 8 ++- helm/software/matita/library/Z/sigma_p.ma | 2 +- helm/software/matita/library/Z/times.ma | 3 +- .../matita/library/algebra/finite_groups.ma | 16 +++--- .../software/matita/library/algebra/groups.ma | 17 +++---- .../matita/library/dama/russell_support.ma | 4 +- helm/software/matita/library/dama/sequence.ma | 2 +- .../software/matita/library/datatypes/bool.ma | 9 ++-- .../matita/library/datatypes/constructors.ma | 9 ++-- .../matita/library/decidable_kit/eqtype.ma | 3 +- .../matita/library/demo/power_derivative.ma | 50 ++++++------------- .../matita/library/demo/realisability.ma | 4 +- helm/software/matita/library/depends | 44 ++++++++-------- .../library/didactic/exercises/duality.ma | 14 ++++++ .../didactic/exercises/natural_deduction.ma | 14 ++++++ .../didactic/exercises/natural_deduction1.ma | 16 +++++- .../exercises/natural_deduction_fst_order.ma | 14 ++++++ .../exercises/natural_deduction_theories.ma | 14 ++++++ .../library/didactic/exercises/shannon.ma | 14 ++++++ .../didactic/exercises/substitution.ma | 14 ++++++ .../didactic/support/natural_deduction.ma | 14 ++++++ .../library/higher_order_defs/functions.ma | 3 +- helm/software/matita/library/list/list.ma | 7 ++- .../matita/library/logic/connectives.ma | 13 ++--- .../software/matita/library/logic/equality.ma | 12 ++--- helm/software/matita/library/nat/chebyshev.ma | 2 +- .../software/matita/library/nat/congruence.ma | 3 +- .../matita/library/nat/div_and_mod.ma | 6 +-- .../matita/library/nat/euler_theorem.ma | 4 +- helm/software/matita/library/nat/exp.ma | 2 +- helm/software/matita/library/nat/factorial.ma | 2 +- helm/software/matita/library/nat/minus.ma | 3 +- helm/software/matita/library/nat/nat.ma | 2 +- helm/software/matita/library/nat/orders.ma | 18 +++---- .../matita/library/nat/permutation.ma | 3 +- helm/software/matita/library/nat/plus.ma | 3 +- helm/software/matita/library/nat/primes.ma | 5 +- helm/software/matita/library/nat/times.ma | 2 +- helm/software/matita/library/nat/totient1.ma | 2 +- 47 files changed, 233 insertions(+), 184 deletions(-) diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index 4504d2999..091987b65 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -49,6 +49,7 @@ type status = { input_type: T.input_kind; output_type: T.output_kind; input_ext: string; + remove_lines: int; includes: (string * string) list; coercions: (string * string) list; files: string list; @@ -115,13 +116,9 @@ let make registry = in load_registry registry; let input_type, input_ext = get_input_type "package.input_type" in - let heading_lines = match input_type with - | T.Grafite -> 0 - | _ -> R.get_int "transcript.heading_lines" - in let st = { heading_path = R.get_string "transcript.heading_path"; - heading_lines = heading_lines; + heading_lines = R.get_int "transcript.heading_lines"; input_package = R.get_string "package.input_name"; output_package = R.get_string "package.output_name"; input_base_uri = R.get_string "package.input_base_uri"; @@ -131,6 +128,7 @@ let make registry = input_type = input_type; output_type = get_output_type "package.output_type"; input_ext = input_ext; + remove_lines = R.get_int "package.heading_lines"; includes = get_pairs "package.include"; coercions = get_pairs "package.coercion"; files = []; @@ -242,9 +240,13 @@ let produce st = try require st name (List.assoc name st.includes) with Not_found -> () in + let rec remove_lines ich n = + if n > 0 then let _ = input_line ich in remove_lines ich (pred n) + in Printf.eprintf "processing file name: %s ...\n" name; flush stderr; let file = Filename.concat st.input_path (name ^ st.input_ext) in let ich = open_in file in + begin try remove_lines ich st.remove_lines with End_of_file -> () end; let lexbuf = Lexing.from_channel ich in try let items = get_items lexbuf in close_in ich; diff --git a/helm/software/components/binaries/transcript/grafiteParser.mly b/helm/software/components/binaries/transcript/grafiteParser.mly index 3163a6a07..1e6855f55 100644 --- a/helm/software/components/binaries/transcript/grafiteParser.mly +++ b/helm/software/components/binaries/transcript/grafiteParser.mly @@ -42,7 +42,7 @@ | "lemma" -> T.Con, Some `Lemma | "fact" -> T.Con, Some `Fact | "remark" -> T.Con, Some `Remark - | "variant" -> T.Con, None + | "variant" -> T.Con, Some `Variant | _ -> assert false %} @@ -127,7 +127,7 @@ { out "OK" $1; [T.Verbatim $1] } | TH SPC id line drops { out "TH" $3; - let a, b = mk_flavour $1 in [T.Inline (true, a, $3, "", b)] + let a, b = mk_flavour $1 in [T.Inline (false, a, $3, "", b)] } | UNX line drops { out "UNX" $1; [T.Verbatim ($1 ^ $2 ^ $3)] } diff --git a/helm/software/matita/contribs/procedural/Makefile.common b/helm/software/matita/contribs/procedural/Makefile.common index ea78a78b1..a6bc20571 100644 --- a/helm/software/matita/contribs/procedural/Makefile.common +++ b/helm/software/matita/contribs/procedural/Makefile.common @@ -8,6 +8,8 @@ MATITAOPTIONS = TRANSCRIPT = $(BIN)../components/binaries/transcript/transcript.opt +OPTIONS = + LOG = log.txt MMAS = $(shell find -name "*.mma") @@ -40,4 +42,4 @@ clean.ma: endif mma: $(DEVEL).conf.xml clean.ma - $(H)$(TRANSCRIPT) -g -C $(BIN) $(DEVEL) + $(H)$(TRANSCRIPT) $(OPTIONS) -C $(BIN) $(DEVEL) diff --git a/helm/software/matita/contribs/procedural/library/library.conf.xml b/helm/software/matita/contribs/procedural/library/library.conf.xml index 8165072d9..355234785 100644 --- a/helm/software/matita/contribs/procedural/library/library.conf.xml +++ b/helm/software/matita/contribs/procedural/library/library.conf.xml @@ -9,5 +9,6 @@ contribs/procedural/library grafite procedural + 14 diff --git a/helm/software/matita/library/Q/frac.ma b/helm/software/matita/library/Q/frac.ma index 9ce493604..863efe283 100644 --- a/helm/software/matita/library/Q/frac.ma +++ b/helm/software/matita/library/Q/frac.ma @@ -12,6 +12,8 @@ (* *) (**************************************************************************) +include "Q/q/qinv.ma". + (* let rec nat_fact_to_fraction_inv l \def match l with @@ -62,14 +64,9 @@ 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)). @@ -109,8 +106,6 @@ 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 9cc2fc3b4..4cc38f191 100644 --- a/helm/software/matita/library/Q/inv.ma +++ b/helm/software/matita/library/Q/inv.ma @@ -12,9 +12,10 @@ (* *) (**************************************************************************) +include "Q/q/q.ma". include "Q/q.ma". +include "Q/fraction/finv.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; @@ -25,7 +26,6 @@ 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 @@ -33,7 +33,6 @@ 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 diff --git a/helm/software/matita/library/Q/q.ma b/helm/software/matita/library/Q/q.ma index 51b66cacc..2e34b3c24 100644 --- a/helm/software/matita/library/Q/q.ma +++ b/helm/software/matita/library/Q/q.ma @@ -15,9 +15,8 @@ include "Z/compare.ma". include "Z/plus.ma". include "nat/factorization.ma". +include "Q/fraction/fraction.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 diff --git a/helm/software/matita/library/Q/q/qtimes.ma b/helm/software/matita/library/Q/q/qtimes.ma index 3b4b24b79..f03b8687c 100644 --- a/helm/software/matita/library/Q/q/qtimes.ma +++ b/helm/software/matita/library/Q/q/qtimes.ma @@ -33,7 +33,7 @@ definition Qtimes : Q \to Q \to Q \def ] ]. -interpretation "rational times" 'times x y = (cic:/matita/Q/q/qtimes/Qtimes.con x y). +interpretation "rational times" 'times x y = (Qtimes x y). theorem Qtimes_q_OQ: ∀q. q * OQ = OQ. intro; diff --git a/helm/software/matita/library/Z/plus.ma b/helm/software/matita/library/Z/plus.ma index 8fdeff3bc..00da44a00 100644 --- a/helm/software/matita/library/Z/plus.ma +++ b/helm/software/matita/library/Z/plus.ma @@ -38,8 +38,7 @@ definition Zplus :Z \to Z \to Z \def | GT \Rightarrow (neg (pred (m-n)))] | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))] ]. -(*CSC: the URI must disappear: there is a bug now *) -interpretation "integer plus" 'plus x y = (cic:/matita/Z/plus/Zplus.con x y). +interpretation "integer plus" 'plus x y = (Zplus x y). theorem Zplus_z_OZ: \forall z:Z. z+OZ = z. intro.elim z. @@ -256,8 +255,7 @@ definition Zopp : Z \to Z \def | (pos n) \Rightarrow (neg n) | (neg n) \Rightarrow (pos n) ]. -(*CSC: the URI must disappear: there is a bug now *) -interpretation "integer unary minus" 'uminus x = (cic:/matita/Z/plus/Zopp.con x). +interpretation "integer unary minus" 'uminus x = (Zopp x). theorem eq_OZ_Zopp_OZ : OZ = (- OZ). reflexivity. @@ -323,4 +321,4 @@ qed. (* minus *) definition Zminus : Z \to Z \to Z \def \lambda x,y:Z. x + (-y). -interpretation "integer minus" 'minus x y = (cic:/matita/Z/plus/Zminus.con x y). +interpretation "integer minus" 'minus x y = (Zminus x y). diff --git a/helm/software/matita/library/Z/sigma_p.ma b/helm/software/matita/library/Z/sigma_p.ma index bf74c7240..c2bdb0901 100644 --- a/helm/software/matita/library/Z/sigma_p.ma +++ b/helm/software/matita/library/Z/sigma_p.ma @@ -85,7 +85,7 @@ unfold sigma_p. apply (iter_p_gen_plusA Z n k p g OZ Zplus) [ apply symmetricZPlus. | intros. - apply cic:/matita/Z/plus/Zplus_z_OZ.con + apply Zplus_z_OZ. | apply associative_Zplus ] qed. diff --git a/helm/software/matita/library/Z/times.ma b/helm/software/matita/library/Z/times.ma index 979cc87aa..742ef5462 100644 --- a/helm/software/matita/library/Z/times.ma +++ b/helm/software/matita/library/Z/times.ma @@ -30,8 +30,7 @@ definition Ztimes :Z \to Z \to Z \def | (pos n) \Rightarrow (neg (pred ((S m) * (S n)))) | (neg n) \Rightarrow (pos (pred ((S m) * (S n))))]]. -(*CSC: the URI must disappear: there is a bug now *) -interpretation "integer times" 'times x y = (cic:/matita/Z/times/Ztimes.con x y). +interpretation "integer times" 'times x y = (Ztimes x y). theorem Ztimes_z_OZ: \forall z:Z. z*OZ = OZ. intro.elim z. diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma index 8dfa31342..36573a8a7 100644 --- a/helm/software/matita/library/algebra/finite_groups.ma +++ b/helm/software/matita/library/algebra/finite_groups.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "algebra/groups.ma". +include "nat/relevant_equations.ma". record finite_enumerable (T:Type) : Type≝ { order: nat; @@ -28,11 +29,9 @@ for @{ 'repr $C $i }. (* CSC: multiple interpretations in the same file are not considered in the right order -interpretation "Finite_enumerable representation" 'repr C i = - (cic:/matita/algebra/finite_groups/repr.con C _ i).*) +interpretation "Finite_enumerable representation" 'repr C i = (repr C _ i).*) -interpretation "Finite_enumerable order" 'card C = - (cic:/matita/algebra/finite_groups/order.con C _). +interpretation "Finite_enumerable order" 'card C = (order C _). record finite_enumerable_SemiGroup : Type≝ { semigroup:> SemiGroup; @@ -40,8 +39,7 @@ record finite_enumerable_SemiGroup : Type≝ }. interpretation "Finite_enumerable representation" 'repr S i = - (cic:/matita/algebra/finite_groups/repr.con S - (cic:/matita/algebra/finite_groups/is_finite_enumerable.con S) i). + (repr S (is_finite_enumerable S) i). notation "hvbox(\iota e)" with precedence 60 for @{ 'index_of_finite_enumerable_semigroup $e }. @@ -49,8 +47,7 @@ for @{ 'index_of_finite_enumerable_semigroup $e }. interpretation "Index_of_finite_enumerable representation" 'index_of_finite_enumerable_semigroup e = - (cic:/matita/algebra/finite_groups/index_of.con _ - (cic:/matita/algebra/finite_groups/is_finite_enumerable.con _) e). + (index_of _ (is_finite_enumerable _) e). (* several definitions/theorems to be moved somewhere else *) @@ -248,8 +245,7 @@ elim n; [ apply (H1 ? ? ? ? Hcut); apply le_S; assumption - | alias id "eq_pred_to_eq" = "cic:/matita/nat/relevant_equations/eq_pred_to_eq.con". -apply eq_pred_to_eq; + | apply eq_pred_to_eq; [ apply (ltn_to_ltO ? ? H7) | apply (ltn_to_ltO ? ? H6) | assumption diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma index d6e77ae8d..f72711aaa 100644 --- a/helm/software/matita/library/algebra/groups.ma +++ b/helm/software/matita/library/algebra/groups.ma @@ -177,8 +177,7 @@ notation "hvbox(x \sub H)" with precedence 79 for @{ 'subgroupimage $H $x }. interpretation "Subgroup image" 'subgroupimage H x = - (cic:/matita/algebra/groups/image.con _ _ - (cic:/matita/algebra/groups/morphism_OF_subgroup.con _ H) x). + (image _ _ (morphism_OF_subgroup _ H) x). definition member_of_subgroup ≝ λG.λH:subgroup G.λx:G.∃y.x=y \sub H. @@ -190,11 +189,10 @@ notation "hvbox(x break \notin H)" with precedence 79 for @{ 'not_member_of $x $H }. interpretation "Member of subgroup" 'member_of x H = - (cic:/matita/algebra/groups/member_of_subgroup.con _ H x). + (member_of_subgroup _ H x). interpretation "Not member of subgroup" 'not_member_of x H = - (cic:/matita/logic/connectives/Not.con - (cic:/matita/algebra/groups/member_of_subgroup.con _ H x)). + (Not (member_of_subgroup _ H x)). (* Left cosets *) @@ -205,21 +203,20 @@ record left_coset (G:Group) : Type ≝ (* Here I would prefer 'magma_op, but this breaks something in the next definition *) interpretation "Left_coset" 'times x C = - (cic:/matita/algebra/groups/left_coset.ind#xpointer(1/1/1) _ x C). + (mk_left_coset _ x C). definition member_of_left_coset ≝ λG:Group.λC:left_coset G.λx:G. ∃y.x=(element ? C)·y \sub (subgrp ? C). interpretation "Member of left_coset" 'member_of x C = - (cic:/matita/algebra/groups/member_of_left_coset.con _ C x). + (member_of_left_coset _ C x). definition left_coset_eq ≝ λG.λC,C':left_coset G. ∀x.((element ? C)·x \sub (subgrp ? C)) ∈ C'. -interpretation "Left cosets equality" 'eq t C C' = - (cic:/matita/algebra/groups/left_coset_eq.con t C C'). +interpretation "Left cosets equality" 'eq t C C' = (left_coset_eq t C C'). definition left_coset_disjoint ≝ λG.λC,C':left_coset G. @@ -230,7 +227,7 @@ notation "hvbox(a break \par b)" for @{ 'disjoint $a $b }. interpretation "Left cosets disjoint" 'disjoint C C' = - (cic:/matita/algebra/groups/left_coset_disjoint.con _ C C'). + (left_coset_disjoint _ C C'). (* The following should be a one-shot alias! *) alias symbol "member_of" (instance 0) = "Member of subgroup". diff --git a/helm/software/matita/library/dama/russell_support.ma b/helm/software/matita/library/dama/russell_support.ma index deb5fc950..41e60359f 100644 --- a/helm/software/matita/library/dama/russell_support.ma +++ b/helm/software/matita/library/dama/russell_support.ma @@ -22,6 +22,6 @@ interpretation "hide" 'hide = (hide _ _). interpretation "hide2" 'hide = (hide _ _ _). definition inject ≝ λP.λa:nat.λp:P a. ex_introT ? P ? p. -coercion cic:/matita/dama/russell_support/inject.con 0 1. +coercion inject 0 1. definition eject ≝ λP.λc: ∃n:nat.P n. match c with [ ex_introT w _ ⇒ w]. -coercion cic:/matita/dama/russell_support/eject.con. +coercion eject. diff --git a/helm/software/matita/library/dama/sequence.ma b/helm/software/matita/library/dama/sequence.ma index 948d14f67..b75c696d3 100644 --- a/helm/software/matita/library/dama/sequence.ma +++ b/helm/software/matita/library/dama/sequence.ma @@ -20,7 +20,7 @@ inductive sequence (O:Type) : Type ≝ definition fun_of_seq: ∀O:Type.sequence O → nat → O ≝ λO.λx:sequence O.match x with [ mk_seq f ⇒ f ]. -coercion cic:/matita/dama/sequence/fun_of_seq.con 1. +coercion fun_of_seq 1. notation < "hvbox((\lfloor term 19 p \rfloor) \sub ident i)" with precedence 90 for @{ 'sequence (\lambda ${ident i} : $t . $p)}. diff --git a/helm/software/matita/library/datatypes/bool.ma b/helm/software/matita/library/datatypes/bool.ma index c9a86165a..da04dd381 100644 --- a/helm/software/matita/library/datatypes/bool.ma +++ b/helm/software/matita/library/datatypes/bool.ma @@ -66,8 +66,7 @@ apply eq_f. assumption. qed. -(*CSC: the URI must disappear: there is a bug now *) -interpretation "boolean not" 'not x = (cic:/matita/datatypes/bool/notb.con x). +interpretation "boolean not" 'not x = (notb x). definition andb : bool \to bool \to bool\def \lambda b1,b2:bool. @@ -75,8 +74,7 @@ definition andb : bool \to bool \to bool\def [ true \Rightarrow b2 | false \Rightarrow false ]. -(*CSC: the URI must disappear: there is a bug now *) -interpretation "boolean and" 'and x y = (cic:/matita/datatypes/bool/andb.con x y). +interpretation "boolean and" 'and x y = (andb x y). theorem andb_elim: \forall b1,b2:bool. \forall P:bool \to Prop. match b1 with @@ -124,8 +122,7 @@ match b1 with intros 3.elim b1.exact H. exact H. qed. -(*CSC: the URI must disappear: there is a bug now *) -interpretation "boolean or" 'or x y = (cic:/matita/datatypes/bool/orb.con x y). +interpretation "boolean or" 'or x y = (orb x y). definition if_then_else : bool \to Prop \to Prop \to Prop \def \lambda b:bool.\lambda P,Q:Prop. diff --git a/helm/software/matita/library/datatypes/constructors.ma b/helm/software/matita/library/datatypes/constructors.ma index d8130d714..6e67c039f 100644 --- a/helm/software/matita/library/datatypes/constructors.ma +++ b/helm/software/matita/library/datatypes/constructors.ma @@ -21,11 +21,9 @@ inductive unit : Set ≝ something: unit. inductive Prod (A,B:Type) : Type \def 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). +interpretation "Pair construction" 'pair x y = (pair _ _ x y). -interpretation "Product" 'product x y = - (cic:/matita/datatypes/constructors/Prod.ind#xpointer(1/1) x y). +interpretation "Product" 'product x y = (Prod x y). definition fst \def \lambda A,B:Type.\lambda p: Prod A B. match p with @@ -51,8 +49,7 @@ inductive Sum (A,B:Type) : Type \def inl : A \to Sum A B | inr : B \to Sum A B. -interpretation "Disjoint union" 'plus A B = - (cic:/matita/datatypes/constructors/Sum.ind#xpointer(1/1) A B). +interpretation "Disjoint union" 'plus A B = (Sum A B). inductive option (A:Type) : Type ≝ None : option A diff --git a/helm/software/matita/library/decidable_kit/eqtype.ma b/helm/software/matita/library/decidable_kit/eqtype.ma index fe3964c65..4c84e85ca 100644 --- a/helm/software/matita/library/decidable_kit/eqtype.ma +++ b/helm/software/matita/library/decidable_kit/eqtype.ma @@ -81,8 +81,7 @@ notation "{x, h}" right associative with precedence 80 for @{'sig $x $h}. -interpretation "sub_eqType" 'sig x h = - (cic:/matita/decidable_kit/eqtype/sigma.ind#xpointer(1/1/1) _ _ x h). +interpretation "sub_eqType" 'sig x h = (mk_sigma _ _ x h). (* restricting an eqType gives an eqType *) lemma sigma_eq_dec : ∀d:eqType.∀p.∀x,y:sigma d p. diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma index adf852499..8a8fedb68 100644 --- a/helm/software/matita/library/demo/power_derivative.ma +++ b/helm/software/matita/library/demo/power_derivative.ma @@ -24,24 +24,17 @@ axiom Rmult: R→R→R. notation "0" with precedence 89 for @{ 'zero }. -interpretation "Rzero" 'zero = - (cic:/matita/demo/power_derivative/R0.con). -interpretation "Nzero" 'zero = - (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)). +interpretation "Rzero" 'zero = (R0). +interpretation "Nzero" 'zero = (O). notation "1" with precedence 89 for @{ 'one }. -interpretation "Rone" 'one = - (cic:/matita/demo/power_derivative/R1.con). -interpretation "None" 'one = - (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) - cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)). +interpretation "Rone" 'one = (R1). +interpretation "None" 'one = (S O). -interpretation "Rplus" 'plus x y = - (cic:/matita/demo/power_derivative/Rplus.con x y). +interpretation "Rplus" 'plus x y = (Rplus x y). -interpretation "Rmult" 'middot x y = - (cic:/matita/demo/power_derivative/Rmult.con x y). +interpretation "Rmult" 'middot x y = (Rmult x y). definition Fplus ≝ λf,g:R→R.λx:R.f x + g x. @@ -49,21 +42,13 @@ definition Fplus ≝ definition Fmult ≝ λf,g:R→R.λx:R.f x · g x. -interpretation "Fplus" 'plus x y = - (cic:/matita/demo/power_derivative/Fplus.con x y). -interpretation "Fmult" 'middot x y = - (cic:/matita/demo/power_derivative/Fmult.con x y). +interpretation "Fplus" 'plus x y = (Fplus x y). +interpretation "Fmult" 'middot x y = (Fmult x y). notation "2" with precedence 89 for @{ 'two }. -interpretation "Rtwo" 'two = - (cic:/matita/demo/power_derivative/Rplus.con - cic:/matita/demo/power_derivative/R1.con - cic:/matita/demo/power_derivative/R1.con). -interpretation "Ntwo" 'two = - (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) - (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) - (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))). +interpretation "Rtwo" 'two = (Rplus R1 R1). +interpretation "Ntwo" 'two = (S (S O)). let rec Rpower (x:R) (n:nat) on n ≝ match n with @@ -71,8 +56,7 @@ let rec Rpower (x:R) (n:nat) on n ≝ | S n ⇒ x · (Rpower x n) ]. -interpretation "Rpower" 'exp x n = - (cic:/matita/demo/power_derivative/Rpower.con x n). +interpretation "Rpower" 'exp x n = (Rpower x n). let rec inj (n:nat) on n : R ≝ match n with @@ -223,8 +207,7 @@ notation "hvbox('D'[f])" non associative with precedence 90 for @{ 'derivative $f }. -interpretation "Rderivative" 'derivative f = - (cic:/matita/demo/power_derivative/derivative.con f). +interpretation "Rderivative" 'derivative f = (derivative f). notation "hvbox('x' \sup n)" non associative with precedence 60 @@ -234,8 +217,7 @@ notation "hvbox('x')" non associative with precedence 60 for @{ 'monomio 1 }. -interpretation "Rmonomio" 'monomio n = - (cic:/matita/demo/power_derivative/monomio.con n). +interpretation "Rmonomio" 'monomio n = (monomio n). axiom derivative_x0: D[x \sup 0] = 0. axiom derivative_x1: D[x] = 1. @@ -286,15 +268,13 @@ for @{ 'derivative ${default @{\lambda ${ident i} : $ty. $p)} @{\lambda ${ident i} . $p}}}. -interpretation "Rderivative" 'derivative \eta.f = - (cic:/matita/demo/power_derivative/derivative.con f). +interpretation "Rderivative" 'derivative \eta.f = (derivative f). *) notation "hvbox(\frac 'd' ('d' 'x') break p)" with precedence 90 for @{ 'derivative $p}. -interpretation "Rderivative" 'derivative f = - (cic:/matita/demo/power_derivative/derivative.con f). +interpretation "Rderivative" 'derivative f = (derivative f). theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n) · x \sup n. assume n:nat. diff --git a/helm/software/matita/library/demo/realisability.ma b/helm/software/matita/library/demo/realisability.ma index d1b569c40..66a96148e 100644 --- a/helm/software/matita/library/demo/realisability.ma +++ b/helm/software/matita/library/demo/realisability.ma @@ -63,9 +63,7 @@ for @{ 'sigma ${default @{\lambda ${ident i} : $ty. $p} @{\lambda ${ident i} . $p}}}. -(*CSC: the URI must disappear: there is a bug now *) -interpretation "Sigma" 'sigma \eta.x = - (cic:/matita/demo/realisability/sigma.ind#xpointer(1/1) _ x). +interpretation "Sigma" 'sigma \eta.x = (sigma _ x). let rec type_OF_SP F ≝ match F return λF.Type with diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index 2a51e3bd5..4e5374dc7 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -1,7 +1,7 @@ -demo/formal_topology.ma logic/cprop_connectives.ma logic/equality.ma dama/sandwich.ma dama/ordered_uniform.ma +demo/formal_topology.ma logic/cprop_connectives.ma logic/equality.ma Q/ratio/rtimes.ma Q/fraction/ftimes.ma Q/ratio/rinv.ma -demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma +demo/power_derivative.ma nat/compare.ma nat/orders.ma nat/plus.ma nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma dama/ordered_uniform.ma dama/uniform.ma nat/lt_arith.ma nat/div_and_mod.ma @@ -9,47 +9,47 @@ demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma na Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma dama/models/nat_order_continuous.ma dama/models/increasing_supremum_stabilizes.ma dama/models/nat_ordered_uniform.ma nat/factorial2.ma nat/exp.ma nat/factorial.ma -nat/orders.ma higher_order_defs/ordering.ma logic/connectives.ma nat/nat.ma -technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma +nat/orders.ma higher_order_defs/ordering.ma nat/nat.ma nat/sieve.ma list/sort.ma nat/primes.ma +technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma nat/div_and_mod_diseq.ma nat/lt_arith.ma logic/cprop_connectives.ma logic/connectives.ma -algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma +algebra/groups.ma algebra/monoids.ma datatypes/bool.ma nat/compare.ma nat/le_arith.ma nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma +dama/models/nat_uniform.ma dama/models/discrete_uniformity.ma dama/nat_ordered_set.ma list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma datatypes/compare.ma -dama/models/nat_uniform.ma dama/models/discrete_uniformity.ma dama/nat_ordered_set.ma didactic/exercises/natural_deduction_fst_order.ma didactic/support/natural_deduction.ma didactic/exercises/substitution.ma nat/minus.ma nat/factorization2.ma list/list.ma nat/factorization.ma nat/sieve.ma -logic/connectives.ma dama/models/increasing_supremum_stabilizes.ma dama/models/nat_uniform.ma dama/russell_support.ma dama/supremum.ma nat/le_arith.ma +logic/connectives.ma Q/nat_fact/times.ma nat/factorization.ma decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma didactic/exercises/duality.ma nat/minus.ma nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma dama/supremum.ma dama/nat_ordered_set.ma dama/sequence.ma datatypes/constructors.ma nat/plus.ma -nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma -didactic/exercises/natural_deduction1.ma didactic/support/natural_deduction.ma +nat/totient1.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma R/Rexp.ma R/root.ma Z/times.ma nat/orders.ma +didactic/exercises/natural_deduction1.ma didactic/support/natural_deduction.ma nat/times.ma nat/plus.ma nat/chebyshev_thm.ma nat/neper.ma Z/z.ma datatypes/bool.ma nat/nat.ma demo/cantor.ma datatypes/constructors.ma demo/formal_topology.ma +dama/models/nat_ordered_uniform.ma dama/bishop_set_rewrite.ma dama/models/nat_uniform.ma dama/ordered_uniform.ma nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma nat/le_arith.ma nat/orders.ma nat/times.ma decidable_kit/fgraph.ma decidable_kit/fintype.ma -dama/models/nat_ordered_uniform.ma dama/bishop_set_rewrite.ma dama/models/nat_uniform.ma dama/ordered_uniform.ma dama/bishop_set.ma dama/ordered_set.ma -nat/euler_theorem.ma nat/map_iter_p.ma nat/nat.ma nat/totient.ma +nat/euler_theorem.ma nat/map_iter_p.ma nat/totient.ma Q/fraction/ftimes.ma Q/fraction/finv.ma Q/nat_fact/times.ma Q/ratio/ratio.ma Z/times.ma nat/factorial.ma nat/le_arith.ma Z/plus.ma Z/z.ma nat/minus.ma Q/ratio/rinv.ma Q/fraction/finv.ma Q/ratio/ratio.ma -decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma dama/ordered_set.ma datatypes/constructors.ma logic/cprop_connectives.ma +decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma Q/q/qplus.ma nat/factorization.ma decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma @@ -64,7 +64,7 @@ nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma didactic/support/natural_deduction.ma nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma -Q/frac.ma Q/q/q.ma Q/q/qinv.ma nat/factorization.ma nat/nat.ma +Q/frac.ma Q/q/qinv.ma didactic/exercises/shannon.ma nat/minus.ma Q/q/qtimes.ma Q/q/qinv.ma Q/ratio/rtimes.ma nat/minus.ma nat/compare.ma nat/le_arith.ma @@ -74,15 +74,15 @@ algebra/finite_groups.ma algebra/groups.ma nat/relevant_equations.ma decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma algebra/semigroups.ma higher_order_defs/functions.ma -dama/models/discrete_uniformity.ma dama/bishop_set_rewrite.ma dama/uniform.ma dama/lebesgue.ma dama/ordered_set.ma dama/property_exhaustivity.ma dama/sandwich.ma +dama/models/discrete_uniformity.ma dama/bishop_set_rewrite.ma dama/uniform.ma higher_order_defs/relations.ma logic/connectives.ma nat/factorization.ma nat/ord.ma nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma Z/moebius.ma Z/sigma_p.ma nat/factorization.ma demo/toolbox.ma logic/cprop_connectives.ma -logic/coimplication.ma logic/connectives.ma nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma +logic/coimplication.ma logic/connectives.ma nat/minimization.ma nat/minus.ma logic/connectives2.ma higher_order_defs/relations.ma datatypes/subsets.ma datatypes/categories.ma logic/cprop_connectives.ma @@ -96,8 +96,8 @@ Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma dama/uniform.ma dama/supremum.ma demo/natural_deduction.ma didactic/support/natural_deduction.ma higher_order_defs/ordering.ma logic/equality.ma -logic/equality.ma logic/connectives.ma higher_order_defs/relations.ma nat/congruence.ma nat/primes.ma nat/relevant_equations.ma +logic/equality.ma higher_order_defs/relations.ma dama/property_exhaustivity.ma dama/ordered_uniform.ma dama/property_sigma.ma nat/gcd.ma nat/lt_arith.ma nat/primes.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma @@ -109,11 +109,11 @@ nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma datatypes/categories.ma logic/cprop_connectives.ma nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma dama/nat_ordered_set.ma nat/orders.ma dama/bishop_set.ma nat/compare.ma -Q/fraction/finv.ma Q/fraction/fraction.ma Z/plus.ma dama/russell_support.ma logic/cprop_connectives.ma nat/nat.ma +Q/fraction/finv.ma Q/fraction/fraction.ma Z/plus.ma nat/binomial.ma nat/factorial2.ma nat/iteration2.ma -nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma R/root.ma logic/connectives.ma Q/q/q.ma R/r.ma +nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma higher_order_defs/functions.ma logic/equality.ma Q/fraction/numerator_denominator.ma Q/fraction/finv.ma nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma @@ -121,15 +121,15 @@ datatypes/constructors.ma logic/equality.ma didactic/exercises/natural_deduction_theories.ma didactic/support/natural_deduction.ma nat/plus.ma nat/plus.ma nat/nat.ma Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma -list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma dama/sequence.ma nat/nat.ma -nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma +nat/primes.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma nat/gcd_properties1.ma nat/gcd.ma +list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma didactic/exercises/natural_deduction.ma didactic/support/natural_deduction.ma dama/bishop_set_rewrite.ma dama/bishop_set.ma Z/times.ma Z/plus.ma nat/lt_arith.ma -Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma R/Rlog.ma R/Rexp.ma +Z/sigma_p.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma nat/o.ma nat/binomial.ma nat/sqrt.ma dama/property_sigma.ma dama/ordered_uniform.ma dama/russell_support.ma -Q/inv.ma Q/fraction/finv.ma Q/q/q.ma Q/q.ma +Q/inv.ma Q/fraction/finv.ma Q/q.ma Q/q/q.ma diff --git a/helm/software/matita/library/didactic/exercises/duality.ma b/helm/software/matita/library/didactic/exercises/duality.ma index dca98ddc7..aa1aa32f8 100644 --- a/helm/software/matita/library/didactic/exercises/duality.ma +++ b/helm/software/matita/library/didactic/exercises/duality.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + (* Esercizio 0 =========== diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma index 078c7fb00..feac0296d 100644 --- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma +++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + (* Istruzioni: http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction1.ma b/helm/software/matita/library/didactic/exercises/natural_deduction1.ma index c2778fbc5..f45089237 100644 --- a/helm/software/matita/library/didactic/exercises/natural_deduction1.ma +++ b/helm/software/matita/library/didactic/exercises/natural_deduction1.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + (* Istruzioni: http://mowgli.cs.unibo.it/~tassi/exercise-natural_deduction.html @@ -182,4 +196,4 @@ apply rule (∨_e (G∨¬L) [h6] (⊥) [h6] (⊥)); ] ] (*END*) -qed. \ No newline at end of file +qed. diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma b/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma index dfecc3c13..2c796236d 100644 --- a/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma +++ b/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + (* Esercizio 0 =========== diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma b/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma index d955bd124..82e3b83fd 100644 --- a/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma +++ b/helm/software/matita/library/didactic/exercises/natural_deduction_theories.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + (* Esercizio 0 =========== diff --git a/helm/software/matita/library/didactic/exercises/shannon.ma b/helm/software/matita/library/didactic/exercises/shannon.ma index f0a191729..152cbb1e9 100644 --- a/helm/software/matita/library/didactic/exercises/shannon.ma +++ b/helm/software/matita/library/didactic/exercises/shannon.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + (* Esercizio 0 =========== diff --git a/helm/software/matita/library/didactic/exercises/substitution.ma b/helm/software/matita/library/didactic/exercises/substitution.ma index 0c9b86b00..e3472c7a4 100644 --- a/helm/software/matita/library/didactic/exercises/substitution.ma +++ b/helm/software/matita/library/didactic/exercises/substitution.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + (* Esercizio 0 =========== diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma index c592b5254..c6bd96df1 100644 --- a/helm/software/matita/library/didactic/support/natural_deduction.ma +++ b/helm/software/matita/library/didactic/support/natural_deduction.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + (* Logic system *) inductive Imply (A,B:CProp) : CProp ≝ diff --git a/helm/software/matita/library/higher_order_defs/functions.ma b/helm/software/matita/library/higher_order_defs/functions.ma index 195cbfc17..a99ad4a08 100644 --- a/helm/software/matita/library/higher_order_defs/functions.ma +++ b/helm/software/matita/library/higher_order_defs/functions.ma @@ -18,8 +18,7 @@ definition compose \def \lambda A,B,C:Type.\lambda f:(B\to C).\lambda g:(A\to B).\lambda x:A. f (g x). -interpretation "function composition" 'compose f g = - (cic:/matita/higher_order_defs/functions/compose.con _ _ _ f g). +interpretation "function composition" 'compose f g = (compose _ _ _ f g). definition injective: \forall A,B:Type.\forall f:A \to B.Prop \def \lambda A,B.\lambda f. diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma index e4787fe84..d0c4f5856 100644 --- a/helm/software/matita/library/list/list.ma +++ b/helm/software/matita/library/list/list.ma @@ -34,9 +34,8 @@ notation "hvbox(l1 break @ l2)" right associative with precedence 47 for @{'append $l1 $l2 }. -interpretation "nil" 'nil = (cic:/matita/list/list/list.ind#xpointer(1/1/1) _). -interpretation "cons" 'cons hd tl = - (cic:/matita/list/list/list.ind#xpointer(1/1/2) _ hd tl). +interpretation "nil" 'nil = (nil _). +interpretation "cons" 'cons hd tl = (cons _ hd tl). (* theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. *) @@ -63,7 +62,7 @@ definition tail := \lambda A:Type. \lambda l: list A. [ nil => [] | (cons hd tl) => tl]. -interpretation "append" 'append l1 l2 = (cic:/matita/list/list/append.con _ l1 l2). +interpretation "append" 'append l1 l2 = (append _ l1 l2). theorem append_nil: \forall A:Type.\forall l:list A.l @ [] = l. intros; diff --git a/helm/software/matita/library/logic/connectives.ma b/helm/software/matita/library/logic/connectives.ma index ba229870f..6a20bc897 100644 --- a/helm/software/matita/library/logic/connectives.ma +++ b/helm/software/matita/library/logic/connectives.ma @@ -24,8 +24,7 @@ default "false" cic:/matita/logic/connectives/False.ind. definition Not: Prop \to Prop \def \lambda A. (A \to False). -(*CSC: the URI must disappear: there is a bug now *) -interpretation "logical not" 'not x = (cic:/matita/logic/connectives/Not.con x). +interpretation "logical not" 'not x = (Not x). theorem absurd : \forall A,C:Prop. A \to \lnot A \to C. intros. elim (H1 H). @@ -36,8 +35,7 @@ default "absurd" cic:/matita/logic/connectives/absurd.con. inductive And (A,B:Prop) : Prop \def conj : A \to B \to (And A B). -(*CSC: the URI must disappear: there is a bug now *) -interpretation "logical and" 'and x y = (cic:/matita/logic/connectives/And.ind#xpointer(1/1) x y). +interpretation "logical and" 'and x y = (And x y). theorem proj1: \forall A,B:Prop. A \land B \to A. intros. elim H. assumption. @@ -52,8 +50,7 @@ inductive Or (A,B:Prop) : Prop \def | or_intror : B \to (Or A B). (*CSC: the URI must disappear: there is a bug now *) -interpretation "logical or" 'or x y = - (cic:/matita/logic/connectives/Or.ind#xpointer(1/1) x y). +interpretation "logical or" 'or x y = (Or x y). theorem Or_ind': \forall A,B:Prop. @@ -73,9 +70,7 @@ definition decidable : Prop \to Prop \def \lambda A:Prop. A \lor \lnot A. inductive ex (A:Type) (P:A \to Prop) : Prop \def ex_intro: \forall x:A. P x \to ex A P. -(*CSC: the URI must disappear: there is a bug now *) -interpretation "exists" 'exists \eta.x = - (cic:/matita/logic/connectives/ex.ind#xpointer(1/1) _ x). +interpretation "exists" 'exists \eta.x = (ex _ x). inductive ex2 (A:Type) (P,Q:A \to Prop) : Prop \def ex_intro2: \forall x:A. P x \to Q x \to ex2 A P Q. diff --git a/helm/software/matita/library/logic/equality.ma b/helm/software/matita/library/logic/equality.ma index 73728dc92..6e38ae71e 100644 --- a/helm/software/matita/library/logic/equality.ma +++ b/helm/software/matita/library/logic/equality.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) @@ -17,13 +17,9 @@ include "higher_order_defs/relations.ma". inductive eq (A:Type) (x:A) : A \to Prop \def refl_eq : eq A x x. -(*CSC: the URI must disappear: there is a bug now *) -interpretation "leibnitz's equality" - 'eq t x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) t x y). -(*CSC: the URI must disappear: there is a bug now *) -interpretation "leibnitz's non-equality" - 'neq t x y = (cic:/matita/logic/connectives/Not.con - (cic:/matita/logic/equality/eq.ind#xpointer(1/1) t x y)). +interpretation "leibnitz's equality" 'eq t x y = (eq t x y). + +interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)). theorem eq_rect': \forall A. \forall x:A. \forall P: \forall y:A. x=y \to Type. diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma index 6ef8624e4..701ad7ad1 100644 --- a/helm/software/matita/library/nat/chebyshev.ma +++ b/helm/software/matita/library/nat/chebyshev.ma @@ -16,6 +16,7 @@ include "nat/log.ma". include "nat/pi_p.ma". include "nat/factorization.ma". include "nat/factorial2.ma". +include "nat/o.ma". definition prim: nat \to nat \def \lambda n. sigma_p (S n) primeb (\lambda p.1). @@ -2098,7 +2099,6 @@ apply (trans_le ? ((exp 2 (2*n))/(2*n))) rewrite < plus_n_O. rewrite > exp_plus_times. apply le_times_l. - alias id "le_times_SSO_n_exp_SSO_n" = "cic:/matita/nat/o/le_times_SSO_n_exp_SSO_n.con". apply le_times_SSO_n_exp_SSO_n ] |apply le_times_to_le_div2 diff --git a/helm/software/matita/library/nat/congruence.ma b/helm/software/matita/library/nat/congruence.ma index 948d10667..4266d3f6f 100644 --- a/helm/software/matita/library/nat/congruence.ma +++ b/helm/software/matita/library/nat/congruence.ma @@ -21,8 +21,7 @@ definition S_mod: nat \to nat \to nat \def definition congruent: nat \to nat \to nat \to Prop \def \lambda n,m,p:nat. mod n p = mod m p. -interpretation "congruent" 'congruent n m p = - (cic:/matita/nat/congruence/congruent.con n m p). +interpretation "congruent" 'congruent n m p = (congruent n m p). notation < "hvbox(n break \cong\sub p m)" (*non associative*) with precedence 45 diff --git a/helm/software/matita/library/nat/div_and_mod.ma b/helm/software/matita/library/nat/div_and_mod.ma index 538515a8c..fbf512761 100644 --- a/helm/software/matita/library/nat/div_and_mod.ma +++ b/helm/software/matita/library/nat/div_and_mod.ma @@ -29,8 +29,7 @@ match m with [O \Rightarrow n | (S p) \Rightarrow mod_aux n n p]. -interpretation "natural remainder" 'module x y = - (cic:/matita/nat/div_and_mod/mod.con x y). +interpretation "natural remainder" 'module x y = (mod x y). let rec div_aux p m n : nat \def match (leb m n) with @@ -46,8 +45,7 @@ match m with [O \Rightarrow S n | (S p) \Rightarrow div_aux n n p]. -interpretation "natural divide" 'divide x y = - (cic:/matita/nat/div_and_mod/div.con x y). +interpretation "natural divide" 'divide x y = (div x y). theorem le_mod_aux_m_m: \forall p,n,m. n \leq p \to (mod_aux p n m) \leq m. diff --git a/helm/software/matita/library/nat/euler_theorem.ma b/helm/software/matita/library/nat/euler_theorem.ma index 9396d444e..e5933ad95 100644 --- a/helm/software/matita/library/nat/euler_theorem.ma +++ b/helm/software/matita/library/nat/euler_theorem.ma @@ -83,7 +83,7 @@ elim (m) reflexivity | rewrite > gcd_O_n. apply not_eq_to_eqb_false. - apply cic:/matita/nat/nat/not_eq_S.con. + apply not_eq_S. unfold Not. intro. cut ( (S n) \le O) @@ -159,7 +159,7 @@ elim n apply (totient_card_aux n2 n2). reflexivity | apply not_eq_to_eqb_false. - apply cic:/matita/nat/nat/not_eq_S.con. + apply not_eq_S. unfold Not. intro. cut ( (S n2) \le O) diff --git a/helm/software/matita/library/nat/exp.ma b/helm/software/matita/library/nat/exp.ma index c9f2c6984..c6e2a008b 100644 --- a/helm/software/matita/library/nat/exp.ma +++ b/helm/software/matita/library/nat/exp.ma @@ -20,7 +20,7 @@ let rec exp n m on m\def [ O \Rightarrow (S O) | (S p) \Rightarrow (times n (exp n p)) ]. -interpretation "natural exponent" 'exp a b = (cic:/matita/nat/exp/exp.con a b). +interpretation "natural exponent" 'exp a b = (exp a b). theorem exp_plus_times : \forall n,p,q:nat. n \sup (p + q) = (n \sup p) * (n \sup q). diff --git a/helm/software/matita/library/nat/factorial.ma b/helm/software/matita/library/nat/factorial.ma index 58220cb0c..9c1a4e97d 100644 --- a/helm/software/matita/library/nat/factorial.ma +++ b/helm/software/matita/library/nat/factorial.ma @@ -19,7 +19,7 @@ let rec fact n \def [ O \Rightarrow (S O) | (S m) \Rightarrow (S m)*(fact m)]. -interpretation "factorial" 'fact n = (cic:/matita/nat/factorial/fact.con n). +interpretation "factorial" 'fact n = (fact n). theorem le_SO_fact : \forall n. (S O) \le n!. intro.elim n.simplify.apply le_n. diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma index 10d218d44..20785c9e8 100644 --- a/helm/software/matita/library/nat/minus.ma +++ b/helm/software/matita/library/nat/minus.ma @@ -24,8 +24,7 @@ let rec minus n m \def [O \Rightarrow (S p) | (S q) \Rightarrow minus p q ]]. -(*CSC: the URI must disappear: there is a bug now *) -interpretation "natural minus" 'minus x y = (cic:/matita/nat/minus/minus.con x y). +interpretation "natural minus" 'minus x y = (minus x y). theorem minus_n_O: \forall n:nat.n=n-O. intros.elim n.simplify.reflexivity. diff --git a/helm/software/matita/library/nat/nat.ma b/helm/software/matita/library/nat/nat.ma index b098279e6..5e3e769ec 100644 --- a/helm/software/matita/library/nat/nat.ma +++ b/helm/software/matita/library/nat/nat.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) diff --git a/helm/software/matita/library/nat/orders.ma b/helm/software/matita/library/nat/orders.ma index 6dd8773f8..8255787f9 100644 --- a/helm/software/matita/library/nat/orders.ma +++ b/helm/software/matita/library/nat/orders.ma @@ -20,32 +20,28 @@ inductive le (n:nat) : nat \to Prop \def | le_n : le n n | le_S : \forall m:nat. le n m \to le n (S m). -interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y). +interpretation "natural 'less or equal to'" 'leq x y = (le x y). -interpretation "natural 'neither less nor equal to'" 'nleq x y = - (cic:/matita/logic/connectives/Not.con - (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y)). +interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)). definition lt: nat \to nat \to Prop \def \lambda n,m:nat.(S n) \leq m. -interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y). +interpretation "natural 'less than'" 'lt x y = (lt x y). -interpretation "natural 'not less than'" 'nless x y = - (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/lt.con x y)). +interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)). definition ge: nat \to nat \to Prop \def \lambda n,m:nat.m \leq n. -interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/nat/orders/ge.con x y). +interpretation "natural 'greater or equal to'" 'geq x y = (ge x y). definition gt: nat \to nat \to Prop \def \lambda n,m:nat.m (eq_gcd_div_div_div_gcd x n (gcd x n)) [ apply (div_n_n (gcd x n) Hcut) | assumption -- 2.39.2