From 6cf3c0175d80cf96862e824f13109c072ffb12d4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 3 Jul 2008 08:00:54 +0000 Subject: [PATCH] ... --- .../matita/contribs/dama/dama/depends | 26 +++++++++---------- .../contribs/dama/dama/models/q_bars.ma | 26 ++++++++----------- 2 files changed, 24 insertions(+), 28 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index 4fc4c9d0f..b466b2e07 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -1,29 +1,29 @@ +sandwich.ma ordered_uniform.ma property_sigma.ma ordered_uniform.ma russell_support.ma +uniform.ma supremum.ma bishop_set.ma ordered_set.ma +sequence.ma nat/nat.ma ordered_uniform.ma uniform.ma +supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma +property_exhaustivity.ma ordered_uniform.ma property_sigma.ma bishop_set_rewrite.ma bishop_set.ma -sequence.ma nat/nat.ma +cprop_connectives.ma datatypes/constructors.ma logic/equality.ma nat_ordered_set.ma bishop_set.ma nat/compare.ma lebesgue.ma property_exhaustivity.ma sandwich.ma -property_exhaustivity.ma ordered_uniform.ma property_sigma.ma -cprop_connectives.ma datatypes/constructors.ma logic/equality.ma ordered_set.ma cprop_connectives.ma -sandwich.ma ordered_uniform.ma russell_support.ma cprop_connectives.ma nat/nat.ma -uniform.ma supremum.ma -supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma +models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma -models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma models/q_support.ma Q/q/qplus.ma Q/q/qtimes.ma cprop_connectives.ma -models/q_shift.ma models/q_bars.ma -models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.ma -models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma -models/list_support.ma list/list.ma -models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma models/discrete_uniformity.ma bishop_set_rewrite.ma uniform.ma -models/q_function.ma Q/q/qtimes.ma models/q_shift.ma nat_ordered_set.ma models/q_bars.ma cprop_connectives.ma models/list_support.ma models/q_support.ma nat_ordered_set.ma +models/q_function.ma Q/q/qtimes.ma models/q_shift.ma nat_ordered_set.ma +models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma +models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma models/q_value_skip.ma models/q_shift.ma +models/q_shift.ma models/q_bars.ma +models/list_support.ma list/list.ma +models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.ma Q/q/qplus.ma Q/q/qtimes.ma datatypes/constructors.ma diff --git a/helm/software/matita/contribs/dama/dama/models/q_bars.ma b/helm/software/matita/contribs/dama/dama/models/q_bars.ma index 06b4a67e0..c1a017dcc 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma @@ -113,8 +113,6 @@ letin value_spec_aux ≝ ( (nth_base f (\fst q) < i ∧ ∀n.(\fst q) < n → n < len f → i ≤ nth_base f n)); alias symbol "lt" (instance 5) = "Q less than". letin value ≝ ( - METTERE IN ACC LA LISTA PROCESSATA SO FAR - E DIRE CHE QUELLA@L=BARS let rec value (acc: nat × ℚ) (l : list bar) on l : nat × ℚ ≝ match l with [ nil ⇒ acc @@ -124,25 +122,23 @@ letin value ≝ ( | q_gt _ ⇒ acc]] in value : ∀acc,l.∃p:nat × ℚ. - (∀i.i < len l → nth_base (bars f) (\fst acc) < nth_base l i) → - nth_height (bars f) (\fst acc) = \snd acc → + ∀story. story @ l = bars f → + value_spec_aux story (Qpos i) acc → value_spec_aux l (Qpos i) p); -[3: intros; unfold; [4: clearbody value; unfold value_spec; generalize in match (bars_begin_OQ f); generalize in match (bars_sorted f); - cases (bars_not_nil f); intro S; generalize in match (sorted_tail_bigger ?? S); - clear S; cases (value 〈O,\snd x〉 (x::l)) (p Hp); intros; - exists[apply (\snd p)];exists [apply (\fst p)] - cases (Hp ?) (Hg HV); + cases (bars_not_nil f) in value; intros (value S); generalize in match (sorted_tail_bigger ?? S); + clear S; cases (value 〈O,\snd x〉 l) (p Hp); intros; + exists[apply (\snd p)];exists [apply (S (\fst p))] simplify; + cases (Hp [x] (refl_eq ??) ?) (Hg HV); [unfold; split[reflexivity]simplify;split; - [rewrite > H1;apply q_pos_OQ; + [rewrite > H;apply q_pos_OQ; |intros; cases n in H2 H3; [intro X; cases (not_le_Sn_O ? X)] - intros; - rewrite > H1; apply q_pos_OQ; - cases HV (Hi Hm); clear Hp value value_spec_aux HV; - exists [apply (\fst p)]; split;[rewrite > Hg;reflexivity|split;[assumption]intros] - apply Hm; assumption; + intros; cases (not_le_Sn_O ? (le_S_S_to_le ?? H3))]] + split;[rewrite > Hg; reflexivity]split; cases HV; [assumption;] + intros; cases n in H4 H5; intros [cases (not_le_Sn_O ? H4)] + apply (H3 n1);apply le_S_S_to_le; assumption; |1: unfold value_spec_aux; clear value value_spec_aux H2;intros; split[2:split] [1: apply (q_lt_le_trans ??? (H4 (\fst p))); clear H4 H5; -- 2.39.2