From e0b4028cb1f8423b40d5f9ad396f10f42db86f0e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 2 Jul 2008 09:18:21 +0000 Subject: [PATCH] ... --- .../contribs/dama/dama/models/q_bars.ma | 5 +- .../contribs/dama/dama/models/q_function.ma | 76 ++++++++++++++++--- .../contribs/dama/dama/models/q_shift.ma | 1 + 3 files changed, 70 insertions(+), 12 deletions(-) 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 2186890f0..f75bed7be 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma @@ -257,15 +257,14 @@ cases H3; simplify; clear H3; cases H4; clear H4; |3: apply (H H3);] |4: cases H7; clear H7; cases w in H3 H4 H5 H6 H8; simplify; intros; constructor 1; assumption;] -qed. +qed. definition same_values ≝ λl1,l2:q_f. ∀input.\snd (\fst (value l1 input)) = \snd (\fst (value l2 input)). definition same_bases ≝ - λl1,l2:q_f. - (∀i.\fst (nth (bars l1) ▭ i) = \fst (nth (bars l2) ▭ i)). + λl1,l2:list bar. (∀i.\fst (nth l1 ▭ i) = \fst (nth l2 ▭ i)). alias symbol "lt" = "Q less than". lemma unpos: ∀x:ℚ.OQ < x → ∃r:ratio.Qpos r = x. 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 e2187b510..b1ff639e4 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_function.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma @@ -20,16 +20,15 @@ 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))). @@ -42,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; @@ -86,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] @@ -96,8 +97,9 @@ in aux : ∀l1,l2,m.∃z.∀s.spec s l1 l2 m z); unfold spec; [1: reflexivity |2: assumption; |3: assumption; - |4: intro; rewrite > (initial_shift_same_values (mk_q_f s2 l2) s1 H input); - rewrite < (H4 input); reflexivity;] + |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] @@ -107,8 +109,9 @@ in aux : ∀l1,l2,m.∃z.∀s.spec s l1 l2 m z); unfold spec; [1: reflexivity |2: assumption; |4: assumption; - |3: intro; rewrite > (initial_shift_same_values (mk_q_f s1 l1) s2 H input); - rewrite < (H3 input); reflexivity;]] + |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; |8: intros; cases (?:False); apply (not_le_Sn_O ? H1); @@ -124,7 +127,7 @@ in aux : ∀l1,l2,m.∃z.∀s.spec s l1 l2 m z); unfold spec; 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; + intro; (* input < s + b1 || input >= s + b1 *) |3: simplify in ⊢ (? ? %);] |4: intros; generalize in match (unpos ??); intro X; cases X; clear X; @@ -132,4 +135,59 @@ in aux : ∀l1,l2,m.∃z.∀s.spec s l1 l2 m z); unfold spec; |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)). + diff --git a/helm/software/matita/contribs/dama/dama/models/q_shift.ma b/helm/software/matita/contribs/dama/dama/models/q_shift.ma index f247fb11d..a63066659 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_shift.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_shift.ma @@ -103,3 +103,4 @@ cases Hv1 (HV1 HV1 HV1 HV1); cases HV1 (Hi1 Hv11 Hv12); clear HV1 Hv1; |1: apply solution; apply (q_eq_to_le ?? (sym_eq ??? H4)); |3: apply solution; apply (q_lt_to_le ?? H4);] qed. + -- 2.39.2