nth_height f j = q → nth_base f j < i → j < \len f →
(∀n.n<j → nth_base f n < i) →
(∀n.j < n → n < \len f → i ≤ nth_base f n) → value_spec f i q.
+
+definition match_pred ≝
+ λi.λx:bar.match q_cmp (Qpos i) (\fst x) with[ q_leq _ ⇒ true| q_gt _ ⇒ false].
+
+definition match_domain ≝
+ λf: list bar.λi:ratio. pred (find ? (match_pred i) f ▭).
+
+definition value_simple ≝
+ λf: list bar.λi:ratio. nth_height f (match_domain f i).
alias symbol "lt" (instance 5) = "Q less than".
alias symbol "lt" (instance 6) = "natural 'less than'".
∀f:list bar.sorted q2_lt f → O < length bar f →
∀i:ratio.nth_base f O < Qpos i → ∃p:ℚ×ℚ.value_spec f (Qpos i) p.
intros (f bars_sorted_f len_bases_gt_O_f i bars_begin_OQ_f);
-letin P ≝
- (λx:bar.match q_cmp (Qpos i) (\fst x) with[ q_leq _ ⇒ true| q_gt _ ⇒ false]);
-exists [apply (nth_height f (pred (find ? P f ▭)));]
-apply (value_of ?? (pred (find ? P f ▭)));
+exists [apply (value_simple f i);]
+apply (value_of ?? (match_domain f i));
[1: reflexivity
-|2: cases (cases_find bar P f ▭);
+|2: unfold match_domain; cases (cases_find bar (match_pred i) f ▭);
[1: cases i1 in H H1 H2 H3; simplify; intros;
[1: generalize in match (bars_begin_OQ_f);
cases (len_gt_non_empty ?? (len_bases_gt_O_f)); simplify; intros;
assumption;
|2: cases (len_gt_non_empty ?? (len_bases_gt_O_f)) in H3;
- intros; lapply (H3 n (le_n ?)) as K; unfold P in K;
+ intros; lapply (H3 n (le_n ?)) as K; unfold match_pred in K;
cases (q_cmp (Qpos i) (\fst (\nth (x::l) ▭ n))) in K;
simplify; intros; [destruct H5] assumption]
|2: destruct H; cases (len_gt_non_empty ?? (len_bases_gt_O_f)) in H2;
simplify; intros; lapply (H (\len l) (le_n ?)) as K; clear H;
- unfold P in K; cases (q_cmp (Qpos i) (\fst (\nth (x::l) ▭ (\len l)))) in K;
+ unfold match_pred in K; cases (q_cmp (Qpos i) (\fst (\nth (x::l) ▭ (\len l)))) in K;
simplify; intros; [destruct H2] assumption;]
-|5: intro; cases (cases_find bar P f ▭); intros;
+|5: intro; unfold match_domain; cases (cases_find bar (match_pred i) f ▭); intros;
[1: generalize in match (bars_sorted_f);
cases (list_break ??? H) in H1; rewrite > H6;
- rewrite < H1; simplify; rewrite > nth_len; unfold P;
+ rewrite < H1; simplify; rewrite > nth_len; unfold match_pred;
cases (q_cmp (Qpos i) (\fst x)); simplify;
intros (X Hs); [2: destruct X] clear X;
cases (sorted_pivot q2_lt ??? ▭ Hs);
repeat rewrite < plus_n_Sm; rewrite < plus_n_O; simplify;
rewrite > sym_plus; rewrite < minus_plus_m_m; reflexivity;]
rewrite > len_append; rewrite > H1; simplify; rewrite < plus_n_SO;
- apply le_S_S; clear H1 H6 H7 Hs H8 H9 Hn x l2 l1 H4 H3 H2 H P;
+ apply le_S_S; clear H1 H6 H7 Hs H8 H9 Hn x l2 l1 H4 H3 H2 H;
elim (\len f) in i1 n H5; [cases (not_le_Sn_O ? H);]
simplify; cases n2; [ repeat rewrite < minus_n_O; apply le_S_S_to_le; assumption]
cases n1 in H1; [intros; rewrite > eq_minus_n_m_O; apply le_O_n]
|2: cases (not_le_Sn_n i1); rewrite > H in ⊢ (??%);
apply (trans_le ??? ? H4); cases i1 in H3; intros; apply le_S_S;
[ apply le_O_n; | assumption]]
-|3: cases (cases_find bar P f ▭); [
+|3: unfold match_domain; cases (cases_find bar (match_pred i) f ▭); [
cases i1 in H; intros; simplify; [assumption]
apply lt_S_to_lt; assumption;]
rewrite > H; cases (\len f) in len_bases_gt_O_f; intros; [cases (not_le_Sn_O ? H3)]
simplify; apply le_n;
-|4: intros; cases (cases_find bar P f ▭) in H; simplify; intros;
+|4: intros; unfold match_domain in H; cases (cases_find bar (match_pred i) f ▭) in H; simplify; intros;
[1: lapply (H3 n); [2: cases i1 in H4; intros [assumption] apply le_S; assumption;]
- unfold P in Hletin; cases (q_cmp (Qpos i) (\fst (\nth f ▭ n))) in Hletin;
+ unfold match_pred in Hletin; cases (q_cmp (Qpos i) (\fst (\nth f ▭ n))) in Hletin;
simplify; intros; [destruct H6] assumption;
|2: destruct H; cases f in len_bases_gt_O_f H2 H3; clear H1; simplify; intros;
[cases (not_le_Sn_O ? H)] lapply (H1 n); [2: apply le_S; assumption]
- unfold P in Hletin; cases (q_cmp (Qpos i) (\fst (\nth (b::l) ▭ n))) in Hletin;
+ unfold match_pred in Hletin; cases (q_cmp (Qpos i) (\fst (\nth (b::l) ▭ n))) in Hletin;
simplify; intros; [destruct H4] assumption;]]
qed.
| apply bars_begin_lt_Qpos;]
qed.
-alias symbol "lt" (instance 5) = "natural 'less than'".
-alias symbol "lt" (instance 4) = "Q less than".
-lemma value_simpl:
- ∀f:list bar.sorted q2_lt f → O < (length bar f) →
- ∀i:ratio.nth_base f O < Qpos i → ℚ × ℚ.
-intros; cases (value_lemma f H H1 i H2); assumption;
-qed.
-
lemma cases_value : ∀f,i. value_spec (bars f) (Qpos i) (value f i).
intros; unfold value;
cases (value_lemma (bars f) (bars_sorted f) (len_bases_gt_O f) i (bars_begin_lt_Qpos f i));
assumption;
qed.
-lemma cases_value_simpl :
- ∀f,H1,H2,i,Hi.value_spec f (Qpos i) (value_simpl f H1 H2 i Hi).
-intros; unfold value_simpl; cases (value_lemma f H1 H2 i Hi);
-assumption;
-qed.
-
definition same_values ≝ λl1,l2:q_f.∀input. value l1 input = value l2 input.
-definition same_values_simpl ≝
- λl1,l2:list bar.∀H1,H2,H3,H4,input,Hi1,Hi2.
- value_simpl l1 H1 H2 input Hi1 = value_simpl l2 H3 H4 input Hi2.
-
-lemma value_head :
- ∀x,y,l,H1,H2,i,H3.
- Qpos i ≤ \fst x → value_simpl (y::x::l) H1 H2 i H3 = \snd y.
-intros; cases (cases_value_simpl ? H1 H2 i H3);
-cases j in H4 H5 H6 H7 H8 (j); simplify; intros;
-[1: symmetry; assumption;
-|2: cases (?:False); cases j in H4 H5 H6 H7 H8; intros;
- [1: lapply (q_le_lt_trans ??? H H5) as K;cases (q_lt_corefl ? K);
- |2: lapply (H7 1); [2: do 2 apply le_S_S; apply le_O_n;]
- simplify in Hletin;
- lapply (q_le_lt_trans ??? H Hletin) as K;cases (q_lt_corefl ? K);]]
-qed.
-lemma same_values_simpl_to_same_values:
- ∀b1,b2,Hs1,Hs2,Hb1,Hb2,He1,He2,input.
- same_values_simpl b1 b2 →
- value (mk_q_f b1 Hs1 Hb1 He1) input =
- value (mk_q_f b2 Hs2 Hb2 He2) input.
-intros;
-lapply (len_bases_gt_O (mk_q_f b1 Hs1 Hb1 He1));
-lapply (len_bases_gt_O (mk_q_f b2 Hs2 Hb2 He2));
-lapply (H ???? input) as K; try assumption;
-[2: rewrite > Hb1; apply q_pos_OQ;
-|3: rewrite > Hb2; apply q_pos_OQ;
-|1: apply K;]
-qed.
-
-include "russell_support.ma".
-
-lemma value_tail :
- ∀x,y,l,H1,H2,i,H3.
- \fst x < Qpos i →
- value_simpl (y::x::l) H1 H2 i H3 =
- value_simpl (x::l) ?? i ?.
-[1: apply hide; apply (sorted_tail q2_lt); [apply y| assumption]
-|2: apply hide; simplify; apply le_S_S; apply le_O_n;
-|3: apply hide; assumption;]
-intros;cases (cases_value_simpl ? H1 H2 i H3);
-generalize in ⊢ (? ? ? (? ? % ? ? ?)); intro;
-generalize in ⊢ (? ? ? (? ? ? % ? ?)); intro;
-generalize in ⊢ (? ? ? (? ? ? ? ? %)); intro;
-cases (cases_value_simpl (x::l) H9 H10 i H11);
-cut (j = S j1) as E; [ destruct E; destruct H12; reflexivity;]
-clear H12 H4; cases j in H8 H5 H6 H7;
-[1: intros;cases (?:False); lapply (H7 1 (le_n ?)); [2: simplify; do 2 apply le_S_S; apply le_O_n]
- simplify in Hletin; apply (q_lt_corefl (\fst x));
- apply (q_lt_le_trans ??? H Hletin);
-|2: simplify; intros; clear q q1 j H11 H10 H1 H2; simplify in H3 H14; apply eq_f;
- cases (cmp_nat n j1); [cases (cmp_nat j1 n);[apply le_to_le_to_eq; assumption]]
- [1: clear H1; cases (?:False);
- lapply (H7 (S j1)); [2: cases j1 in H2; intros[cases (not_le_Sn_O ? H1)] apply le_S_S; assumption]
- [2: apply le_S_S; assumption;] simplify in Hletin;
- apply (q_lt_corefl ? (q_le_lt_trans ??? Hletin H13));
- |2: cases (?:False);
- lapply (H16 n); [2: assumption|3:simplify; apply le_S_S_to_le; assumption]
- apply (q_lt_corefl ? (q_le_lt_trans ??? Hletin H4));]]
-qed.
-
definition same_bases ≝ λl1,l2:list bar. ∀i.\fst (\nth l1 ▭ i) = \fst (\nth l2 ▭ i).
lemma same_bases_cons: ∀a,b,l1,l2.
projects / helm.git / blobdiff