(* *)
(**************************************************************************)
+include "nat_ordered_set.ma".
include "models/q_support.ma".
include "models/list_support.ma".
include "cprop_connectives.ma".
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<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;]]
+qed.
+
definition eject1 ≝
λP.λp:∃x:nat × ℚ.P x.match p with [ex_introT p _ ⇒ p].
coercion eject1.
definition value :
∀f:q_f.∀i:ℚ.∃p:nat × ℚ.
- match q_cmp i (start f) with
- [ 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)))
- (\snd p = \snd (nth (bars f) ▭ (\fst p)))].
+ 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
+ (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))))).
intros;
-alias symbol "pi2" = "pair pi2".
-alias symbol "pi1" = "pair pi1".
letin value ≝ (
let rec value (p: ℚ) (l : list bar) on l ≝
match l with
(\snd p = \snd (nth l ▭ (\fst p))));
[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 (q_dist_ge_OQ ? ?)); clear Hp value;
- exists[1,3:apply p]; simplify; split; assumption;]
+ [2: exists [apply 〈O,OQ〉] simplify; constructor 1; split; try assumption;
+ try reflexivity; apply q_lt_to_le; assumption;
+ |1: exists [apply 〈O,OQ〉] simplify; constructor 1; split; try assumption;
+ try reflexivity; apply q_eq_to_le; assumption;
+ |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;
+ |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 <H2; assumption|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)));
|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)).
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.
-
projects / helm.git / blobdiff