From: Enrico Tassi Date: Fri, 26 Sep 2008 08:00:53 +0000 (+0000) Subject: some work X-Git-Tag: make_still_working~4735 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=99feea74c16b4801a2b1596d5e48e27224ffbfaa;p=helm.git some work --- diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index 393b547d8..2a59fb1aa 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -1,31 +1,28 @@ -bishop_set.ma ordered_set.ma -nat_ordered_set.ma bishop_set.ma nat/compare.ma -models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma -models/q_rebase.ma Q/q/qtimes.ma models/q_function.ma property_exhaustivity.ma ordered_uniform.ma property_sigma.ma -ordered_uniform.ma uniform.ma -models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma -models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma -ordered_set.ma datatypes/constructors.ma logic/cprop_connectives.ma -models/list_support.ma list/list.ma logic/cprop_connectives.ma nat/minus.ma -uniform.ma supremum.ma -sandwich.ma ordered_uniform.ma -models/q_value_skip.ma -models/q_shift.ma +sequence.ma nat/nat.ma +supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma +property_sigma.ma ordered_uniform.ma russell_support.ma +bishop_set_rewrite.ma bishop_set.ma models/q_support.ma Q/q/qplus.ma Q/q/qtimes.ma logic/cprop_connectives.ma +sandwich.ma ordered_uniform.ma +nat_ordered_set.ma bishop_set.ma nat/compare.ma +ordered_set.ma datatypes/constructors.ma logic/cprop_connectives.ma +models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma models/q_bars.ma logic/cprop_connectives.ma models/list_support.ma models/q_support.ma nat_ordered_set.ma russell_support.ma -models/q_copy.ma models/q_bars.ma -models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.ma -property_sigma.ma ordered_uniform.ma russell_support.ma +models/list_support.ma list/list.ma logic/cprop_connectives.ma nat/le_arith.ma nat/minus.ma +bishop_set.ma ordered_set.ma lebesgue.ma property_exhaustivity.ma sandwich.ma +models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.ma models/discrete_uniformity.ma bishop_set_rewrite.ma uniform.ma -models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma -bishop_set_rewrite.ma bishop_set.ma russell_support.ma logic/cprop_connectives.ma nat/nat.ma -.unnamed.ma models/q_bars.ma -supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma +models/q_copy.ma models/q_bars.ma +models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma +models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma models/q_function.ma models/q_copy.ma russell_support.ma -sequence.ma nat/nat.ma +models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma +uniform.ma supremum.ma +ordered_uniform.ma uniform.ma +models/q_rebase.ma Q/q/qtimes.ma models/q_function.ma Q/q/qplus.ma Q/q/qtimes.ma datatypes/constructors.ma diff --git a/helm/software/matita/contribs/dama/dama/depends.png b/helm/software/matita/contribs/dama/dama/depends.png index 7f2a60dcc..87c0beacb 100644 Binary files a/helm/software/matita/contribs/dama/dama/depends.png and b/helm/software/matita/contribs/dama/dama/depends.png differ 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 baf0bcfda..79cc540a8 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma @@ -249,7 +249,26 @@ clear H12 H4; cases j in H8 H5 H6 H7; lapply (H16 n); [2: assumption|3:simplify; apply le_S_S_to_le; assumption] apply (q_lt_corefl ? (q_le_lt_trans ??? Hletin H4));]] qed. - + +lemma value_unit: + ∀x,i,h1,h2,h3.value_simpl [x] h1 h2 i h3 = \snd x. +intros; cases (cases_value_simpl [x] h1 h2 i h3); cases j in H H2; simplify; +intros; [2: cases (?:False); apply (not_le_Sn_O n); apply le_S_S_to_le; apply H2] +symmetry; assumption; +qed. + +lemma same_value_tail: + ∀b,b1,h1,h3,xs,r1,input,H12,H13,Hi1,H14,H15,Hi2. + same_values_simpl (〈b1,h1〉::xs) (〈b1,h3〉::r1) → + value_simpl (b::〈b1,h1〉::xs) H12 H13 input Hi1 + =value_simpl (b::〈b1,h3〉::r1) H14 H15 input Hi2. +intros; cases (q_cmp (Qpos input) b1); +[1: rewrite > (value_head 〈b1,h1〉 b xs); [2:assumption] + rewrite > (value_head 〈b1,h3〉 b r1); [2:assumption] reflexivity; +|2: rewrite > (value_tail 〈b1,h1〉 b xs);[2: assumption] + rewrite > (value_tail 〈b1,h3〉 b r1);[2: assumption] apply H;] +qed. + definition same_bases ≝ λl1,l2:list bar. ∀i.\fst (\nth l1 ▭ i) = \fst (\nth l2 ▭ i). lemma same_bases_cons: ∀a,b,l1,l2. diff --git a/helm/software/matita/contribs/dama/dama/models/q_copy.ma b/helm/software/matita/contribs/dama/dama/models/q_copy.ma index 78e4ea821..00788cd16 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_copy.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_copy.ma @@ -24,76 +24,43 @@ apply (nat_elim2 ???? i j); simplify; intros; |3: apply H; apply le_S_S_to_le; assumption;] qed. -definition copy ≝ - λl:list bar.make_list ? (λn.〈nth_base l (\len l - S n),〈OQ,OQ〉〉) (\len l). +alias symbol "lt" = "bar lt". +lemma inversion_sorted: + ∀a,l. sorted q2_lt (a::l) → Or (a < \hd ▭ l) (l = []). +intros 2; elim l; [right;reflexivity] left; inversion H1; intros; +[1,2:destruct H2| destruct H5; assumption] +qed. + +lemma inversion_sorted2: + ∀a,b,l. sorted q2_lt (a::b::l) → a < b. +intros; inversion H; intros; [1,2:destruct H1] destruct H4; assumption; +qed. + +let rec copy (l : list bar) on l : list bar ≝ + match l with + [ nil ⇒ [] + | cons x tl ⇒ 〈\fst x, 〈OQ,OQ〉〉 :: copy tl]. lemma sorted_copy: ∀l:list bar.sorted q2_lt l → sorted q2_lt (copy l). -intros 2; unfold copy; generalize in match (le_n (\len l)); -elim (\len l) in ⊢ (?%?→? ? (? ? ? %)); -simplify; [apply (sorted_nil q2_lt);] cases n in H1 H2; -simplify; intros; [apply (sorted_one q2_lt);] -apply (sorted_cons q2_lt); -[2: apply H1; apply lt_to_le; apply H2; -|1: elim l in H2 H; simplify; [simplify in H2; cases (not_le_Sn_O ? H2)] - simplify in H3; unfold nth_base; - unfold canonical_q_lt; unfold q2_trel; unfold q2_lt; simplify; - change with (q2_lt (\nth (a::l1) ▭ (\len l1-S n1)) (\nth (a::l1) ▭ (\len l1-n1))); - cut (∃w.w = \len l1 - S n1); [2: exists[apply (\len l1 - S n1)] reflexivity] - cases Hcut; rewrite < H4; rewrite < (?:S w = \len l1 - n1); - [1: apply (sorted_near q2_lt (a::l1) H2); rewrite > H4; - simplify; apply le_S_S; elim (\len l1) in H3; simplify; - [ cases (not_le_Sn_O ? (le_S_S_to_le ?? H3)); - | lapply le_S_S_to_le to H5 as H6; - lapply le_S_S_to_le to H6 as H7; clear H5 H6; - cases H7 in H3; intros; [rewrite < minus_n_n; apply le_S_S; apply le_O_n] - simplify in H5; apply le_S_S; apply (trans_le ???? (H5 ?)); - [2: apply le_S_S; apply le_S_S; assumption; - |1: apply (lt_minus_S_n_to_le_minus_n n1 (S m) (S (minus m n1)) ?). - apply (not_le_to_lt (S (minus m n1)) (minus (S m) (S n1)) ?). - apply (not_le_Sn_n (minus (S m) (S n1))).]] - |2: rewrite > H4; lapply le_S_S_to_le to H3 as K; - clear H4 Hcut H3 H H1 H2; generalize in match K; clear K; - apply (nat_elim2 ???? n1 (\len l1)); simplify; intros; - [1: rewrite < minus_n_O; cases n2 in H; [intro; cases (not_le_Sn_O ? H)] - intros; cases n3; simplify; reflexivity; - |2: cases (not_le_Sn_O ? H); - |3: apply H; apply le_S_S_to_le; apply H1;]]] +intro l; elim l; [apply (sorted_nil q2_lt)] simplify; +cases l1 in H H1; simplify; intros; [apply (sorted_one q2_lt)] +apply (sorted_cons q2_lt); [2: apply H; apply (sorted_tail q2_lt ?? H1);] +apply (inversion_sorted2 ??? H1); qed. lemma len_copy: ∀l. \len (copy l) = \len l. -intro; unfold copy; apply len_mk_list; +intro; elim l; [reflexivity] simplify; apply eq_f; assumption; qed. lemma copy_same_bases: ∀l. same_bases l (copy l). -intro; unfold copy; elim l using list_elim_with_len; [1: intro;reflexivity] -simplify; rewrite < minus_n_n; -simplify in ⊢ (? ? (? ? (? ? ? % ?) ?)); -apply same_bases_cons; [2: reflexivity] -cases l1 in H; [intros 2; reflexivity] -simplify in ⊢ (? ? (? ? (λ_:?.? ? ? (? ? %) ?) ?)→?); -simplify in ⊢ (?→? ? (? ? (λ_:?.? ? ? (? ? (? % ?)) ?) ?)); -intro; rewrite > (mk_list_ext ?? (λn:nat.〈nth_base (b::l2) (\len l2-n),〈OQ,OQ〉〉));[assumption] -intro; elim x; [simplify; rewrite < minus_n_O; reflexivity] -simplify in ⊢ (? ? (? ? ? (? ? %) ?) ?); -simplify in H2:(? ? %); rewrite > minus_lt; [reflexivity] apply le_S_S_to_le; -assumption; -qed. - -lemma rewrite_ext_nth_height : ∀n,m,f,f1,g,g1. (∀t.g t = g1 t) → -nth_height (\mk_list (λn.〈f n,g n〉) m) n = nth_height (\mk_list (λn.〈f1 n,g1 n〉) m) n. -intros; generalize in match n; clear n; elim m; [reflexivity] simplify; -cases n1; [simplify;apply H;] simplify; apply (H1 n2); +intros; elim l; [intro; reflexivity] intro; simplify; cases i; [reflexivity] +simplify; apply (H n); qed. lemma copy_OQ : ∀l,n.nth_height (copy l) n = 〈OQ,OQ〉. -intro; elim l; [cases n; [reflexivity] simplify; rewrite > nth_nil; reflexivity] -cases n; simplify [reflexivity] -change with (nth_height (\mk_list (λn:ℕ.〈nth_base (a::l1) (\len l1-n),〈OQ,OQ〉〉) (\len l1)) n1 = 〈OQ,OQ〉); -rewrite > (rewrite_ext_nth_height ??? (λ_.OQ) ? (λ_.〈OQ,OQ〉)); [2: intros; reflexivity] -generalize in match n1; -elim (\len l1); simplify; unfold nth_height; [rewrite > nth_nil; reflexivity] -cases n3; simplify; [reflexivity] apply (H1 n4); +intro; elim l; [elim n;[reflexivity] simplify; assumption] +simplify; cases n; [reflexivity] simplify; apply (H n1); qed. lemma prepend_sorted_with_same_head: @@ -118,17 +85,6 @@ try assumption; intros; unfold nth_base in H2; whd in H4; |2: cases (H3 H4);] qed. -alias symbol "lt" = "bar lt". -lemma inversion_sorted: - ∀a,l. sorted q2_lt (a::l) → Or (a < \hd ▭ l) (l = []). -intros 2; elim l; [right;reflexivity] left; inversion H1; intros; -[1,2:destruct H2| destruct H5; assumption] -qed. - -lemma inversion_sorted2: - ∀a,b,l. sorted q2_lt (a::b::l) → a < b. -intros; inversion H; intros; [1,2:destruct H1] destruct H4; assumption; -qed. lemma sort_q2lt_same_base: ∀b,h1,h2,l. sorted q2_lt (〈b,h1〉::l) → sorted q2_lt (〈b,h2〉::l). @@ -137,3 +93,17 @@ lapply (sorted_tail q2_lt ?? H) as K; clear H; cases l in H1 K; simplify; intros [apply (sorted_one q2_lt);|apply (sorted_cons q2_lt);[2: assumption] apply H] qed. + +lemma value_copy : + ∀l,h1,h2,i,h3. + value_simpl (copy l) h1 h2 i h3 = 〈OQ,OQ〉. +intros; elim l in h1 h2 h3; [cases (not_le_Sn_O ? H1);] +cases l1 in H H1 H2 H3; +[1: intros; simplify in ⊢ (? ? (? % ? ? ? ?) ?); + rewrite > (value_unit 〈\fst a,〈OQ,OQ〉〉); reflexivity; +|2: intros; simplify in H2 H3 H4 ⊢ (? ? (? % ? ? ? ?) ?); + cases (q_cmp (Qpos i) (\fst b)); + [2: rewrite > (value_tail ??? H2 H3 ? H4 H1); apply H; + |1: rewrite > (value_head ??? H2 H3 ? H4 H1); reflexivity]] +qed. + \ No newline at end of file diff --git a/helm/software/matita/contribs/dama/dama/models/q_function.ma b/helm/software/matita/contribs/dama/dama/models/q_function.ma index e16f75116..26c319c74 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_function.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma @@ -23,13 +23,9 @@ definition rebase_spec ≝ (same_values l2 (\snd p)). inductive rebase_cases : list bar → list bar → (list bar) × (list bar) → Prop ≝ -| rb_fst_full : ∀b,h1,xs. (*〈b,h1〉 < \hd ▭ ys → *) -(* \snd(\last ▭ (〈b,h1〉::xs)) = \snd(\last ▭ (〈b,h1〉::r1)) → - \snd(\last ▭ (〈b,h1〉::xs)) = \snd(\last ▭ (〈b,h2〉::r2)) →*) +| rb_fst_full : ∀b,h1,xs. rebase_cases (〈b,h1〉::xs) [] 〈〈b,h1〉::xs,〈b,〈OQ,OQ〉〉::copy xs〉 -| rb_snd_full : ∀b,h1,ys. (*〈b,h1〉 < \hd ▭ xs →*) - (* \snd(\last ▭ (〈b,h1〉::ys)) = \snd(\last ▭ (〈b,h1〉::r2)) → - \snd(\last ▭ (〈b,h1〉::ys)) = \snd(\last ▭ (〈b,h2〉::r1)) →*) +| rb_snd_full : ∀b,h1,ys. rebase_cases [] (〈b,h1〉::ys) 〈〈b,〈OQ,OQ〉〉::copy ys,〈b,h1〉::ys〉 | rb_all_full : ∀b,h1,h2,h3,h4,xs,ys,r1,r2. \snd(\last ▭ (〈b,h1〉::xs)) = \snd(\last ▭ (〈b,h3〉::r1)) → @@ -39,12 +35,12 @@ inductive rebase_cases : list bar → list bar → (list bar) × (list bar) → \snd(\last ▭ (〈b1,h1〉::xs)) = \snd(\last ▭ (〈b1,h1〉::r1)) → \snd(\last ▭ (〈b2,h2〉::ys)) = \snd(\last ▭ (〈b1,h2〉::r2)) → b1 < b2 → - rebase_cases (〈b1,h1〉::xs) (〈b2,h2〉::ys) 〈〈b1,h1〉::r1,〈b1,h2〉::r2〉 + rebase_cases (〈b1,h1〉::xs) (〈b2,h2〉::ys) 〈〈b1,h1〉::r1,〈b1,〈OQ,OQ〉〉::r2〉 | rb_all_full_r : ∀b1,b2,h1,h2,xs,ys,r1,r2. \snd(\last ▭ (〈b1,h1〉::xs)) = \snd(\last ▭ (〈b2,h1〉::r1)) → \snd(\last ▭ (〈b2,h2〉::ys)) = \snd(\last ▭ (〈b2,h2〉::r2)) → b2 < b1 → - rebase_cases (〈b1,h1〉::xs) (〈b2,h2〉::ys) 〈〈b2,h1〉::r1,〈b2,h2〉::r2〉 + rebase_cases (〈b1,h1〉::xs) (〈b2,h2〉::ys) 〈〈b2,〈OQ,OQ〉〉::r1,〈b2,h2〉::r2〉 | rb_all_empty : rebase_cases [] [] 〈[],[]〉. alias symbol "pi2" = "pair pi2". @@ -54,16 +50,10 @@ inductive rebase_spec_aux_p (l1, l2:list bar) (p:(list bar) × (list bar)) : Pro | prove_rebase_spec_aux: rebase_cases l1 l2 p → (sorted q2_lt (\fst p)) → - (sorted q2_lt (\snd p)) → True → True → (* - ((l1 ≠ [] ∧ \snd (\last ▭ (\fst p)) = 〈OQ,OQ〉) ∨ - (l1 = [] ∧ ∀i.\snd (\nth (\fst p) ▭ i) = 〈OQ,OQ〉)) → - ((l2 ≠ [] ∧ \snd (\last ▭ (\snd p)) = 〈OQ,OQ〉) ∨ - (l2 = [] ∧ ∀i.\snd (\nth (\snd p) ▭ i) = 〈OQ,OQ〉)) →*) + (sorted q2_lt (\snd p)) → (same_bases (\fst p) (\snd p)) → (same_values_simpl l1 (\fst p)) → (same_values_simpl l2 (\snd p)) → - (*\len (\fst p) ≤ \len l1 + \len l2 → *) - (*\len (\fst p) = \len (\snd p) → *) rebase_spec_aux_p l1 l2 p. lemma aux_preserves_sorting: diff --git a/helm/software/matita/contribs/dama/dama/models/q_rebase.ma b/helm/software/matita/contribs/dama/dama/models/q_rebase.ma index f2423954f..93e0d19e7 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_rebase.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_rebase.ma @@ -13,7 +13,24 @@ (**************************************************************************) include "models/q_function.ma". - + +alias symbol "lt" = "Q less than". +alias symbol "Q" = "Rationals". +axiom q_unlimited: ∀x:ℚ.∃y:ratio.x (value_unit 〈b1,h1〉) in K; + rewrite > (value_unit 〈b2,〈OQ,OQ〉〉) in K; assumption; +|2: intros; (* MANCA che le basi sono positive, + poi con halving prendi tra b1 e \fst p e hai h1=OQ,OQ*) + + definition eject ≝ λP.λp:∃x:(list bar) × (list bar).P x.match p with [ex_introT p _ ⇒ p]. coercion eject. @@ -57,34 +74,45 @@ in aux : ∀l1,l2,m.∃z.\len l1 + \len l2 ≤ m → rebase_spec_aux l1 l2 z); [7: clearbody aux; cases (aux b1 b2 (\len b1 + \len b2)) (res Hres); exists; [split; constructor 1; [apply (\fst res)|5:apply (\snd res)]] [1,4: apply hide; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); assumption; - |2,5: apply hide; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); lapply (H5 O) as K; - clear H1 H2 H3 H4 H5 H6 H7 Hres aux; unfold nth_base; + |2,5: apply hide; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); clear Hres aux; + lapply (H3 O) as K; clear H1 H2 H3 H4 H5; unfold nth_base; cases H in K He1 He2 Hb1 Hb2; simplify; intros; assumption; - |3,6: apply hide; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); + |3,6: apply hide; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); clear Hres aux; cases H in He1 He2; simplify; intros; [1,6,8,12: assumption; |2,7: rewrite > len_copy; generalize in match (\len ?); intro X; cases X; [1,3: reflexivity] simplify; [apply (copy_OQ ys n);|apply (copy_OQ xs n);] - |3,4,5: rewrite < H8; assumption; - |9,10,11: rewrite < H9; assumption]] - split; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); unfold same_values; intros; + |3,4: rewrite < H6; assumption; + |5: cases r1 in H6; simplify; intros; [reflexivity] rewrite < H6; assumption; + |9,11: rewrite < H7; assumption; + |10: cases r2 in H7; simplify; intros; [reflexivity] rewrite < H7; assumption]] + split; cases (Hres (le_n ?) Hs1 He1 Hs2 He2); clear Hres; unfold same_values; intros; [1: assumption |2,3: simplify in match (\snd 〈?,?〉); simplify in match (\fst 〈?,?〉); apply same_values_simpl_to_same_values; assumption] |3: cut (\fst b3 = \fst b) as E; [2: apply q_le_to_le_to_eq; assumption] - clear H6 H5 H4 H3 He2 Hb2 Hs2 b2 He1 Hb1 Hs1 b1; cases (aux l2 l3 n1); + clear H6 H5 H4 H3 He2 Hb2 Hs2 b2 He1 Hb1 Hs1 b1; cases (aux l2 l3 n1) (rc Hrc); clear aux; intro K; simplify in K; rewrite H3; rewrite > len_copy; elim (\len ys); [reflexivity] + [1: cases b in E Hsbl2 Hendbl2; cases b3 in Hsb3l3 Hendb3l3; intros (Hsbl3 Hendbl2 E Hsb3l2 Hendb3l3); + simplify in E; destruct E; constructor 3; + [1: clear Hendbl2 Hsbl3 SV2 SB S2; + cases RC in S1 SV1 Hsb3l2 Hendb3l3; intros; + [1,6: reflexivity; + |3,4: assumption; + |5: simplify in H6:(??%) ⊢ %; rewrite > H3; cases r1 in H6; intros [2:reflexivity] + use same_values_unit_OQ; + + |2: simplify in H3:(??%) ⊢ %; rewrite > H3; rewrite > len_copy; elim (\len ys); [reflexivity] symmetry; apply (copy_OQ ys n2); | cases H8 in H5 H7; simplify; intros; [2,6:reflexivity|3,4,5: assumption] simplify; rewrite > H5; rewrite > len_copy; elim (\len xs); [reflexivity] @@ -98,16 +126,20 @@ in aux : ∀l1,l2,m.∃z.\len l1 + \len l2 ≤ m → rebase_spec_aux l1 l2 z); |4: apply I |5: apply I |6: intro; elim i; intros; simplify; solve [symmetry;assumption|apply H13] - |7: unfold; intros; cases H8 in H13 H14 H15 Hi1 Hi2 H17 H18 H3 H16; intros; - [1: simplify in match (\fst 〈?,?〉) in H16 H17 H20 H21 H22 H23 ⊢ %; - cases (q_cmp (Qpos input) b1); - [1: do 2 (rewrite > value_head; [id|assumption]); reflexivity; - |2: do 2 (rewrite > value_tail;[id|assumption]); apply H16;] - |2: simplify in match (\fst 〈?,?〉) in H16 H17 H20 H21 H22 H23 ⊢ %; - cases (q_cmp (Qpos input) b1); - [1: rewrite > value_head; [2:assumption] - |2: rewrite > value_tail;[2:assumption] - simplify in H15; + |7: unfold; intros; clear H9 H10 H11 H12 H13; simplify in Hi1 Hi2 H16 H18; + cases H8 in H14 H15 H17 H3 H16 H18 H5 H6; + simplify in match (\fst 〈?,?〉); simplify in match (\snd 〈?,?〉); intros; + [1: reflexivity; + |2: simplify in H3; rewrite > (value_unit b); rewrite > H3; symmetry; + cases b in H3 H12 Hi2; intros 2; simplify in H12; rewrite > H12; + intros; change in ⊢ (? ? (? % ? ? ? ?) ?) with (copy (〈q,〈OQ,OQ〉〉::〈b1,〈OQ,OQ〉〉::ys)); + apply (value_copy (〈q,〈OQ,OQ〉〉::〈b1,〈OQ,OQ〉〉::ys)); + |3: apply (same_value_tail b b1 h1 h3 xs r1 input); assumption; + |4: apply (same_value_tail b b1 h1 h1 xs r1 input); assumption; + |5: simplify in H9; STOP + + |6: reflexivity;] + ] |8: diff --git a/helm/software/matita/contribs/dama/dama/models/q_shift.ma b/helm/software/matita/contribs/dama/dama/models/q_shift.ma deleted file mode 100644 index e69de29bb..000000000 diff --git a/helm/software/matita/contribs/dama/dama/models/q_value_skip.ma b/helm/software/matita/contribs/dama/dama/models/q_value_skip.ma deleted file mode 100644 index e69de29bb..000000000