minor changes to make the library compile after wilmers new exists.

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 46aa96eb1c141b1a0a29554efdfc4157104dd913..f84b740441602122456119aa101139489fb58c86 100644 (file)
--- 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 8d563b1e351d469c4cb2097dda9fcd094b689915..2657aba89dd37f3f76645fdd7fcc81f0aafbe0bf 100644 (file)
--- 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 f76660190d59476dca1d8bef9c1e0fb8bdc3e879..0d35ca981b8d864692376b0d6dd0e4bc6ab6a81b 100644 (file)
--- 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 64edcc026fca842588f9fdde63a05971faf3572c..2a51e3bd569120b1ef4b8dd53e316c3045a3cc16 100644 (file)
--- 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 266bb11a46484b921f2aa228257ebd3b21ea5ee2..31cd9c576c236355b73e9335319c88c9b97d1c95 100644 (file)
--- 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 ≝