Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / transc / Pi.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/transc/Pi.mma b/helm/software/matita/contribs/CoRN-Procedural/transc/Pi.mma
index ee9e30e7077c71336ff241e3e1d5985f7284fffb..e3d6eec67f5b0ef7fe0097f5d6df3045c3600d95 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/transc/Pi.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/transc/Pi.mma
@@ -29,7 +29,7 @@ Section Properties_of_Pi
 [Pi] is defined as twice the first positive zero of the cosine.  In order to do this, we follow the construction described in Bishop 1969, section 7.
 *)
 
-inline procedural "cic:/CoRN/transc/Pi/pi_seq.con".
+inline procedural "cic:/CoRN/transc/Pi/pi_seq.con" as definition.
 
 (* UNEXPORTED
 Opaque Cosine.
@@ -41,7 +41,7 @@ Opaque Cosine.
 Opaque Sine.
 *)
 
-inline procedural "cic:/CoRN/transc/Pi/pi_seq_lemma.con".
+inline procedural "cic:/CoRN/transc/Pi/pi_seq_lemma.con" as lemma.
 
 (* end hide *)
 
@@ -51,64 +51,64 @@ This sequence is nonnegative and the cosine of any number between
 sequence is strictly increasing.
 *)
 
-inline procedural "cic:/CoRN/transc/Pi/pi_seq_nonneg.con".
+inline procedural "cic:/CoRN/transc/Pi/pi_seq_nonneg.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/cos_pi_seq_pos.con".
+inline procedural "cic:/CoRN/transc/Pi/cos_pi_seq_pos.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/pi_seq_incr.con".
+inline procedural "cic:/CoRN/transc/Pi/pi_seq_incr.con" as lemma.
 
 (*#* Trivial---but useful---consequences. *)
 
-inline procedural "cic:/CoRN/transc/Pi/sin_pi_seq_mon.con".
+inline procedural "cic:/CoRN/transc/Pi/sin_pi_seq_mon.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/sin_pi_seq_nonneg.con".
+inline procedural "cic:/CoRN/transc/Pi/sin_pi_seq_nonneg.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/sin_pi_seq_gt_one.con".
+inline procedural "cic:/CoRN/transc/Pi/sin_pi_seq_gt_one.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/cos_pi_seq_mon.con".
+inline procedural "cic:/CoRN/transc/Pi/cos_pi_seq_mon.con" as lemma.
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/transc/Pi/pi_seq_gt_one.con".
+inline procedural "cic:/CoRN/transc/Pi/pi_seq_gt_one.con" as lemma.
 
 (* UNEXPORTED
 Opaque Sine Cosine.
 *)
 
-inline procedural "cic:/CoRN/transc/Pi/pi_seq_bnd.con".
+inline procedural "cic:/CoRN/transc/Pi/pi_seq_bnd.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/pi_seq_bnd'.con".
+inline procedural "cic:/CoRN/transc/Pi/pi_seq_bnd'.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/pi_seq_bnd''.con".
+inline procedural "cic:/CoRN/transc/Pi/pi_seq_bnd''.con" as lemma.
 
 (* end hide *)
 
 (*#* An auxiliary result. *)
 
-inline procedural "cic:/CoRN/transc/Pi/Sin_One_pos.con".
+inline procedural "cic:/CoRN/transc/Pi/Sin_One_pos.con" as lemma.
 
 (*#* We can now prove that this is a Cauchy sequence.  We define [Pi] as 
 twice its limit.
 *)
 
-inline procedural "cic:/CoRN/transc/Pi/pi_seq_Cauchy.con".
+inline procedural "cic:/CoRN/transc/Pi/pi_seq_Cauchy.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/Pi.con".
+inline procedural "cic:/CoRN/transc/Pi/Pi.con" as definition.
 
 (*#*
 For $x\in[0,\frac{\pi}2)$#x∈[0,π/2)#, [(Cos x) [>] 0];
 $\cos(\frac{pi}2)=0$#cos(π/2)=0#.
 *)
 
-inline procedural "cic:/CoRN/transc/Pi/pos_cos.con".
+inline procedural "cic:/CoRN/transc/Pi/pos_cos.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/Cos_HalfPi.con".
+inline procedural "cic:/CoRN/transc/Pi/Cos_HalfPi.con" as lemma.
 
 (*#* Convergence to [Pi [/] Two] is increasing; therefore, [Pi] is positive. *)
 
-inline procedural "cic:/CoRN/transc/Pi/HalfPi_gt_pi_seq.con".
+inline procedural "cic:/CoRN/transc/Pi/HalfPi_gt_pi_seq.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/pos_Pi.con".
+inline procedural "cic:/CoRN/transc/Pi/pos_Pi.con" as lemma.
 
 (* UNEXPORTED
 End Properties_of_Pi
@@ -137,45 +137,45 @@ A summary of what is being proved is simply:
 [PiSolve] will prove any of these inequalities.
 *)
 
-inline procedural "cic:/CoRN/transc/Pi/pos_HalfPi.con".
+inline procedural "cic:/CoRN/transc/Pi/pos_HalfPi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/pos_QuarterPi.con".
+inline procedural "cic:/CoRN/transc/Pi/pos_QuarterPi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/QuarterPi_less_HalfPi.con".
+inline procedural "cic:/CoRN/transc/Pi/QuarterPi_less_HalfPi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/HalfPi_less_Pi.con".
+inline procedural "cic:/CoRN/transc/Pi/HalfPi_less_Pi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/QuarterPi_less_Pi.con".
+inline procedural "cic:/CoRN/transc/Pi/QuarterPi_less_Pi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/neg_invPi.con".
+inline procedural "cic:/CoRN/transc/Pi/neg_invPi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/neg_invHalfPi.con".
+inline procedural "cic:/CoRN/transc/Pi/neg_invHalfPi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/neg_invQuarterPi.con".
+inline procedural "cic:/CoRN/transc/Pi/neg_invQuarterPi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/invHalfPi_less_invQuarterPi.con".
+inline procedural "cic:/CoRN/transc/Pi/invHalfPi_less_invQuarterPi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/invPi_less_invHalfPi.con".
+inline procedural "cic:/CoRN/transc/Pi/invPi_less_invHalfPi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/invPi_less_invQuarterPi.con".
+inline procedural "cic:/CoRN/transc/Pi/invPi_less_invQuarterPi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/invPi_less_Pi.con".
+inline procedural "cic:/CoRN/transc/Pi/invPi_less_Pi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/invPi_less_HalfPi.con".
+inline procedural "cic:/CoRN/transc/Pi/invPi_less_HalfPi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/invPi_less_QuarterPi.con".
+inline procedural "cic:/CoRN/transc/Pi/invPi_less_QuarterPi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/invHalfPi_less_Pi.con".
+inline procedural "cic:/CoRN/transc/Pi/invHalfPi_less_Pi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/invHalfPi_less_HalfPi.con".
+inline procedural "cic:/CoRN/transc/Pi/invHalfPi_less_HalfPi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/invHalfPi_less_QuarterPi.con".
+inline procedural "cic:/CoRN/transc/Pi/invHalfPi_less_QuarterPi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/invQuarterPi_less_Pi.con".
+inline procedural "cic:/CoRN/transc/Pi/invQuarterPi_less_Pi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/invQuarterPi_less_HalfPi.con".
+inline procedural "cic:/CoRN/transc/Pi/invQuarterPi_less_HalfPi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/invQuarterPi_less_QuarterPi.con".
+inline procedural "cic:/CoRN/transc/Pi/invQuarterPi_less_QuarterPi.con" as lemma.
 
 (* UNEXPORTED
 End Pi_and_Order
@@ -208,23 +208,23 @@ We now move back to trigonometric identities: sine, cosine and tangent of
 the double.
 *)
 
-inline procedural "cic:/CoRN/transc/Pi/Cos_double.con".
+inline procedural "cic:/CoRN/transc/Pi/Cos_double.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/Sin_double.con".
+inline procedural "cic:/CoRN/transc/Pi/Sin_double.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/Tan_double.con".
+inline procedural "cic:/CoRN/transc/Pi/Tan_double.con" as lemma.
 
 (* begin hide *)
 
-inline procedural "cic:/CoRN/transc/Pi/sqrt_lemma.con".
+inline procedural "cic:/CoRN/transc/Pi/sqrt_lemma.con" as lemma.
 
 (* end hide *)
 
 (*#* Value of trigonometric functions at [Pi[/]Four]. *)
 
-inline procedural "cic:/CoRN/transc/Pi/Cos_QuarterPi.con".
+inline procedural "cic:/CoRN/transc/Pi/Cos_QuarterPi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/Sin_QuarterPi.con".
+inline procedural "cic:/CoRN/transc/Pi/Sin_QuarterPi.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve Sin_QuarterPi Cos_QuarterPi: algebra.
@@ -234,31 +234,31 @@ Hint Resolve Sin_QuarterPi Cos_QuarterPi: algebra.
 Opaque Sine Cosine.
 *)
 
-inline procedural "cic:/CoRN/transc/Pi/Tan_QuarterPi.con".
+inline procedural "cic:/CoRN/transc/Pi/Tan_QuarterPi.con" as lemma.
 
 (*#* Shifting sine and cosine by [Pi[/]Two] and [Pi]. *)
 
-inline procedural "cic:/CoRN/transc/Pi/Sin_HalfPi.con".
+inline procedural "cic:/CoRN/transc/Pi/Sin_HalfPi.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve Sin_HalfPi: algebra.
 *)
 
-inline procedural "cic:/CoRN/transc/Pi/Sin_plus_HalfPi.con".
+inline procedural "cic:/CoRN/transc/Pi/Sin_plus_HalfPi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/Sin_HalfPi_minus.con".
+inline procedural "cic:/CoRN/transc/Pi/Sin_HalfPi_minus.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/Cos_plus_HalfPi.con".
+inline procedural "cic:/CoRN/transc/Pi/Cos_plus_HalfPi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/Cos_HalfPi_minus.con".
+inline procedural "cic:/CoRN/transc/Pi/Cos_HalfPi_minus.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/Sin_Pi.con".
+inline procedural "cic:/CoRN/transc/Pi/Sin_Pi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/Cos_Pi.con".
+inline procedural "cic:/CoRN/transc/Pi/Cos_Pi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/Sin_plus_Pi.con".
+inline procedural "cic:/CoRN/transc/Pi/Sin_plus_Pi.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/Cos_plus_Pi.con".
+inline procedural "cic:/CoRN/transc/Pi/Cos_plus_Pi.con" as lemma.
 
 (* UNEXPORTED
 Hint Resolve Sin_plus_Pi Cos_plus_Pi: algebra.
@@ -266,11 +266,11 @@ Hint Resolve Sin_plus_Pi Cos_plus_Pi: algebra.
 
 (*#* Sine and cosine have period [Two Pi], tangent has period [Pi]. *)
 
-inline procedural "cic:/CoRN/transc/Pi/Sin_periodic.con".
+inline procedural "cic:/CoRN/transc/Pi/Sin_periodic.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/Cos_periodic.con".
+inline procedural "cic:/CoRN/transc/Pi/Cos_periodic.con" as lemma.
 
-inline procedural "cic:/CoRN/transc/Pi/Tan_periodic.con".
+inline procedural "cic:/CoRN/transc/Pi/Tan_periodic.con" as lemma.
 
 (* UNEXPORTED
 End Sin_And_Cos