X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fq_function.ma;h=a38cf6e4cda648377be8ea314956b673a2f2becd;hb=b12a46d53cf80d40b253ca5dd495397c5c0b4287;hp=2ca8fc3ce753d07b058d68de09e28680d5e13061;hpb=6080552519697d67971ff21c17b563359fab9a05;p=helm.git 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 2ca8fc3ce..a38cf6e4c 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_function.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma @@ -52,23 +52,124 @@ coercion inject with 0 1 nocomposites. axiom devil : False. definition copy ≝ - λl:list bar.make_list ? (λn.〈nth_base l (n - \len l),〈OQ,OQ〉〉) (\len l). + λ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)); +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;]]] +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; +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; +simplify in ⊢ (? ? (? ? (? ? ? % ?) ?)); +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; 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 copy_rebases: ∀l1.rebase_spec_aux l1 [] 〈l1, copy l1〉. -intros; cases l1; intros 4; +intros; elim l1; intros 4; [1: split; [left; reflexivity]; split; try assumption; unfold; intros; unfold same_values; intros; reflexivity; -|2: rewrite > H2; [2: intro X; destruct X] clear H2 H3; +|2: rewrite > H3; [2: intro X; destruct X] split; [left; reflexivity] split; unfold same_values_simpl; unfold same_values; intros; try reflexivity; - try assumption; [4: normalize in p2; destruct p2|2: cases H2; reflexivity;] - simplify; clear H1; - [1: elim (\len l) in H; simplify; [apply (sorted_one q2_lt);] - - - - + try assumption; [4: normalize in p2; destruct p2|2: cases H5; reflexivity;] + [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; +[1: split; [left; reflexivity]; split; try assumption; unfold; intros; + unfold same_values; intros; reflexivity; +|2: rewrite > H4; [2: intro X; destruct X] + split; [right; simplify; rewrite < minus_n_n; reflexivity] split; + unfold same_values_simpl; unfold same_values; intros; try reflexivity; + try assumption; [4: normalize in p2; destruct p2|2: cases H5; reflexivity;] + [1: apply (sorted_copy ? H2); + |2: intro; symmetry; apply (copy_same_bases (a::l));]] +qed. + 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". @@ -104,9 +205,9 @@ match n with let rest ≝ base1 - base2 in let rc ≝ aux (〈rest,height1〉 :: tl1) tl2 m in 〈〈base2,height1〉 :: \fst rc,〈base2,height2〉 :: \snd rc〉]]]] -in aux : ∀l1,l2,m.∃z.m = \len l1 + \len l2 → rebase_spec_aux l1 l2 z); +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)) (w Hw); clear aux; - cases (Hw (refl_eq ??) Hs1 Hs2 (λ_.He1) (λ_.He2)); clear Hw; cases H1; cases H2; cases H3; clear H3 H1 H2; + cases (Hw (le_n ?) Hs1 Hs2 (λ_.He1) (λ_.He2)); clear Hw; cases H1; cases H2; cases H3; clear H3 H1 H2; exists [constructor 1;constructor 1;[apply (\fst w)|5:apply (\snd w)]] try assumption; [1,3: apply hide; cases H (X X); try rewrite < (H8 O); try rewrite < X; assumption |2,4: apply hide;[apply H6|apply H7]intro X;[rewrite > X in Hb1|rewrite > X in Hb2] @@ -115,11 +216,30 @@ in aux : ∀l1,l2,m.∃z.m = \len l1 + \len l2 → rebase_spec_aux l1 l2 z); simplify in match (\snd 〈?,?〉); simplify in match (\fst 〈?,?〉); split; [assumption; |apply H9;|apply H10] |6: intro ABS; unfold; intros 4; clear H1 H2; - cases l in ABS H3; intros 1; [2: simplify in H1; destruct H1] - cases l1 in H4 H1; intros; [2: simplify in H2; destruct H2] - split; [left;reflexivity|split; apply (sorted_nil q2_lt);|split; assumption;] + cases l in ABS H3; intros 1; [2: simplify in H1; cases (not_le_Sn_O ? H1)] + cases l1 in H4 H1; intros; [2: simplify in H2; cases (not_le_Sn_O ? H2)] + split; [ left; reflexivity|split; apply (sorted_nil q2_lt);|split; assumption;] split; unfold; intros; unfold same_values; intros; reflexivity; -|5: unfold rebase_spec_aux; intros; cases l1 in H2 H4 H6; intros; [ simplify in H2; destruct H2;] +|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≫); + simplify in match (\fst 〈?,?〉); simplify in match (\snd 〈?,?〉); + cases H4; + [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] + |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; + [1: left; reflexivity; + |2: cases H10; + + + + unfold rebase_spec_aux; intros; cases l1 in H2 H4 H6; intros; [ simplify in H2; destruct H2;] lapply H6 as H7; [2: intro X; destruct X] clear H6 H5; rewrite > H7; split; [right; simplify;