From b82d421fb24bd0eb8848dc7b978ce1165fb526ab Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 26 Jun 2008 11:43:08 +0000 Subject: [PATCH] more work on q --- .../contribs/dama/dama/models/q_function.ma | 255 ++++++++++++------ helm/software/matita/library/list/list.ma | 34 ++- helm/software/matita/matita.lang | 1 - 3 files changed, 195 insertions(+), 95 deletions(-) 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 c458d418d..21e51808a 100644 --- a/helm/software/matita/contribs/dama/dama/models/q_function.ma +++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma @@ -44,9 +44,21 @@ interpretation "Q less or equal than" 'leq x y = (qle x y). axiom q_le_minus: ∀a,b,c:ℚ. a ≤ c - b → a + b ≤ c. axiom q_lt_plus: ∀a,b,c:ℚ. a - b < c → a < c + b. +axiom q_lt_minus: ∀a,b,c:ℚ. a + b < c → a < c - b. -axiom dist : ℚ → ℚ → ℚ. +axiom q_dist : ℚ → ℚ → ℚ. +notation "hbox(\dd [term 19 x, break term 19 y])" with precedence 90 +for @{'distance $x $y}. +interpretation "ℚ distance" 'distance x y = (q_dist x y). + +axiom q_dist_ge_OQ : ∀x,y:ℚ. OQ ≤ ⅆ[x,y]. + +axiom q_lt_to_le: ∀a,b:ℚ.a < b → a ≤ b. +axiom q_le_to_diff_ge_OQ : ∀a,b.a ≤ b → OQ ≤ b-a. +axiom q_plus_OQ: ∀x:ℚ.x + OQ = x. +axiom q_plus_sym: ∀x,y:ℚ.x + y = y + x. +axiom nat_of_q: ℚ → nat. interpretation "list nth" 'nth = (nth _). interpretation "list nth" 'nth_appl l d i = (nth _ l d i). @@ -82,9 +94,6 @@ interpretation "len" 'len = (length _). notation < "'len' \nbsp term 90 l" with precedence 69 for @{'len_appl $l}. interpretation "len appl" 'len_appl l = (length _ l). -(* a local letin makes russell fail *) -definition cb0h ≝ (λl.mk_list (λi.〈\fst (nth l ▭ i),OQ〉) (len l)). - lemma len_mk_list : ∀T:Type.∀f:nat→T.∀n.len (mk_list f n) = n. intros; elim n; [reflexivity] simplify; rewrite > H; reflexivity; qed. @@ -96,6 +105,13 @@ let rec sum_bases (l:list bar) (i:nat)on i ≝ match l with [ nil ⇒ sum_bases l m + Qpos one | cons x tl ⇒ sum_bases tl m + Qpos (\fst x)]]. + +axiom sum_bases_empty_nat_of_q_ge_OQ: + ∀q:ℚ.OQ ≤ sum_bases [] (nat_of_q q). +axiom sum_bases_empty_nat_of_q_le_q: + ∀q:ℚ.sum_bases [] (nat_of_q q) ≤ q. +axiom sum_bases_empty_nat_of_q_le_q_one: + ∀q:ℚ.q < sum_bases [] (nat_of_q q) + Qpos one. definition eject1 ≝ λP.λp:∃x:nat × ℚ.P x.match p with [ex_introT p _ ⇒ p]. @@ -109,8 +125,8 @@ definition value : [ q_lt _ ⇒ \snd p = OQ | _ ⇒ And3 - (sum_bases (bars f) (\fst p) ≤ i - start f) - (i - start f < sum_bases (bars f) (S (\fst p))) + (sum_bases (bars f) (\fst p) ≤ ⅆ[i,start f]) + (ⅆ[i, start f] < sum_bases (bars f) (S (\fst p))) (\snd p = \snd (nth (bars f) ▭ (\fst p)))]. intros; alias symbol "pi2" = "pair pi2". @@ -118,7 +134,7 @@ alias symbol "pi1" = "pair pi1". letin value ≝ ( let rec value (p: ℚ) (l : list bar) on l ≝ match l with - [ nil ⇒ 〈O,OQ〉 + [ nil ⇒ 〈nat_of_q p,OQ〉 | cons x tl ⇒ match q_cmp p (Qpos (\fst x)) with [ q_lt _ ⇒ 〈O, \snd x〉 @@ -134,69 +150,129 @@ letin value ≝ ( [5: clearbody value; cases (q_cmp i (start f)); [2: exists [apply 〈O,OQ〉] simplify; reflexivity; - |*: cases (value (i - start f) (bars f)) (p Hp); - cases Hp; clear Hp value; + |*: cases (value ⅆ[i,start f] (bars f)) (p Hp); + cases (Hp (q_dist_ge_OQ ? ?)); clear Hp value; exists[1,3:apply p]; simplify; split; assumption;] |1,3: intros; split; - [1,4: clear H2; cases (value (q-Qpos (\fst b)) l1); cases H2; clear H2; + [1,4: clear H2; cases (value (q-Qpos (\fst b)) l1); + cases (H2 (q_le_to_diff_ge_OQ ?? (? H1))); + [1,3: intros; [right|left;symmetry] assumption] simplify; apply q_le_minus; assumption; - |2,5: cases (value (q-Qpos (\fst b)) l1); cases H3; clear H3 H2 value; + |2,5: cases (value (q-Qpos (\fst b)) l1); + cases (H4 (q_le_to_diff_ge_OQ ?? (? H1))); + [1,3: intros; [right|left;symmetry] assumption] + clear H3 H2 value; change with (q < sum_bases l1 (S (\fst w)) + Qpos (\fst b)); apply q_lt_plus; assumption; - |*: cases (value (q-Qpos (\fst b)) l1); simplify; cases H3; clear H3 value H2; + |*: cases (value (q-Qpos (\fst b)) l1); simplify; + cases (H4 (q_le_to_diff_ge_OQ ?? (? H1))); + [1,3: intros; [right|left;symmetry] assumption] assumption;] -|2: clear value H2; simplify; split; - [1: +|2: clear value H2; simplify; intros; 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]] +qed. -definition same_shape ≝ +definition same_values ≝ λl1,l2:q_f. - ∀input.∃col. - - And3 - (sum_bases (bars l2) j ≤ offset - start l2) - (offset - start l2 ≤ sum_bases (bars l2) (S j)) - (\snd (nth (bars l2)) q0 j) = \snd (nth (bars l1) q0 i). + ∀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)). + +axiom q_lt_corefl: ∀x:Q.x < x → False. +axiom q_lt_antisym: ∀x,y:Q.x < y → y < x → False. +axiom q_neg_gt: ∀r:ratio.OQ < Qneg r → False. +axiom q_d_x_x: ∀x:Q.ⅆ[x,x] = OQ. +axiom q_pos_OQ: ∀x.Qpos x ≤ OQ → False. +axiom q_lt_plus_trans: + ∀x,y:Q.OQ ≤ x → OQ < y → OQ < x + y. +axiom q_pos_lt_OQ: ∀x.OQ < Qpos x. +axiom q_le_plus_trans: + ∀x,y:Q. OQ ≤ x → OQ ≤ y → OQ ≤ x + y. + +lemma unpos: ∀x:ℚ.OQ < x → ∃r:ratio.Qpos r = x. +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 (bars l) n. +intro; elim (bars l); simplify; intros; +[1: elim n; [left;reflexivity] simplify; + apply q_le_plus_trans; try assumption; apply q_lt_to_le; apply q_pos_lt_OQ; +|2: cases n; [left;reflexivity] simplify; + apply q_le_plus_trans; [apply H| apply q_lt_to_le; apply q_pos_lt_OQ;]] +qed. -…┐─┌┐… -\ldots\boxdl\boxh\boxdr\boxdl\ldots +lemma sum_bases_O: + ∀l:q_f.∀x.sum_bases (bars l) x ≤ OQ → x = O. +intros; cases x in H; [intros; reflexivity] intro; cases (?:False); +cases H; +[1: apply (q_lt_corefl OQ); rewrite < H1 in ⊢ (?? %); +|2: apply (q_lt_antisym ??? H1);] clear H H1; cases (bars l); +simplify; apply q_lt_plus_trans; +try apply q_pos_lt_OQ; +try apply (sum_bases_ge_OQ (mk_q_f OQ [])); +apply (sum_bases_ge_OQ (mk_q_f OQ l1)); +qed. +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] +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); +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 (mk_q_f init (〈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; + 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))) + (*len (bars (\fst p)) = len (bars (\snd p))*) (start (\fst p) = start (\snd p)) - (∀i.\fst (nth (bars (\fst p)) q0 i) = \fst (nth (bars (\snd p)) q0 i)) - (∀i,offset. - sum_bases (bars l1) i ≤ offset - start l1 → - offset - start l1 ≤ sum_bases (bars l1) (S i) → - ∃j. - And3 - (sum_bases (bars (\fst p)) j ≤ offset - start (\fst p)) - (offset - start (\fst p) ≤ sum_bases (bars (\fst p)) (S j)) - (\snd (nth (bars (\fst p)) q0 j) = \snd (nth (bars l1) q0 i)) ∧ - And3 - (sum_bases (bars (\snd p)) j ≤ offset - start (\snd p)) - (offset - start (\snd p) ≤ sum_bases (bars (\snd p)) (S j)) - (\snd (nth (bars (\snd p)) q0 j) = \snd (nth (bars l2) q0 i))). + (same_bases (\fst p) (\snd p)) + (same_values l1 (\fst p)) + (same_values l2 (\snd p)). definition rebase_spec_simpl ≝ - λl1,l2:list (ℚ × ℚ).λp:(list (ℚ × ℚ)) × (list (ℚ × ℚ)). - len ( (\fst p)) = len ( (\snd p)) ∧ - (∀i. - \fst (nth ( (\fst p)) q0 i) = - \fst (nth ( (\snd p)) q0 i)) ∧ - ∀i,offset. - sum_bases ( l1) i ≤ offset ∧ - offset ≤ sum_bases ( l1) (S i) - → - ∃j. - sum_bases ( (\fst p)) j ≤ offset ∧ - offset ≤ sum_bases ((\fst p)) (S j) ∧ - \snd (nth ( (\fst p)) q0 j) = - \snd (nth ( l1) q0 i). + λ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_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))). + +(* a local letin makes russell fail *) +definition cb0h : list bar → list bar ≝ + λl.mk_list (λi.〈\fst (nth l ▭ i),OQ〉) (len l). definition eject ≝ λP.λp:∃x:(list bar) × (list bar).P x.match p with [ex_introT p _ ⇒ p]. @@ -207,10 +283,11 @@ coercion inject with 0 1 nocomposites. definition rebase: rebase_spec. intros 2 (f1 f2); cases f1 (s1 l1); cases f2 (s2 l2); clear f1 f2; letin spec ≝ ( - λl1,l2:list (ℚ × ℚ).λm:nat.λz:(list (ℚ × ℚ)) × (list (ℚ × ℚ)). - len l1 + len l2 < m → rebase_spec_simpl l1 l2 z); + λs.λl1,l2.λm.λz.len l1 + len l2 < m → rebase_spec_simpl s l1 l2 z); +alias symbol "pi1" (instance 34) = "exT \fst". +alias symbol "pi1" (instance 21) = "exT \fst". letin aux ≝ ( -let rec aux (l1,l2:list (ℚ × ℚ)) (n:nat) on n : (list (ℚ × ℚ)) × (list (ℚ × ℚ)) ≝ +let rec aux (l1,l2:list bar) (n:nat) on n : (list bar) × (list bar) ≝ match n with [ O ⇒ 〈 nil ? , nil ? 〉 | S m ⇒ @@ -220,43 +297,59 @@ match n with match l2 with [ nil ⇒ 〈l1, cb0h l1〉 | cons he2 tl2 ⇒ - let base1 ≝ (\fst he1) in - let base2 ≝ (\fst he2) in + let base1 ≝ Qpos (\fst he1) in + let base2 ≝ Qpos (\fst he2) in let height1 ≝ (\snd he1) in let height2 ≝ (\snd he2) in match q_cmp base1 base2 with [ q_eq _ ⇒ let rc ≝ aux tl1 tl2 m in 〈he1 :: \fst rc,he2 :: \snd rc〉 - | q_lt _ ⇒ + | q_lt Hp ⇒ let rest ≝ base2 - base1 in - let rc ≝ aux tl1 (〈rest,height2〉 :: tl2) m in - 〈〈base1,height1〉 :: \fst rc,〈base1,height2〉 :: \snd rc〉 - | q_gt _ ⇒ + let rc ≝ aux tl1 (〈\fst (unpos rest ?),height2〉 :: tl2) m in + 〈〈\fst he1,height1〉 :: \fst rc,〈\fst he1,height2〉 :: \snd rc〉 + | q_gt Hp ⇒ let rest ≝ base1 - base2 in - let rc ≝ aux (〈rest,height1〉 :: tl1) tl2 m in - 〈〈base2,height1〉 :: \fst rc,〈base2,height2〉 :: \snd rc〉 + let rc ≝ aux (〈\fst (unpos rest ?),height1〉 :: tl1) tl2 m in + 〈〈\fst he2,height1〉 :: \fst rc,〈\fst he2,height2〉 :: \snd rc〉 ]]]] -in aux : ∀l1,l2,m.∃z.spec l1 l2 m z); unfold spec; -[7: clearbody aux; unfold spec in aux; clear spec; +in aux : ∀l1,l2,m.∃z.∀s.spec s l1 l2 m z); unfold spec; +[9: clearbody aux; unfold spec in aux; clear spec; cases (q_cmp s1 s2); [1: cases (aux l1 l2 (S (len l1 + len l2))); - cases (H1 (le_n ?)); clear H1; - exists [apply 〈mk_q_f s1 (\fst w), mk_q_f s2 (\snd w)〉] repeat split; - [1: cases H2; assumption; + cases (H1 s1 (le_n ?)); clear H1; + exists [apply 〈mk_q_f s1 (\fst w), mk_q_f s2 (\snd w)〉] split; + [1,2: assumption; + |3: intro; apply (H3 input); + |4: intro; rewrite > H in H4; + rewrite > (H4 input); reflexivity;] + |2: letin l2' ≝ (〈\fst (unpos (s2-s1) ?),OQ〉::l2);[ + apply q_lt_minus; rewrite > q_plus_sym; rewrite > q_plus_OQ; + assumption] + cases (aux l1 l2' (S (len l1 + len l2'))); + cases (H1 s1 (le_n ?)); clear H1 aux; + exists [apply 〈mk_q_f s1 (\fst w), mk_q_f s1 (\snd w)〉] split; + [1: reflexivity |2: assumption; - |3: cases H2; assumption; - |4: intros; cases (H3 i (offset - s1)); - [2: - - -|1,2: simplify; generalize in ⊢ (? ? (? (? ? (? ? ? (? ? %)))) (? (? ? (? ? ? (? ? %))))); intro X; - cases X (rc OK); clear X; simplify; apply eq_f; assumption; -|3: cases (aux l4 l5 n1) (rc OK); simplify; apply eq_f; assumption; -|4,5: simplify; unfold cb0h; rewrite > len_mk_list; reflexivity; -|6: reflexivity] -clearbody aux; unfold spec in aux; clear spec; - - - + |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 *) ]] +|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);] qed. \ No newline at end of file diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma index 2e0df971e..e4787fe84 100644 --- a/helm/software/matita/library/list/list.ma +++ b/helm/software/matita/library/list/list.ma @@ -142,21 +142,29 @@ reflexivity. qed. *) -let rec nth (A:Type) l d n on n ≝ - match n with - [ O ⇒ - match l with - [ nil ⇒ d - | cons (x : A) _ ⇒ x - ] - | S n' ⇒ nth A (tail ? l) d n' - ]. +definition nth ≝ + λA:Type. + let rec nth l d n on n ≝ + match n with + [ O ⇒ + match l with + [ nil ⇒ d + | cons (x : A) _ ⇒ x + ] + | S n' ⇒ nth (tail ? l) d n'] + in nth. -let rec map (A,B:Type) (f: A → B) (l : list A) on l : list B ≝ - match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)]. +definition map ≝ + λA,B:Type.λf:A→B. + let rec map (l : list A) on l : list B ≝ + match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map tl)] + in map. -let rec foldr (A,B:Type) (f : A → B → B) (b : B) (l : list A) on l : B := - match l with [ nil ⇒ b | (cons a l) ⇒ f a (foldr ? ? f b l)]. +definition foldr ≝ + λA,B:Type.λf:A→B→B.λb:B. + let rec foldr (l : list A) on l : B := + match l with [ nil ⇒ b | (cons a l) ⇒ f a (foldr l)] + in foldr. definition length ≝ λT:Type.λl:list T.foldr T nat (λx,c.S c) O l. diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang index caffee3f1..bcad516e0 100644 --- a/helm/software/matita/matita.lang +++ b/helm/software/matita/matita.lang @@ -114,7 +114,6 @@ left letin normalize - reduce reflexivity replace rewrite -- 2.39.2