From fdab21f9db0c8536718001e38213c34595170182 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 15 Feb 2009 14:56:26 +0000 Subject: [PATCH] minor changes to make the library compile after wilmers new exists. --- .../models/increasing_supremum_stabilizes.ma | 2 ++ .../library/dama/models/nat_lebesgue.ma | 1 + .../library/dama/property_exhaustivity.ma | 5 +-- helm/software/matita/library/depends | 33 ++++++++----------- .../matita/library/logic/cprop_connectives.ma | 12 +++---- 5 files changed, 26 insertions(+), 27 deletions(-) diff --git a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma index 46aa96eb1..f84b74044 100644 --- a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma +++ b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma @@ -27,6 +27,7 @@ coercion hint1 nocomposites. alias symbol "pi1" = "exT \fst". alias symbol "N" = "ordered set N". +alias symbol "dependent_pair" = "dependent pair". lemma increasing_supremum_stabilizes: ∀sg:‡ℕ.∀a:sequence {[sg]}. a is_increasing → @@ -98,6 +99,7 @@ letin m ≝ (hide ? ( 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; +alias symbol "exists" = "CProp exists". letin find ≝ ( let rec find i u on u : nat ≝ match u with diff --git a/helm/software/matita/library/dama/models/nat_lebesgue.ma b/helm/software/matita/library/dama/models/nat_lebesgue.ma index 8d563b1e3..2657aba89 100644 --- a/helm/software/matita/library/dama/models/nat_lebesgue.ma +++ b/helm/software/matita/library/dama/models/nat_lebesgue.ma @@ -15,6 +15,7 @@ include "dama/lebesgue.ma". include "dama/models/nat_order_continuous.ma". +alias symbol "dependent_pair" = "dependent pair". theorem nat_lebesgue_oc: ∀a:sequence ℕ.∀s:‡ℕ.∀H:∀i:nat.a i ∈ s. ∀x:ℕ.a order_converges x → diff --git a/helm/software/matita/library/dama/property_exhaustivity.ma b/helm/software/matita/library/dama/property_exhaustivity.ma index f76660190..0d35ca981 100644 --- a/helm/software/matita/library/dama/property_exhaustivity.ma +++ b/helm/software/matita/library/dama/property_exhaustivity.ma @@ -93,6 +93,7 @@ notation "'downarrow_to_in_segment'" non associative with precedence 90 for @{'d interpretation "uparrow_to_in_segment" 'uparrow_to_in_segment = (h_uparrow_to_in_segment (os_l _)). interpretation "downarrow_to_in_segment" 'downarrow_to_in_segment = (h_uparrow_to_in_segment (os_r _)). +alias symbol "dependent_pair" = "dependent pair". (* Lemma 3.8 NON DUALIZZATO *) lemma restrict_uniform_convergence_uparrow: ∀C:ordered_uniform_space.property_sigma C → @@ -105,13 +106,13 @@ intros; split; simplify; intros; cases (a i); assumption; |2: intros; lapply (uparrow_upperlocated a ≪x,h≫) as Ha1; - [2: apply (segment_preserves_uparrow s); assumption;] + [2: apply (segment_preserves_uparrow s); assumption;] lapply (segment_preserves_supremum s a ≪?,h≫ H2) as Ha2; cases Ha2; clear Ha2; cases (H1 a a); lapply (H5 H3 Ha1) as HaC; lapply (segment_cauchy C s ? HaC) as Ha; lapply (sigma_cauchy ? H ? x ? Ha); [left; assumption] - apply (restric_uniform_convergence C s ≪x,h≫ a Hletin)] + apply (restric_uniform_convergence C s ≪?,h≫ a Hletin)] qed. lemma hint_mah1: diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index 64edcc026..2a51e3bd5 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -1,5 +1,5 @@ -dama/sandwich.ma dama/ordered_uniform.ma demo/formal_topology.ma logic/cprop_connectives.ma logic/equality.ma +dama/sandwich.ma dama/ordered_uniform.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 nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma @@ -10,8 +10,8 @@ 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 -nat/sieve.ma list/sort.ma nat/primes.ma technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma +nat/sieve.ma list/sort.ma nat/primes.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 @@ -24,33 +24,32 @@ dama/models/nat_uniform.ma dama/models/discrete_uniformity.ma dama/nat_ordered_s 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 -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 +dama/models/increasing_supremum_stabilizes.ma dama/models/nat_uniform.ma dama/russell_support.ma dama/supremum.ma nat/le_arith.ma Q/nat_fact/times.ma nat/factorization.ma decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma -Fsub/defn.ma Fsub/util.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 -R/Rexp.ma R/root.ma Z/times.ma nat/orders.ma didactic/exercises/natural_deduction1.ma didactic/support/natural_deduction.ma +R/Rexp.ma R/root.ma Z/times.ma nat/orders.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 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 -dama/ordered_set.ma datatypes/constructors.ma logic/cprop_connectives.ma decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma +dama/ordered_set.ma datatypes/constructors.ma logic/cprop_connectives.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 @@ -66,7 +65,6 @@ 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 -.unnamed.ma logic/connectives.ma nat/nat.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 @@ -76,16 +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/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 -Fsub/part1a.ma Fsub/defn.ma +dama/lebesgue.ma dama/ordered_set.ma dama/property_exhaustivity.ma dama/sandwich.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 -nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma logic/coimplication.ma logic/connectives.ma +nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.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 @@ -99,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 -nat/congruence.ma nat/primes.ma nat/relevant_equations.ma logic/equality.ma logic/connectives.ma higher_order_defs/relations.ma +nat/congruence.ma nat/primes.ma nat/relevant_equations.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 @@ -112,29 +109,27 @@ 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 -dama/russell_support.ma logic/cprop_connectives.ma nat/nat.ma Q/fraction/finv.ma Q/fraction/fraction.ma Z/plus.ma -Fsub/util.ma list/in.ma list/list.ma logic/equality.ma nat/compare.ma +dama/russell_support.ma logic/cprop_connectives.ma nat/nat.ma nat/binomial.ma nat/factorial2.ma nat/iteration2.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 +R/root.ma logic/connectives.ma Q/q/q.ma R/r.ma higher_order_defs/functions.ma logic/equality.ma Q/fraction/numerator_denominator.ma Q/fraction/finv.ma -Fsub/part1a_inversion.ma Fsub/defn.ma nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma datatypes/constructors.ma logic/equality.ma didactic/exercises/natural_deduction_theories.ma didactic/support/natural_deduction.ma nat/plus.ma -Q/fraction/fraction.ma Z/compare.ma nat/factorization.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/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 -R/Rlog.ma R/Rexp.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 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 diff --git a/helm/software/matita/library/logic/cprop_connectives.ma b/helm/software/matita/library/logic/cprop_connectives.ma index 266bb11a4..31cd9c576 100644 --- a/helm/software/matita/library/logic/cprop_connectives.ma +++ b/helm/software/matita/library/logic/cprop_connectives.ma @@ -112,12 +112,12 @@ definition pi1exP ≝ λA,P.λx:exP A P.match x with [ex_introP x _ ⇒ x]. definition pi2exP ≝ λA,P.λx:exP A P.match x return λx.P (pi1exP ?? x) with [ex_introP _ p ⇒ p]. -interpretation "exT \fst" 'pi1 = (pi1exP _ _). -interpretation "exT \fst" 'pi1a x = (pi1exP _ _ x). -interpretation "exT \fst" 'pi1b x y = (pi1exP _ _ x y). -interpretation "exT \snd" 'pi2 = (pi2exP _ _). -interpretation "exT \snd" 'pi2a x = (pi2exP _ _ x). -interpretation "exT \snd" 'pi2b x y = (pi2exP _ _ x y). +interpretation "exP \fst" 'pi1 = (pi1exP _ _). +interpretation "exP \fst" 'pi1a x = (pi1exP _ _ x). +interpretation "exP \fst" 'pi1b x y = (pi1exP _ _ x y). +interpretation "exP \snd" 'pi2 = (pi2exP _ _). +interpretation "exP \snd" 'pi2a x = (pi2exP _ _ x). +interpretation "exP \snd" 'pi2b x y = (pi2exP _ _ x y). inductive exT23 (A:Type) (P:A→CProp) (Q:A→CProp) (R:A→A→CProp) : CProp ≝ -- 2.39.2