From: Enrico Tassi Date: Tue, 26 Aug 2008 14:56:18 +0000 (+0000) Subject: fixed some stuff X-Git-Tag: make_still_working~4838 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a660b97f5a882da420809831581a7c3202fdaf35;p=helm.git fixed some stuff --- diff --git a/helm/software/matita/contribs/dama/dama/models/list_support.ma b/helm/software/matita/contribs/dama/dama/models/list_support.ma index ea701bb9d..a9d26a9ce 100644 --- a/helm/software/matita/contribs/dama/dama/models/list_support.ma +++ b/helm/software/matita/contribs/dama/dama/models/list_support.ma @@ -38,6 +38,11 @@ interpretation "len" 'len = (length _). notation < "\len \nbsp term 90 l" with precedence 69 for @{'len_appl $l}. interpretation "len appl" 'len_appl l = (length _ l). +lemma mk_list_ext: ∀T:Type.∀f1,f2:nat→T.∀n. (∀x.x H1; [2: apply le_n] +apply eq_f; apply H; intros; apply H1; apply (trans_le ??? H2); apply le_S; apply le_n; +qed. + lemma len_mk_list : ∀T:Type.∀f:nat→T.∀n.\len (\mk_list f n) = n. intros; elim n; [reflexivity] simplify; rewrite > H; reflexivity; qed. @@ -242,3 +247,20 @@ intros; cases (find_lemma ? f l t); apply w; qed. lemma cases_find: ∀T,P,l,d. find_spec T P l d (find T P l d) (find T P l d). intros; unfold find; cases (find_lemma T P l d); simplify; assumption; qed. + +lemma list_elim_with_len: + ∀T:Type.∀P: nat → list T → CProp. + P O [] → (∀l,a,n.P (\len l) l → P (S n) (a::l)) → + ∀l.P (\len l) l. +intros;elim l; [assumption] simplify; apply H1; apply H2; +qed. + +lemma sorted_near: + ∀r,l. sorted r l → ∀i,d. S i < \len l → r (\nth l d i) (\nth l d (S i)). + intros 3; elim H; + [1: cases (not_le_Sn_O ? H1); + |2: simplify in H1; cases (not_le_Sn_O ? (le_S_S_to_le ?? H1)); + |3: simplify; cases i in H4; intros; [apply H1] + apply H3; apply le_S_S_to_le; apply H4] +qed. + 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 de3958907..5098fa724 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma @@ -75,6 +75,11 @@ cases (cmp_nat (\len l) i); apply (H2 n1); simplify in H3; apply (le_S_S_to_le ?? H3);] qed. +alias symbol "lt" (instance 5) = "Q less than". +alias symbol "lt" (instance 4) = "natural 'less than'". +alias symbol "lt" (instance 2) = "natural 'less than'". +alias symbol "leq" = "Q less or equal than". +alias symbol "Q" = "Rationals". coinductive value_spec (f : q_f) (i : ℚ) : ℚ × ℚ → CProp ≝ | value_of : ∀j,q. nth_height (bars f) j = q → nth_base (bars f) j < i → 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 a38cf6e4c..47dccaf5d 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_function.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma @@ -15,61 +15,19 @@ include "russell_support.ma". include "models/q_bars.ma". -definition rebase_spec ≝ - λl1,l2:q_f.λp:q_f × q_f. - And3 - (same_bases (bars (\fst p)) (bars (\snd p))) - (same_values l1 (\fst p)) - (same_values l2 (\snd p)). - -definition same_values_simpl ≝ - λl1,l2.∀p1,p2,p3,p4,p5,p6.same_values (mk_q_f l1 p1 p2 p3) (mk_q_f l2 p4 p5 p6). - -alias symbol "pi2" = "pair pi2". -alias symbol "pi1" = "pair pi1". -definition rebase_spec_aux ≝ - λl1,l2:list bar.λp:(list bar) × (list bar). - sorted q2_lt l1 → sorted q2_lt l2 → - (l1 ≠ [] → \snd (\nth l1 ▭ (pred (\len l1))) = 〈OQ,OQ〉) → - (l2 ≠ [] → \snd (\nth l2 ▭ (pred (\len l2))) = 〈OQ,OQ〉) → - And4 - (nth_base l1 O = nth_base (\fst p) O ∨ - nth_base l2 O = nth_base (\fst p) O) - (sorted q2_lt (\fst p) ∧ sorted q2_lt (\snd p)) - ((l1 ≠ [] → \snd (\nth (\fst p) ▭ (pred (\len (\fst p)))) = 〈OQ,OQ〉) ∧ - (l2 ≠ [] → \snd (\nth (\snd p) ▭ (pred (\len (\snd p)))) = 〈OQ,OQ〉)) - (And3 - (same_bases (\fst p) (\snd p)) - (same_values_simpl l1 (\fst p)) - (same_values_simpl l2 (\snd p))). - -definition eject ≝ - λP.λp:∃x:(list bar) × (list bar).P x.match p with [ex_introT p _ ⇒ p]. -coercion eject. -definition inject ≝ λP.λp:(list bar) × (list bar).λh:P p. ex_introT ? P p h. -coercion inject with 0 1 nocomposites. +(* move in nat/minus *) +lemma minus_lt : ∀i,j. i < j → j - i = S (j - S i). +intros 2; +apply (nat_elim2 ???? i j); simplify; intros; +[1: cases n in H; intros; rewrite < minus_n_O; [cases (not_le_Sn_O ? H);] + simplify; rewrite < minus_n_O; reflexivity; +|2: cases (not_le_Sn_O ? H); +|3: apply H; apply le_S_S_to_le; assumption;] +qed. -axiom devil : False. - definition copy ≝ λl:list bar.make_list ? (λn.〈nth_base l (\len l - S n),〈OQ,OQ〉〉) (\len l). -lemma list_elim_with_len: - ∀T:Type.∀P: nat → list T → CProp. - P O [] → (∀l,a,n.P (\len l) l → P (S n) (a::l)) → - ∀l.P (\len l) l. -intros;elim l; [assumption] simplify; apply H1; apply H2; -qed. - -lemma sorted_near: - ∀r,l. sorted r l → ∀i,d. S i < \len l → r (\nth l d i) (\nth l d (S i)). - intros 3; elim H; - [1: cases (not_le_Sn_O ? H1); - |2: simplify in H1; cases (not_le_Sn_O ? (le_S_S_to_le ?? H1)); - |3: simplify; cases i in H4; intros; [apply H1] - apply H3; apply le_S_S_to_le; apply H4] - qed. - 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)); @@ -104,31 +62,15 @@ apply (sorted_cons q2_lt); |3: apply H; apply le_S_S_to_le; apply H1;]]] qed. -lemma make_list_ext: ∀T,f1,f2,n. (∀x.x H1; [2: apply le_n] -apply eq_f; apply H; intros; apply H1; apply (trans_le ??? H2); apply le_S; apply le_n; +lemma len_copy: ∀l. \len (copy l) = \len l. +intro; unfold copy; apply len_mk_list; qed. - -lemma len_copy: ∀l. \len l = \len (copy l). -intro; elim l; [reflexivity] simplify; rewrite > H; clear H; -apply eq_f; elim (\len (copy l1)) in ⊢ (??%(??(???%))); [reflexivity] simplify; -rewrite > H in ⊢ (??%?); reflexivity; -qed. lemma same_bases_cons: ∀a,b,l1,l2. same_bases l1 l2 → \fst a = \fst b → same_bases (a::l1) (b::l2). intros; intro; cases i; simplify; [assumption;] apply (H n); qed. -lemma minus_lt : ∀i,j. i < j → j - i = S (j - S i). -intros 2; -apply (nat_elim2 ???? i j); simplify; intros; -[1: cases n in H; intros; rewrite < minus_n_O; [cases (not_le_Sn_O ? H);] - simplify; rewrite < minus_n_O; reflexivity; -|2: cases (not_le_Sn_O ? H); -|3: apply H; apply le_S_S_to_le; 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; @@ -137,13 +79,64 @@ apply same_bases_cons; [2: reflexivity] cases l1 in H; [intros 2; reflexivity] simplify in ⊢ (? ? (? ? (λ_:?.? ? ? (? ? %) ?) ?)→?); simplify in ⊢ (?→? ? (? ? (λ_:?.? ? ? (? ? (? % ?)) ?) ?)); -intro; rewrite > (make_list_ext ?? (λn:nat.〈nth_base (b::l2) (\len l2-n),〈OQ,OQ〉〉));[assumption] +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 prepend_sorted_with_same_head: + ∀r,x,l1,l2,d1,d2. + sorted r (x::l1) → sorted r l2 → + (r x (\nth l1 d1 O) → r x (\nth l2 d2 O)) → (l1 = [] → r x d1) → + sorted r (x::l2). +intros 8 (R x l1 l2 d1 d2 Sl1 Sl2); inversion Sl1; inversion Sl2; +intros; destruct; try assumption; [3: apply (sorted_one R);] +[1: apply sorted_cons;[2:assumption] apply H2; apply H3; reflexivity; +|2: apply sorted_cons;[2: assumption] apply H5; apply H6; reflexivity; +|3: apply sorted_cons;[2: assumption] apply H5; assumption; +|4: apply sorted_cons;[2: assumption] apply H8; apply H4;] +qed. + +lemma move_head_sorted: ∀x,l1,l2. + sorted q2_lt (x::l1) → sorted q2_lt l2 → nth_base l2 O = nth_base l1 O → + l1 ≠ [] → sorted q2_lt (x::l2). +intros; apply (prepend_sorted_with_same_head q2_lt x l1 l2 ▭ ▭); +try assumption; intros; unfold nth_base in H2; whd in H4; +[1: rewrite < H2 in H4; assumption; +|2: cases (H3 H4);] +qed. + +definition rebase_spec ≝ + λl1,l2:q_f.λp:q_f × q_f. + And3 + (same_bases (bars (\fst p)) (bars (\snd p))) + (same_values l1 (\fst p)) + (same_values l2 (\snd p)). + + +definition same_values_simpl ≝ + λl1,l2.∀p1,p2,p3,p4,p5,p6.same_values (mk_q_f l1 p1 p2 p3) (mk_q_f l2 p4 p5 p6). + +alias symbol "pi2" = "pair pi2". +alias symbol "pi1" = "pair pi1". +definition rebase_spec_aux ≝ + λl1,l2:list bar.λp:(list bar) × (list bar). + sorted q2_lt l1 → sorted q2_lt l2 → + (l1 ≠ [] → \snd (\nth l1 ▭ (pred (\len l1))) = 〈OQ,OQ〉) → + (l2 ≠ [] → \snd (\nth l2 ▭ (pred (\len l2))) = 〈OQ,OQ〉) → + And4 + (nth_base l1 O = nth_base (\fst p) O ∨ + nth_base l2 O = nth_base (\fst p) O) + (sorted q2_lt (\fst p) ∧ sorted q2_lt (\snd p)) + ((l1 ≠ [] → \snd (\nth (\fst p) ▭ (pred (\len (\fst p)))) = 〈OQ,OQ〉) ∧ + (l2 ≠ [] → \snd (\nth (\snd p) ▭ (pred (\len (\snd p)))) = 〈OQ,OQ〉)) + (And3 + (same_bases (\fst p) (\snd p)) + (same_values_simpl l1 (\fst p)) + (same_values_simpl l2 (\snd p))). + lemma copy_rebases: ∀l1.rebase_spec_aux l1 [] 〈l1, copy l1〉. intros; elim l1; intros 4; @@ -156,7 +149,7 @@ intros; elim l1; intros 4; [1: apply (sorted_copy ? H1); |2: apply (copy_same_bases (a::l));]] qed. - + lemma copy_rebases_r: ∀l1.rebase_spec_aux [] l1 〈copy l1, l1〉. intros; elim l1; intros 4; @@ -169,12 +162,16 @@ intros; elim l1; intros 4; [1: apply (sorted_copy ? H2); |2: intro; symmetry; apply (copy_same_bases (a::l));]] qed. - + +definition eject ≝ + λP.λp:∃x:(list bar) × (list bar).P x.match p with [ex_introT p _ ⇒ p]. +coercion eject. +definition inject ≝ λP.λp:(list bar) × (list bar).λh:P p. ex_introT ? P p h. +coercion inject with 0 1 nocomposites. + definition rebase: ∀l1,l2:q_f.∃p:q_f × q_f.rebase_spec l1 l2 p. intros 2 (f1 f2); cases f1 (b1 Hs1 Hb1 He1); cases f2 (b2 Hs2 Hb2 He2); clear f1 f2; -alias symbol "plus" = "natural plus". -alias symbol "pi2" = "pair pi2". -alias symbol "pi1" = "pair pi1". +alias symbol "leq" = "natural 'less or equal to'". alias symbol "minus" = "Q minus". letin aux ≝ ( let rec aux (l1,l2:list bar) (n : nat) on n : (list bar) × (list bar) ≝ @@ -223,19 +220,27 @@ in aux : ∀l1,l2,m.∃z.\len l1 + \len l2 ≤ m → rebase_spec_aux l1 l2 z); |5: intros; apply copy_rebases_r; |4: intros; rewrite < H1; apply copy_rebases; |3: cut (\fst b = \fst b3) as K; [2: apply q_le_to_le_to_eq; assumption] clear H6 H5 H4 H3; - intros; cases (aux l2 l3 n1); intros 4; simplify in match (\fst ≪w,H≫); + intros; cases (aux l2 l3 n1); cases w in H4 (w1 w2); clear w; + intros 5; simplify in match (\fst 〈?,?〉); simplify in match (\snd 〈?,?〉); - cases H4; + cases H5; [2: apply le_S_S_to_le; apply (trans_le ???? H3); simplify; rewrite < plus_n_Sm; apply le_S; apply le_n; - |3,4: apply (sorted_tail q2_lt); [2: apply H5|4:apply H6] + |3,4: apply (sorted_tail q2_lt); [2: apply H4|4:apply H6] |5: intro; cases l2 in H7 H9; intros; [cases H9; reflexivity] simplify in H7 ⊢ %; apply H7; intro; destruct H10; |6: intro; cases l3 in H8 H9; intros; [cases H9; reflexivity] simplify in H8 ⊢ %; apply H8; intro; destruct H10;] - clear aux; split; + clear aux H5; + simplify in match (\fst 〈?,?〉) in H9 H10 H11 H12; + simplify in match (\snd 〈?,?〉) in H9 H10 H11 H12; + split; [1: left; reflexivity; - |2: cases H10; + |2: cases H10; cases H12; clear H15 H16 H12 H7 H8 H11 H10; + cases H9; clear H9; + [1: lapply (H14 O) as K1; clear H14; change in K1 with (nth_base w1 O = nth_base w2 O); + split; + [1: apply (move_head_sorted ??? H4 H5 H7); STOP diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma index 45a8a1b37..06c222830 100644 --- a/helm/software/matita/contribs/dama/dama/ordered_set.ma +++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "datatypes/constructors.ma". include "logic/cprop_connectives.ma". (* Definition 2.1 *)