From: Enrico Tassi Date: Mon, 30 Jun 2008 22:50:55 +0000 (+0000) Subject: new specification X-Git-Tag: make_still_working~4979 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d309714a7f00acfae311fa24612e57e9be085ff3;p=helm.git new specification --- diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index 559194e76..16d378876 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -1,27 +1,27 @@ -sandwich.ma ordered_uniform.ma property_sigma.ma ordered_uniform.ma russell_support.ma -uniform.ma supremum.ma bishop_set.ma ordered_set.ma -sequence.ma nat/nat.ma ordered_uniform.ma uniform.ma -supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma -property_exhaustivity.ma ordered_uniform.ma property_sigma.ma bishop_set_rewrite.ma bishop_set.ma -cprop_connectives.ma datatypes/constructors.ma logic/equality.ma +sequence.ma nat/nat.ma nat_ordered_set.ma bishop_set.ma nat/compare.ma lebesgue.ma property_exhaustivity.ma sandwich.ma +property_exhaustivity.ma ordered_uniform.ma property_sigma.ma +cprop_connectives.ma datatypes/constructors.ma logic/equality.ma ordered_set.ma cprop_connectives.ma +sandwich.ma ordered_uniform.ma russell_support.ma cprop_connectives.ma nat/nat.ma -models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma +uniform.ma supremum.ma +supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma models/nat_ordered_uniform.ma bishop_set_rewrite.ma models/nat_uniform.ma ordered_uniform.ma -models/q_support.ma Q/q/q.ma -models/discrete_uniformity.ma bishop_set_rewrite.ma uniform.ma -models/q_bars.ma cprop_connectives.ma models/list_support.ma models/q_support.ma -models/q_function.ma models/q_bars.ma models/nat_uniform.ma models/discrete_uniformity.ma nat_ordered_set.ma -models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma -models/list_support.ma list/list.ma +models/q_support.ma Q/q/q.ma cprop_connectives.ma models/nat_order_continuous.ma models/nat_dedekind_sigma_complete.ma models/nat_ordered_uniform.ma +models/nat_lebesgue.ma lebesgue.ma models/nat_order_continuous.ma +models/list_support.ma list/list.ma +models/nat_dedekind_sigma_complete.ma models/nat_uniform.ma nat/le_arith.ma russell_support.ma supremum.ma +models/discrete_uniformity.ma bishop_set_rewrite.ma uniform.ma +models/q_function.ma models/q_bars.ma nat_ordered_set.ma +models/q_bars.ma cprop_connectives.ma models/list_support.ma models/q_support.ma nat_ordered_set.ma Q/q/q.ma datatypes/constructors.ma list/list.ma diff --git a/helm/software/matita/contribs/dama/dama/depends.png b/helm/software/matita/contribs/dama/dama/depends.png index 0365b1fad..a09d7cd89 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 75721e4db..2b4c8abd0 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma @@ -35,7 +35,7 @@ let rec sum_bases (l:list bar) (i:nat) on i ≝ [ O ⇒ OQ | S m ⇒ match l with - [ nil ⇒ sum_bases l m + Qpos one + [ nil ⇒ sum_bases [] m + Qpos one | cons x tl ⇒ sum_bases tl m + Qpos (\fst x)]]. axiom sum_bases_empty_nat_of_q_ge_OQ: @@ -50,10 +50,11 @@ lemma sum_bases_ge_OQ: intro; elim l; simplify; intros; [1: elim n; [apply q_eq_to_le;reflexivity] simplify; apply q_le_plus_trans; try assumption; apply q_lt_to_le; apply q_pos_lt_OQ; -|2: cases n; [apply q_eq_to_le;reflexivity] simplify; +|2: cases n; [apply q_eq_to_le;reflexivity] simplify; apply q_le_plus_trans; [apply H| apply q_lt_to_le; apply q_pos_lt_OQ;]] qed. +alias symbol "leq" = "Q less or equal than". lemma sum_bases_O: ∀l.∀x.sum_bases l x ≤ OQ → x = O. intros; cases x in H; [intros; reflexivity] intro; cases (?:False); @@ -66,43 +67,8 @@ try apply (sum_bases_ge_OQ []); apply (sum_bases_ge_OQ l1); qed. -lemma sum_bases_increasing: - ∀l,x.sum_bases l x < sum_bases l (S x). -intro; elim l; -[1: elim x; - [1: simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ; - apply q_pos_lt_OQ; - |2: simplify in H ⊢ %; - 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: elim x; - [1: simplify; rewrite > q_plus_sym; rewrite > q_plus_OQ; - apply q_pos_lt_OQ; - |2: simplify; change in ⊢ (? ? (? % ?)) with (sum_bases l1 (S n)) ; - apply q_lt_plus; rewrite > q_elim_minus; - rewrite < q_plus_assoc; rewrite < q_elim_minus; - rewrite > q_plus_minus; rewrite > q_plus_OQ; apply H]] -qed. - -lemma sum_bases_lt_canc: - ∀l,x,y.sum_bases l (S x) < sum_bases l (S y) → sum_bases l x < sum_bases l y. -intro; elim l; [apply (q_lt_canc_plus_r ?? (Qpos one));apply H] -generalize in match H1;apply (nat_elim2 (?:? → ? → CProp) ??? x y); -intros 2; -[3: intros 2; simplify; apply q_lt_inj_plus_r; apply H; - apply (q_lt_canc_plus_r ?? (Qpos (\fst a))); apply H3; -|2: cases (?:False); simplify in H2; - apply (q_lt_le_incompat (sum_bases l1 (S n)) OQ);[2: apply sum_bases_ge_OQ;] - apply (q_lt_canc_plus_r ?? (Qpos (\fst a))); apply H2; -|1: cases n in H2; intro; - [1: cases (?:False); apply (q_lt_corefl ? H2); - |2: simplify; apply q_lt_plus_trans; [apply sum_bases_ge_OQ] - apply q_pos_lt_OQ;]] -qed. -lemma sum_bars_increasing2: +lemma sum_bases_increasing: ∀l.∀n1,n2:nat.n1 H; apply q_eq_to_le; + rewrite > q_d_x_x; reflexivity; + |1: exists [apply p] simplify; constructor 4; rewrite > H1; split; + try split; try rewrite > q_d_x_x; try autobatch depth=2; + [1: rewrite > H; rewrite > q_plus_sym; apply q_lt_plus; + rewrite > q_plus_minus; apply q_lt_plus_trans; [apply sum_bases_ge_OQ] + apply q_pos_lt_OQ; + |2: rewrite > H; rewrite > q_d_x_x; apply q_eq_to_le; reflexivity; + |3: rewrite > H; rewrite > q_d_x_x; apply q_lt_plus_trans; + try apply sum_bases_ge_OQ; apply q_pos_lt_OQ;]] |3: cases (q_cmp i (start f+sum_bases (bars f) (len (bars f)))); [1: exists [apply 〈O,OQ〉] simplify; constructor 2; split; try assumption; try reflexivity; rewrite > H1; apply q_eq_to_le; reflexivity; @@ -176,46 +157,85 @@ letin value ≝ ( intros; [1: exists [apply 〈O,OQ〉] simplify; constructor 3; split; reflexivity; |2: cases (value ⅆ[i,start f] (b::l)) (p Hp); - cases (Hp (q_dist_ge_OQ ? ?)); clear Hp value; + cases (Hp (q_dist_ge_OQ ? ?)); clear Hp value; [cases H3;destruct H4] + cases H3; clear H3; exists [apply p]; constructor 4; split; try split; try assumption; - [1: apply q_lt_to_le; assumption; - |2: rewrite < H2; assumption; - |3: cases (cmp_nat (\fst p) (len (bars f))); - [1:apply lt_to_le;rewrite H6;rewrite < H2;apply le_n] + [1: intro X; destruct X; + |2: apply q_lt_to_le; assumption; + |3: rewrite < H2; assumption; + |4: cases (cmp_nat (\fst p) (len (bars f))); + [1:apply lt_to_le;rewrite H3;rewrite < H2;apply le_n] cases (?:False); cases (\fst p) in H3 H4 H6; clear H5; - [1: intros; apply (not_le_Sn_O ? H5); - |2: rewrite > q_d_sym; rewrite > q_d_noabs; [2: apply q_lt_to_le; assumption] + [1: intros; apply (not_le_Sn_O ? H5); + |2: rewrite > q_d_sym; rewrite > q_d_noabs; [2: apply q_lt_to_le; assumption] intros; lapply (q_lt_inj_plus_r ?? (Qopp (start f)) H1); clear H1; generalize in match Hletin; rewrite > (q_plus_sym (start f)); rewrite < q_plus_assoc; do 2 rewrite < q_elim_minus; rewrite > q_plus_minus; rewrite > q_plus_OQ; intro K; apply (q_lt_corefl (i-start f)); apply (q_lt_le_trans ???? H3); rewrite < H2; - apply (q_lt_trans ??? K); apply sum_bars_increasing2; + apply (q_lt_trans ??? K); apply sum_bases_increasing; assumption;]]]]] -|1,3: intros; split; - [1,4: clear H2; cases (value (q-Qpos (\fst b)) l1); +|1,3: intros; right; split; + [1,4: clear H2; cases (value (q-Qpos (\fst b)) l1); cases (H2 (q_le_to_diff_ge_OQ ?? (? H1))); - [1,3: intros; [apply q_lt_to_le|apply q_eq_to_le;symmetry] assumption] - simplify; apply q_le_minus; assumption; + [1: intro; apply q_lt_to_le;assumption; + |3: simplify; cases H4; apply q_le_minus; assumption; + |2,5: simplify; cases H4; rewrite > H5; rewrite > H6; + apply q_le_minus; apply sum_bases_empty_nat_of_q_le_q; + |4: intro X; rewrite > X; apply q_eq_to_le; reflexivity; + |*: simplify; apply q_le_minus; cases H4; assumption;] |2,5: cases (value (q-Qpos (\fst b)) l1); cases (H4 (q_le_to_diff_ge_OQ ?? (? H1))); - [1,3: intros; [apply q_lt_to_le|apply q_eq_to_le;symmetry] assumption] - clear H3 H2 value; - change with (q < sum_bases l1 (S (\fst w)) + Qpos (\fst b)); - apply q_lt_plus; assumption; + [1,4: intros; [apply q_lt_to_le|apply q_eq_to_le;symmetry] assumption; + |3,6: cases H5; simplify; change with (q < sum_bases l1 (S (\fst w)) + Qpos (\fst b)); + apply q_lt_plus; assumption; + |2,5: simplify; cases H5; rewrite > H6; simplify; rewrite > H7; + apply q_lt_plus; apply sum_bases_empty_nat_of_q_le_q_one;] |*: cases (value (q-Qpos (\fst b)) l1); simplify; cases (H4 (q_le_to_diff_ge_OQ ?? (? H1))); - [1,3: intros; [apply q_lt_to_le|apply q_eq_to_le;symmetry] assumption] - assumption;] -|2: clear value H2; simplify; intros; split; [assumption|3:reflexivity] + [1,4: intros; [apply q_lt_to_le|apply q_eq_to_le;symmetry] assumption; + |3,6: cases H5; assumption; + |*: cases H5; rewrite > H6; rewrite > H8; + elim (\fst w); [1,3:reflexivity;] simplify; assumption;]] +|2: clear value H2; simplify; intros; right; split; [assumption|3:reflexivity] rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption; -|4: simplify; intros; split; - [1: apply sum_bases_empty_nat_of_q_le_q; - |2: apply sum_bases_empty_nat_of_q_le_q_one; - |3: elim (nat_of_q q); [reflexivity] simplify; assumption]] +|4: intros; left; split; reflexivity;] +qed. + +lemma value_OQ_l: + ∀l,i.i < start l → \snd (\fst (value l i)) = OQ. +intros; cases (value l i) (q Hq); cases Hq; clear Hq; simplify; cases H1; clear H1; +try assumption; cases H2; cases (?:False); apply (q_lt_le_incompat ?? H H6); +qed. + +lemma value_OQ_r: + ∀l,i.start l + sum_bases (bars l) (len (bars l)) ≤ i → \snd (\fst (value l i)) = OQ. +intros; cases (value l i) (q Hq); cases Hq; clear Hq; simplify; cases H1; clear H1; +try assumption; cases H2; cases (?:False); apply (q_lt_le_incompat ?? H7 H); +qed. + +lemma value_OQ_e: + ∀l,i.bars l = [] → \snd (\fst (value l i)) = OQ. +intros; cases (value l i) (q Hq); cases Hq; clear Hq; simplify; cases H1; clear H1; +try assumption; cases H2; cases (?:False); apply (H1 H); +qed. + +lemma value_ok: + ∀f,i. bars f ≠ [] → start f ≤ i → i < start f + sum_bases (bars f) (len (bars f)) → + And4 + (\fst (\fst (value f i)) ≤ (len (bars f))) + (\snd (\fst (value f i)) = \snd (nth (bars f) ▭ (\fst (\fst (value f i))))) + (sum_bases (bars f) (\fst (\fst (value f i))) ≤ ⅆ[i,start f]) + (ⅆ[i, start f] < sum_bases (bars f) (S (\fst (\fst (value f i))))). +intros; cases (value f i); cases H3; simplify; clear H3; cases H4; +[1,2,3: cases (?:False); + [1: apply (q_lt_le_incompat ?? H3 H1); + |2: apply (q_lt_le_incompat ?? H2 H3); + |3: apply (H H3);] +|4: split; cases H7; try assumption;] qed. - + definition same_values ≝ λl1,l2:q_f. ∀input.\snd (\fst (value l1 input)) = \snd (\fst (value l2 input)). 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..bf2eb82d8 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_function.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma @@ -24,218 +24,21 @@ 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; +cases Hv1 (HV1 HV1 HV1 HV1); cases HV1 (Hi1 Hv11 Hv12); clear HV1 Hv1; +[1: cut (input < start l1) as K;[2: apply (q_lt_trans ??? Hi1 H)] + rewrite > (value_OQ_l ?? K); simplify; symmetry; assumption; +|2: cut (start l1 + sum_bases (bars l1) (len (bars l1)) ≤ input) as K;[2: + simplify in Hi1; apply (q_le_trans ???? Hi1); rewrite > H2; + rewrite > q_plus_sym in ⊢ (? ? (? ? %)); + rewrite > q_plus_assoc; rewrite > q_elim_minus; + rewrite > q_plus_sym in ⊢ (? ? (? (? ? %) ?)); + rewrite > q_plus_assoc; rewrite < q_elim_minus; + rewrite > q_plus_minus; rewrite > q_plus_sym in ⊢ (? ? (? % ?)); + rewrite > q_plus_OQ; apply q_eq_to_le; reflexivity;] + rewrite > (value_OQ_r ?? K); simplify; symmetry; assumption; |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; +|4: - - - - -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.