(* 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) 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))) Hw j' z' (or_intror H))). destruct (negb (Bool.eqb (E1 j) (E2 j)) && (sg * z * (1 - 2 * b2z (E2 j)) | ->]; 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.