Library hydras.Epsilon0.Large_Sets
From hydras Require Import E0 Canon Paths.
From hydras Require Import MoreLists Iterates Exp2.
From Coq Require Import Lia Compare_dec.
Import Relation_Operators Sorted Operators_Properties.
Open Scope t1_scope.
Definition mlarge alpha (s: list nat) := path_to zero s alpha.
Definition mlargeS alpha s := path_toS zero s alpha.
Inductive L_spec : T1 → (nat → nat) → Prop :=
L_spec0 :
∀ f, (∀ k, f (S k) = S k) → L_spec zero f
| L_spec1 : ∀ alpha f,
alpha ≠ zero →
(∀ k,
mlarge alpha (interval (S k) (Nat.pred (f (S k))))) →
L_spec alpha f.
Test functions
- If f is correct w.r.t. L_spec, "Compute L_test alpha f k" should return (one=one).
- If f k is too small, returns (alpha = one) (with one < alpha)
- If f k is too big, returns (zero = one)
Lemma gnaw_finite_1_iota :
∀ n i, gnaw (S n) (iota_from (S i) n) = 1.
Lemma gnaw_finite_1 : ∀ n i, gnaw (S n) (interval (S i) (n + i)%nat) = 1.
Lemma gnaw_finite : ∀ n i, gnaw (S n) (iota_from (S i) (S n)) = 0.
Lemma gnaw_n_R : ∀ s n, ¬ In 0 s →
(n < List.length s)%nat →
gnaw (S n) s = zero.
Lemma mlarge_unicity alpha k l l' :
mlarge alpha (interval (S k) l) →
mlarge alpha (interval (S k) l') →
l = l'.
Lemma mlargeS_iff alpha x s : s ≠nil →
mlargeS alpha (x::s) ↔
gnawS alpha (but_last x s) = one.
Lemma mlarge_unshift alpha s :
¬In 0 s → mlarge alpha s ↔ mlargeS alpha (unshift s).
Lemma mlarge_iff alpha x (s:list nat) :
s ≠ nil → ¬ In 0 (x::s) →
mlarge alpha (x::s) ↔ gnaw alpha (but_last x s) = one.
Lemma L_spec_inv2 alpha f :
L_spec alpha f → alpha ≠ zero →
(∀ k, mlarge alpha (interval (S k) (Nat.pred (f (S k))))).
Lemma L_spec_compat alpha (f g : nat → nat) :
L_spec alpha f → (∀ n, f n = g n) → L_spec alpha g.
Lemma L_zero_inv f : L_spec zero f → ∀ k, f (S k) = S k.
Lemma L_pos_inv alpha f : alpha ≠ zero → L_spec alpha f →
∀ k, (S k < f (S k))%nat.
Lemma L_spec_unicity alpha f g :
L_spec alpha f → L_spec alpha g → ∀ k, f (S k) = g (S k).
Composition lemmas for computing L_ alpha
Section succ.
Variables (beta : T1) (f : nat → nat).
Hypotheses (Hbeta : nf beta)
(f_mono : strict_mono f)
(f_Sle : S <<= f)
(f_ok : L_spec beta f).
Definition L_succ := fun k ⇒ f (S k).
Lemma L_succ_mono : strict_mono L_succ.
Lemma L_succ_Sle : S <<= L_succ.
Lemma L_succ_ok : L_spec (succ beta) L_succ. End succ.
Section lim.
Variables (lambda : T1)
(Hnf : nf lambda)
(Hlim : T1limit lambda)
(f : nat → nat → nat)
(H : ∀ k, L_spec (canon lambda (S k)) (f (S k))).
Remark canon_not_null : ∀ k, canon lambda (S k) ≠ zero.
Definition L_lim k := f k (S k).
Lemma L_lim_ok : L_spec lambda L_lim.
End lim.
Definition L_fin i := fun k ⇒ (i + k)%nat.
Lemma L_finS_S_le i : S <<= L_fin (S i).
Lemma L_fin_smono i: strict_mono (L_fin i).
Lemma L_S_succ_rw i : ∀ k, L_fin (S i) k = L_succ (L_fin i) k.
Lemma L_fin_ok i : L_spec (\F i) (L_fin i).
Lemma mlarge_FS :
∀ i k, mlarge (FS i) (interval (S k) (S (i+k)%nat)).
Definition L_omega k := S (2 × k)%nat.
Lemma L_omega_Sle : S <<= L_omega.
Lemma L_omega_smono : strict_mono L_omega.
Lemma mlarge_omega k : mlarge T1omega (interval (S k) (2 × (S k))%nat).
Lemma L_omega_ok : L_spec T1omega L_omega.
Lemma path_to_omega_mult (i k:nat) :
path_to (T1omega × i)
(interval (S k) (2 × (S k))%nat)
(T1omega × (S i)).
Lemma omega_mult_mlarge_0 i : ∀ k,
mlarge (T1omega × (S i))
(interval (S k)
(Nat.pred (iterate (fun p ⇒ S (2 × p)%nat)
(S i)
(S k)))).
Definition L_omega_mult i (x:nat) := iterate L_omega i x.
Example Ex : L_omega_mult 8 5 = 1535.
Lemma L_omega_mult_Sle i : S <<= L_omega_mult (S i).
Lemma L_omega_mult_ok (i: nat) :
L_spec (T1omega × i) (L_omega_mult i).
Lemma L_omega_mult_eqn (i : nat) :
∀ (k : nat),
(0 < k)%nat → L_omega_mult i k = (exp2 i × S k - 1)%nat.
Definition L_omega_square k :=
iterate (fun z ⇒ S (2 × z)%nat) k (S k).
Remark L_omega_square_eqn1 k : L_omega_square k =
L_omega_mult k (S k).
Lemma L_omega_square_eqn k :
(0 < k)%nat →
L_omega_square k = (exp2 k × (k + 2) - 1)%nat.
Lemma L_omega_square_Sle : S <<= L_omega_square.
Lemma L_omega_square_smono : strict_mono L_omega_square.
Lemma L_omega_square_ok:
L_spec (T1omega × T1omega) L_omega_square.
Section phi0_mult.
Variables (alpha : T1) (f : nat → nat).
Hypotheses (Halpha : nf alpha)
(f_mono : strict_mono f)
(f_Sle : S <<= f)
(f_ok : L_spec (T1.phi0 alpha) f).
Definition L_phi0_mult i := iterate f i.
Remark f_ok_inv :
∀ k, mlarge (T1.phi0 alpha) (interval (S k) (Nat.pred (f (S k)))).
Lemma L_phi0_mult_ok i:
L_spec (T1.cons alpha i zero) (L_phi0_mult (S i)).
Lemma L_phi0_mult_smono i: strict_mono (L_phi0_mult i).
Lemma L_phi0_mult_Sle i: S <<= L_phi0_mult (S i).
End phi0_mult.
Definition L_omega_square_times i := iterate L_omega_square i.
Lemma L_omega_square_times_ok i : L_spec (T1.cons 2 i zero)
(L_omega_square_times (S i)).
Definition L_omega_cube := L_lim L_omega_square_times .
Lemma L_omega_cube_ok : L_spec (T1.phi0 3) L_omega_cube.
Lemma L_omega_cube_eqn i :
L_omega_cube i = L_omega_square_times i (S i).
Lemma exp2_k_mult_pos k:
(0 < k → 4 ≤ exp2 k × (k + 2))%nat.
Example omega_square_thrice_eqn : ∀ k,
(0 < k)%nat →
let M := (exp2 k × (k + 2) - 1)%nat in
let N := exp2 M in
let P := (N × (M + 2) - 1)%nat in
L_omega_square_times 3 k =
(exp2 P × (P + 2) - 1)%nat.
Lemma L_omega_cube_3_eq:
let N := exp2 95 in
let P := (N × 97 - 1)%nat in
L_omega_cube 3 = (exp2 P × (P + 2) - 1)%nat.
Plain large sequences (not necessarily minimal)
large sequences (as in KS ) (may contain zeros)
Definition largeb (alpha : T1) (s: list nat) :=
match (gnaw alpha s)
with zero ⇒ true | _ ⇒ false end.
Definition large (alpha : T1) (s : list nat) : Prop :=
largeb alpha s.
Definition largeSb (alpha : T1) (s: list nat) :=
match gnawS alpha s with
| T1.zero ⇒ true
| _ ⇒ false
end.
Definition largeS (alpha : T1) (s : list nat) : Prop :=
largeSb alpha s.
Definition Large alpha s := large (@cnf alpha) s.
Lemma large_iff (alpha : T1) (s : list nat) :
large alpha s ↔ gnaw alpha s = 0.
Lemma largeSb_b (alpha : T1) (s: list nat) :
largeSb alpha s = largeb alpha (shift s).
Lemma largeb_Sb alpha s :
largeb alpha s = largeSb alpha (unshift s).
Lemma largeS_iff (alpha : T1) (s : list nat) :
largeS alpha s ↔ gnawS alpha s = T1.zero.
Section Lemma_4_4_Proof.
Variables alpha beta : T1.
Hypothesis Halpha : nf alpha.
Hypothesis Hbeta : nf beta.
Variable n : nat.
Variable s : list nat.
Hypothesis Hs : sorted_ge n s.
Hypothesis H : const_pathS_eps n alpha beta.
Hypothesis H0 : largeS alpha s.
Lemma Lemma4_4 : largeS beta s.
End Lemma_4_4_Proof.
Lemma Lemma_4_4_2 :
∀ (s : list nat) (n : nat) (alpha beta : T1),
nf alpha → nf beta → sorted_ge n s →
const_pathS_eps n alpha beta → gnawS beta s t1≤ gnawS alpha s.
Lemma Lemma_4_5_1 n alpha:
nf alpha →
∀ s t ,
ptwise_le s t →
sorted_ge n s →
sorted_ge n t →
const_pathS_eps (simple_last n t)
(gnawS alpha t) (gnawS alpha s).
Section Proof_of_4_5_2.
Variables (A B1 B2 : list nat).
Variable alpha : T1.
Hypothesis Halpha : nf alpha.
Hypothesis HA : sorted_ge 0 A.
Hypothesis HB : sorted_ge 0 (B1 ++ B2).
Hypothesis HAB1 : ptwise_le B1 A.
Hypothesis HlargeA : largeS alpha A .
Remark R1 : gnawS alpha A = T1.zero.
Remark R2 : gnawS alpha B1 = T1.zero.
Lemma Lemma_4_5_2: gnawS alpha (B1 ++ B2) = zero.
End Proof_of_4_5_2.
Theorem Theorem_4_5 (alpha: T1)(Halpha : nf alpha)
(A B : list nat)
(HA : Sorted Peano.lt A)
(HB : Sorted Peano.lt B)
(HAB : incl A B) :
largeS alpha A → largeS alpha B.
Lemma gnaw_last_step alpha s i :
gnaw alpha s = 1 → gnaw alpha (s ++ S i :: nil) = 0.
For alpha in class E0
Definition LargeS (alpha : E0) s := largeS (@cnf alpha) s.
Definition Gnaw alpha s := gnaw (@cnf alpha) s.
Definition GnawS alpha s := gnawS (@cnf alpha) s.
Lemma Gnaw_GnawS s alpha :
GnawS alpha s = Gnaw alpha (shift s).
Lemma GnawS_Gnaw (s:list nat) :
∀ alpha, Gnaw alpha s = GnawS alpha (unshift s).
Lemma GnawS_omega : ∀ i s, GnawS E0_omega (i::s) = GnawS (E0finS i) s.
Lemma Gnaw_omega i s : Gnaw E0_omega (S i::s) = Gnaw (E0finS i) s.
Definition Largeb (alpha: E0) (s: list nat) :=
largeb (@cnf alpha) s.
Definition LargeSb (alpha: E0) (s: list nat) :=
largeSb (@cnf alpha) s.
Lemma LargeSb_b (alpha : E0) (s: list nat) :
LargeSb alpha s = Largeb alpha (List.map S s).
Lemma Largeb_Sb alpha s :
Largeb alpha s = LargeSb alpha (unshift s).
Lemma largeb_finite :
∀ n i, largeb (S n) (iota_from (S i) (S n)) = true.
Lemma largeb_n (n:nat): ∀ s, ¬ In 0 s →
large n s →
(n ≤ List.length s)%nat.
Lemma largeb_n_R : ∀ s n, ¬ In 0 s →
(n < List.length s)%nat →
largeb (S n) s = true.
Lemma large_n_iff : ∀ s (n:nat) , ¬ In 0 s →
large n s ↔ (n ≤ List.length s)%nat.
Example ex3 : ¬ large 156 (interval 100 254).
Gnawing omega omega-large intervals
Lemma gnaw_omega_n_SSn :
∀ n, gnaw T1omega (iota_from (S n) (S (S n))) = zero.
Lemma gnaw_omega_1 (n:nat) :
gnaw T1omega (interval (S n) (S n + n)%nat) = 1.
Example omega_ex1 : gnaw T1omega (interval 7 13) = 1.
Qed.
Example omega_ex2 : gnaw T1omega (interval 1000 1999) = 1.
Qed.
Lemma large_omega_1 : ∀ s n, ¬ In 0 (n::s) →
gnaw T1omega (n::s) = 0 →
(n ≤ List.length s)%nat.
Lemma large_omega_2 : ∀ s n, ¬In 0 (n::s) →
(n ≤ List.length s)%nat →
gnaw T1omega (n::s) = zero.
Lemma large_omega_iff : ∀ s n, ¬ In 0 (n::s) →
large T1omega (n::s) ↔
(n ≤ List.length s)%nat.