From: Enrico Tassi Date: Mon, 30 Jun 2008 18:54:26 +0000 (+0000) Subject: some more work on q X-Git-Tag: make_still_working~4981 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=98c84d48f4511cb52c8dc03881e113bd4bd9c6ce;p=helm.git some more work on q --- diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma index 14e217000..09b9a6c67 100644 --- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma +++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma @@ -21,6 +21,25 @@ inductive Or (A,B:CProp) : CProp ≝ interpretation "constructive or" 'or x y = (Or x y). +inductive Or3 (A,B,C:CProp) : CProp ≝ + | Left3 : A → Or3 A B C + | Middle3 : B → Or3 A B C + | Right3 : C → Or3 A B C. + +interpretation "constructive ternary or" 'or3 x y z= (Or3 x y z). + +notation < "hvbox(a break ∨ b break ∨ c)" with precedence 35 for @{'or3 $a $b $c}. + +inductive Or4 (A,B,C,D:CProp) : CProp ≝ + | Left3 : A → Or4 A B C D + | Middle3 : B → Or4 A B C D + | Right3 : C → Or4 A B C D + | Extra3: D → Or4 A B C D. + +interpretation "constructive ternary or" 'or4 x y z t = (Or4 x y z t). + +notation < "hvbox(a break ∨ b break ∨ c break ∨ d)" with precedence 35 for @{'or4 $a $b $c $d}. + inductive And (A,B:CProp) : CProp ≝ | Conj : A → B → And A B. @@ -29,16 +48,16 @@ interpretation "constructive and" 'and x y = (And x y). inductive And3 (A,B,C:CProp) : CProp ≝ | Conj3 : A → B → C → And3 A B C. -notation < "a ∧ b ∧ c" with precedence 35 for @{'and3 $a $b $c}. +notation < "hvbox(a break ∧ b break ∧ c)" with precedence 35 for @{'and3 $a $b $c}. -interpretation "constructive ternary and" 'and3 x y z = (Conj3 x y z). +interpretation "constructive ternary and" 'and3 x y z = (And3 x y z). inductive And4 (A,B,C,D:CProp) : CProp ≝ | Conj4 : A → B → C → D → And4 A B C D. -notation < "a ∧ b ∧ c ∧ d" with precedence 35 for @{'and4 $a $b $c $d}. +notation < "hvbox(a break ∧ b break ∧ c break ∧ d)" with precedence 35 for @{'and4 $a $b $c $d}. -interpretation "constructive quaternary and" 'and4 x y z t = (Conj4 x y z t). +interpretation "constructive quaternary and" 'and4 x y z t = (And4 x y z t). inductive exT (A:Type) (P:A→CProp) : CProp ≝ ex_introT: ∀w:A. P w → exT A P. @@ -93,3 +112,4 @@ definition antisymmetric ≝ λA:Type.λR:A→A→CProp.λeq:A→A→Prop.∀x:A definition reflexive ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x. definition transitive ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z. + diff --git a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma index bc009b5c6..cb73c2d5f 100644 --- a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma +++ b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma @@ -17,17 +17,6 @@ include "supremum.ma". include "nat/le_arith.ma". include "russell_support.ma". -inductive cmp_cases (n,m:nat) : CProp ≝ - | cmp_lt : n < m → cmp_cases n m - | cmp_eq : n = m → cmp_cases n m - | cmp_gt : m < n → cmp_cases n m. - -lemma cmp_nat: ∀n,m.cmp_cases n m. -intros; generalize in match (nat_compare_to_Prop n m); -cases (nat_compare n m); intros; -[constructor 1|constructor 2|constructor 3] assumption; -qed. - alias symbol "pi1" = "exT \fst". alias symbol "leq" = "natural 'less or equal to'". lemma nat_dedekind_sigma_complete: 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 efa45f7f3..75721e4db 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "nat_ordered_set.ma". include "models/q_support.ma". include "models/list_support.ma". include "cprop_connectives.ma". @@ -44,6 +45,84 @@ axiom sum_bases_empty_nat_of_q_le_q: axiom sum_bases_empty_nat_of_q_le_q_one: ∀q:ℚ.q < sum_bases [] (nat_of_q q) + Qpos one. +lemma sum_bases_ge_OQ: + ∀l,n. OQ ≤ sum_bases l n. +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; + apply q_le_plus_trans; [apply H| apply q_lt_to_le; apply q_pos_lt_OQ;]] +qed. + +lemma sum_bases_O: + ∀l.∀x.sum_bases l x ≤ OQ → x = O. +intros; cases x in H; [intros; reflexivity] intro; cases (?:False); +cases (q_le_cases ?? H); +[1: apply (q_lt_corefl OQ); rewrite < H1 in ⊢ (?? %); +|2: apply (q_lt_antisym ??? H1);] clear H H1; cases l; +simplify; apply q_lt_plus_trans; +try apply q_pos_lt_OQ; +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: + ∀l.∀n1,n2:nat.n1 H1; apply q_eq_to_le; reflexivity; + |3: exists [apply 〈O,OQ〉] simplify; constructor 2; split; try assumption; + try reflexivity; apply q_lt_to_le; assumption; + |2: generalize in match (refl_eq ? (bars f): bars f = bars f); + generalize in match (bars f) in ⊢ (??? % → %); intro X; cases X; clear X; + 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; + 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] + 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] + 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; + assumption;]]]]] |1,3: intros; split; [1,4: clear H2; cases (value (q-Qpos (\fst b)) l1); cases (H2 (q_le_to_diff_ge_OQ ?? (? H1))); @@ -106,8 +215,7 @@ letin value ≝ ( |2: apply sum_bases_empty_nat_of_q_le_q_one; |3: elim (nat_of_q q); [reflexivity] simplify; assumption]] qed. - - + definition same_values ≝ λl1,l2:q_f. ∀input.\snd (\fst (value l1 input)) = \snd (\fst (value l2 input)). @@ -122,65 +230,3 @@ intro; cases x; intros; [2:exists [apply r] reflexivity] cases (?:False); [ apply (q_lt_corefl ? H)|apply (q_neg_gt ? H)] qed. - -notation < "\blacksquare" non associative with precedence 90 for @{'hide}. -definition hide ≝ λT:Type.λx:T.x. -interpretation "hide" 'hide = (hide _ _). - -lemma sum_bases_ge_OQ: - ∀l,n. OQ ≤ sum_bases l n. -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; - apply q_le_plus_trans; [apply H| apply q_lt_to_le; apply q_pos_lt_OQ;]] -qed. - -lemma sum_bases_O: - ∀l.∀x.sum_bases l x ≤ OQ → x = O. -intros; cases x in H; [intros; reflexivity] intro; cases (?:False); -cases (q_le_cases ?? H); -[1: apply (q_lt_corefl OQ); rewrite < H1 in ⊢ (?? %); -|2: apply (q_lt_antisym ??? H1);] clear H H1; cases l; -simplify; apply q_lt_plus_trans; -try apply q_pos_lt_OQ; -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. - 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 a58a82b1f..6c8fc1cae 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_function.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma @@ -15,17 +15,43 @@ include "nat_ordered_set.ma". include "models/q_bars.ma". -axiom le_le_eq: ∀x,y:Q. x ≤ y → y ≤ x → x = y. - 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 hide; apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ; assumption] +[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); +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; diff --git a/helm/software/matita/library/nat/compare.ma b/helm/software/matita/library/nat/compare.ma index dd9589e7b..c01f089bd 100644 --- a/helm/software/matita/library/nat/compare.ma +++ b/helm/software/matita/library/nat/compare.ma @@ -317,3 +317,14 @@ apply ((H H3)). apply ((H1 H3)). apply ((H2 H3)). qed. + +inductive cmp_cases (n,m:nat) : CProp ≝ + | cmp_lt : n < m → cmp_cases n m + | cmp_eq : n = m → cmp_cases n m + | cmp_gt : m < n → cmp_cases n m. + +lemma cmp_nat: ∀n,m.cmp_cases n m. +intros; generalize in match (nat_compare_to_Prop n m); +cases (nat_compare n m); intros; +[constructor 1|constructor 2|constructor 3] assumption; +qed.