X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fq_function.ma;h=b1ff639e44b959bd6a2a482c001df38d552316f9;hb=1c2cadee5d666f0e31085a4ff358d667379c4f25;hp=6c8fc1caea5a23390c4664ccec94f8eaa76a4e37;hpb=98c84d48f4511cb52c8dc03881e113bd4bd9c6ce;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 6c8fc1cae..b1ff639e4 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_function.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma @@ -13,250 +13,22 @@ (**************************************************************************) include "nat_ordered_set.ma". -include "models/q_bars.ma". +include "models/q_shift.ma". -lemma initial_shift_same_values: - ∀l1:q_f.∀init.init < start l1 → - same_values l1 - (mk_q_f init (〈\fst (unpos (start l1 - init) ?),OQ〉:: bars l1)). -[apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption] -intros; generalize in ⊢ (? ? (? ? (? ? (? ? ? (? ? ? (? ? %)) ?) ?))); intro; -cases (unpos (start l1-init) H1); intro input; -simplify in ⊢ (? ? ? (? ? ? (? ? ? (? (? ? (? ? (? ? ? % ?) ?)) ?)))); -cases (value (mk_q_f init (〈w,OQ〉::bars l1)) input) (v1 Hv1); -(*cases (value l1 input) (v2 Hv2); *) -cases Hv1 (HV1 HV1 HV1 HV1); (* cases Hv2 (HV2 HV2 HV2 HV2); clear Hv1 Hv2; *) -cases HV1 (Hi1 Hv11 Hv12); (*cases HV2 (Hi2 Hv21 Hv22);*) clear HV1 (*HV2*); -(* simplify; *) -rewrite > Hv12; (*rewrite > Hv22;*) try reflexivity; -[1: simplify in Hi1; cases (?:False); - apply (q_lt_corefl (start l1)); cases (Hi2); - autobatch by Hi2, Hi1, q_le_trans, H4, H, q_le_lt_trans, q_lt_le_trans. -|2: simplify in Hi1; cases (?:False); - apply (q_lt_corefl (start l1+sum_bases (bars l1) (len (bars l1)))); - cases Hi2; apply (q_le_lt_trans ???? H5); - apply (q_le_trans ???? Hi1); - rewrite > H2; rewrite > (q_plus_sym ? (start l1-init)); - rewrite > q_plus_assoc; apply q_le_inj_plus_r; - apply q_eq_to_le; - rewrite > q_elim_minus; rewrite > (q_plus_sym (start l1)); - rewrite > q_plus_assoc; rewrite < q_elim_minus; - rewrite > q_plus_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ; - reflexivity; -|3: simplify in Hi1; destruct Hi1; -|4: simplify in Hi1 H3 Hv12 Hv11 ⊢ %; cases H3; clear H3; - cases (\fst v1) in H4; [intros;reflexivity] intros; - simplify; simplify in H3; - - - - - -simplify in ⊢ (? ? ? (? ? ? %)); -cases (q_cmp input (start (mk_q_f init (〈w,OQ〉::bars l1)))) in H3; -whd in ⊢ (% → ?); simplify in H3; -[1: intro; cases H4; clear H4; rewrite > H3; - cases (value l1 init); simplify; cases (q_cmp init (start l1)) in H4; - [1: cases (?:False); apply (q_lt_corefl init); rewrite > H4 in ⊢ (?? %); apply H; - |3: cases (?:False); apply (q_lt_antisym init (start l1)); assumption; - |2: whd in ⊢ (% → ?); intro; rewrite > H8; clear H8 H4; - rewrite > H7; clear H7; rewrite > (?:\fst w1 = O); [reflexivity] - symmetry; apply le_n_O_to_eq; - rewrite > (sum_bases_O (〈w,OQ〉::bars l1) (\fst w1)); [apply le_n] - clear H6 w2; simplify in H5:(? ? (? ? %)); - destruct H3; rewrite > q_d_x_x in H5; assumption;] -|2: intros; cases (value l1 input); simplify in ⊢ (? ? (? ? ? %) ?); - cases (q_cmp input (start l1)) in H5; whd in ⊢ (% → ?); - [1: cases (?:False); clear w2 H4 w1 H2 w H1; - apply (q_lt_antisym init (start l1)); [assumption] rewrite < H5; assumption - |2: intros; rewrite > H6; clear H6; rewrite > H4; reflexivity; - |3: cases (?:False); apply (q_lt_antisym input (start l1)); [2: assumption] - apply (q_lt_trans ??? H3 H);] -|3: intro; cases H4; clear H4; - cases (value l1 input); simplify; cases (q_cmp input (start l1)) in H4; whd in ⊢ (% → ?); - [1: intro; cases H8; clear H8; rewrite > H11; rewrite > H7; clear H11 H7; - simplify in ⊢ (? ? ? (? ? ? (? ? % ? ?))); - cut (\fst w1 = S (\fst w2)) as Key; [rewrite > Key; reflexivity;] - cut (\fst w2 = O); [2: clear H10; - symmetry; apply le_n_O_to_eq; rewrite > (sum_bases_O (bars l1) (\fst w2)); [apply le_n] - apply (q_le_trans ??? H9); rewrite < H4; rewrite > q_d_x_x; - apply q_eq_to_le; reflexivity;] - rewrite > Hcut; clear Hcut H10 H9; simplify in H5 H6; - cut (ⅆ[input,init] = Qpos w) as E; [2: - rewrite > H2; rewrite < H4; rewrite > q_d_sym; - rewrite > q_d_noabs; [reflexivity] apply q_lt_to_le; assumption;] - cases (\fst w1) in H5 H6; intros; - [1: cases (?:False); clear H5; simplify in H6; - apply (q_lt_corefl ⅆ[input,init]); - rewrite > E in ⊢ (??%); rewrite < q_plus_OQ in ⊢ (??%); - rewrite > q_plus_sym; assumption; - |2: cases n in H5 H6; [intros; reflexivity] intros; - cases (?:False); clear H6; cases (bars l1) in H5; simplify; intros; - [apply (q_pos_OQ one);|apply (q_pos_OQ (\fst b));] - apply (q_le_S ??? (sum_bases_ge_OQ ? n1));[apply []|3:apply l] - simplify in ⊢ (? (? (? % ?) ?) ?); rewrite < (q_plus_minus (Qpos w)); - rewrite > q_elim_minus; apply q_le_minus_r; - rewrite > q_elim_opp; rewrite < E in ⊢ (??%); assumption;] - |2: intros; rewrite > H8; rewrite > H7; clear H8 H7; - simplify in H5 H6 ⊢ %; - cases (\fst w1) in H5 H6; [intros; reflexivity] - cases (bars l1); - [1: intros; simplify; elim n [reflexivity] simplify; assumption; - |2: simplify; intros; cases (?:False); clear H6; - apply (q_lt_le_incompat (input - init) (Qpos w) ); - [1: rewrite > H2; do 2 rewrite > q_elim_minus; - apply q_lt_plus; rewrite > q_elim_minus; - rewrite < q_plus_assoc; rewrite < q_elim_minus; - rewrite > q_plus_minus;rewrite > q_plus_OQ; assumption; - |2: rewrite < q_d_noabs; [2: apply q_lt_to_le; assumption] - rewrite > q_d_sym - - ; apply (q_le_S ???? H5);apply sum_bases_ge_OQ;]] - |3: intro; cases H8; clear H8; rewrite > H11; rewrite > H7; clear H11 H7; - simplify in H5 H6 ⊢ (? ? ? (? ? ? (? ? % ? ?))); - -axiom nth_nil: ∀T,n.∀d:T. nth [] d n = d. - - -lemma case1 : - ∀init,st,input,l. - init q_d_sym; rewrite > q_d_noabs; [2: - apply (q_le_trans ? st); apply q_lt_to_le; assumption] -do 2 rewrite > q_elim_minus; rewrite > q_plus_assoc; -intro X; lapply (q_lt_canc_plus_r ??? X) as Y; -simplify in Y; cases (?:False); -apply (q_lt_corefl st); apply (q_lt_trans ??? H1); -apply (q_lt_le_trans ??? Y); rewrite > q_plus_sym; rewrite > q_plus_OQ; -apply q_eq_to_le; reflexivity; -qed. - -lemma case2: - ∀a,l1,init,st,input,n. - init < st → st < input → - sum_bases (a::l1) n + (st-init) ≤ ⅆ[input,init] → - ⅆ[input,st] < sum_bases l1 O + Qpos (\fst a) → - n = O. -intros; cut (input - st < Qpos (\fst a)) as H6';[2: - rewrite < q_d_noabs;[2:apply q_lt_to_le; assumption] - rewrite > q_d_sym; apply (q_lt_le_trans ??? H3); - rewrite > q_plus_sym; rewrite > q_plus_OQ; - apply q_eq_to_le; reflexivity] clear H3; -generalize in match H2; rewrite > q_d_sym; rewrite > q_d_noabs; - [2: apply (q_le_trans ? st); apply q_lt_to_le; assumption] -do 2 rewrite > q_elim_minus; rewrite > q_plus_assoc; intro X; -lapply (q_le_canc_plus_r ??? X) as Y; clear X; -lapply (q_le_inj_plus_r ?? (Qopp st) Y) as X; clear Y; -cut (input + Qopp st < Qpos (\fst a)) as H6''; - [2: rewrite < q_elim_minus; assumption;] clear H6'; -generalize in match (q_le_lt_trans ??? X H6''); clear X H6''; -rewrite < q_plus_assoc; rewrite < q_elim_minus; -rewrite > q_plus_minus; rewrite > q_plus_OQ; cases n; intro X; [reflexivity] -cases (?:False); -apply (q_lt_le_incompat (sum_bases l1 n1) OQ);[2: apply sum_bases_ge_OQ;] -apply (q_lt_canc_plus_r ?? (Qpos (\fst a))); -rewrite >(q_plus_sym OQ); rewrite > q_plus_OQ; apply X; -qed. - -lemma case3: - ∀init,st,input,l1,a,n. - init q_elim_minus; - rewrite < q_plus_assoc; rewrite > (q_plus_sym (Qopp ?)); - rewrite < q_elim_minus; rewrite > q_plus_minus; rewrite > q_plus_OQ; - apply q_eq_to_le; reflexivity;] clear H3; - rewrite > q_elim_minus; apply (q_lt_canc_plus_r ?? ⅆ[input,st]); - rewrite < q_plus_assoc; rewrite > (q_plus_sym (Qopp ?)); - rewrite < q_elim_minus; rewrite > q_plus_minus; rewrite > q_plus_OQ; - apply (q_le_lt_trans ??? H7'); clear H7'; rewrite > q_elim_minus; - rewrite > q_plus_sym; apply q_lt_inj_plus_r; - rewrite > q_plus_sym; apply q_lt_plus; rewrite > q_elim_opp; - rewrite > q_plus_sym; apply (q_lt_canc_plus_r ?? (Qpos a)); - rewrite < q_plus_assoc; rewrite > (q_plus_sym (Qopp ?)); - rewrite < q_elim_minus; rewrite > q_plus_minus; rewrite > q_plus_OQ; - apply (q_lt_le_trans ??? H2); rewrite > (q_plus_sym OQ); rewrite > q_plus_OQ; - rewrite > q_plus_sym; apply q_eq_to_le; reflexivity;] -generalize in match Hcut; clear H2 H3 Hcut; -rewrite > q_d_sym; rewrite > q_d_noabs; [2:apply q_lt_to_le; assumption] -rewrite > q_d_sym; rewrite > q_d_noabs; [2: apply (q_le_trans ? st); apply q_lt_to_le; assumption] -rewrite < q_plus_sym; rewrite < q_elim_minus; -rewrite > (q_elim_minus input init); -rewrite > q_minus_distrib; rewrite > q_elim_opp; -rewrite > (q_elim_minus input st); -rewrite > q_minus_distrib; rewrite > q_elim_opp; -repeat rewrite > q_elim_minus; -rewrite < q_plus_assoc in ⊢ (??% → ?); -rewrite > (q_plus_sym (Qopp input) init); -rewrite > q_plus_assoc; -rewrite < q_plus_assoc in ⊢ (??(?%?) → ?); -rewrite > (q_plus_sym (Qopp init) init); -rewrite < (q_elim_minus init); rewrite >q_plus_minus; -rewrite > q_plus_OQ; rewrite > (q_plus_sym st); -rewrite < q_plus_assoc; -rewrite < (q_plus_OQ (Qopp input + st)) in ⊢ (??% → ?); -rewrite > (q_plus_sym ? OQ); intro X; -lapply (q_lt_canc_plus_r ??? X) as Y; clear X; -apply (q_lt_le_incompat ?? Y); apply sum_bases_ge_OQ; -qed. - -lemma key: - ∀init,input,l1,w1,w2,w. - Qpos w = start l1 - init → - init < start l1 → - start l1 < input → - sum_bases (〈w,OQ〉::bars l1) w1 ≤ ⅆ[input,init] → - ⅆ[input,init] < sum_bases (bars l1) w1 + (start l1-init) → - sum_bases (bars l1) w2 ≤ ⅆ[input,start l1] → - ⅆ[input,start l1] < sum_bases (bars l1) (S w2) → - \snd (nth (bars l1) ▭ w2) = \snd (nth (〈w,OQ〉::bars l1) ▭ w1). -intros 3 (init input l); cases l (st l); -change in match (start (mk_q_f st l)) with st; -change in match (bars (mk_q_f st l)) with l; -elim l; clear l; -[1: rewrite > nth_nil; cases w1 in H4; - [1: intro X; cases (case1 ?????? X); assumption; - |2: intros; simplify; rewrite > nth_nil; reflexivity;] -|2: cases w1 in H4 H5; clear w1; - [1: intros (Y X); cases (case1 ?????? X); assumption; - |2: intros; simplify in H4 H5 H7 ⊢ %; - generalize in match H6; generalize in match H7; - generalize in match H4; generalize in match H5; clear H4 H5 H6 H7; - apply (nat_elim2 ???? w2 n); clear w2 n; intros; - [1: rewrite > (case2 a l1 init st input n); [reflexivity] - try rewrite < H1; assumption; - |2: simplify in H4 H7; cases (case3 ???????? H4 H7); assumption; - |3: (* dipende se vanno oltre la lunghezza di l1, - forse dovevo gestire il caso prima dell'induzione *) - simplify in ⊢ (? ? (? ? ? %) ?); - rewrite > (H (S m) ? w); [reflexivity] try assumption; -STOP - -qed. - - - alias symbol "pi2" = "pair pi2". alias symbol "pi1" = "pair pi1". definition rebase_spec ≝ ∀l1,l2:q_f.∃p:q_f × q_f. And4 - (*len (bars (\fst p)) = len (bars (\snd p))*) (start (\fst p) = start (\snd p)) - (same_bases (\fst p) (\snd p)) + (same_bases (bars (\fst p)) (bars (\snd p))) (same_values l1 (\fst p)) (same_values l2 (\snd p)). definition rebase_spec_simpl ≝ λstart.λl1,l2:list bar.λp:(list bar) × (list bar). And3 - (same_bases (mk_q_f start (\fst p)) (mk_q_f start (\snd p))) + (same_bases (\fst p) (\snd p)) (same_values (mk_q_f start l1) (mk_q_f start (\fst p))) (same_values (mk_q_f start l2) (mk_q_f start (\snd p))). @@ -269,6 +41,8 @@ definition eject ≝ coercion eject. definition inject ≝ λP.λp:(list bar) × (list bar).λh:P p. ex_introT ? P p h. coercion inject with 0 1 nocomposites. + +axiom devil : False. definition rebase: rebase_spec. intros 2 (f1 f2); cases f1 (s1 l1); cases f2 (s2 l2); clear f1 f2; @@ -313,7 +87,7 @@ in aux : ∀l1,l2,m.∃z.∀s.spec s l1 l2 m z); unfold spec; [1,2: assumption; |3: intro; apply (H3 input); |4: intro; rewrite > H in H4; - rewrite > (H4 input); reflexivity;] + rewrite > (H4 input) in ⊢ (? ? % ?); reflexivity;] |2: letin l2' ≝ (〈\fst (unpos (s2-s1) ?),OQ〉::l2);[ apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption] @@ -323,23 +97,97 @@ in aux : ∀l1,l2,m.∃z.∀s.spec s l1 l2 m z); unfold spec; [1: reflexivity |2: assumption; |3: assumption; - |4: intro; rewrite < (H4 input); clear H3 H4 H2 w; - cases (value (mk_q_f s1 l2') input); - cases (q_cmp input (start (mk_q_f s1 l2'))) in H1; - whd in ⊢ (% → ?); - [1: intros; cases H2; clear H2; whd in ⊢ (??? %); - cases (value (mk_q_f s2 l2) input); - cases (q_cmp input (start (mk_q_f s2 l2))) in H2; - whd in ⊢ (% → ?); - [1: intros; cases H6; clear H6; change with (w1 = w); - - (* TODO *) ]] + |4: intro; + rewrite > (initial_shift_same_values (mk_q_f s2 l2) s1 H input) in ⊢ (? ? % ?); + rewrite < (H4 input)in ⊢ (? ? ? %); reflexivity;] + |3: letin l1' ≝ (〈\fst (unpos (s1-s2) ?),OQ〉::l1);[ + apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ; + assumption] + cases (aux l1' l2 (S (len l1' + len l2))); + cases (H1 s2 (le_n ?)); clear H1 aux; + exists [apply 〈mk_q_f s2 (\fst w), mk_q_f s2 (\snd w)〉] split; + [1: reflexivity + |2: assumption; + |4: assumption; + |3: intro; simplify in ⊢ (? ? ? (? ? ? (? ? ? (? % ?)))); + rewrite > (initial_shift_same_values (mk_q_f s1 l1) s2 H input) in ⊢ (? ? % ?); + rewrite < (H3 input) in ⊢ (? ? ? %); reflexivity;]] |1,2: unfold rest; apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption; -|3:(* TODO *) -|4:(* TODO *) -|5:(* TODO *) -|6:(* TODO *) -|7:(* TODO *) -|8: intros; cases (?:False); apply (not_le_Sn_O ? H1);] +|8: intros; cases (?:False); apply (not_le_Sn_O ? H1); +|3: intros; generalize in match (unpos ??); intro X; cases X; clear X; + simplify in ⊢ (???? (??? (??? (??? (?? (? (?? (??? % ?) ?) ??)))) ?)); + simplify in ⊢ (???? (???? (??? (??? (?? (? (?? (??? % ?) ?) ??)))))); + clear H4; cases (aux (〈w,\snd b〉::l4) l5 n1); clear aux; + cut (len (〈w,\snd b〉::l4) + len l5 < n1) as K;[2: + simplify in H5; simplify; rewrite > sym_plus in H5; simplify in H5; + rewrite > sym_plus in H5; apply le_S_S_to_le; apply H5;] + split; + [1: simplify in ⊢ (? % ?); simplify in ⊢ (? ? %); + cases (H4 s K); clear K H4; intro input; cases input; [reflexivity] + simplify; apply H7; + |2: simplify in ⊢ (? ? %); cases (H4 s K); clear H4 K H5 spec; + intro; + (* input < s + b1 || input >= s + b1 *) + |3: simplify in ⊢ (? ? %);] +|4: intros; generalize in match (unpos ??); intro X; cases X; clear X; + (* duale del 3 *) +|5: intros; (* triviale, caso in cui non fa nulla *) +|6,7: (* casi base in cui allunga la lista più corta *) +] +elim devil; qed. + +include "Q/q/qtimes.ma". + +let rec area (l:list bar) on l ≝ + match l with + [ nil ⇒ OQ + | cons he tl ⇒ area tl + Qpos (\fst he) * ⅆ[OQ,\snd he]]. + +alias symbol "pi1" = "exT \fst". +alias symbol "minus" = "Q minus". +alias symbol "exists" = "CProp exists". +definition minus_spec_bar ≝ + λf,g,h:list bar. + same_bases f g → len f = len g → + ∀s,i:ℚ. \snd (\fst (value (mk_q_f s h) i)) = + \snd (\fst (value (mk_q_f s f) i)) - \snd (\fst (value (mk_q_f s g) i)). + +definition minus_spec ≝ + λf,g:q_f. + ∃h:q_f. + ∀i:ℚ. \snd (\fst (value h i)) = + \snd (\fst (value f i)) - \snd (\fst (value g i)). + +definition eject_bar : ∀P:list bar → CProp.(∃l:list bar.P l) → list bar ≝ + λP.λp.match p with [ex_introT x _ ⇒ x]. +definition inject_bar ≝ ex_introT (list bar). + +coercion inject_bar with 0 1 nocomposites. +coercion eject_bar with 0 0 nocomposites. + +lemma minus_q_f : ∀f,g. minus_spec f g. +intros; +letin aux ≝ ( + let rec aux (l1, l2 : list bar) on l1 ≝ + match l1 with + [ nil ⇒ [] + | cons he1 tl1 ⇒ + match l2 with + [ nil ⇒ [] + | cons he2 tl2 ⇒ 〈\fst he1, \snd he1 - \snd he2〉 :: aux tl1 tl2]] + in aux : ∀l1,l2 : list bar.∃h.minus_spec_bar l1 l2 h); +[2: intros 4; simplify in H3; destruct H3; +|3: intros 4; simplify in H3; cases l1 in H2; [2: intro X; simplify in X; destruct X] + intros; rewrite > (value_OQ_e (mk_q_f s []) i); [2: reflexivity] + rewrite > q_elim_minus; rewrite > q_plus_OQ; reflexivity; +|1: cases (aux l2 l3); unfold in H2; intros 4; + simplify in ⊢ (? ? (? ? ? (? ? ? (? % ?))) ?); + cases (q_cmp i (s + Qpos (\fst b))); + + + +definition excess ≝ + λf,g.∃i.\snd (\fst (value f i)) < \snd (\fst (value g i)). +