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;
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";
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 = [];
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;
| "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
%}
{ 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)] }
TRANSCRIPT = $(BIN)../components/binaries/transcript/transcript.opt
+OPTIONS =
+
LOG = log.txt
MMAS = $(shell find -name "*.mma")
endif
mma: $(DEVEL).conf.xml clean.ma
- $(H)$(TRANSCRIPT) -g -C $(BIN) $(DEVEL)
+ $(H)$(TRANSCRIPT) $(OPTIONS) -C $(BIN) $(DEVEL)
<key name="output_path">contribs/procedural/library</key>
<key name="input_type">grafite</key>
<key name="output_type">procedural</key>
+ <key name="heading_lines">14</key>
</section>
</helm_registry>
(* *)
(**************************************************************************)
+include "Q/q/qinv.ma".
+
(*
let rec nat_fact_to_fraction_inv l \def
match l 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)).
]
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
(* *)
(**************************************************************************)
+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;
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
| _ ⇒ False
].
-alias id "Qneg" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/3)".
definition is_negative ≝
λq.
match q with
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
]
].
-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;
| 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.
| (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.
(* 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).
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.
| (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.
(**************************************************************************)
include "algebra/groups.ma".
+include "nat/relevant_equations.ma".
record finite_enumerable (T:Type) : Type≝
{ order: nat;
(* 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;
}.
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 }.
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 *)
[ 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
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.
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 *)
(* 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.
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".
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.
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)}.
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.
[ 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
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.
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
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
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.
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.
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
| 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
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
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.
@{\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.
@{\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
-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
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
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
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
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
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
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
+(**************************************************************************)
+(* ___ *)
+(* ||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
===========
+(**************************************************************************)
+(* ___ *)
+(* ||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
+(**************************************************************************)
+(* ___ *)
+(* ||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
]
]
(*END*)
-qed.
\ No newline at end of file
+qed.
+(**************************************************************************)
+(* ___ *)
+(* ||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
===========
+(**************************************************************************)
+(* ___ *)
+(* ||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
===========
+(**************************************************************************)
+(* ___ *)
+(* ||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
===========
+(**************************************************************************)
+(* ___ *)
+(* ||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
===========
+(**************************************************************************)
+(* ___ *)
+(* ||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 ≝
\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.
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) :: []. *)
[ 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;
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).
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.
| 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.
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.
(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
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.
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).
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
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
[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
[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.
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)
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)
[ 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).
[ 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.
[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.
(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
| 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<n.
-interpretation "natural 'greater than'" 'gt x y = (cic:/matita/nat/orders/gt.con x y).
+interpretation "natural 'greater than'" 'gt x y = (gt x y).
-interpretation "natural 'not greater than'" 'ngtr x y =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/gt.con x y)).
+interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)).
theorem transitive_le : transitive nat le.
unfold transitive.intros.elim H1.
notation < "(❲i \atop j❳)n" with precedence 71
for @{ 'transposition $i $j $n}.
-interpretation "natural transposition" 'transposition i j n =
- (cic:/matita/nat/permutation/transpose.con i j n).
+interpretation "natural transposition" 'transposition i j n = (transpose i j n).
lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j.
intros.unfold transpose.
[ O \Rightarrow m
| (S p) \Rightarrow S (plus p m) ].
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural plus" 'plus x y = (cic:/matita/nat/plus/plus.con x y).
+interpretation "natural plus" 'plus x y = (plus x y).
theorem plus_n_O: \forall n:nat. n = n+O.
intros.elim n.
inductive divides (n,m:nat) : Prop \def
witness : \forall p:nat.m = times n p \to divides n m.
-interpretation "divides" 'divides n m = (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m).
-interpretation "not divides" 'ndivides n m =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m)).
+interpretation "divides" 'divides n m = (divides n m).
+interpretation "not divides" 'ndivides n m = (Not (divides n m)).
theorem reflexive_divides : reflexive nat divides.
unfold reflexive.
[ O \Rightarrow O
| (S p) \Rightarrow m+(times p m) ].
-interpretation "natural times" 'times x y = (cic:/matita/nat/times/times.con x y).
+interpretation "natural times" 'times x y = (times x y).
theorem times_Sn_m:
\forall n,m:nat. m+n*m = S n*m.
| apply divides_gcd_n
]
]
- | apply cic:/matita/nat/compare/eq_to_eqb_true.con.
+ | apply eq_to_eqb_true.
rewrite > (eq_gcd_div_div_div_gcd x n (gcd x n))
[ apply (div_n_n (gcd x n) Hcut)
| assumption
projects / helm.git / commitdiff