include "models/list_support.ma".
include "cprop_connectives.ma".
-definition bar ≝ ratio × ℚ. (* base (Qpos) , height *)
-record q_f : Type ≝ { start : ℚ; bars: list bar }.
+definition bar ≝ ℚ × ℚ.
notation < "\rationals \sup 2" non associative with precedence 90 for @{'q2}.
interpretation "Q x Q" 'q2 = (Prod Q Q).
-definition empty_bar : bar ≝ 〈one,OQ〉.
+definition empty_bar : bar ≝ 〈Qpos one,OQ〉.
notation "\rect" with precedence 90 for @{'empty_bar}.
interpretation "q0" 'empty_bar = empty_bar.
notation < "\ldots\rect\square\EmptySmallSquare\ldots" with precedence 90 for @{'lq2}.
-interpretation "lq2" 'lq2 = (list bar).
-
-let rec sum_bases (l:list bar) (i:nat) on i ≝
- match i with
- [ O ⇒ OQ
- | S m ⇒
- match l with
- [ 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:
- ∀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.
-
-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.
-
-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);
-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.∀n1,n2:nat.n1<n2→sum_bases l n1 < sum_bases l n2.
-intro; elim l 0;
-[1: intros 2; apply (cic:/matita/dama/nat_ordered_set/nat_elim2.con ???? n1 n2);
- [1: intro; cases n;
- [1: intro X; cases (not_le_Sn_O ? X);
- |2: simplify; intros; apply q_lt_plus_trans;
- [1: apply sum_bases_ge_OQ;|2: apply (q_pos_lt_OQ one)]]
- |2: simplify; intros; cases (not_le_Sn_O ? H);
- |3: simplify; intros; apply q_lt_inj_plus_r;
- apply H; apply le_S_S_to_le; apply H1;]
-|2: intros 5; apply (cic:/matita/dama/nat_ordered_set/nat_elim2.con ???? n1 n2);
- [1: simplify; intros; cases n in H1; intros;
- [1: cases (not_le_Sn_O ? H1);
- |2: simplify; apply q_lt_plus_trans;
- [1: apply sum_bases_ge_OQ;|2: apply q_pos_lt_OQ]]
- |2: simplify; intros; cases (not_le_Sn_O ? H1);
- |3: simplify; intros; apply q_lt_inj_plus_r; apply H;
- apply le_S_S_to_le; apply H2;]]
+interpretation "lq2" 'lq2 = (list bar).
+
+inductive sorted : list bar → Prop ≝
+| sorted_nil : sorted []
+| sorted_one : ∀x. sorted [x]
+| sorted_cons : ∀x,y,tl. \fst x < \fst y → sorted (y::tl) → sorted (x::y::tl).
+
+definition nth_base ≝ λf,n. \fst (nth f ▭ n).
+definition nth_height ≝ λf,n. \snd (nth f ▭ n).
+
+record q_f : Type ≝ {
+ bars: list bar;
+ increasing_bars : sorted bars;
+ bars_begin_OQ : nth_base bars O = OQ;
+ bars_tail_OQ : nth_height bars (pred (len bars)) = OQ
+}.
+
+lemma nth_nil: ∀T,i.∀def:T. nth [] def i = def.
+intros; elim i; simplify; [reflexivity;] assumption; qed.
+
+lemma all_bases_positives : ∀f:q_f.∀i.i < len (bars f) → OQ < nth_base (bars f) i.
+intro f; elim (increasing_bars f);
+[1: unfold nth_base; rewrite > nth_nil; apply (q_pos_OQ one);
+|2: cases i in H; [2: cases (?:False);
qed.
-lemma sum_bases_n_m:
- ∀n,m,l.
- sum_bases l n < sum_bases l (S m) →
- sum_bases l m < sum_bases l (S n) →
- n = m.
-intros 2; apply (nat_elim2 ???? n m);
-[1: intro X; cases X; intros; [reflexivity] cases (?:False);
- cases l in H H1; simplify; intros;
- apply (q_lt_le_incompat ??? (sum_bases_ge_OQ ? n1));
- apply (q_lt_canc_plus_r ??? H1);
-|2: intros 2; cases l; simplify; intros; cases (?:False);
- apply (q_lt_le_incompat ??? (sum_bases_ge_OQ ? n1));
- apply (q_lt_canc_plus_r ??? H); (* magia ... *)
-|3: intros 4; cases l; simplify; intros;
- [1: rewrite > (H []); [reflexivity]
- apply (q_lt_canc_plus_r ??(Qpos one)); assumption;
- |2: rewrite > (H l1); [reflexivity]
- apply (q_lt_canc_plus_r ??(Qpos (\fst b))); assumption;]]
-qed.
+definition eject_Q ≝
+ λP.λp:∃x:ℚ.P x.match p with [ex_introT p _ ⇒ p].
+coercion eject_Q.
+definition inject_Q ≝ λP.λp:ℚ.λh:P p. ex_introT ? P p h.
+coercion inject_Q with 0 1 nocomposites.
-definition eject1 ≝
- λP.λp:∃x:nat × ℚ.P x.match p with [ex_introT p _ ⇒ p].
-coercion eject1.
-definition inject1 ≝ λP.λp:nat × ℚ.λh:P p. ex_introT ? P p h.
-coercion inject1 with 0 1 nocomposites.
+definition value_spec : q_f → ℚ → ℚ → Prop ≝
+ λf,i,q.
+ ∃j. q = nth_height (bars f) j ∧
+ (nth_base (bars f) j < i ∧
+ ∀n.j < n → n < len (bars f) → i ≤ nth_base (bars f) n).
-definition value :
- ∀f:q_f.∀i:ℚ.∃p:nat × ℚ.
- Or4
- (And3 (i < start f) (\fst p = O) (\snd p = OQ))
- (And3
- (start f + sum_bases (bars f) (len (bars f)) ≤ i)
- (\fst p = O) (\snd p = OQ))
- (And3 (bars f = []) (\fst p = O) (\snd p = OQ))
- (And4
- (And3 (bars f ≠ []) (start f ≤ i) (i < start f + sum_bases (bars f) (len (bars f))))
- (\fst p ≤ (len (bars f)))
- (\snd p = \snd (nth (bars f) ▭ (\fst p)))
- (sum_bases (bars f) (\fst p) ≤ ⅆ[i,start f] ∧
- (ⅆ[i, start f] < sum_bases (bars f) (S (\fst p))))).
+definition value : ∀f:q_f.∀i:ratio.∃p:ℚ.value_spec f (Qpos i) p.
intros;
+alias symbol "lt" (instance 5) = "Q less than".
+alias symbol "leq" = "Q less or equal than".
+letin value_spec_aux ≝ (
+ λf,i,q.∃j. q = nth_height f j ∧
+ (nth_base f j < i ∧ ∀n.j < n → n < len f → i ≤ nth_base f n));
letin value ≝ (
- let rec value (p: ℚ) (l : list bar) on l ≝
+ let rec value (acc: ℚ) (l : list bar) on l : ℚ ≝
match l with
- [ nil ⇒ 〈nat_of_q p,OQ〉
+ [ nil ⇒ acc
| cons x tl ⇒
- match q_cmp p (Qpos (\fst x)) with
- [ q_lt _ ⇒ 〈O, \snd x〉
- | _ ⇒
- let rc ≝ value (p - Qpos (\fst x)) tl in
- 〈S (\fst rc),\snd rc〉]]
+ match q_cmp (\fst x) (Qpos i) with
+ [ q_leq _ ⇒ value (\snd x) tl
+ | q_gt _ ⇒ acc]]
in value :
- ∀acc,l.∃p:nat × ℚ.OQ ≤ acc →
- Or
- (And3 (l = []) (\fst p = nat_of_q acc) (\snd p = OQ))
- (And3
- (sum_bases l (\fst p) ≤ acc)
- (acc < sum_bases l (S (\fst p)))
- (\snd p = \snd (nth l ▭ (\fst p)))));
+ ∀acc,l.∃p:ℚ. OQ ≤ acc → value_spec_aux l (Qpos i) p);
+[4: clearbody value; cases (value OQ (bars f)) (p Hp); exists[apply p];
+ cases (Hp (q_le_n ?)) (j Hj); cases Hj (Hjp H); cases H (Hin Hmax);
+ clear Hp value value_spec_aux Hj H; exists [apply j]; split[2:split;intros;]
+ try apply Hmax; assumption;
+|1: intro Hacc; clear H2; cases (value (\snd b) l1) (j Hj);
+ cases (q_cmp (\snd b) (Qpos i)) (Hib Hib);
+ [1: cases (Hj Hib) (w Hw); simplify in ⊢ (? ? ? %); clear Hib Hj;
+ exists [apply (S w)] cases Hw; cases H3; clear Hw H3;
+ split; try assumption; split; try assumption; intros;
+ apply (q_le_trans ??? (H5 (pred n) ??)); [3: apply q_le_n]
+
+
+
+
[5: clearbody value;
cases (q_cmp i (start f));
[2: exists [apply 〈O,OQ〉] simplify; constructor 1; split; try assumption;
(* *)
(**************************************************************************)
-include "Q/q/q.ma".
+include "Q/q/qtimes.ma".
+include "Q/q/qplus.ma".
include "cprop_connectives.ma".
notation "\rationals" non associative with precedence 99 for @{'q}.
(* group over Q *)
axiom qp : ℚ → ℚ → ℚ.
-axiom qm : ℚ → ℚ → ℚ.
interpretation "Q plus" 'plus x y = (qp x y).
-interpretation "Q minus" 'minus x y = (qm x y).
+interpretation "Q minus" 'minus x y = (qp x (Qopp y)).
axiom q_plus_OQ: ∀x:ℚ.x + OQ = x.
axiom q_plus_sym: ∀x,y:ℚ.x + y = y + x.
axiom q_plus_minus: ∀x.x - x = OQ.
-axiom q_minus: ∀x,y. y - Qpos x = y + Qneg x.
-axiom q_minus_r: ∀x,y. y + Qpos x = y - Qneg x.
axiom q_plus_assoc: ∀x,y,z.x + (y + z) = x + y + z.
-axiom q_elim_minus: ∀x,y.x - y = x + Qopp y.
-axiom q_elim_opp: ∀x,y.x - Qopp y = x + y.
-axiom q_minus_distrib:∀x,y,z:Q.x - (y + z) = x - y - z.
+axiom q_opp_plus: ∀x,y,z:Q. Qopp (y + z) = Qopp y + Qopp z.
(* order over Q *)
-axiom qlt : ℚ → ℚ → CProp.
-axiom qle : ℚ → ℚ → CProp.
+axiom qlt : ℚ → ℚ → Prop.
+axiom qle : ℚ → ℚ → Prop.
interpretation "Q less than" 'lt x y = (qlt x y).
interpretation "Q less or equal than" 'leq x y = (qle x y).
inductive q_comparison (a,b:ℚ) : CProp ≝
- | q_eq : a = b → q_comparison a b
- | q_lt : a < b → q_comparison a b
+ | q_leq : a ≤ b → q_comparison a b
| q_gt : b < a → q_comparison a b.
axiom q_cmp:∀a,b:ℚ.q_comparison a b.
-axiom q_le_minus: ∀a,b,c:ℚ. a ≤ c - b → a + b ≤ c.
-axiom q_le_minus_r: ∀a,b,c:ℚ. a - b ≤ c → a ≤ c + b.
-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 q_le_plus: ∀a,b,c:ℚ. a ≤ c + b → a - b ≤ c.
-axiom q_le_plus_r: ∀a,b,c:ℚ. a + b ≤ c → a ≤ c - b.
-axiom q_lt_plus_r: ∀a,b,c:ℚ. a + b < c → a < c - b.
-axiom q_lt_minus_r: ∀a,b,c:ℚ. a - b < c → a < c + b.
+inductive q_le_elimination (a,b:ℚ) : CProp ≝
+| q_le_from_eq : a = b → q_le_elimination a b
+| q_le_from_lt : a < b → q_le_elimination a b.
+
+axiom q_le_cases : ∀x,y:ℚ.x ≤ y → q_le_elimination x y.
+
+axiom q_le_plus_l: ∀a,b,c:ℚ. a ≤ c - b → a + b ≤ c.
+axiom q_le_plus_r: ∀a,b,c:ℚ. a - b ≤ c → a ≤ c + b.
+axiom q_lt_plus_l: ∀a,b,c:ℚ. a < c - b → a + b < c.
+axiom q_lt_plus_r: ∀a,b,c:ℚ. a - b < c → a < c + b.
+
axiom q_lt_opp_opp: ∀a,b.b < a → Qopp a < Qopp b.
+
+axiom q_le_n: ∀x. x ≤ x.
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_lt_corefl: ∀x:Q.x < x → False.
-axiom q_lt_antisym: ∀x,y:Q.x < y → y < x → False.
axiom q_lt_le_incompat: ∀x,y:Q.x < y → y ≤ x → False.
-axiom q_neg_gt: ∀r:ratio.OQ < Qneg r → False.
+
+axiom q_neg_gt: ∀r:ratio.Qneg r < OQ.
+axiom q_pos_OQ: ∀x.OQ < Qpos x.
+
axiom q_lt_trans: ∀x,y,z:Q. x < y → y < z → x < z.
axiom q_lt_le_trans: ∀x,y,z:Q. x < y → y ≤ z → x < z.
axiom q_le_lt_trans: ∀x,y,z:Q. x ≤ y → y < z → x < z.
axiom q_le_trans: ∀x,y,z:Q. x ≤ y → y ≤ z → x ≤ z.
-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.
-axiom q_le_S: ∀x,y,z.OQ ≤ x → x + y ≤ z → y ≤ z.
-axiom q_eq_to_le: ∀x,y. x = y → x ≤ y.
-axiom q_le_OQ_Qpos: ∀x.OQ ≤ Qpos x.
-
-inductive q_le_elimination (a,b:ℚ) : CProp ≝
-| q_le_from_eq : a = b → q_le_elimination a b
-| q_le_from_lt : a < b → q_le_elimination a b.
+axiom q_le_lt_OQ_plus_trans: ∀x,y:Q.OQ ≤ x → OQ < y → OQ < x + y.
+axiom q_lt_le_OQ_plus_trans: ∀x,y:Q.OQ < x → OQ ≤ y → OQ < x + y.
+axiom q_le_OQ_plus_trans: ∀x,y:Q.OQ ≤ x → OQ ≤ y → OQ ≤ x + y.
-axiom q_le_cases : ∀x,y:ℚ.x ≤ y → q_le_elimination x y.
+axiom q_leWl: ∀x,y,z.OQ ≤ x → x + y ≤ z → y ≤ z.
+axiom q_ltWl: ∀x,y,z.OQ ≤ x → x + y < z → y < z.
(* distance *)
axiom q_dist : ℚ → ℚ → ℚ.
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_d_x_x: ∀x:Q.ⅆ[x,x] = OQ.
-axiom q_d_noabs: ∀x,y. x ≤ y → ⅆ[x,y] = y - x.
-axiom q_d_sym: ∀x,y. ⅆ[x,y] = ⅆ[y,x].
+axiom q_d_ge_OQ : ∀x,y:ℚ. OQ ≤ ⅆ[x,y].
+axiom q_d_OQ: ∀x:Q.ⅆ[x,x] = OQ.
+axiom q_d_noabs: ∀x,y. x ≤ y → ⅆ[y,x] = y - x.
+axiom q_d_sym: ∀x,y. ⅆ[x,y] = ⅆ[y,x].
-(* integral part *)
-axiom nat_of_q: ℚ → nat.
+lemma q_2opp: ∀x:ℚ.Qopp (Qopp x) = x.
+intros; cases x; reflexivity; qed.
(* derived *)
lemma q_lt_canc_plus_r:
∀x,y,z:Q.x + z < y + z → x < y.
intros; rewrite < (q_plus_OQ y); rewrite < (q_plus_minus z);
-rewrite > q_elim_minus; rewrite > q_plus_assoc;
-apply q_lt_plus; rewrite > q_elim_opp; assumption;
+rewrite > q_plus_assoc; apply q_lt_plus_r; rewrite > q_2opp; assumption;
qed.
lemma q_lt_inj_plus_r:
∀x,y,z:Q.x < y → x + z < y + z.
intros; apply (q_lt_canc_plus_r ?? (Qopp z));
-do 2 (rewrite < q_plus_assoc;rewrite < q_elim_minus);
-rewrite > q_plus_minus;
+do 2 rewrite < q_plus_assoc; rewrite > q_plus_minus;
do 2 rewrite > q_plus_OQ; assumption;
qed.
lemma q_le_inj_plus_r:
∀x,y,z:Q.x ≤ y → x + z ≤ y + z.
intros;cases (q_le_cases ?? H);
-[1: rewrite > H1; apply q_eq_to_le; reflexivity;
+[1: rewrite > H1; apply q_le_n;
|2: apply q_lt_to_le; apply q_lt_inj_plus_r; assumption;]
qed.
∀x,y,z:Q.x + z ≤ y + z → x ≤ y.
intros; lapply (q_le_inj_plus_r ?? (Qopp z) H) as H1;
do 2 rewrite < q_plus_assoc in H1;
-rewrite < q_elim_minus in H1; rewrite > q_plus_minus in H1;
-do 2 rewrite > q_plus_OQ in H1; assumption;
+rewrite > q_plus_minus in H1; do 2 rewrite > q_plus_OQ in H1; assumption;
qed.
projects / helm.git / commitdiff