(* Proposition 8.14: the restoration bound for the threefold amplification. The rows of the layered map are unrolled
along a run, the first layer of each step reading the last layer of the step before through a device that writes
every copy of its cells with the values of the run. Under independent Gaussian perturbations of every
pre-activation of the threefold amplification, the probability that the state read by majority leaves the run
within T steps is at most the sum of the bounds b(t) that the recursion of the proposition computes along it.
The probability space is that of Noise.v, with P additive on the events built from the threshold events. *)
From Stdlib Require Import List Bool Arith ZArith Reals Lia Lra FunctionalExtensionality.
Import ListNotations.
Set Warnings "-ambiguous-paths".
From TH Require Import TwoHead Net Lev Margin Erfc Noise.
Set Warnings "ambiguous-paths".
Local Open Scope R_scope.
(* ---- counts and sums ------------------------------------------------------------------------------------------ *)
Lemma ncnt_pos : forall m f, (0 < ncnt m f)%nat -> exists k, (k < m)%nat /\ f k = true.
Proof.
induction m as [|m IH]; intros f H; cbn [ncnt] in H; [lia|].
destruct (f m) eqn:E; [exists m; split; [lia | exact E]|].
destruct (IH f ltac:(lia)) as (k & Hk & Hf). exists k. split; [lia | exact Hf].
Qed.
Lemma ncnt_false : forall k, ncnt k (fun _ => false) = 0%nat.
Proof. induction k as [|k IH]; cbn [ncnt]; [reflexivity | rewrite IH; reflexivity]. Qed.
Lemma ncnt_add : forall a b f, ncnt (a + b) f = (ncnt a f + ncnt b (fun k => f (a + k)%nat))%nat.
Proof.
intros a b f. induction b as [|b IH]; cbn [ncnt]; [rewrite Nat.add_0_r; lia|].
rewrite Nat.add_succ_r. cbn [ncnt]. rewrite IH. lia.
Qed.
Lemma ncnt_point : forall m f j, (j < m)%nat -> ncnt m (fun k => f k && Nat.eqb k j) = if f j then 1%nat else 0%nat.
Proof.
induction m as [|m IH]; intros f j Hj; [lia|]. cbn [ncnt].
destruct (Nat.eq_dec j m) as [->|E].
- rewrite Nat.eqb_refl, andb_true_r.
rewrite (ncnt_ext m _ (fun _ => false)) by (intros c Hc; destruct (Nat.eqb_spec c m); [lia | apply andb_false_r]).
rewrite ncnt_false. destruct (f m); reflexivity.
- rewrite IH by lia. destruct (Nat.eqb_spec m j); [lia|]. rewrite andb_false_r. destruct (f j); reflexivity.
Qed.
(* the positions c w + j, c < r, of one row j among r w positions *)
Lemma ncnt_row : forall r w j D, (j < w)%nat ->
ncnt (r * w) (fun q => D q && Nat.eqb (q mod w) j) = ncnt r (fun c => D (c * w + j)%nat).
Proof.
intros r w j D Hj. induction r as [|r IH]; [reflexivity|].
replace (S r * w)%nat with (r * w + w)%nat by lia. rewrite ncnt_add, IH. cbn [ncnt]. f_equal.
rewrite (ncnt_ext w _ (fun k => D (r * w + k)%nat && Nat.eqb k j)).
- exact (ncnt_point w (fun k => D (r * w + k)%nat) j Hj).
- intros k Hk. replace ((r * w + k) mod w)%nat with k; [reflexivity|].
rewrite Nat.add_comm, Nat.Div0.mod_add. symmetry. apply Nat.mod_small. exact Hk.
Qed.
Lemma ncnt_two : forall f, (2 <= ncnt 3 f)%nat -> exists c1 c2, (c1 < c2)%nat /\ (c2 < 3)%nat /\ f c1 = true /\ f c2 = true.
Proof.
intros f H. cbn [ncnt] in H. destruct (f 0%nat) eqn:E0, (f 1%nat) eqn:E1, (f 2%nat) eqn:E2; cbn [Nat.add] in H;
try lia; solve [exists 0%nat, 1%nat; auto | exists 0%nat, 2%nat; auto | exists 1%nat, 2%nat; auto].
Qed.
Lemma ncnt_three : forall f, ncnt 3 f = 3%nat -> f 0%nat = true /\ f 1%nat = true /\ f 2%nat = true.
Proof. intros f H. cbn [ncnt] in H. destruct (f 0%nat), (f 1%nat), (f 2%nat); cbn [Nat.add] in H; try lia; auto. Qed.
Lemma rsum_add : forall a b g, rsum (a + b) g = rsum a g + rsum b (fun k => g (a + k)%nat).
Proof.
intros a b g. induction b as [|b IH]; cbn [rsum]; [rewrite Nat.add_0_r; lra|].
rewrite Nat.add_succ_r. cbn [rsum]. rewrite IH. lra.
Qed.
Lemma rsum_blocks : forall T m g, rsum (T * m) g = rsum T (fun t => rsum m (fun l => g (t * m + l)%nat)).
Proof.
induction T as [|T IH]; intros m g; [cbn; lra|]. replace (S T * m)%nat with (T * m + m)%nat by lia.
rewrite rsum_add, IH. cbn [rsum]. reflexivity.
Qed.
(* the first index at which a test holds *)
Lemma first_true : forall (f : nat -> bool) a, f a = true ->
exists a0, (a0 <= a)%nat /\ f a0 = true /\ forall a', (a' < a0)%nat -> f a' = false.
Proof.
intros f a Ha. assert (Hd : forall k, f k = true \/ ~ f k = true) by (intro k; destruct (f k); [left | right]; congruence).
assert (G : forall m, (exists k, (k < m)%nat /\ f k = true) ->
exists a0, (a0 < m)%nat /\ f a0 = true /\ forall a', (a' < a0)%nat -> f a' = false).
{ induction m as [|m IH]; intros (k & Hk & Hf); [lia|].
destruct (search m (fun k => f k = true) Hd) as [H|H].
- destruct (IH H) as (a0 & H0 & H1 & H2). exists a0. split; [lia | split; assumption].
- exists m. split; [lia|]. split.
+ destruct (Nat.eq_dec k m) as [->|E]; [exact Hf | exfalso; exact (H k ltac:(lia) Hf)].
+ intros a' Ha'. destruct (f a') eqn:E; [exfalso; exact (H a' Ha' E) | reflexivity]. }
destruct (G (S a) (ex_intro _ a (conj (Nat.lt_succ_diag_r a) Ha))) as (a0 & H0 & H1 & H2).
exists a0. split; [lia | split; assumption].
Qed.
(* ---- the inputs that move a row toward its comparator -------------------------------------------------------- *)
(* the weight with which a row reads position j, 0 if it does not *)
Definition wgt (u : tu) (j : nat) : Z := fold_right (fun p a => if Nat.eqb (fst p) j then snd p else a) 0%Z (tin u).
Lemma wgt_in : forall u j z, NoDup (map fst (tin u)) -> In (j, z) (tin u) -> wgt u j = z.
Proof.
intros [b ins] j z. unfold wgt. cbn [tin]. induction ins as [|[j' z'] t IH]; intros Hnd Hin; [destruct Hin|].
cbn [fold_right fst snd]. cbn [map fst] in Hnd. inversion Hnd as [|? ? Hj Ht]; subst. destruct Hin as [E|Hin].
- injection E as -> ->. rewrite Nat.eqb_refl. reflexivity.
- destruct (Nat.eqb_spec j' j) as [->|E]; [|apply IH; assumption].
exfalso. apply Hj. apply in_map_iff. exists (j, z). split; [reflexivity | exact Hin].
Qed.
(* the sign of z + 1/2 for an integer z *)
Definition sgn (z : Z) : Z := if Z.leb 0 z then 1%Z else (-1)%Z.
(* an error at an input of weight wt and value y moves a row of pre-activation z toward the comparator, that is
wt (1 - 2 y) (z + 1/2) < 0 *)
Definition tw (z wt : Z) (y : bool) : bool := (sgn z * wt * (1 - 2 * b2z y) <? 0)%Z.
Lemma tw_paper : forall z wt y, tw z wt y = (wt * (1 - 2 * b2z y) * (2 * z + 1) <? 0)%Z.
Proof.
intros z wt y. unfold tw, sgn. rewrite <- Z.mul_assoc. generalize (wt * (1 - 2 * b2z y))%Z as x. intro x.
destruct (Z.leb_spec 0 z) as [H|H].
- rewrite Z.mul_1_l. destruct (Z.ltb_spec x 0), (Z.ltb_spec (x * (2 * z + 1)) 0); try reflexivity; exfalso; nia.
- destruct (Z.ltb_spec (-1 * x) 0), (Z.ltb_spec (x * (2 * z + 1)) 0); try reflexivity; exfalso; nia.
Qed.
Lemma in_arow : forall r w u q z, In (q, z) (tin (arow r w u)) ->
exists c j, (c < r)%nat /\ In (j, z) (tin u) /\ q = (c * w + j)%nat.
Proof.
intros r w u q z Hin. unfold arow in Hin. cbn [tin] in Hin. apply in_concat in Hin as (l & Hl & Hin).
apply in_map_iff in Hl as (c & <- & Hc). apply in_seq in Hc. apply in_map_iff in Hin as ([j z'] & E & Hj).
cbn [fst snd] in E. injection E as <- <-. exists c, j. split; [lia | split; [exact Hj | reflexivity]].
Qed.
(* the inputs that differ move a weighted sum by their weights; those that move it against the sign sg number at most
the count of the toward inputs that differ *)
Lemma wsum_dir : forall ins E1 E2 (sg : Z), (sg = 1 \/ sg = -1)%Z -> (forall j z, In (j, z) ins -> (z = 1 \/ z = -1)%Z) ->
(- Z.of_nat (length (filter (fun p => negb (Bool.eqb (E1 (fst p)) (E2 (fst p)))
&& (sg * snd p * (1 - 2 * b2z (E2 (fst p))) <? 0)%Z) ins))
<= sg * (wsum ins E1 - wsum ins E2))%Z.
Proof.
intros ins E1 E2 sg Hsg. induction ins as [|[j z] t IH]; intro Hw; cbn [wsum filter fst snd]; [lia|].
specialize (IH (fun j' z' H => Hw j' z' (or_intror H))).
destruct (negb (Bool.eqb (E1 j) (E2 j)) && (sg * z * (1 - 2 * b2z (E2 j)) <? 0)%Z) eqn:Hc; cbn [length];
rewrite ?Nat2Z.inj_succ; destruct (Hw j z (or_introl eq_refl)) as [-> | ->]; destruct Hsg as [-> | ->];
destruct (E1 j), (E2 j); cbn in Hc; try discriminate; cbn [b2z]; lia.
Qed.
(* a perturbation fails a copy of the threefold amplification of row u, whose input differs from rep 3 y in at most k
copies of inputs that move it toward the comparator, only beyond D - k on the far side, D = 3 |z + 1/2| *)
Definition far (z : Z) (k : nat) (e : R) : Prop :=
if Z.leb 0 z then e < - (3 * Rabs (IZR z + 1/2) - INR k) else 3 * Rabs (IZR z + 1/2) - INR k <= e.
Lemma far_core : forall u y y' e k, rowok (length y) u ->
(length (filter (fun p => negb (Bool.eqb (nth (fst p) y' false) (nth (fst p) (rep 3 y) false))
&& tw (pre u y) (snd p) (nth (fst p) (rep 3 y) false)) (tin (arow 3 (length y) u))) <= k)%nat ->
H12 (IZR (pre (arow 3 (length y) u) y') + e) <> Z.leb 0 (pre u y) -> far (pre u y) k e.
Proof.
intros u y y' e k Hu Hk Hw.
assert (Hr : reads_lt (length y) u) by (intros j z Hin; exact (proj1 (proj2 Hu j z Hin))).
destruct (arow_ok 3 _ _ Hu) as [_ Hlt].
pose proof (wsum_dir (tin (arow 3 (length y) u)) (fun i => nth i y' false) (fun i => nth i (rep 3 y) false) (sgn (pre u y))
ltac:(unfold sgn; destruct (Z.leb 0 (pre u y)); [left | right]; reflexivity)
(fun j z Hin => proj2 (Hlt j z Hin))) as D.
cbv beta in D. unfold tw in Hk. apply Nat2Z.inj_le in Hk.
pose proof (pre_arow 3 u y Hr) as Hp0.
replace (Z.of_nat 3 * pre u y + Z.of_nat ((3 - 1) / 2))%Z with (3 * pre u y + 1)%Z in Hp0 by reflexivity.
assert (Ed : (pre (arow 3 (length y) u) y' - pre (arow 3 (length y) u) (rep 3 y))%Z
= (wsum (tin (arow 3 (length y) u)) (fun i => nth i y' false)
- wsum (tin (arow 3 (length y) u)) (fun i => nth i (rep 3 y) false))%Z) by (unfold pre; ring).
rewrite Hp0 in Ed.
set (zv := pre u y) in *. set (p' := pre (arow 3 (length y) u) y') in *. unfold far, sgn in *.
destruct (Z.leb_spec 0 zv) as [Hz|Hz]; unfold H12 in Hw.
- destruct (Rle_dec (-1/2) (IZR p' + e)) as [Hle|Hlt']; [exfalso; apply Hw; reflexivity|].
assert (Hp : (3 * zv + 1 - Z.of_nat k <= p')%Z) by lia.
apply IZR_le in Hp. rewrite minus_IZR, plus_IZR, mult_IZR, <- INR_IZR_INZ in Hp. apply IZR_le in Hz.
rewrite Rabs_right by lra. apply Rnot_le_lt in Hlt'. lra.
- destruct (Rle_dec (-1/2) (IZR p' + e)) as [Hle|Hlt']; [|exfalso; apply Hw; reflexivity].
assert (Hp : (p' <= 3 * zv + 1 + Z.of_nat k)%Z) by lia.
apply IZR_le in Hp. rewrite !plus_IZR, mult_IZR, <- INR_IZR_INZ in Hp.
assert (Hz' : (zv <= -1)%Z) by lia. apply IZR_le in Hz'. rewrite Rabs_left by lra. lra.
Qed.
(* ---- layers evaluated in sequence --------------------------------------------------------------------------------- *)
Lemma lmapp_app : forall A L l0 E y, lmapp (A ++ [L]) l0 E y = lfirep L (E (l0 + length A)%nat) (lmapp A l0 E y).
Proof.
induction A as [|L' A IH]; intros L l0 E y; cbn [app lmapp length]; [rewrite Nat.add_0_r; reflexivity|].
rewrite IH. replace (S l0 + length A)%nat with (l0 + S (length A))%nat by lia. reflexivity.
Qed.
Lemma nth_lfirep : forall L e y q, (q < length L)%nat -> nth q (lfirep L e y) false = H12 (IZR (pre (nth q L tu0) y) + e q y).
Proof. intros L e y q Hq. unfold lfirep. rewrite nth_map_seq by exact Hq. reflexivity. Qed.
Lemma length_lfirep : forall L e y, length (lfirep L e y) = length L.
Proof. intros L e y. unfold lfirep. rewrite length_map, length_seq. reflexivity. Qed.
Lemma lin_S : forall Ls x l, (l < length Ls)%nat -> lin Ls x (S l) = lfire (nth l Ls []) (lin Ls x l).
Proof. intros Ls x l Hl. unfold lin. rewrite (firstn_snoc _ Ls l []) by exact Hl. apply lmap_app. Qed.
Lemma lfirep_ext : forall L e1 e2 y, (forall q y', e1 q y' = e2 q y') -> lfirep L e1 y = lfirep L e2 y.
Proof. intros L e1 e2 y H. unfold lfirep. apply map_ext. intro q. rewrite H. reflexivity. Qed.
(* copy c of row i of a layer of m rows is c m + i *)
Lemma cp_inj : forall c1 c2 i1 i2 m, (i1 < m)%nat -> (i2 < m)%nat -> (c1 * m + i1 = c2 * m + i2)%nat -> c1 = c2 /\ i1 = i2.
Proof.
intros c1 c2 i1 i2 m H1 H2 E.
assert (Q1 : c1 = ((c1 * m + i1) / m)%nat) by (apply (Nat.div_unique _ _ c1 i1 H1); lia).
assert (Q2 : c2 = ((c2 * m + i2) / m)%nat) by (apply (Nat.div_unique _ _ c2 i2 H2); lia).
assert (R1 : i1 = ((c1 * m + i1) mod m)%nat) by (apply (Nat.mod_unique _ _ c1 i1 H1); lia).
assert (R2 : i2 = ((c2 * m + i2) mod m)%nat) by (apply (Nat.mod_unique _ _ c2 i2 H2); lia).
rewrite E in Q1, R1. split; congruence.
Qed.
Lemma cp_mod : forall c i m, (i < m)%nat -> ((c * m + i) mod m = i)%nat.
Proof. intros c i m H. rewrite Nat.add_comm, Nat.Div0.mod_add. apply Nat.mod_small. exact H. Qed.
Lemma cp_split : forall q m, (0 < m)%nat -> q = (q / m * m + q mod m)%nat.
Proof. intros q m H. rewrite Nat.mul_comm. apply Nat.div_mod. lia. Qed.
Lemma existsb_seq_false : forall f m, existsb f (seq 0 m) = false -> forall q, (q < m)%nat -> f q = false.
Proof.
intros f m H q Hq. destruct (f q) eqn:E; [|reflexivity].
assert (C : existsb f (seq 0 m) = true) by (apply existsb_exists; exists q; split; [apply in_seq; lia | exact E]).
congruence.
Qed.
Lemma existsb_seq_true : forall f m, existsb f (seq 0 m) = true -> exists q, (q < m)%nat /\ f q = true.
Proof. intros f m H. apply existsb_exists in H as (q & Hq & E). apply in_seq in Hq. exists q. split; [lia | exact E]. Qed.
Lemma ncnt_ge1 : forall k f c, (c < k)%nat -> f c = true -> (0 < ncnt k f)%nat.
Proof.
induction k as [|k IH]; intros f c Hc Hf; [lia|]. cbn [ncnt].
destruct (Nat.eq_dec c k) as [->|E]; [rewrite Hf; lia|]. specialize (IH f c ltac:(lia) Hf). lia.
Qed.
(* sum over j1 <> j2 of p j1 p j2 is at most the product of the sums *)
Lemma sum_ne_le : forall m (T1 T2 : nat -> bool) (p : nat -> R), (forall j, 0 <= p j) ->
rsum m (fun j1 => rsum m (fun j2 => if T1 j1 && T2 j2 && negb (Nat.eqb j1 j2) then p j1 * p j2 else 0))
<= rsum m (fun j => if T1 j then p j else 0) * rsum m (fun j => if T2 j then p j else 0).
Proof.
intros m T1 T2 p Hp. rewrite Rmult_comm, <- rsum_scal. apply rsum_le. intros j1 Hj1.
rewrite Rmult_comm, <- rsum_scal. apply rsum_le. intros j2 Hj2.
pose proof (Hp j1). pose proof (Hp j2).
destruct (T1 j1), (T2 j2), (Nat.eqb j1 j2); cbn [andb negb]; nra.
Qed.
Section Restore.
(* ---- the run, unrolled layer by layer ------------------------------------------------------------------------------ *)
Variable Omega : Type.
Variable X : nat -> Omega -> R.
(* the layers of the map, its n state bits, the states xs t of the run and the device cells Dv *)
Variables (Ls : list (list tu)) (n : nat) (xs : nat -> list bool) (Dv : nat -> bool).
Hypothesis HL : lwf n Ls.
Hypothesis Hne : Ls <> [].
Hypothesis Hlast : length (last Ls []) = n.
Hypothesis Hxs : forall t, length (xs t) = n.
(* off the device cells the run takes the step of the map *)
Hypothesis Hstep : forall t j, (j < n)%nat -> Dv j = false -> nth j (xs (S t)) false = nth j (lmap Ls (xs t)) false.
(* the perturbation of copy q of layer a of the unrolled run is the variable vid a q *)
Variable vid : nat -> nat -> nat.
Lemma NL_pos : (0 < length Ls)%nat.
Proof. destruct (length Ls) eqn:E; [|lia]. apply length_zero_iff_nil in E. contradiction. Qed.
(* layer a of the unrolled run is layer lyr a of step stp a *)
Definition stp (a : nat) : nat := a / length Ls.
Definition lyr (a : nat) : nat := a mod length Ls.
Lemma lyr_lt : forall a, (lyr a < length Ls)%nat.
Proof. intro a. apply Nat.mod_upper_bound. pose proof NL_pos. lia. Qed.
Lemma a_decomp : forall a, a = (stp a * length Ls + lyr a)%nat.
Proof. intro a. unfold stp, lyr. pose proof NL_pos. rewrite Nat.mul_comm. apply Nat.div_mod. lia. Qed.
Lemma stp_lyr : forall t l, (l < length Ls)%nat -> stp (t * length Ls + l) = t /\ lyr (t * length Ls + l) = l.
Proof.
intros t l Hl. unfold stp, lyr. split.
- symmetry. apply (Nat.div_unique _ _ t l Hl). lia.
- symmetry. apply (Nat.mod_unique _ _ t l Hl). lia.
Qed.
Lemma lyr_succ : forall a, (lyr (S a) = 0 /\ lyr a = length Ls - 1 /\ stp (S a) = S (stp a))%nat
\/ (lyr (S a) = S (lyr a) /\ lyr (S a) <> 0 /\ stp (S a) = stp a)%nat.
Proof.
intro a. pose proof (lyr_lt a) as H. pose proof (a_decomp a) as Ea. pose proof NL_pos.
destruct (Nat.eq_dec (S (lyr a)) (length Ls)) as [E|E].
- left. assert (Es : S a = (S (stp a) * length Ls + 0)%nat) by lia.
destruct (stp_lyr (S (stp a)) 0 NL_pos) as [E1 E2]. rewrite <- Es in E1, E2. lia.
- right. assert (Es : S a = (stp a * length Ls + S (lyr a))%nat) by lia.
destruct (stp_lyr (stp a) (S (lyr a)) ltac:(lia)) as [E1 E2]. rewrite <- Es in E1, E2. lia.
Qed.
Definition lay (a : nat) : list tu := nth (lyr a) Ls [].
Definition nla (a : nat) : nat := length (lay a).
Definition wia (a : nat) : nat := win Ls n (lyr a).
(* the input and the output of layer a on the run, its row i, and the pre-activation of that row *)
Definition exin (a : nat) : list bool := lin Ls (xs (stp a)) (lyr a).
Definition exo (a : nat) : list bool := lfire (lay a) (exin a).
Definition rowa (a i : nat) : tu := nth i (lay a) tu0.
Definition zv (a i : nat) : Z := pre (rowa a i) (exin a).
(* T(v): the inputs j of row i whose error moves it toward the comparator *)
Definition tT (a i j : nat) : bool := tw (zv a i) (wgt (rowa a i) j) (nth j (exin a) false).
(* the device writes every copy of a device cell with its value in the run *)
Definition reset (x o : list bool) : list bool :=
map (fun k => if Dv (k mod n) then nth (k mod n) x false else nth k o false) (seq 0 (length o)).
(* the perturbations of step t: copy q of layer l reads the variable vid (t L + l) q *)
Definition Et (w : Omega) (t : nat) : nat -> nat -> list bool -> R := fun l q _ => X (vid (t * length Ls + l) q) w.
(* the perturbed run of the threefold amplification, from the replicated initial state *)
Fixpoint run3 (w : Omega) (t : nat) : list bool :=
match t with O => rep 3 (xs 0) | S t' => reset (xs (S t')) (lmapp (amap 3 n Ls) 0 (Et w t') (run3 w t')) end.
Definition pn (w : Omega) (t l : nat) : list bool := lmapp (firstn l (amap 3 n Ls)) 0 (Et w t) (run3 w t).
Definition inp (w : Omega) (a : nat) : list bool := pn w (stp a) (lyr a).
Definition out (w : Omega) (a : nat) : list bool := pn w (stp a) (S (lyr a)).
(* copy q of layer a is wrong, input copy q of layer a is wrong *)
Definition wb (w : Omega) (a q : nat) : bool := negb (Bool.eqb (nth q (out w a) false) (nth (q mod nla a) (exo a) false)).
Definition wib (w : Omega) (a q : nat) : bool := negb (Bool.eqb (nth q (inp w a) false) (nth (q mod wia a) (exin a) false)).
(* |S_v|: the wrong copies of the inputs of row i that move it toward the comparator *)
Definition Sc (w : Omega) (a i : nat) : nat := ncnt (3 * wia a) (fun q => wib w a q && tT a i (q mod wia a)).
(* the wrong copies of row i, and of input j *)
Definition ncw (w : Omega) (a i : nat) : nat := ncnt 3 (fun c => wb w a (c * nla a + i)).
Definition nci (w : Omega) (a j : nat) : nat := ncnt 3 (fun c => wib w a (c * wia a + j)).
Lemma out_eq : forall w a, out w a = lfirep (alayer 3 (wia a) (lay a)) (fun q _ => X (vid a q) w) (inp w a).
Proof.
intros w a. unfold out, inp, pn. pose proof (lyr_lt a) as Hl.
rewrite (firstn_snoc _ (amap 3 n Ls) (lyr a) []) by (rewrite length_amap; exact Hl).
rewrite lmapp_app, length_firstn, length_amap, Nat.min_l by lia. rewrite nth_amap by exact Hl.
unfold Et. cbn [Nat.add]. rewrite <- (a_decomp a). reflexivity.
Qed.
Lemma inp_0 : forall w, inp w 0 = rep 3 (xs 0).
Proof. intro w. unfold inp, pn, stp, lyr. rewrite Nat.Div0.div_0_l, Nat.Div0.mod_0_l. reflexivity. Qed.
Lemma inp_S : forall w a, lyr (S a) <> 0%nat -> inp w (S a) = out w a.
Proof.
intros w a H. destruct (lyr_succ a) as [(E & _)|(E1 & _ & E2)]; [contradiction|].
unfold inp, out. rewrite E1, E2. reflexivity.
Qed.
Lemma inp_B : forall w a, lyr (S a) = 0%nat -> inp w (S a) = reset (xs (S (stp a))) (out w a).
Proof.
intros w a H. destruct (lyr_succ a) as [(_ & E1 & E2)|(_ & E & _)]; [|contradiction].
unfold inp, out. rewrite H, E2, E1. unfold pn. rewrite firstn_0. cbn [lmapp run3].
replace (S (length Ls - 1)) with (length Ls) by (pose proof NL_pos; lia).
rewrite firstn_all2 by (rewrite length_amap; lia). reflexivity.
Qed.
Lemma exin_0 : exin 0 = xs 0.
Proof. unfold exin, stp, lyr. rewrite Nat.Div0.div_0_l, Nat.Div0.mod_0_l. reflexivity. Qed.
Lemma exin_S : forall a, lyr (S a) <> 0%nat -> exin (S a) = exo a.
Proof.
intros a H. destruct (lyr_succ a) as [(E & _)|(E1 & _ & E2)]; [contradiction|].
unfold exin, exo, lay. rewrite E1, E2. apply lin_S. apply lyr_lt.
Qed.
Lemma exin_B : forall a, lyr (S a) = 0%nat -> exin (S a) = xs (S (stp a)) /\ exo a = lmap Ls (xs (stp a)).
Proof.
intros a H. destruct (lyr_succ a) as [(_ & E1 & E2)|(_ & E & _)]; [|contradiction]. split.
- unfold exin. rewrite H, E2. reflexivity.
- unfold exo, lay, exin. rewrite E1. rewrite <- lin_S by (pose proof NL_pos; lia).
replace (S (length Ls - 1)) with (length Ls) by (pose proof NL_pos; lia). unfold lin. rewrite firstn_all. reflexivity.
Qed.
Lemma wia_0 : wia 0 = n.
Proof. unfold wia, lyr. rewrite Nat.Div0.mod_0_l. reflexivity. Qed.
Lemma wia_S : forall a, lyr (S a) <> 0%nat -> wia (S a) = nla a.
Proof.
intros a H. destruct (lyr_succ a) as [(E & _)|(E1 & _ & _)]; [contradiction|]. unfold wia, nla, lay. rewrite E1. reflexivity.
Qed.
Lemma wia_B : forall a, lyr (S a) = 0%nat -> wia (S a) = n /\ nla a = n.
Proof.
intros a H. destruct (lyr_succ a) as [(_ & E1 & _)|(_ & E & _)]; [|contradiction]. split.
- unfold wia. rewrite H. reflexivity.
- unfold nla, lay. rewrite E1, <- (last_nth' _ Ls [] Hne). exact Hlast.
Qed.
Lemma len_exin : forall a, length (exin a) = wia a.
Proof. intro a. unfold exin, wia. rewrite lin_len' by (pose proof (lyr_lt a); lia). rewrite Hxs. reflexivity. Qed.
Lemma len_exo : forall a, length (exo a) = nla a.
Proof. intro a. unfold exo, lfire. rewrite length_map. reflexivity. Qed.
Lemma len_out : forall w a, length (out w a) = (3 * nla a)%nat.
Proof. intros w a. rewrite out_eq, length_lfirep, length_alayer. reflexivity. Qed.
Lemma len_reset : forall x o, length (reset x o) = length o.
Proof. intros x o. unfold reset. rewrite length_map, length_seq. reflexivity. Qed.
Lemma len_inp : forall w a, length (inp w a) = (3 * wia a)%nat.
Proof.
intros w [|a].
- rewrite inp_0, wia_0, length_rep, Hxs. reflexivity.
- destruct (Nat.eq_dec (lyr (S a)) 0) as [H|H].
+ rewrite inp_B, len_reset, len_out by exact H. destruct (wia_B a H) as [-> ->]. reflexivity.
+ rewrite inp_S, len_out, wia_S by exact H. reflexivity.
Qed.
Lemma nth_reset : forall x o q, (q < length o)%nat ->
nth q (reset x o) false = if Dv (q mod n) then nth (q mod n) x false else nth q o false.
Proof. intros x o q Hq. unfold reset. rewrite nth_map_seq by exact Hq. reflexivity. Qed.
(* the inputs of step 0 are exact; inside a step the inputs of a layer are the outputs of the layer before; between
steps the device cells are exact and the other state bits are the outputs of the last layer *)
Lemma wib_0 : forall w q, (q < 3 * n)%nat -> wib w 0 q = false.
Proof.
intros w q Hq. unfold wib. rewrite inp_0, exin_0, wia_0. rewrite nth_rep_mod by (rewrite Hxs; exact Hq).
rewrite Hxs, Bool.eqb_reflx. reflexivity.
Qed.
Lemma wib_S : forall w a q, lyr (S a) <> 0%nat -> wib w (S a) q = wb w a q.
Proof. intros w a q H. unfold wib, wb. rewrite inp_S, exin_S, wia_S by exact H. reflexivity. Qed.
Lemma wib_B : forall w a q, lyr (S a) = 0%nat -> (q < 3 * n)%nat ->
wib w (S a) q = if Dv (q mod n) then false else wb w a q.
Proof.
intros w a q H Hq. destruct (exin_B a H) as [E1 E2]. destruct (wia_B a H) as [W1 W2].
unfold wib, wb. rewrite inp_B by exact H. rewrite E1, W1. rewrite nth_reset by (rewrite len_out, W2; exact Hq).
assert (Hj : (q mod n < n)%nat) by (apply Nat.mod_upper_bound; lia).
destruct (Dv (q mod n)) eqn:Ed.
- rewrite Bool.eqb_reflx. reflexivity.
- rewrite E2, W2, (Hstep (stp a) (q mod n) Hj Ed). reflexivity.
Qed.
Lemma rowa_ok : forall a i, (i < nla a)%nat -> rowok (wia a) (rowa a i).
Proof. intros a i Hi. exact (urow_ok Ls n HL (lyr a) i (lyr_lt a) Hi). Qed.
Lemma exo_nth : forall a i, (i < nla a)%nat -> nth i (exo a) false = Z.leb 0 (zv a i).
Proof. intros a i Hi. unfold exo. rewrite lfire_nth by exact Hi. reflexivity. Qed.
(* a wrong copy of row i is a perturbation beyond D - |S_v| on the far side *)
Lemma wrong_far : forall w a q, (q < 3 * nla a)%nat -> wb w a q = true ->
far (zv a (q mod nla a)) (Sc w a (q mod nla a)) (X (vid a q) w).
Proof.
intros w a q Hq Hw. assert (Hn0 : nla a <> 0%nat) by lia.
set (i := (q mod nla a)%nat). assert (Hi : (i < nla a)%nat) by (apply Nat.mod_upper_bound; exact Hn0).
pose proof (rowa_ok a i Hi) as Hu. set (u := rowa a i) in *.
unfold zv. fold u. rewrite <- len_exin in Hu. apply (far_core u (exin a) (inp w a)); [exact Hu | |].
- rewrite len_exin in Hu |- *. destruct (arow_ok 3 _ _ Hu) as [Hnd Hlt].
assert (E : forall p, In p (tin (arow 3 (wia a) u)) ->
(negb (Bool.eqb (nth (fst p) (inp w a) false) (nth (fst p) (rep 3 (exin a)) false))
&& tw (pre u (exin a)) (snd p) (nth (fst p) (rep 3 (exin a)) false))
= (wib w a (fst p) && tT a i (fst p mod wia a))).
{ intros [q' z] Hin. cbn [fst snd]. destruct (in_arow _ _ _ _ _ Hin) as (c & j & Hc & Hj & ->).
destruct Hu as [Hnd' Hl']. destruct (Hl' j z Hj) as [Hjw _].
assert (Hm : ((c * wia a + j) mod wia a = j)%nat)
by (rewrite Nat.add_comm, Nat.Div0.mod_add; apply Nat.mod_small; exact Hjw).
assert (Hr : nth (c * wia a + j) (rep 3 (exin a)) false = nth j (exin a) false).
{ rewrite <- len_exin. apply nth_rep; [exact Hc | rewrite len_exin; exact Hjw]. }
unfold wib, tT. fold u. rewrite Hm, Hr, (wgt_in u j z Hnd' Hj). reflexivity. }
rewrite (filter_ext_in _ _ _ E). unfold Sc.
exact (filter_pos_le (tin (arow 3 (wia a) u)) (fun q => wib w a q && tT a i (q mod wia a)) (3 * wia a) Hnd
(fun j z Hin => proj1 (Hlt j z Hin))).
- rewrite len_exin. intro E. unfold wb in Hw. rewrite out_eq in Hw.
rewrite nth_lfirep in Hw by (rewrite length_alayer; exact Hq).
rewrite nth_alayer in Hw by exact Hq. fold (nla a) in Hw. fold i in Hw. fold (rowa a i) in Hw. fold u in Hw.
rewrite exo_nth in Hw by exact Hi. fold i u in Hw. unfold zv in Hw. fold u in Hw. rewrite E, Bool.eqb_reflx in Hw.
discriminate.
Qed.
(* ---- stops ----------------------------------------------------------------------------------------------------------- *)
(* a layer is a stop when a wrong copy of one of its rows has |S_v| >= 2, or when it is the last layer of a step and one
of its rows has two wrong copies *)
Definition stop1 (w : Omega) (a : nat) : bool :=
existsb (fun q => wb w a q && Nat.leb 2 (Sc w a (q mod nla a))) (seq 0 (3 * nla a)).
Definition stop2 (w : Omega) (a : nat) : bool :=
Nat.eqb (lyr a) (length Ls - 1) && existsb (fun i => Nat.leb 2 (ncw w a i)) (seq 0 (nla a)).
Definition stopb (w : Omega) (a : nat) : bool := stop1 w a || stop2 w a.
(* no stop up to layer a, no stop before layer a *)
Definition Gu (a : nat) (w : Omega) : Prop := forall a', (a' <= a)%nat -> stopb w a' = false.
Definition Gb (a : nat) (w : Omega) : Prop := forall a', (a' < a)%nat -> stopb w a' = false.
(* W_v: row i of layer a has a wrong copy and no layer up to a is a stop; the same for input j of layer a *)
Definition Wv (a i : nat) (w : Omega) : Prop := (0 < ncw w a i)%nat /\ Gu a w.
Definition Win (a j : nat) (w : Omega) : Prop := (0 < nci w a j)%nat /\ Gb a w.
(* no layer before a is a stop, |S_v| <= 1, and row i has two wrong copies, or three *)
Definition E2 (a i : nat) (w : Omega) : Prop := Gb a w /\ (Sc w a i <= 1)%nat /\ (2 <= ncw w a i)%nat.
Definition E3 (a i : nat) (w : Omega) : Prop := Gb a w /\ (Sc w a i <= 1)%nat /\ ncw w a i = 3%nat.
Lemma Gu_Gb : forall a w, Gu a w <-> Gb (S a) w.
Proof. intros a w. unfold Gu, Gb. split; intros H a' Ha'; apply H; lia. Qed.
(* where no stop lies, a wrong copy has |S_v| <= 1, and in the last layer of a step no row has two wrong copies *)
Lemma nostop_Sc : forall w a q, stopb w a = false -> (q < 3 * nla a)%nat -> wb w a q = true -> (Sc w a (q mod nla a) <= 1)%nat.
Proof.
intros w a q H Hq Hw. apply orb_false_iff in H as [H1 _]. pose proof (existsb_seq_false _ _ H1 q Hq) as E.
cbv beta in E. rewrite Hw in E. cbn [andb] in E. apply Nat.leb_gt in E. lia.
Qed.
Lemma nostop_ncw : forall w a i, stopb w a = false -> lyr a = (length Ls - 1)%nat -> (i < nla a)%nat -> (ncw w a i <= 1)%nat.
Proof.
intros w a i H Hl Hi. apply orb_false_iff in H as [_ H2]. unfold stop2 in H2. rewrite Hl, Nat.eqb_refl in H2.
cbn [andb] in H2. pose proof (existsb_seq_false _ _ H2 i Hi) as E. cbv beta in E. apply Nat.leb_gt in E. lia.
Qed.
Lemma ncw_copy : forall w a i, (0 < ncw w a i)%nat -> exists c, (c < 3)%nat /\ wb w a (c * nla a + i) = true.
Proof. intros w a i H. apply ncnt_pos in H as (c & Hc & E). exists c. split; assumption. Qed.
(* |S_v| >= 1 gives an input j in T(v) with a wrong copy *)
Lemma Sc_pos : forall w a i, (0 < Sc w a i)%nat -> exists j, (j < wia a)%nat /\ tT a i j = true /\ (0 < nci w a j)%nat.
Proof.
intros w a i H. apply ncnt_pos in H as (q & Hq & E). apply andb_prop in E as [E1 E2].
assert (Hw : (0 < wia a)%nat) by lia. exists (q mod wia a). split; [apply Nat.mod_upper_bound; lia|]. split; [exact E2|].
apply (ncnt_ge1 3 _ (q / wia a)); [apply Nat.Div0.div_lt_upper_bound; lia|].
rewrite <- (cp_split q (wia a) Hw). exact E1.
Qed.
(* |S_v| >= 2: two distinct inputs in T(v) with wrong copies, or all of them copies of one input j, |S_v| its wrong
copies *)
Lemma Sc_two : forall w a i, (2 <= Sc w a i)%nat ->
(exists j1 j2, (j1 < j2)%nat /\ (j2 < wia a)%nat /\ tT a i j1 = true /\ tT a i j2 = true /\ (0 < nci w a j1)%nat /\ (0 < nci w a j2)%nat)
\/ (exists j, (j < wia a)%nat /\ tT a i j = true /\ Sc w a i = nci w a j).
Proof.
intros w a i H. assert (Hw : (0 < wia a)%nat) by (unfold Sc in H; destruct (wia a); [cbn in H; lia | lia]).
destruct (ncnt_pos (3 * wia a) (fun q => wib w a q && tT a i (q mod wia a)) ltac:(unfold Sc in H; lia)) as (q1 & Hq1 & E1).
set (j := (q1 mod wia a)%nat). apply andb_prop in E1 as [W1 T1].
assert (Hj : (j < wia a)%nat) by (apply Nat.mod_upper_bound; lia).
assert (N1 : (0 < nci w a j)%nat).
{ apply (ncnt_ge1 3 _ (q1 / wia a)); [apply Nat.Div0.div_lt_upper_bound; lia|]. cbv beta. unfold j.
rewrite <- (cp_split q1 (wia a) Hw). exact W1. }
destruct (search (3 * wia a) (fun q => wib w a q && tT a i (q mod wia a) && negb (Nat.eqb (q mod wia a) j) = true))
as [(q2 & Hq2 & E2)|Hn].
- intro q. destruct (wib w a q && tT a i (q mod wia a) && negb (Nat.eqb (q mod wia a) j)); [left | right]; congruence.
- left. apply andb_prop in E2 as [E2 Ne]. apply andb_prop in E2 as [W2 T2]. apply negb_true_iff, Nat.eqb_neq in Ne.
assert (Hj2 : (q2 mod wia a < wia a)%nat) by (apply Nat.mod_upper_bound; lia).
assert (N2 : (0 < nci w a (q2 mod wia a))%nat).
{ apply (ncnt_ge1 3 _ (q2 / wia a)); [apply Nat.Div0.div_lt_upper_bound; lia|]. rewrite <- (cp_split q2 (wia a) Hw). exact W2. }
destruct (Nat.lt_ge_cases j (q2 mod wia a)) as [L|L].
+ exists j, (q2 mod wia a). repeat split; assumption.
+ exists (q2 mod wia a), j. repeat split; try assumption; lia.
- right. exists j. split; [exact Hj|]. split; [exact T1|]. unfold Sc, nci.
rewrite (ncnt_ext (3 * wia a) _ (fun q => wib w a q && Nat.eqb (q mod wia a) j)).
+ apply ncnt_row. exact Hj.
+ intros q Hq. specialize (Hn q Hq). destruct (wib w a q) eqn:Wq; [|reflexivity]. cbn [andb] in Hn |- *.
destruct (Nat.eqb_spec (q mod wia a) j) as [Eq|Eq].
* rewrite Eq. exact T1.
* destruct (tT a i (q mod wia a)); [exfalso; apply Hn; reflexivity | reflexivity].
Qed.
(* ---- the probability space ---------------------------------------------------------------------------------- *)
Variable P : (Omega -> Prop) -> R.
Hypothesis P_mono : forall A B : Omega -> Prop, (forall w, A w -> B w) -> P A <= P B.
Hypothesis P_or : forall A B : Omega -> Prop, P (fun w => A w \/ B w) <= P A + P B.
Hypothesis P_empty : P (fun _ => False) = 0.
Hypothesis P_true : P (fun _ => True) = 1.
Hypothesis P_indep : forall (I J : nat -> Prop) (A B : Omega -> Prop), (forall g, I g -> J g -> False) ->
dep Omega X I A -> dep Omega X J B -> P (fun w => A w /\ B w) = P A * P B.
(* P adds on disjoint events built from the threshold events *)
Hypothesis P_add : forall A B, meas Omega X A -> meas Omega X B -> (forall w, A w -> B w -> False) ->
P (fun w => A w \/ B w) = P A + P B.
Variable s : R.
Hypothesis Hs : 0 < s.
Hypothesis tail_ge : forall g c, P (fun w => c <= X g w) = Q (c / s).
Hypothesis tail_le : forall g c, P (fun w => X g w <= c) = Q (- c / s).
Hypothesis vid_inj : forall a q a' q', vid a q = vid a' q' -> a = a' /\ q = q'.
Lemma Pex : forall m (A : nat -> Omega -> Prop), P (fun w => exists k, (k < m)%nat /\ A k w) <= rsum m (fun k => P (A k)).
Proof. exact (P_exists Omega P P_mono P_or P_empty). Qed.
Lemma Pnn : forall A, 0 <= P A.
Proof. exact (P_nonneg Omega P P_mono P_empty). Qed.
Lemma Ple1 : forall A, P A <= 1.
Proof. exact (P_le1 Omega P P_mono P_true). Qed.
Lemma Pnone : forall A : Omega -> Prop, (forall w, ~ A w) -> P A = 0.
Proof. intros A H. apply Rle_antisym; [rewrite <- P_empty; apply P_mono; intros w Hw; exact (H w Hw) | apply Pnn]. Qed.
Lemma P_or3 : forall A B C : Omega -> Prop, P (fun w => A w \/ B w \/ C w) <= P A + P B + P C.
Proof. intros A B C. eapply Rle_trans; [apply P_or|]. pose proof (P_or B C). lra. Qed.
(* the union bound over the j < m that pass a test T *)
Lemma P_sum : forall m (T : nat -> bool) (A : nat -> Omega -> Prop) (b : nat -> R),
(forall j, (j < m)%nat -> T j = true -> P (A j) <= b j) ->
P (fun w => exists j, (j < m)%nat /\ T j = true /\ A j w) <= rsum m (fun j => if T j then b j else 0).
Proof.
intros m T A b H. eapply Rle_trans; [apply (Pex m (fun j w => T j = true /\ A j w))|]. apply rsum_le. intros j Hj.
destruct (T j) eqn:E.
- eapply Rle_trans; [|apply (H j Hj E)]. apply P_mono. intros w [_ Hw]. exact Hw.
- right. apply Pnone. intros w [C _]. discriminate.
Qed.
(* events on distinct variables are independent *)
Lemma P_ind2 : forall g1 g2 (A B : R -> Prop), g1 <> g2 ->
P (fun w => A (X g1 w) /\ B (X g2 w)) = P (fun w => A (X g1 w)) * P (fun w => B (X g2 w)).
Proof.
intros g1 g2 A B Hg. apply (P_indep (fun g => g = g1) (fun g => g = g2)).
- intros g -> E. exact (Hg E).
- intros w w' H. rewrite (H g1 eq_refl). reflexivity.
- intros w w' H. rewrite (H g2 eq_refl). reflexivity.
Qed.
Lemma P_ind3 : forall g1 g2 g3 (A B C : R -> Prop), g1 <> g2 -> g1 <> g3 -> g2 <> g3 ->
P (fun w => A (X g1 w) /\ B (X g2 w) /\ C (X g3 w))
= P (fun w => A (X g1 w)) * P (fun w => B (X g2 w)) * P (fun w => C (X g3 w)).
Proof.
intros g1 g2 g3 A B C H12 H13 H23.
rewrite (P_indep (fun g => g = g1) (fun g => g = g2 \/ g = g3) (fun w => A (X g1 w)) (fun w => B (X g2 w) /\ C (X g3 w))).
- rewrite P_ind2 by exact H23. ring.
- intros g -> [E|E]; [exact (H12 E) | exact (H13 E)].
- intros w w' H. rewrite (H g1 eq_refl). reflexivity.
- intros w w' H. rewrite (H g2 (or_introl eq_refl)), (H g3 (or_intror eq_refl)). reflexivity.
Qed.
(* unions over the three copies of a row, and over pairs of copies *)
Lemma P_copies : forall (g : nat -> nat) (A : R -> Prop) p, (forall c, (c < 3)%nat -> P (fun w => A (X (g c) w)) <= p) ->
P (fun w => exists c, (c < 3)%nat /\ A (X (g c) w)) <= 3 * p.
Proof.
intros g A p H. eapply Rle_trans; [apply (Pex 3 (fun c w => A (X (g c) w)))|].
cbn [rsum]. pose proof (H 0%nat ltac:(lia)). pose proof (H 1%nat ltac:(lia)). pose proof (H 2%nat ltac:(lia)). lra.
Qed.
Lemma P_copy_pairs : forall (g1 g2 : nat -> nat) (A B : R -> Prop) pA pB,
(forall c1 c2, (c1 < 3)%nat -> (c2 < 3)%nat -> g1 c1 <> g2 c2) ->
(forall c, (c < 3)%nat -> P (fun w => A (X (g1 c) w)) <= pA) -> (forall c, (c < 3)%nat -> P (fun w => B (X (g2 c) w)) <= pB) ->
P (fun w => exists c1, (c1 < 3)%nat /\ exists c2, (c2 < 3)%nat /\ A (X (g1 c1) w) /\ B (X (g2 c2) w)) <= 9 * pA * pB.
Proof.
intros g1 g2 A B pA pB Hg HA HB.
eapply Rle_trans; [apply (Pex 3 (fun c1 w => exists c2, (c2 < 3)%nat /\ A (X (g1 c1) w) /\ B (X (g2 c2) w)))|].
assert (Hc : forall c1, (c1 < 3)%nat ->
P (fun w => exists c2, (c2 < 3)%nat /\ A (X (g1 c1) w) /\ B (X (g2 c2) w)) <= 3 * (pA * pB)).
{ intros c1 Hc1. eapply Rle_trans; [apply (Pex 3 (fun c2 w => A (X (g1 c1) w) /\ B (X (g2 c2) w)))|].
assert (Hp : forall c2, (c2 < 3)%nat -> P (fun w => A (X (g1 c1) w) /\ B (X (g2 c2) w)) <= pA * pB).
{ intros c2 Hc2. rewrite P_ind2 by (apply Hg; assumption).
apply Rmult_le_compat; [apply Pnn | apply Pnn | apply HA; exact Hc1 | apply HB; exact Hc2]. }
cbn [rsum]. pose proof (Hp 0%nat ltac:(lia)). pose proof (Hp 1%nat ltac:(lia)). pose proof (Hp 2%nat ltac:(lia)). lra. }
cbn [rsum]. pose proof (Hc 0%nat ltac:(lia)). pose proof (Hc 1%nat ltac:(lia)). pose proof (Hc 2%nat ltac:(lia)). lra.
Qed.
Lemma P_copy_lt : forall (g : nat -> nat) (A B : R -> Prop) pA pB, (forall c1 c2, (c1 < 3)%nat -> (c2 < 3)%nat -> c1 <> c2 -> g c1 <> g c2) ->
(forall c, (c < 3)%nat -> P (fun w => A (X (g c) w)) <= pA) -> (forall c, (c < 3)%nat -> P (fun w => B (X (g c) w)) <= pB) ->
P (fun w => exists c1 c2, (c1 < c2)%nat /\ (c2 < 3)%nat /\ A (X (g c1) w) /\ B (X (g c2) w)) <= 3 * pA * pB.
Proof.
intros g A B pA pB Hg HA HB.
eapply Rle_trans; [apply (P_mono _ (fun w => (A (X (g 0%nat) w) /\ B (X (g 1%nat) w)) \/ (A (X (g 0%nat) w) /\ B (X (g 2%nat) w))
\/ (A (X (g 1%nat) w) /\ B (X (g 2%nat) w))))|].
- intros w (c1 & c2 & H1 & H2 & Ha & Hb).
destruct c1 as [|[|c1]]; destruct c2 as [|[|[|c2]]]; try lia; auto.
- eapply Rle_trans; [apply P_or3|].
assert (Hp : forall c1 c2, (c1 < 3)%nat -> (c2 < 3)%nat -> c1 <> c2 -> P (fun w => A (X (g c1) w) /\ B (X (g c2) w)) <= pA * pB).
{ intros c1 c2 H1 H2 H12. rewrite P_ind2 by (apply Hg; assumption).
apply Rmult_le_compat; [apply Pnn | apply Pnn | apply HA; exact H1 | apply HB; exact H2]. }
pose proof (Hp 0%nat 1%nat ltac:(lia) ltac:(lia) ltac:(lia)). pose proof (Hp 0%nat 2%nat ltac:(lia) ltac:(lia) ltac:(lia)).
pose proof (Hp 1%nat 2%nat ltac:(lia) ltac:(lia) ltac:(lia)). lra.
Qed.
(* ---- the perturbation that fails a copy ------------------------------------------------------------------------ *)
(* q_k(v) = Q((D_v - k)/s) and Delta_v = q_1(v) - q_0(v) *)
Definition qk (a i k : nat) : R := Q ((3 * Rabs (IZR (zv a i) + 1/2) - INR k) / s).
Definition dl (a i : nat) : R := qk a i 1 - qk a i 0.
Lemma qk_range : forall a i k, 0 <= qk a i k <= 1.
Proof. intros. apply Q_range. Qed.
Lemma qk_mono : forall a i k k', (k <= k')%nat -> qk a i k <= qk a i k'.
Proof.
intros a i k k' H. unfold qk. apply Q_decr. apply le_INR in H. unfold Rdiv.
apply Rmult_le_compat_r; [apply Rlt_le, Rinv_0_lt_compat; exact Hs | lra].
Qed.
Lemma dl_nn : forall a i, 0 <= dl a i.
Proof. intros a i. unfold dl. pose proof (qk_mono a i 0 1 ltac:(lia)). lra. Qed.
Lemma far_dec : forall z k e, far z k e \/ ~ far z k e.
Proof.
intros z k e. unfold far. destruct (Z.leb 0 z).
- destruct (Rlt_dec e (- (3 * Rabs (IZR z + 1/2) - INR k))); [left | right]; assumption.
- destruct (Rle_dec (3 * Rabs (IZR z + 1/2) - INR k) e); [left | right]; assumption.
Qed.
Lemma far_mono : forall z k k' e, (k <= k')%nat -> far z k e -> far z k' e.
Proof. intros z k k' e H. apply le_INR in H. unfold far. destruct (Z.leb 0 z); lra. Qed.
Lemma P_far : forall a i k g, P (fun w => far (zv a i) k (X g w)) <= qk a i k.
Proof.
intros a i k g. unfold far, qk. set (D := 3 * Rabs (IZR (zv a i) + 1/2)). destruct (Z.leb 0 (zv a i)).
- eapply Rle_trans; [apply (P_mono _ (fun w => X g w <= - (D - INR k))); intros w H; lra|].
rewrite tail_le. right. f_equal. field. lra.
- rewrite tail_ge. right. reflexivity.
Qed.
Lemma P_band : forall g c1 c0, c1 <= c0 -> P (fun w => c1 <= X g w /\ ~ c0 <= X g w) = Q (c1 / s) - Q (c0 / s).
Proof.
intros g c1 c0 H.
assert (E : P (fun w => c1 <= X g w) = P (fun w => c0 <= X g w) + P (fun w => c1 <= X g w /\ ~ c0 <= X g w)).
{ rewrite <- P_add.
- apply (P_ext Omega P P_mono). intro w. split.
+ intro H1. destruct (Rle_dec c0 (X g w)) as [H0|H0]; [left; exact H0 | right; split; assumption].
+ intros [H0|[H1 _]]; [lra | exact H1].
- apply meas_ge.
- apply meas_and; [apply meas_ge | apply meas_not, meas_ge].
- intros w H0 [_ H1]. exact (H1 H0). }
rewrite !tail_ge in E. lra.
Qed.
Lemma P_far10 : forall a i g, P (fun w => far (zv a i) 1 (X g w) /\ ~ far (zv a i) 0 (X g w)) <= dl a i.
Proof.
intros a i g. unfold far, dl, qk. set (D := 3 * Rabs (IZR (zv a i) + 1/2)). cbn [INR]. destruct (Z.leb 0 (zv a i)).
- rewrite (P_ext Omega P P_mono _ (fun w => - D <= X g w /\ ~ - (D - 1) <= X g w)).
+ rewrite P_band by lra. replace (- D / s) with (- (D / s)) by (field; lra).
replace (- (D - 1) / s) with (- ((D - 1) / s)) by (field; lra). rewrite !Q_sym. replace (D - 0) with D by ring. lra.
+ intro w. split; intros [H1 H2]; (split; [lra | intro; lra]).
- rewrite (P_ext Omega P P_mono _ (fun w => D - 1 <= X g w /\ ~ D <= X g w)).
+ rewrite P_band by lra. replace (D - 0) with D by ring. lra.
+ intro w. split; intros [H1 H2]; (split; [lra | intro; lra]).
Qed.
(* ---- what the events depend on --------------------------------------------------------------------------------- *)
(* the variables of the layers before a, and of layer a *)
Definition pastv (a g : nat) : Prop := exists a' q, (a' < a)%nat /\ g = vid a' q.
Definition nowv (a g : nat) : Prop := exists q, g = vid a q.
Lemma past_now : forall a g, pastv a g -> nowv a g -> False.
Proof. intros a g (a' & q & Ha & ->) (q' & E). apply vid_inj in E as [E _]. lia. Qed.
Lemma P_pn : forall a (A B : Omega -> Prop), dep Omega X (pastv a) A -> dep Omega X (nowv a) B ->
P (fun w => A w /\ B w) = P A * P B.
Proof. intros a A B HA HB. apply (P_indep (pastv a) (nowv a)); [exact (past_now a) | exact HA | exact HB]. Qed.
Lemma dep_now : forall a (F : (nat -> R) -> Prop), dep Omega X (nowv a) (fun w => F (fun q => X (vid a q) w)).
Proof.
intros a F w w' H. replace (fun q => X (vid a q) w') with (fun q => X (vid a q) w); [reflexivity|].
apply functional_extensionality. intro q. apply H. exists q. reflexivity.
Qed.
Lemma dep_and : forall I (A B : Omega -> Prop), dep Omega X I A -> dep Omega X I B -> dep Omega X I (fun w => A w /\ B w).
Proof. intros I A B HA HB w w' H. rewrite (HA w w' H), (HB w w' H). reflexivity. Qed.
Lemma dep_or : forall I (A B : Omega -> Prop), dep Omega X I A -> dep Omega X I B -> dep Omega X I (fun w => A w \/ B w).
Proof. intros I A B HA HB w w' H. rewrite (HA w w' H), (HB w w' H). reflexivity. Qed.
Lemma dep_ex : forall I m (T : nat -> Prop) (A : nat -> Omega -> Prop), (forall j, dep Omega X I (A j)) ->
dep Omega X I (fun w => exists j, (j < m)%nat /\ T j /\ A j w).
Proof.
intros I m T A HA w w' H. split; intros (j & Hj & Tj & Aj); exists j; split; [exact Hj | | exact Hj |];
(split; [exact Tj|]); [apply (HA j w w' H) | apply (HA j w w' H)]; exact Aj.
Qed.
Lemma dep_mono : forall I J (A : Omega -> Prop), (forall g, I g -> J g) -> dep Omega X I A -> dep Omega X J A.
Proof. intros I J A HIJ HA w w' H. apply HA. intros g Hg. apply H. apply HIJ. exact Hg. Qed.
Lemma pastv_S : forall a g, pastv a g -> pastv (S a) g.
Proof. intros a g (a' & q & Ha & E). exists a', q. split; [lia | exact E]. Qed.
(* the run up to layer a reads only the variables of layers up to a *)
Lemma inp_ext : forall w w' a, (forall a' q, (a' < a)%nat -> X (vid a' q) w = X (vid a' q) w') -> inp w a = inp w' a.
Proof.
intros w w' a. induction a as [|a IH]; intro H; [rewrite !inp_0; reflexivity|].
assert (Eo : out w a = out w' a).
{ rewrite !out_eq, (IH (fun a' q Ha' => H a' q ltac:(lia))). apply lfirep_ext. intros q _. apply H. lia. }
destruct (Nat.eq_dec (lyr (S a)) 0) as [B|B]; [rewrite !inp_B by exact B | rewrite !inp_S by exact B]; rewrite Eo; reflexivity.
Qed.
Lemma out_ext : forall w w' a, (forall a' q, (a' <= a)%nat -> X (vid a' q) w = X (vid a' q) w') -> out w a = out w' a.
Proof.
intros w w' a H. rewrite !out_eq, (inp_ext w w' a (fun a' q Ha' => H a' q ltac:(lia))). apply lfirep_ext.
intros q _. apply H. lia.
Qed.
Lemma stop_ext : forall w w' a, (forall a' q, (a' <= a)%nat -> X (vid a' q) w = X (vid a' q) w') -> stopb w a = stopb w' a.
Proof.
intros w w' a H. unfold stopb, stop1, stop2, ncw, Sc, wb, wib.
rewrite (out_ext w w' a H), (inp_ext w w' a (fun a' q Ha' => H a' q ltac:(lia))). reflexivity.
Qed.
Lemma agree : forall a w w', (forall g, pastv a g -> X g w = X g w') -> forall a' q, (a' < a)%nat -> X (vid a' q) w = X (vid a' q) w'.
Proof. intros a w w' H a' q Ha'. apply H. exists a', q. split; [exact Ha' | reflexivity]. Qed.
Lemma dep_Gb : forall a, dep Omega X (pastv a) (Gb a).
Proof.
intros a w w' H. pose proof (agree a w w' H) as Ag. unfold Gb.
assert (E : forall a', (a' < a)%nat -> stopb w a' = stopb w' a')
by (intros a' Ha'; apply stop_ext; intros a'' q Ha''; apply Ag; lia).
split; intros HG a' Ha'; [rewrite <- (E a' Ha') | rewrite (E a' Ha')]; apply HG; exact Ha'.
Qed.
Lemma dep_Win : forall a j, dep Omega X (pastv a) (Win a j).
Proof.
intros a j w w' H. pose proof (agree a w w' H) as Ag. unfold Win, nci, wib.
rewrite (inp_ext w w' a Ag). rewrite (dep_Gb a w w' H). reflexivity.
Qed.
Lemma dep_Wv : forall a i, dep Omega X (pastv (S a)) (Wv a i).
Proof.
intros a i w w' H. pose proof (agree (S a) w w' H) as Ag. unfold Wv, ncw, wb.
rewrite (out_ext w w' a (fun a' q Ha' => Ag a' q ltac:(lia))). rewrite !Gu_Gb, (dep_Gb (S a) w w' H). reflexivity.
Qed.
Lemma dep_E2 : forall a i, dep Omega X (pastv (S a)) (E2 a i).
Proof.
intros a i w w' H. pose proof (agree (S a) w w' H) as Ag. unfold E2, ncw, Sc, wb, wib.
rewrite (out_ext w w' a (fun a' q Ha' => Ag a' q ltac:(lia))), (inp_ext w w' a (fun a' q Ha' => Ag a' q ltac:(lia))).
rewrite (dep_mono _ _ _ (pastv_S a) (dep_Gb a) w w' H). reflexivity.
Qed.
Lemma dep_E3 : forall a i, dep Omega X (pastv (S a)) (E3 a i).
Proof.
intros a i w w' H. pose proof (agree (S a) w w' H) as Ag. unfold E3, ncw, Sc, wb, wib.
rewrite (out_ext w w' a (fun a' q Ha' => Ag a' q ltac:(lia))), (inp_ext w w' a (fun a' q Ha' => Ag a' q ltac:(lia))).
rewrite (dep_mono _ _ _ (pastv_S a) (dep_Gb a) w w' H). reflexivity.
Qed.
(* ---- the recursion of Proposition 8.14 ------------------------------------------------------------------------- *)
(* X_v = sum of p over T(v) *)
Definition Xs (a i : nat) (p : nat -> R) : R := rsum (wia a) (fun j => if tT a i j then p j else 0).
(* the sum over T(v1) and T(v2) in K_{v1 v2} *)
Definition Kpair (a i1 i2 : nat) (p : nat -> R) (k : nat -> nat -> R) : R :=
rsum (wia a) (fun j => if tT a i1 j && tT a i2 j then p j else 0)
+ rsum (wia a) (fun j1 => rsum (wia a) (fun j2 => if tT a i1 j1 && tT a i2 j2 && negb (Nat.eqb j1 j2) then k j1 j2 else 0)).
(* P and K of the inputs of layer a: zero on the state of step 0 and on the device cells of every state *)
Fixpoint PK (a : nat) : (nat -> R) * (nat -> nat -> R) :=
match a with
| O => (fun _ => 0, fun _ _ => 0)
| S a' =>
let pv := fun i => 3 * qk a' i 0 + 3 * dl a' i * Xs a' i (fst (PK a')) in
let kv := fun i1 i2 => 9 * dl a' i1 * dl a' i2 * Kpair a' i1 i2 (fst (PK a')) (snd (PK a')) in
if Nat.eqb (lyr (S a')) 0 then (fun j => if Dv j then 0 else pv j, fun j1 j2 => if Dv j1 || Dv j2 then 0 else kv j1 j2)
else (pv, kv)
end.
Definition Pin (a : nat) : nat -> R := fst (PK a).
Definition Kin (a : nat) : nat -> nat -> R := snd (PK a).
(* P_v, K_{v1 v2}, P^(2)_v and P^(3)_v of the rows of layer a *)
Definition Pv (a i : nat) : R := 3 * qk a i 0 + 3 * dl a i * Xs a i (Pin a).
Definition Kv (a i1 i2 : nat) : R := 9 * dl a i1 * dl a i2 * Kpair a i1 i2 (Pin a) (Kin a).
Definition P2v (a i : nat) : R := 3 * qk a i 0 ^ 2 + 3 * (qk a i 1 ^ 2 - qk a i 0 ^ 2) * Xs a i (Pin a).
Definition P3v (a i : nat) : R := qk a i 0 ^ 3 + (qk a i 1 ^ 3 - qk a i 0 ^ 3) * Xs a i (Pin a).
(* P^(2) and P^(3) of the inputs of layer a, zero on every state *)
Definition P2in (a j : nat) : R := if Nat.eqb (lyr a) 0 then 0 else P2v (a - 1) j.
Definition P3in (a j : nat) : R := if Nat.eqb (lyr a) 0 then 0 else P3v (a - 1) j.
(* the contribution of layer a to b(t) *)
Definition bl (a : nat) : R :=
rsum (nla a) (fun i =>
Rmin 1 (3 * qk a i 2) * Xs a i (P2in a) + Rmin 1 (3 * qk a i 3) * Xs a i (P3in a)
+ rsum (wia a) (fun j1 => rsum (wia a) (fun j2 =>
if tT a i j1 && tT a i j2 && Nat.ltb j1 j2 then Pin a j1 * Pin a j2 + Kin a j1 j2 else 0)))
+ (if Nat.eqb (lyr a) (length Ls - 1) then rsum (nla a) (fun i => P2v a i) else 0).
(* b(t): the sum over the layers of step t *)
Definition bt (t : nat) : R := rsum (length Ls) (fun l => bl (t * length Ls + l)).
Lemma Pin_S : forall a j, Pin (S a) j = if Nat.eqb (lyr (S a)) 0 then (if Dv j then 0 else Pv a j) else Pv a j.
Proof. intros a j. unfold Pin, Pv. cbn [PK]. destruct (Nat.eqb (lyr (S a)) 0); reflexivity. Qed.
Lemma Kin_S : forall a j1 j2,
Kin (S a) j1 j2 = if Nat.eqb (lyr (S a)) 0 then (if Dv j1 || Dv j2 then 0 else Kv a j1 j2) else Kv a j1 j2.
Proof. intros a j1 j2. unfold Kin, Kv. cbn [PK]. destruct (Nat.eqb (lyr (S a)) 0); reflexivity. Qed.
Lemma Xs_nn : forall a i p, (forall j, 0 <= p j) -> 0 <= Xs a i p.
Proof. intros a i p H. apply rsum_nonneg. intros j _. destruct (tT a i j); [apply H | lra]. Qed.
Lemma PK_nn : forall a, (forall j, 0 <= Pin a j) /\ (forall j1 j2, 0 <= Kin a j1 j2).
Proof.
induction a as [|a [IP IK]]; [split; intros; unfold Pin, Kin; cbn; lra|].
assert (HP : forall i, 0 <= Pv a i).
{ intro i. unfold Pv. pose proof (qk_range a i 0). pose proof (dl_nn a i). pose proof (Xs_nn a i _ IP). nra. }
assert (HK : forall i1 i2, 0 <= Kv a i1 i2).
{ intros i1 i2. unfold Kv. pose proof (dl_nn a i1). pose proof (dl_nn a i2).
assert (0 <= Kpair a i1 i2 (Pin a) (Kin a)).
{ unfold Kpair. apply Rplus_le_le_0_compat; apply rsum_nonneg; intros j1 _; [destruct (tT a i1 j1 && tT a i2 j1); [apply IP | lra]|].
apply rsum_nonneg. intros j2 _. destruct (tT a i1 j1 && tT a i2 j2 && negb (Nat.eqb j1 j2)); [apply IK | lra]. }
assert (0 <= 9 * dl a i1 * dl a i2) by (apply Rmult_le_pos; [apply Rmult_le_pos; lra | lra]). nra. }
split; [intro j; rewrite Pin_S | intros j1 j2; rewrite Kin_S];
destruct (Nat.eqb (lyr (S a)) 0); try destruct (Dv j); try destruct (Dv j1 || Dv j2); (lra || apply HP || apply HK).
Qed.
Lemma rsum_if_scal : forall m (T : nat -> bool) (p : nat -> R) c,
rsum m (fun j => if T j then p j * c else 0) = c * rsum m (fun j => if T j then p j else 0).
Proof. intros m T p c. rewrite <- rsum_scal. apply rsum_ext. intros j _. destruct (T j); ring. Qed.
(* ---- P(W_v) <= P_v ------------------------------------------------------------------------------------------------- *)
Lemma claim_P : forall a i, (i < nla a)%nat -> (forall j, (j < wia a)%nat -> P (Win a j) <= Pin a j) -> P (Wv a i) <= Pv a i.
Proof.
intros a i Hi HW. set (g := fun c => vid a (c * nla a + i)%nat).
eapply Rle_trans; [apply (P_mono _ (fun w => (exists c, (c < 3)%nat /\ far (zv a i) 0 (X (g c) w))
\/ (exists j, (j < wia a)%nat /\ tT a i j = true /\ (Win a j w /\
(exists c, (c < 3)%nat /\ (far (zv a i) 1 (X (g c) w) /\ ~ far (zv a i) 0 (X (g c) w)))))))|].
- intros w [Hn HG]. destruct (ncw_copy w a i Hn) as (c & Hc & Hwc).
assert (Hq : (c * nla a + i < 3 * nla a)%nat) by nia.
pose proof (wrong_far w a _ Hq Hwc) as Hf. pose proof (nostop_Sc w a _ (HG a (le_n a)) Hq Hwc) as HS.
rewrite cp_mod in Hf, HS by exact Hi.
destruct (far_dec (zv a i) 0 (X (g c) w)) as [F0|F0]; [left; exists c; split; assumption|].
right. assert (S1 : Sc w a i = 1%nat) by (destruct (Sc w a i) as [|[|k]]; [exfalso; apply F0; exact Hf | reflexivity | lia]).
destruct (Sc_pos w a i ltac:(lia)) as (j & Hj & Tj & Nj). exists j. split; [exact Hj|]. split; [exact Tj|]. split.
+ split; [exact Nj|]. intros a' Ha'. apply HG. lia.
+ exists c. split; [exact Hc|]. split; [rewrite S1 in Hf; exact Hf | exact F0].
- eapply Rle_trans; [apply P_or|].
pose proof (P_copies g (far (zv a i) 0) (qk a i 0) (fun c _ => P_far a i 0 (g c))) as B0.
assert (B1 : P (fun w => exists j, (j < wia a)%nat /\ tT a i j = true /\ (Win a j w /\
(exists c, (c < 3)%nat /\ (far (zv a i) 1 (X (g c) w) /\ ~ far (zv a i) 0 (X (g c) w)))))
<= rsum (wia a) (fun j => if tT a i j then Pin a j * (3 * dl a i) else 0)).
{ apply P_sum. intros j Hj Tj. rewrite (P_pn a).
- apply Rmult_le_compat; [apply Pnn | apply Pnn | apply HW; exact Hj|].
exact (P_copies g (fun e => far (zv a i) 1 e /\ ~ far (zv a i) 0 e) (dl a i) (fun c _ => P_far10 a i (g c))).
- apply dep_Win.
- exact (dep_now a (fun f => exists c, (c < 3)%nat /\
(far (zv a i) 1 (f (c * nla a + i)%nat) /\ ~ far (zv a i) 0 (f (c * nla a + i)%nat)))). }
rewrite rsum_if_scal in B1. unfold Pv, Xs. lra.
Qed.
(* ---- two and three wrong copies, and pairs of rows ---------------------------------------------------------------- *)
Definition cpy (a i c : nat) : nat := (c * nla a + i)%nat.
Definition F0 (z : Z) (e : R) : Prop := far z 0 e.
Definition F10 (z : Z) (e : R) : Prop := far z 1 e /\ ~ far z 0 e.
Lemma cpy_lt : forall a i c, (i < nla a)%nat -> (c < 3)%nat -> (cpy a i c < 3 * nla a)%nat.
Proof. intros a i c Hi Hc. unfold cpy. nia. Qed.
Lemma cpy_mod : forall a i c, (i < nla a)%nat -> (cpy a i c mod nla a = i)%nat.
Proof. intros a i c Hi. apply cp_mod. exact Hi. Qed.
Lemma vid_cpy : forall a i1 i2 c1 c2, (i1 < nla a)%nat -> (i2 < nla a)%nat -> (c1 <> c2 \/ i1 <> i2) ->
vid a (cpy a i1 c1) <> vid a (cpy a i2 c2).
Proof.
intros a i1 i2 c1 c2 H1 H2 Hd E. apply vid_inj in E as [_ E]. apply cp_inj in E as [E1 E2]; [|exact H1 | exact H2].
destruct Hd; contradiction.
Qed.
Lemma P_or4 : forall A B C D : Omega -> Prop, P (fun w => A w \/ B w \/ C w \/ D w) <= P A + P B + P C + P D.
Proof. intros A B C D. eapply Rle_trans; [apply P_or|]. pose proof (P_or3 B C D). lra. Qed.
Lemma P_trip : forall g1 g2 g3 (A B C : R -> Prop) pa pb pc, g1 <> g2 -> g1 <> g3 -> g2 <> g3 ->
P (fun w => A (X g1 w)) <= pa -> P (fun w => B (X g2 w)) <= pb -> P (fun w => C (X g3 w)) <= pc ->
P (fun w => A (X g1 w) /\ B (X g2 w) /\ C (X g3 w)) <= pa * pb * pc.
Proof.
intros g1 g2 g3 A B C pa pb pc H12 H13 H23 Ha Hb Hc. rewrite P_ind3 by assumption.
apply Rmult_le_compat; [apply Rmult_le_pos; apply Pnn | apply Pnn | | exact Hc].
apply Rmult_le_compat; [apply Pnn | apply Pnn | exact Ha | exact Hb].
Qed.
Lemma dep_ex0 : forall I m (A : nat -> Omega -> Prop), (forall j, dep Omega X I (A j)) ->
dep Omega X I (fun w => exists j, (j < m)%nat /\ A j w).
Proof.
intros I m A HA w w' H. split; intros (j & Hj & Aj); exists j; split; [exact Hj | | exact Hj |];
[apply (HA j w w' H) | apply (HA j w w' H)]; exact Aj.
Qed.
(* the copies of the present layer: two of row i, then three, then one of each of two rows *)
Definition N2 (a i : nat) (f : nat -> R) : Prop :=
(exists c1 c2, (c1 < c2)%nat /\ (c2 < 3)%nat /\ F10 (zv a i) (f (cpy a i c1)) /\ far (zv a i) 1 (f (cpy a i c2)))
\/ (exists c1 c2, (c1 < c2)%nat /\ (c2 < 3)%nat /\ F0 (zv a i) (f (cpy a i c1)) /\ F10 (zv a i) (f (cpy a i c2))).
Definition N3 (a i : nat) (f : nat -> R) : Prop :=
(F10 (zv a i) (f (cpy a i 0)) /\ far (zv a i) 1 (f (cpy a i 1)) /\ far (zv a i) 1 (f (cpy a i 2)))
\/ (F0 (zv a i) (f (cpy a i 0)) /\ F10 (zv a i) (f (cpy a i 1)) /\ far (zv a i) 1 (f (cpy a i 2)))
\/ (F0 (zv a i) (f (cpy a i 0)) /\ F0 (zv a i) (f (cpy a i 1)) /\ F10 (zv a i) (f (cpy a i 2))).
Definition Npr (a i1 i2 : nat) (A B : Z -> R -> Prop) (f : nat -> R) : Prop :=
exists c1, (c1 < 3)%nat /\ exists c2, (c2 < 3)%nat /\ A (zv a i1) (f (cpy a i1 c1)) /\ B (zv a i2) (f (cpy a i2 c2)).
Lemma P_N2 : forall a i, (i < nla a)%nat ->
P (fun w => N2 a i (fun q => X (vid a q) w)) <= 3 * dl a i * qk a i 1 + 3 * qk a i 0 * dl a i.
Proof.
intros a i Hi.
assert (Hg : forall c1 c2, (c1 < 3)%nat -> (c2 < 3)%nat -> c1 <> c2 -> vid a (cpy a i c1) <> vid a (cpy a i c2))
by (intros c1 c2 _ _ Hd; apply vid_cpy; [exact Hi | exact Hi | left; exact Hd]).
unfold N2. eapply Rle_trans; [apply P_or|]. apply Rplus_le_compat.
- exact (P_copy_lt (fun c => vid a (cpy a i c)) (F10 (zv a i)) (far (zv a i) 1) (dl a i) (qk a i 1) Hg
(fun c _ => P_far10 a i _) (fun c _ => P_far a i 1 _)).
- exact (P_copy_lt (fun c => vid a (cpy a i c)) (F0 (zv a i)) (F10 (zv a i)) (qk a i 0) (dl a i) Hg
(fun c _ => P_far a i 0 _) (fun c _ => P_far10 a i _)).
Qed.
Lemma P_N3 : forall a i, (i < nla a)%nat ->
P (fun w => N3 a i (fun q => X (vid a q) w))
<= dl a i * qk a i 1 * qk a i 1 + qk a i 0 * dl a i * qk a i 1 + qk a i 0 * qk a i 0 * dl a i.
Proof.
intros a i Hi.
assert (Hg : forall c1 c2, c1 <> c2 -> vid a (cpy a i c1) <> vid a (cpy a i c2))
by (intros c1 c2 Hd; apply vid_cpy; [exact Hi | exact Hi | left; exact Hd]).
unfold N3. eapply Rle_trans; [apply P_or3|]. apply Rplus_le_compat; [apply Rplus_le_compat|].
- exact (P_trip _ _ _ (F10 (zv a i)) (far (zv a i) 1) (far (zv a i) 1) _ _ _ (Hg 0%nat 1%nat ltac:(lia))
(Hg 0%nat 2%nat ltac:(lia)) (Hg 1%nat 2%nat ltac:(lia)) (P_far10 a i _) (P_far a i 1 _) (P_far a i 1 _)).
- exact (P_trip _ _ _ (F0 (zv a i)) (F10 (zv a i)) (far (zv a i) 1) _ _ _ (Hg 0%nat 1%nat ltac:(lia))
(Hg 0%nat 2%nat ltac:(lia)) (Hg 1%nat 2%nat ltac:(lia)) (P_far a i 0 _) (P_far10 a i _) (P_far a i 1 _)).
- exact (P_trip _ _ _ (F0 (zv a i)) (F0 (zv a i)) (F10 (zv a i)) _ _ _ (Hg 0%nat 1%nat ltac:(lia))
(Hg 0%nat 2%nat ltac:(lia)) (Hg 1%nat 2%nat ltac:(lia)) (P_far a i 0 _) (P_far a i 0 _) (P_far10 a i _)).
Qed.
Lemma P_Npr : forall a i1 i2 (A B : Z -> R -> Prop) pA pB, (i1 < nla a)%nat -> (i2 < nla a)%nat -> i1 <> i2 ->
(forall g, P (fun w => A (zv a i1) (X g w)) <= pA) -> (forall g, P (fun w => B (zv a i2) (X g w)) <= pB) ->
P (fun w => Npr a i1 i2 A B (fun q => X (vid a q) w)) <= 9 * pA * pB.
Proof.
intros a i1 i2 A B pA pB H1 H2 Hd HA HB. unfold Npr.
exact (P_copy_pairs (fun c => vid a (cpy a i1 c)) (fun c => vid a (cpy a i2 c)) (A (zv a i1)) (B (zv a i2)) pA pB
(fun c1 c2 _ _ => vid_cpy a i1 i2 c1 c2 H1 H2 (or_intror Hd)) (fun c _ => HA _) (fun c _ => HB _)).
Qed.
(* a wrong copy of row i fails beyond D - |S_v|, and in a layer without a stop |S_v| <= 1 *)
Lemma wrong_cpy : forall w a i c, (i < nla a)%nat -> (c < 3)%nat -> wb w a (cpy a i c) = true ->
far (zv a i) (Sc w a i) (X (vid a (cpy a i c)) w).
Proof.
intros w a i c Hi Hc Hw. pose proof (wrong_far w a _ (cpy_lt a i c Hi Hc) Hw) as Hf. rewrite cpy_mod in Hf by exact Hi.
exact Hf.
Qed.
Lemma wrong_Sc : forall w a i c, (i < nla a)%nat -> (c < 3)%nat -> wb w a (cpy a i c) = true -> stopb w a = false ->
(Sc w a i <= 1)%nat.
Proof.
intros w a i c Hi Hc Hw Hst. pose proof (nostop_Sc w a _ Hst (cpy_lt a i c Hi Hc) Hw) as HS. rewrite cpy_mod in HS by exact Hi.
exact HS.
Qed.
(* a copy that fails without failing at threshold D has |S_v| = 1 and an input in T(v) with a wrong copy *)
Lemma one_input : forall w a i e, (Sc w a i <= 1)%nat -> far (zv a i) (Sc w a i) e -> ~ far (zv a i) 0 e ->
Sc w a i = 1%nat /\ exists j, (j < wia a)%nat /\ tT a i j = true /\ (0 < nci w a j)%nat.
Proof.
intros w a i e HS Hf H0. assert (S1 : Sc w a i = 1%nat) by (destruct (Sc w a i) as [|[|k]]; [contradiction | reflexivity | lia]).
split; [exact S1|]. apply Sc_pos. lia.
Qed.
(* ---- P^(2) and P^(3) -------------------------------------------------------------------------------------------- *)
Lemma claim_P2 : forall a i, (i < nla a)%nat -> (forall j, (j < wia a)%nat -> P (Win a j) <= Pin a j) -> P (E2 a i) <= P2v a i.
Proof.
intros a i Hi HW.
assert (Hg : forall c1 c2, (c1 < 3)%nat -> (c2 < 3)%nat -> c1 <> c2 -> vid a (cpy a i c1) <> vid a (cpy a i c2))
by (intros c1 c2 _ _ Hd; apply vid_cpy; [exact Hi | exact Hi | left; exact Hd]).
eapply Rle_trans; [apply (P_mono _ (fun w =>
(exists c1 c2, (c1 < c2)%nat /\ (c2 < 3)%nat /\ F0 (zv a i) (X (vid a (cpy a i c1)) w) /\ F0 (zv a i) (X (vid a (cpy a i c2)) w))
\/ (exists j, (j < wia a)%nat /\ tT a i j = true /\ (Win a j w /\ N2 a i (fun q => X (vid a q) w)))))|].
- intros w (HG & HS & H2). destruct (ncnt_two (fun c => wb w a (cpy a i c)) H2) as (c1 & c2 & H12 & Hc2 & W1 & W2).
pose proof (wrong_cpy w a i c1 Hi ltac:(lia) W1) as Hf1. pose proof (wrong_cpy w a i c2 Hi Hc2 W2) as Hf2.
destruct (far_dec (zv a i) 0 (X (vid a (cpy a i c1)) w)) as [A1|A1];
destruct (far_dec (zv a i) 0 (X (vid a (cpy a i c2)) w)) as [A2|A2].
+ left. exists c1, c2. repeat split; assumption.
+ right. destruct (one_input w a i _ HS Hf2 A2) as [S1 (j & Hj & Tj & Nj)]. rewrite S1 in Hf1, Hf2.
exists j. split; [exact Hj|]. split; [exact Tj|]. split; [split; assumption|].
right. exists c1, c2. repeat split; assumption.
+ right. destruct (one_input w a i _ HS Hf1 A1) as [S1 (j & Hj & Tj & Nj)]. rewrite S1 in Hf1, Hf2.
exists j. split; [exact Hj|]. split; [exact Tj|]. split; [split; assumption|].
left. exists c1, c2. repeat split; assumption.
+ right. destruct (one_input w a i _ HS Hf1 A1) as [S1 (j & Hj & Tj & Nj)]. rewrite S1 in Hf1, Hf2.
exists j. split; [exact Hj|]. split; [exact Tj|]. split; [split; assumption|].
left. exists c1, c2. repeat split; assumption.
- eapply Rle_trans; [apply P_or|].
replace (P2v a i) with (3 * qk a i 0 * qk a i 0
+ rsum (wia a) (fun j => if tT a i j then Pin a j * (3 * dl a i * qk a i 1 + 3 * qk a i 0 * dl a i) else 0))
by (rewrite rsum_if_scal; unfold P2v, Xs, dl; ring).
apply Rplus_le_compat.
+ exact (P_copy_lt (fun c => vid a (cpy a i c)) (F0 (zv a i)) (F0 (zv a i)) (qk a i 0) (qk a i 0) Hg
(fun c _ => P_far a i 0 _) (fun c _ => P_far a i 0 _)).
+ apply (P_sum (wia a) (tT a i) (fun j w => Win a j w /\ N2 a i (fun q => X (vid a q) w))).
intros j Hj Tj. cbv beta. rewrite (P_pn a).
* apply Rmult_le_compat; [apply Pnn | apply Pnn | apply HW; exact Hj | apply P_N2; exact Hi].
* apply dep_Win.
* apply (dep_now a (N2 a i)).
Qed.
Lemma claim_P3 : forall a i, (i < nla a)%nat -> (forall j, (j < wia a)%nat -> P (Win a j) <= Pin a j) -> P (E3 a i) <= P3v a i.
Proof.
intros a i Hi HW.
assert (Hg : forall c1 c2, c1 <> c2 -> vid a (cpy a i c1) <> vid a (cpy a i c2))
by (intros c1 c2 Hd; apply vid_cpy; [exact Hi | exact Hi | left; exact Hd]).
eapply Rle_trans; [apply (P_mono _ (fun w =>
(F0 (zv a i) (X (vid a (cpy a i 0)) w) /\ F0 (zv a i) (X (vid a (cpy a i 1)) w) /\ F0 (zv a i) (X (vid a (cpy a i 2)) w))
\/ (exists j, (j < wia a)%nat /\ tT a i j = true /\ (Win a j w /\ N3 a i (fun q => X (vid a q) w)))))|].
- intros w (HG & HS & H3). destruct (ncnt_three (fun c => wb w a (cpy a i c)) H3) as (W0 & W1 & W2).
pose proof (wrong_cpy w a i 0 Hi ltac:(lia) W0) as Hf0. pose proof (wrong_cpy w a i 1 Hi ltac:(lia) W1) as Hf1.
pose proof (wrong_cpy w a i 2 Hi ltac:(lia) W2) as Hf2.
destruct (far_dec (zv a i) 0 (X (vid a (cpy a i 0)) w)) as [A0|A0].
+ destruct (far_dec (zv a i) 0 (X (vid a (cpy a i 1)) w)) as [A1|A1].
* destruct (far_dec (zv a i) 0 (X (vid a (cpy a i 2)) w)) as [A2|A2].
-- left. repeat split; assumption.
-- right. destruct (one_input w a i _ HS Hf2 A2) as [S1 (j & Hj & Tj & Nj)]. rewrite S1 in Hf0, Hf1, Hf2.
exists j. split; [exact Hj|]. split; [exact Tj|]. split; [split; assumption|]. right. right. repeat split; assumption.
* right. destruct (one_input w a i _ HS Hf1 A1) as [S1 (j & Hj & Tj & Nj)]. rewrite S1 in Hf0, Hf1, Hf2.
exists j. split; [exact Hj|]. split; [exact Tj|]. split; [split; assumption|]. right. left. repeat split; assumption.
+ right. destruct (one_input w a i _ HS Hf0 A0) as [S1 (j & Hj & Tj & Nj)]. rewrite S1 in Hf0, Hf1, Hf2.
exists j. split; [exact Hj|]. split; [exact Tj|]. split; [split; assumption|]. left. repeat split; assumption.
- eapply Rle_trans; [apply P_or|].
replace (P3v a i) with (qk a i 0 * qk a i 0 * qk a i 0
+ rsum (wia a) (fun j => if tT a i j then Pin a j * (dl a i * qk a i 1 * qk a i 1
+ qk a i 0 * dl a i * qk a i 1 + qk a i 0 * qk a i 0 * dl a i) else 0))
by (rewrite rsum_if_scal; unfold P3v, Xs, dl; ring).
apply Rplus_le_compat.
+ exact (P_trip _ _ _ (F0 (zv a i)) (F0 (zv a i)) (F0 (zv a i)) _ _ _ (Hg 0%nat 1%nat ltac:(lia))
(Hg 0%nat 2%nat ltac:(lia)) (Hg 1%nat 2%nat ltac:(lia)) (P_far a i 0 _) (P_far a i 0 _) (P_far a i 0 _)).
+ apply (P_sum (wia a) (tT a i) (fun j w => Win a j w /\ N3 a i (fun q => X (vid a q) w))).
intros j Hj Tj. cbv beta. rewrite (P_pn a).
* apply Rmult_le_compat; [apply Pnn | apply Pnn | apply HW; exact Hj | apply P_N3; exact Hi].
* apply dep_Win.
* apply (dep_now a (N3 a i)).
Qed.
(* ---- P(W_v1 and W_v2) <= P_v1 P_v2 + K_v1v2 ----------------------------------------------------------------- *)
Lemma claim_K : forall a i1 i2, (i1 < nla a)%nat -> (i2 < nla a)%nat -> i1 <> i2 ->
(forall j, (j < wia a)%nat -> P (Win a j) <= Pin a j) ->
(forall j1 j2, (j1 < wia a)%nat -> (j2 < wia a)%nat -> j1 <> j2 ->
P (fun w => Win a j1 w /\ Win a j2 w) <= Pin a j1 * Pin a j2 + Kin a j1 j2) ->
P (fun w => Wv a i1 w /\ Wv a i2 w) <= Pv a i1 * Pv a i2 + Kv a i1 i2.
Proof.
intros a i1 i2 H1 H2 Hd HW HK.
eapply Rle_trans; [apply (P_mono _ (fun w =>
Npr a i1 i2 F0 F0 (fun q => X (vid a q) w)
\/ ((exists j, (j < wia a)%nat /\ tT a i1 j = true /\ Win a j w) /\ Npr a i1 i2 F10 F0 (fun q => X (vid a q) w))
\/ ((exists j, (j < wia a)%nat /\ tT a i2 j = true /\ Win a j w) /\ Npr a i1 i2 F0 F10 (fun q => X (vid a q) w))
\/ (((exists j, (j < wia a)%nat /\ (tT a i1 j && tT a i2 j) = true /\ Win a j w)
\/ (exists j1, (j1 < wia a)%nat /\ exists j2, (j2 < wia a)%nat
/\ (tT a i1 j1 && tT a i2 j2 && negb (Nat.eqb j1 j2)) = true /\ (Win a j1 w /\ Win a j2 w)))
/\ Npr a i1 i2 F10 F10 (fun q => X (vid a q) w))))|].
- intros w [[N1 G1] [N2' G2]].
destruct (ncw_copy w a i1 N1) as (c1 & Hc1 & W1). destruct (ncw_copy w a i2 N2') as (c2 & Hc2 & W2).
pose proof (wrong_cpy w a i1 c1 H1 Hc1 W1) as Hf1. pose proof (wrong_cpy w a i2 c2 H2 Hc2 W2) as Hf2.
pose proof (wrong_Sc w a i1 c1 H1 Hc1 W1 (G1 a (le_n a))) as HS1. pose proof (wrong_Sc w a i2 c2 H2 Hc2 W2 (G2 a (le_n a))) as HS2.
assert (HGb : Gb a w) by (intros a' Ha'; apply G1; lia).
destruct (far_dec (zv a i1) 0 (X (vid a (cpy a i1 c1)) w)) as [A1|A1];
destruct (far_dec (zv a i2) 0 (X (vid a (cpy a i2 c2)) w)) as [A2|A2].
+ left. exists c1. split; [exact Hc1|]. exists c2. split; [exact Hc2|]. split; assumption.
+ right; right; left. destruct (one_input w a i2 _ HS2 Hf2 A2) as [S2 (j & Hj & Tj & Nj)]. rewrite S2 in Hf2.
split; [exists j; split; [exact Hj|]; split; [exact Tj | split; assumption]|].
exists c1. split; [exact Hc1|]. exists c2. split; [exact Hc2|]. repeat split; assumption.
+ right; left. destruct (one_input w a i1 _ HS1 Hf1 A1) as [S1 (j & Hj & Tj & Nj)]. rewrite S1 in Hf1.
split; [exists j; split; [exact Hj|]; split; [exact Tj | split; assumption]|].
exists c1. split; [exact Hc1|]. exists c2. split; [exact Hc2|]. repeat split; assumption.
+ right; right; right. destruct (one_input w a i1 _ HS1 Hf1 A1) as [S1 (j1 & Hj1 & Tj1 & Nj1)].
destruct (one_input w a i2 _ HS2 Hf2 A2) as [S2 (j2 & Hj2 & Tj2 & Nj2)]. rewrite S1 in Hf1. rewrite S2 in Hf2. split.
* destruct (Nat.eq_dec j1 j2) as [<-|E].
-- left. exists j1. split; [exact Hj1|]. split; [rewrite Tj1, Tj2; reflexivity | split; assumption].
-- right. exists j1. split; [exact Hj1|]. exists j2. split; [exact Hj2|]. split.
++ rewrite Tj1, Tj2. cbn [andb]. apply negb_true_iff, Nat.eqb_neq. exact E.
++ split; split; assumption.
* exists c1. split; [exact Hc1|]. exists c2. split; [exact Hc2|]. repeat split; assumption.
- eapply Rle_trans; [apply P_or4|].
assert (B0 : P (fun w => Npr a i1 i2 F0 F0 (fun q => X (vid a q) w)) <= 9 * qk a i1 0 * qk a i2 0)
by (apply P_Npr; [exact H1 | exact H2 | exact Hd | intro g; exact (P_far a i1 0 g) | intro g; exact (P_far a i2 0 g)]).
assert (B1 : P (fun w => (exists j, (j < wia a)%nat /\ tT a i1 j = true /\ Win a j w) /\ Npr a i1 i2 F10 F0 (fun q => X (vid a q) w))
<= Xs a i1 (Pin a) * (9 * dl a i1 * qk a i2 0)).
{ rewrite (P_pn a).
- apply Rmult_le_compat; [apply Pnn | apply Pnn | |].
+ unfold Xs. apply (P_sum (wia a) (tT a i1) (fun j => Win a j)). intros j Hj _. apply HW. exact Hj.
+ apply P_Npr; [exact H1 | exact H2 | exact Hd | intro g; exact (P_far10 a i1 g) | intro g; exact (P_far a i2 0 g)].
- apply dep_ex. intro j. apply dep_Win.
- apply (dep_now a (Npr a i1 i2 F10 F0)). }
assert (B2 : P (fun w => (exists j, (j < wia a)%nat /\ tT a i2 j = true /\ Win a j w) /\ Npr a i1 i2 F0 F10 (fun q => X (vid a q) w))
<= Xs a i2 (Pin a) * (9 * qk a i1 0 * dl a i2)).
{ rewrite (P_pn a).
- apply Rmult_le_compat; [apply Pnn | apply Pnn | |].
+ unfold Xs. apply (P_sum (wia a) (tT a i2) (fun j => Win a j)). intros j Hj _. apply HW. exact Hj.
+ apply P_Npr; [exact H1 | exact H2 | exact Hd | intro g; exact (P_far a i1 0 g) | intro g; exact (P_far10 a i2 g)].
- apply dep_ex. intro j. apply dep_Win.
- apply (dep_now a (Npr a i1 i2 F0 F10)). }
set (SN := rsum (wia a) (fun j => if tT a i1 j && tT a i2 j then Pin a j else 0)).
set (SP := rsum (wia a) (fun j1 => rsum (wia a) (fun j2 =>
if tT a i1 j1 && tT a i2 j2 && negb (Nat.eqb j1 j2) then Pin a j1 * Pin a j2 else 0))).
set (SK := rsum (wia a) (fun j1 => rsum (wia a) (fun j2 =>
if tT a i1 j1 && tT a i2 j2 && negb (Nat.eqb j1 j2) then Kin a j1 j2 else 0))).
assert (B3 : P (fun w => ((exists j, (j < wia a)%nat /\ (tT a i1 j && tT a i2 j) = true /\ Win a j w)
\/ (exists j1, (j1 < wia a)%nat /\ exists j2, (j2 < wia a)%nat
/\ (tT a i1 j1 && tT a i2 j2 && negb (Nat.eqb j1 j2)) = true /\ (Win a j1 w /\ Win a j2 w)))
/\ Npr a i1 i2 F10 F10 (fun q => X (vid a q) w))
<= (SN + (SP + SK)) * (9 * dl a i1 * dl a i2)).
{ rewrite (P_pn a).
- apply Rmult_le_compat; [apply Pnn | apply Pnn | |].
+ eapply Rle_trans; [apply P_or|]. apply Rplus_le_compat.
* apply (P_sum (wia a) (fun j => tT a i1 j && tT a i2 j) (fun j => Win a j)). intros j Hj _. apply HW. exact Hj.
* replace (SP + SK) with (rsum (wia a) (fun j1 => rsum (wia a) (fun j2 =>
if tT a i1 j1 && tT a i2 j2 && negb (Nat.eqb j1 j2) then Pin a j1 * Pin a j2 + Kin a j1 j2 else 0))).
-- eapply Rle_trans; [apply (Pex (wia a) (fun j1 w => exists j2, (j2 < wia a)%nat
/\ (tT a i1 j1 && tT a i2 j2 && negb (Nat.eqb j1 j2)) = true /\ (Win a j1 w /\ Win a j2 w)))|].
apply rsum_le. intros j1 Hj1.
apply (P_sum (wia a) (fun j2 => tT a i1 j1 && tT a i2 j2 && negb (Nat.eqb j1 j2)) (fun j2 w => Win a j1 w /\ Win a j2 w)).
intros j2 Hj2 T. apply HK; [exact Hj1 | exact Hj2|]. apply andb_prop in T as [_ T].
apply negb_true_iff, Nat.eqb_neq in T. exact T.
-- unfold SP, SK. rewrite <- rsum_plus. apply rsum_ext. intros j1 _. rewrite <- rsum_plus. apply rsum_ext.
intros j2 _. destruct (tT a i1 j1 && tT a i2 j2 && negb (Nat.eqb j1 j2)); ring.
+ apply P_Npr; [exact H1 | exact H2 | exact Hd | intro g; exact (P_far10 a i1 g) | intro g; exact (P_far10 a i2 g)].
- apply dep_or; [apply dep_ex; intro j; apply dep_Win|]. apply dep_ex0. intro j1. apply dep_ex. intro j2.
apply dep_and; apply dep_Win.
- apply (dep_now a (Npr a i1 i2 F10 F10)). }
pose proof (sum_ne_le (wia a) (tT a i1) (tT a i2) (Pin a) (proj1 (PK_nn a))) as HSP. fold SP in HSP.
change (rsum (wia a) (fun j => if tT a i1 j then Pin a j else 0)) with (Xs a i1 (Pin a)) in HSP.
change (rsum (wia a) (fun j => if tT a i2 j then Pin a j else 0)) with (Xs a i2 (Pin a)) in HSP.
pose proof (dl_nn a i1). pose proof (dl_nn a i2).
assert (HD : 0 <= 9 * dl a i1 * dl a i2) by (apply Rmult_le_pos; [apply Rmult_le_pos|]; lra).
pose proof (Rmult_le_compat_l _ _ _ HD HSP) as HSP'.
unfold Pv, Kv, Kpair. fold SN SK. nra.
Qed.
(* ---- the bounds hold layer by layer -------------------------------------------------------------------------------- *)
Lemma lyr_0 : lyr 0 = 0%nat.
Proof. unfold lyr. apply Nat.Div0.mod_0_l. Qed.
Lemma nci_0 : forall w j, (j < n)%nat -> nci w 0 j = 0%nat.
Proof.
intros w j Hj. unfold nci. rewrite wia_0. rewrite (ncnt_ext 3 _ (fun _ => false)); [apply ncnt_false|].
intros c Hc. apply wib_0. nia.
Qed.
Lemma nci_S : forall w a j, lyr (S a) <> 0%nat -> nci w (S a) j = ncw w a j.
Proof. intros w a j H. unfold nci, ncw. rewrite (wia_S a H). apply ncnt_ext. intros c Hc. apply wib_S. exact H. Qed.
Lemma nci_B : forall w a j, lyr (S a) = 0%nat -> (j < n)%nat -> nci w (S a) j = if Dv j then 0%nat else ncw w a j.
Proof.
intros w a j H Hj. destruct (wia_B a H) as [W1 W2]. unfold nci, ncw. rewrite W1, W2. destruct (Dv j) eqn:E.
- rewrite (ncnt_ext 3 _ (fun _ => false)); [apply ncnt_false|]. intros c Hc.
rewrite wib_B by (exact H || nia). rewrite cp_mod by exact Hj. rewrite E. reflexivity.
- apply ncnt_ext. intros c Hc. rewrite wib_B by (exact H || nia). rewrite cp_mod by exact Hj. rewrite E. reflexivity.
Qed.
Lemma Win_S : forall w a j, lyr (S a) <> 0%nat -> (Win (S a) j w <-> Wv a j w).
Proof. intros w a j H. unfold Win, Wv. rewrite nci_S by exact H. rewrite Gu_Gb. reflexivity. Qed.
Lemma Win_B : forall w a j, lyr (S a) = 0%nat -> (j < n)%nat -> Win (S a) j w -> Dv j = false /\ Wv a j w.
Proof.
intros w a j H Hj [Hn HG]. rewrite nci_B in Hn by assumption. destruct (Dv j); [lia|]. split; [reflexivity|].
split; [exact Hn | apply Gu_Gb; exact HG].
Qed.
Lemma Pin_N : forall a j, lyr (S a) <> 0%nat -> Pin (S a) j = Pv a j.
Proof. intros a j H. rewrite Pin_S. destruct (Nat.eqb_spec (lyr (S a)) 0); [contradiction | reflexivity]. Qed.
Lemma Pin_Bd : forall a j, lyr (S a) = 0%nat -> Dv j = true -> Pin (S a) j = 0.
Proof. intros a j H E. rewrite Pin_S, H, E. reflexivity. Qed.
Lemma Pin_Bn : forall a j, lyr (S a) = 0%nat -> Dv j = false -> Pin (S a) j = Pv a j.
Proof. intros a j H E. rewrite Pin_S, H, E. reflexivity. Qed.
Lemma Kin_N : forall a j1 j2, lyr (S a) <> 0%nat -> Kin (S a) j1 j2 = Kv a j1 j2.
Proof. intros a j1 j2 H. rewrite Kin_S. destruct (Nat.eqb_spec (lyr (S a)) 0); [contradiction | reflexivity]. Qed.
Lemma Kin_Bd : forall a j1 j2, lyr (S a) = 0%nat -> Dv j1 = true \/ Dv j2 = true -> Kin (S a) j1 j2 = 0.
Proof. intros a j1 j2 H [E|E]; rewrite Kin_S, H, E; [reflexivity | rewrite orb_true_r; reflexivity]. Qed.
Lemma Kin_Bn : forall a j1 j2, lyr (S a) = 0%nat -> Dv j1 = false -> Dv j2 = false -> Kin (S a) j1 j2 = Kv a j1 j2.
Proof. intros a j1 j2 H E1 E2. rewrite Kin_S, H, E1, E2. reflexivity. Qed.
(* P(W) <= P and P(W and W') <= P P' + K for the inputs of every layer, by induction over the layers *)
Lemma claims : forall a, (forall j, (j < wia a)%nat -> P (Win a j) <= Pin a j) /\
(forall j1 j2, (j1 < wia a)%nat -> (j2 < wia a)%nat -> j1 <> j2 ->
P (fun w => Win a j1 w /\ Win a j2 w) <= Pin a j1 * Pin a j2 + Kin a j1 j2).
Proof.
induction a as [|a [IW IK]].
- rewrite wia_0. assert (E : forall j w, (j < n)%nat -> ~ Win 0 j w) by (intros j w Hj [Hn _]; rewrite nci_0 in Hn by exact Hj; lia).
split.
+ intros j Hj. rewrite (Pnone (Win 0 j)) by (intro w; apply E; exact Hj). unfold Pin. cbn. lra.
+ intros j1 j2 Hj1 Hj2 _. rewrite Pnone by (intros w [W _]; exact (E j1 w Hj1 W)). unfold Pin, Kin. cbn. lra.
- pose proof (fun i Hi => claim_P a i Hi IW) as CP. pose proof (fun i1 i2 H1 H2 Hd => claim_K a i1 i2 H1 H2 Hd IW IK) as CK.
destruct (PK_nn (S a)) as [NP NK].
destruct (Nat.eq_dec (lyr (S a)) 0) as [B|B].
+ destruct (wia_B a B) as [W1 W2]. rewrite W1. split.
* intros j Hj. destruct (Dv j) eqn:E.
-- rewrite (Pin_Bd a j B E). right. apply Pnone. intros w Hw. destruct (Win_B w a j B Hj Hw) as [C _]. congruence.
-- rewrite (Pin_Bn a j B E).
eapply Rle_trans; [apply P_mono; intros w Hw; exact (proj2 (Win_B w a j B Hj Hw))|]. apply CP. lia.
* intros j1 j2 Hj1 Hj2 Hd. pose proof (NP j1). pose proof (NP j2).
destruct (Dv j1) eqn:E1; [|destruct (Dv j2) eqn:E2].
-- rewrite Pnone by (intros w [Hw _]; destruct (Win_B w a j1 B Hj1 Hw) as [C _]; congruence).
rewrite (Kin_Bd a j1 j2 B (or_introl E1)). nra.
-- rewrite Pnone by (intros w [_ Hw]; destruct (Win_B w a j2 B Hj2 Hw) as [C _]; congruence).
rewrite (Kin_Bd a j1 j2 B (or_intror E2)). nra.
-- rewrite (Pin_Bn a j1 B E1), (Pin_Bn a j2 B E2), (Kin_Bn a j1 j2 B E1 E2).
eapply Rle_trans; [apply P_mono; intros w [Hw1 Hw2];
exact (conj (proj2 (Win_B w a j1 B Hj1 Hw1)) (proj2 (Win_B w a j2 B Hj2 Hw2)))|].
apply CK; [lia | lia | exact Hd].
+ rewrite (wia_S a B). split.
* intros j Hj. rewrite (Pin_N a j B).
eapply Rle_trans; [apply P_mono; intros w Hw; exact (proj1 (Win_S w a j B) Hw)|]. apply CP. exact Hj.
* intros j1 j2 Hj1 Hj2 Hd. rewrite (Pin_N a j1 B), (Pin_N a j2 B), (Kin_N a j1 j2 B).
eapply Rle_trans; [apply P_mono; intros w [Hw1 Hw2]; exact (conj (proj1 (Win_S w a j1 B) Hw1) (proj1 (Win_S w a j2 B) Hw2))|].
apply CK; assumption.
Qed.
(* ---- the first stop ------------------------------------------------------------------------------------------------ *)
(* the input j of layer a has two wrong copies, or three, and no layer before is a stop; empty on the state *)
Definition B2 (a j : nat) (w : Omega) : Prop := lyr a <> 0%nat /\ E2 (a - 1) j w.
Definition B3 (a j : nat) (w : Omega) : Prop := lyr a <> 0%nat /\ E3 (a - 1) j w.
(* some copy of row i fails beyond D - k *)
Definition N1 (a i k : nat) (f : nat -> R) : Prop := exists c, (c < 3)%nat /\ far (zv a i) k (f (cpy a i c)).
Lemma P_B2 : forall a j, (j < wia a)%nat -> P (B2 a j) <= P2in a j.
Proof.
intros a j Hj. unfold P2in. destruct (Nat.eqb_spec (lyr a) 0) as [B|B].
- right. apply Pnone. intros w [C _]. contradiction.
- destruct a as [|a]; [rewrite lyr_0 in B; contradiction|]. replace (S a - 1)%nat with a by lia.
eapply Rle_trans; [apply P_mono; intros w [_ H]; replace (S a - 1)%nat with a in H by lia; exact H|].
apply claim_P2; [rewrite (wia_S a B) in Hj; exact Hj | exact (proj1 (claims a))].
Qed.
Lemma P_B3 : forall a j, (j < wia a)%nat -> P (B3 a j) <= P3in a j.
Proof.
intros a j Hj. unfold P3in. destruct (Nat.eqb_spec (lyr a) 0) as [B|B].
- right. apply Pnone. intros w [C _]. contradiction.
- destruct a as [|a]; [rewrite lyr_0 in B; contradiction|]. replace (S a - 1)%nat with a by lia.
eapply Rle_trans; [apply P_mono; intros w [_ H]; replace (S a - 1)%nat with a in H by lia; exact H|].
apply claim_P3; [rewrite (wia_S a B) in Hj; exact Hj | exact (proj1 (claims a))].
Qed.
Lemma dep_B2 : forall a j, dep Omega X (pastv a) (B2 a j).
Proof.
intros [|a] j w w' H; unfold B2; [rewrite lyr_0; split; intros [C _]; contradiction|].
replace (S a - 1)%nat with a by lia. rewrite (dep_E2 a j w w' H). reflexivity.
Qed.
Lemma dep_B3 : forall a j, dep Omega X (pastv a) (B3 a j).
Proof.
intros [|a] j w w' H; unfold B3; [rewrite lyr_0; split; intros [C _]; contradiction|].
replace (S a - 1)%nat with a by lia. rewrite (dep_E3 a j w w' H). reflexivity.
Qed.
Lemma P_N1 : forall a i k, P (fun w => N1 a i k (fun q => X (vid a q) w)) <= Rmin 1 (3 * qk a i k).
Proof.
intros a i k. apply Rmin_glb; [apply Ple1|]. unfold N1.
exact (P_copies (fun c => vid a (cpy a i c)) (far (zv a i) k) (qk a i k) (fun c _ => P_far a i k _)).
Qed.
Lemma Rmin_nn : forall a i k, 0 <= Rmin 1 (3 * qk a i k).
Proof. intros a i k. apply Rmin_glb; [lra|]. pose proof (qk_range a i k). lra. Qed.
(* the first stop at layer a: P <= the contribution of a to b(t) *)
Lemma claim_stop : forall a, P (fun w => stopb w a = true /\ Gb a w) <= bl a.
Proof.
intro a. destruct (claims a) as [HW HK].
eapply Rle_trans; [apply (P_mono _ (fun w =>
(exists i, (i < nla a)%nat /\ exists j1, (j1 < wia a)%nat /\ exists j2, (j2 < wia a)%nat
/\ (tT a i j1 && tT a i j2 && Nat.ltb j1 j2) = true /\ (Win a j1 w /\ Win a j2 w))
\/ (exists i, (i < nla a)%nat /\ exists j, (j < wia a)%nat /\ tT a i j = true /\ (B2 a j w /\ N1 a i 2 (fun q => X (vid a q) w)))
\/ (exists i, (i < nla a)%nat /\ exists j, (j < wia a)%nat /\ tT a i j = true /\ (B3 a j w /\ N1 a i 3 (fun q => X (vid a q) w)))
\/ (lyr a = (length Ls - 1)%nat /\ exists i, (i < nla a)%nat /\ E2 a i w)))|].
- intros w [Hst HG]. unfold stopb in Hst. destruct (stop1 w a) eqn:S1.
+ apply existsb_seq_true in S1 as (q & Hq & E). apply andb_prop in E as [Wq Sq]. apply Nat.leb_le in Sq.
assert (HN : (0 < nla a)%nat) by lia.
assert (Hdec : exists i c, (i < nla a)%nat /\ (c < 3)%nat /\ q = cpy a i c).
{ exists (q mod nla a)%nat, (q / nla a)%nat. split; [apply Nat.mod_upper_bound; lia|].
split; [apply Nat.Div0.div_lt_upper_bound; lia|]. unfold cpy. apply cp_split. exact HN. }
destruct Hdec as (i & c & Hi & Hc & ->). rewrite cpy_mod in Sq by exact Hi.
pose proof (wrong_cpy w a i c Hi Hc Wq) as Hf.
destruct (Sc_two w a i Sq) as [(j1 & j2 & H12 & Hj2 & T1 & T2 & N1' & N2') | (j & Hj & Tj & ES)].
* left. exists i. split; [exact Hi|]. exists j1. split; [lia|]. exists j2. split; [exact Hj2|]. split.
-- rewrite T1, T2. cbn [andb]. apply Nat.ltb_lt. exact H12.
-- split; split; assumption.
* assert (Hj3 : (nci w a j <= 3)%nat) by apply ncnt_le.
destruct a as [|a].
-- exfalso. rewrite wia_0 in Hj. rewrite nci_0 in ES by exact Hj. lia.
-- destruct (Nat.eq_dec (lyr (S a)) 0) as [B|B].
++ exfalso. destruct (wia_B a B) as [W1 W2]. rewrite W1 in Hj. rewrite (nci_B w a j B Hj) in ES.
destruct (Dv j) eqn:Ed; [lia|].
assert (Hs2 : stopb w a = true).
{ unfold stopb. apply orb_true_iff. right. unfold stop2. apply andb_true_iff. split.
- apply Nat.eqb_eq. destruct (lyr_succ a) as [(_ & L & _)|(_ & L & _)]; [exact L | contradiction].
- apply existsb_exists. exists j. split; [apply in_seq; lia|]. apply Nat.leb_le. lia. }
rewrite (HG a (Nat.lt_succ_diag_r a)) in Hs2. discriminate.
++ rewrite (nci_S w a j B) in ES, Hj3. rewrite (wia_S a B) in Hj.
assert (HGa : stopb w a = false) by (apply HG; lia).
assert (HSj : (Sc w a j <= 1)%nat).
{ destruct (ncw_copy w a j ltac:(lia)) as (c' & Hc' & W'). exact (wrong_Sc w a j c' Hj Hc' W' HGa). }
assert (HGb' : Gb a w) by (intros a'' Ha''; apply HG; lia).
assert (Ea : (S a - 1)%nat = a) by lia.
destruct (Nat.eq_dec (ncw w a j) 3) as [E3'|E3'].
** right; right; left. exists i. split; [exact Hi|]. exists j. split; [rewrite (wia_S a B); exact Hj|].
split; [exact Tj|]. split.
--- split; [exact B|]. rewrite Ea. split; [exact HGb'|]. split; [exact HSj | exact E3'].
--- exists c. split; [exact Hc|]. rewrite ES, E3' in Hf. exact Hf.
** right; left. exists i. split; [exact Hi|]. exists j. split; [rewrite (wia_S a B); exact Hj|].
split; [exact Tj|]. split.
--- split; [exact B|]. rewrite Ea. split; [exact HGb'|]. split; [exact HSj | lia].
--- exists c. split; [exact Hc|]. replace (Sc w (S a) i) with 2%nat in Hf by lia. exact Hf.
+ cbn [orb] in Hst. unfold stop2 in Hst. apply andb_prop in Hst as [L Ex]. apply Nat.eqb_eq in L.
apply existsb_seq_true in Ex as (i & Hi & E). apply Nat.leb_le in E.
right; right; right. split; [exact L|]. exists i. split; [exact Hi|]. split; [exact HG|]. split; [|exact E].
destruct (ncw_copy w a i ltac:(lia)) as (c & Hc & W).
pose proof (existsb_seq_false _ _ S1 (cpy a i c) (cpy_lt a i c Hi Hc)) as F. cbv beta in F.
assert (W' : wb w a (cpy a i c) = true) by exact W. rewrite W' in F. cbn [andb] in F. apply Nat.leb_gt in F.
rewrite cpy_mod in F by exact Hi. lia.
- eapply Rle_trans; [apply P_or4|]. unfold bl.
rewrite rsum_plus, rsum_plus.
assert (Bp : P (fun w => exists i, (i < nla a)%nat /\ exists j1, (j1 < wia a)%nat /\ exists j2, (j2 < wia a)%nat
/\ (tT a i j1 && tT a i j2 && Nat.ltb j1 j2) = true /\ (Win a j1 w /\ Win a j2 w))
<= rsum (nla a) (fun i => rsum (wia a) (fun j1 => rsum (wia a) (fun j2 =>
if tT a i j1 && tT a i j2 && Nat.ltb j1 j2 then Pin a j1 * Pin a j2 + Kin a j1 j2 else 0)))).
{ eapply Rle_trans; [apply Pex|]. apply rsum_le. intros i Hi.
eapply Rle_trans; [apply Pex|]. apply rsum_le. intros j1 Hj1.
apply (P_sum (wia a) (fun j2 => tT a i j1 && tT a i j2 && Nat.ltb j1 j2) (fun j2 w => Win a j1 w /\ Win a j2 w)).
intros j2 Hj2 T. apply HK; [exact Hj1 | exact Hj2|]. apply andb_prop in T as [_ T]. apply Nat.ltb_lt in T. lia. }
assert (Bk : forall k (Bk : nat -> Omega -> Prop) (pk : nat -> R),
(forall j, (j < wia a)%nat -> P (Bk j) <= pk j) -> (forall j, dep Omega X (pastv a) (Bk j)) ->
P (fun w => exists i, (i < nla a)%nat /\ exists j, (j < wia a)%nat /\ tT a i j = true
/\ (Bk j w /\ N1 a i k (fun q => X (vid a q) w)))
<= rsum (nla a) (fun i => Rmin 1 (3 * qk a i k) * Xs a i pk)).
{ intros k Bk pk HB HD. eapply Rle_trans; [apply Pex|]. apply rsum_le. intros i Hi.
unfold Xs. rewrite <- rsum_if_scal.
apply (P_sum (wia a) (tT a i) (fun j w => Bk j w /\ N1 a i k (fun q => X (vid a q) w))).
intros j Hj _. cbv beta. rewrite (P_pn a).
- apply Rmult_le_compat; [apply Pnn | apply Pnn | apply HB; exact Hj | apply P_N1].
- apply HD.
- apply (dep_now a (N1 a i k)). }
pose proof (Bk 2%nat (B2 a) (P2in a) (P_B2 a) (dep_B2 a)) as B2'.
pose proof (Bk 3%nat (B3 a) (P3in a) (P_B3 a) (dep_B3 a)) as B3'.
assert (B4 : P (fun w => lyr a = (length Ls - 1)%nat /\ exists i, (i < nla a)%nat /\ E2 a i w)
<= (if Nat.eqb (lyr a) (length Ls - 1) then rsum (nla a) (fun i => P2v a i) else 0)).
{ destruct (Nat.eqb_spec (lyr a) (length Ls - 1)) as [L|L].
- eapply Rle_trans; [apply P_mono; intros w [_ H]; exact H|]. eapply Rle_trans; [apply Pex|].
apply rsum_le. intros i Hi. apply claim_P2; [exact Hi | exact HW].
- right. apply Pnone. intros w [C _]. contradiction. }
lra.
Qed.
(* ---- Proposition 8.14 ------------------------------------------------------------------------------------------- *)
Lemma out_last : forall w t, out w (t * length Ls + (length Ls - 1)) = lmapp (amap 3 n Ls) 0 (Et w t) (run3 w t).
Proof.
intros w t. pose proof NL_pos. destruct (stp_lyr t (length Ls - 1) ltac:(lia)) as [E1 E2].
unfold out, pn. rewrite E1, E2. replace (S (length Ls - 1)) with (length Ls) by lia.
rewrite firstn_all2 by (rewrite length_amap; lia). reflexivity.
Qed.
Lemma exo_last : forall a, lyr a = (length Ls - 1)%nat -> exo a = lmap Ls (xs (stp a)) /\ nla a = n.
Proof.
intros a L. pose proof NL_pos. split.
- unfold exo, lay, exin. rewrite L. rewrite <- lin_S by lia. replace (S (length Ls - 1)) with (length Ls) by lia.
unfold lin. rewrite firstn_all. reflexivity.
- unfold nla, lay. rewrite L, <- (last_nth' _ Ls [] Hne). exact Hlast.
Qed.
(* every copy is its value in the run, flipped where it is wrong *)
Lemma out_xorv : forall w a, out w a = xorv (rep 3 (exo a)) (wb w a).
Proof.
intros w a. apply nth_ext with (d := false) (d' := false).
- rewrite len_out, length_xorv, length_rep, len_exo. reflexivity.
- intros k Hk. rewrite len_out in Hk. rewrite nth_xorv by (rewrite length_rep, len_exo; exact Hk).
rewrite nth_rep_mod by (rewrite len_exo; exact Hk). rewrite len_exo. unfold wb.
destruct (nth k (out w a) false), (nth (k mod nla a) (exo a) false); reflexivity.
Qed.
(* without a stop at the last layer of a step the state read by majority is the state of the run *)
Lemma maj_out : forall w a, lyr a = (length Ls - 1)%nat -> stopb w a = false -> maj 3 n (out w a) = lmap Ls (xs (stp a)).
Proof.
intros w a L Hst. destruct (exo_last a L) as [E1 E2]. rewrite out_xorv, <- E1.
apply maj_ok; [reflexivity | rewrite len_exo; exact E2 |].
intros j Hj. pose proof (nostop_ncw w a j Hst L ltac:(lia)) as H. unfold ncw in H. rewrite E2 in H.
change (3 / 2)%nat with 1%nat. exact H.
Qed.
(* Proposition 8.14: the state of the threefold amplification read by majority leaves the run within T steps with
probability at most sum_{t < T} b(t) *)
Theorem restoration : forall T,
P (fun w => exists t, (t < T)%nat /\ maj 3 n (lmapp (amap 3 n Ls) 0 (Et w t) (run3 w t)) <> lmap Ls (xs t))
<= rsum T bt.
Proof.
intro T. pose proof NL_pos.
eapply Rle_trans; [apply (P_mono _ (fun w => exists a, (a < T * length Ls)%nat /\ (stopb w a = true /\ Gb a w)))|].
- intros w (t & Ht & Hm). set (a := (t * length Ls + (length Ls - 1))%nat).
destruct (stp_lyr t (length Ls - 1) ltac:(lia)) as [E1 E2]. fold a in E1, E2.
assert (Hst : stopb w a = true).
{ destruct (stopb w a) eqn:Es; [reflexivity|]. exfalso. apply Hm. rewrite <- out_last. fold a.
rewrite <- E1. apply maj_out; assumption. }
destruct (first_true (stopb w) a Hst) as (a0 & Ha0 & H0 & Hb). exists a0. split; [unfold a in Ha0; nia|].
split; [exact H0 | exact Hb].
- eapply Rle_trans; [apply Pex|]. unfold bt. rewrite <- rsum_blocks. apply rsum_le. intros a _. apply claim_stop.
Qed.
End Restore.
(* Proposition 8.14: the restoration bound for the threefold amplification. The rows of the layered map are unrolled
along a run, the first layer of each step reading the last layer of the step before through a device that writes
every copy of its cells with the values of the run. Under independent Gaussian perturbations of every
pre-activation of the threefold amplification, the probability that the state read by majority leaves the run
within T steps is at most the sum of the bounds b(t) that the recursion of the proposition computes along it.
The probability space is that of Noise.v, with P additive on the events built from the threshold events. *)
From Stdlib Require Import List Bool Arith ZArith Reals Lia Lra FunctionalExtensionality.
Import ListNotations.
Set Warnings "-ambiguous-paths".
From TH Require Import TwoHead Net Lev Margin Erfc Noise.
Set Warnings "ambiguous-paths".
Local Open Scope R_scope.
(* ---- counts and sums ------------------------------------------------------------------------------------------ *)
Lemma ncnt_pos : forall m f, (0 < ncnt m f)%nat -> exists k, (k < m)%nat /\ f k = true.
Proof.
induction m as [|m IH]; intros f H; cbn [ncnt] in H; [lia|].
destruct (f m) eqn:E; [exists m; split; [lia | exact E]|].
destruct (IH f ltac:(lia)) as (k & Hk & Hf). exists k. split; [lia | exact Hf].
Qed.
Lemma ncnt_false : forall k, ncnt k (fun _ => false) = 0%nat.
Proof. induction k as [|k IH]; cbn [ncnt]; [reflexivity | rewrite IH; reflexivity]. Qed.
Lemma ncnt_add : forall a b f, ncnt (a + b) f = (ncnt a f + ncnt b (fun k => f (a + k)%nat))%nat.
Proof.
intros a b f. induction b as [|b IH]; cbn [ncnt]; [rewrite Nat.add_0_r; lia|].
rewrite Nat.add_succ_r. cbn [ncnt]. rewrite IH. lia.
Qed.
Lemma ncnt_point : forall m f j, (j < m)%nat -> ncnt m (fun k => f k && Nat.eqb k j) = if f j then 1%nat else 0%nat.
Proof.
induction m as [|m IH]; intros f j Hj; [lia|]. cbn [ncnt].
destruct (Nat.eq_dec j m) as [->|E].
- rewrite Nat.eqb_refl, andb_true_r.
rewrite (ncnt_ext m _ (fun _ => false)) by (intros c Hc; destruct (Nat.eqb_spec c m); [lia | apply andb_false_r]).
rewrite ncnt_false. destruct (f m); reflexivity.
- rewrite IH by lia. destruct (Nat.eqb_spec m j); [lia|]. rewrite andb_false_r. destruct (f j); reflexivity.
Qed.
(* the positions c w + j, c < r, of one row j among r w positions *)
Lemma ncnt_row : forall r w j D, (j < w)%nat ->
ncnt (r * w) (fun q => D q && Nat.eqb (q mod w) j) = ncnt r (fun c => D (c * w + j)%nat).
Proof.
intros r w j D Hj. induction r as [|r IH]; [reflexivity|].
replace (S r * w)%nat with (r * w + w)%nat by lia. rewrite ncnt_add, IH. cbn [ncnt]. f_equal.
rewrite (ncnt_ext w _ (fun k => D (r * w + k)%nat && Nat.eqb k j)).
- exact (ncnt_point w (fun k => D (r * w + k)%nat) j Hj).
- intros k Hk. replace ((r * w + k) mod w)%nat with k; [reflexivity|].
rewrite Nat.add_comm, Nat.Div0.mod_add. symmetry. apply Nat.mod_small. exact Hk.
Qed.
Lemma ncnt_two : forall f, (2 <= ncnt 3 f)%nat -> exists c1 c2, (c1 < c2)%nat /\ (c2 < 3)%nat /\ f c1 = true /\ f c2 = true.
Proof.
intros f H. cbn [ncnt] in H. destruct (f 0%nat) eqn:E0, (f 1%nat) eqn:E1, (f 2%nat) eqn:E2; cbn [Nat.add] in H;
try lia; solve [exists 0%nat, 1%nat; auto | exists 0%nat, 2%nat; auto | exists 1%nat, 2%nat; auto].
Qed.
Lemma ncnt_three : forall f, ncnt 3 f = 3%nat -> f 0%nat = true /\ f 1%nat = true /\ f 2%nat = true.
Proof. intros f H. cbn [ncnt] in H. destruct (f 0%nat), (f 1%nat), (f 2%nat); cbn [Nat.add] in H; try lia; auto. Qed.
Lemma rsum_add : forall a b g, rsum (a + b) g = rsum a g + rsum b (fun k => g (a + k)%nat).
Proof.
intros a b g. induction b as [|b IH]; cbn [rsum]; [rewrite Nat.add_0_r; lra|].
rewrite Nat.add_succ_r. cbn [rsum]. rewrite IH. lra.
Qed.
Lemma rsum_blocks : forall T m g, rsum (T * m) g = rsum T (fun t => rsum m (fun l => g (t * m + l)%nat)).
Proof.
induction T as [|T IH]; intros m g; [cbn; lra|]. replace (S T * m)%nat with (T * m + m)%nat by lia.
rewrite rsum_add, IH. cbn [rsum]. reflexivity.
Qed.
(* the first index at which a test holds *)
Lemma first_true : forall (f : nat -> bool) a, f a = true ->
exists a0, (a0 <= a)%nat /\ f a0 = true /\ forall a', (a' < a0)%nat -> f a' = false.
Proof.
intros f a Ha. assert (Hd : forall k, f k = true \/ ~ f k = true) by (intro k; destruct (f k); [left | right]; congruence).
assert (G : forall m, (exists k, (k < m)%nat /\ f k = true) ->
exists a0, (a0 < m)%nat /\ f a0 = true /\ forall a', (a' < a0)%nat -> f a' = false).
{ induction m as [|m IH]; intros (k & Hk & Hf); [lia|].
destruct (search m (fun k => f k = true) Hd) as [H|H].
- destruct (IH H) as (a0 & H0 & H1 & H2). exists a0. split; [lia | split; assumption].
- exists m. split; [lia|]. split.
+ destruct (Nat.eq_dec k m) as [->|E]; [exact Hf | exfalso; exact (H k ltac:(lia) Hf)].
+ intros a' Ha'. destruct (f a') eqn:E; [exfalso; exact (H a' Ha' E) | reflexivity]. }
destruct (G (S a) (ex_intro _ a (conj (Nat.lt_succ_diag_r a) Ha))) as (a0 & H0 & H1 & H2).
exists a0. split; [lia | split; assumption].
Qed.
(* ---- the inputs that move a row toward its comparator -------------------------------------------------------- *)
(* the weight with which a row reads position j, 0 if it does not *)
Definition wgt (u : tu) (j : nat) : Z := fold_right (fun p a => if Nat.eqb (fst p) j then snd p else a) 0%Z (tin u).
Lemma wgt_in : forall u j z, NoDup (map fst (tin u)) -> In (j, z) (tin u) -> wgt u j = z.
Proof.
intros [b ins] j z. unfold wgt. cbn [tin]. induction ins as [|[j' z'] t IH]; intros Hnd Hin; [destruct Hin|].
cbn [fold_right fst snd]. cbn [map fst] in Hnd. inversion Hnd as [|? ? Hj Ht]; subst. destruct Hin as [E|Hin].
- injection E as -> ->. rewrite Nat.eqb_refl. reflexivity.