brgc_oneBit_step

proof body

Tactic-mode proof.

 218          oneBitDiff_snocBit_flip (p := brgcPath 0 0)
 219        simpa [brgcPath] using this
 220      · -- 1 → 0 (wrap), use symmetry
 221        have h : OneBitDiff (snocBit (brgcPath 0 0) false) (snocBit (brgcPath 0 0) true) :=
 222          oneBitDiff_snocBit_flip (p := brgcPath 0 0)
 223        have : OneBitDiff (snocBit (brgcPath 0 0) true) (snocBit (brgcPath 0 0) false) :=
 224          OneBitDiff_symm h
 225        simpa [brgcPath] using this
 226  | (d + 2), _ => by
 227      -- Inductive step: assume one-bit stepping for dimension `d+1`, prove for `d+2`.
 228      have ih :
 229          ∀ i : Fin (2 ^ (d + 1)), OneBitDiff (brgcPath (d + 1) i) (brgcPath (d + 1) (i + 1)) :=
 230        brgc_oneBit_step (d := d + 1) (Nat.succ_pos _)
 231      intro i
 232      classical
 233      let T : Nat := 2 ^ (d + 1)
 234      have hTT : 2 ^ (d + 2) = T + T := by
 235        simpa [T] using twoPow_succ_eq_add (d := d + 1)
 236      let left : Fin T → Pattern (d + 2) := fun k => snocBit (brgcPath (d + 1) k) false
 237      let right : Fin T → Pattern (d + 2) := fun k => snocBit (brgcPath (d + 1) (Fin.rev k)) true
 238      let i' : Fin (T + T) := i.cast hTT
 239
 240      have hTpos : 0 < T := pow_pos (by decide : 0 < (2 : Nat)) (d + 1)
 241      letI : NeZero T := ⟨Nat.ne_zero_of_lt hTpos⟩
 242      letI : NeZero (T + T) := ⟨Nat.ne_zero_of_lt (Nat.add_pos_left hTpos T)⟩
 243
 244      have hcast_succ : (i + 1).cast hTT = i' + 1 := by
 245        -- `cast` commutes with `+1` along definitional equalities
 246        simpa [i'] using (cast_add_one (n := 2 ^ (d + 2)) (m := T + T) (h := hTT) i)
 247
 248      -- Reduce to the `Fin (T+T)` index space.
 249      have hTTgoal : OneBitDiff (Fin.append left right i') (Fin.append left right (i' + 1)) := by
 250        -- case split on whether `i'` lies in the left or right half, and whether we cross a boundary
 251        induction i' using Fin.addCases with
 252        | left k =>
 253            -- i' = castAdd T k
 254            by_cases hk : k.val + 1 < T
 255            · -- successor stays in the left half
 256              have hk_big : (Fin.castAdd T k : Fin (T + T)).val + 1 < T + T := by
 257                -- k.val + 1 < T ≤ T+T
 258                exact lt_of_lt_of_le hk (Nat.le_add_right T T)
 259              have hnext : (Fin.castAdd T k : Fin (T + T)) + 1 = Fin.castAdd T (k + 1) := by
 260                apply Fin.ext
 261                have hk1 : (k + 1).val = k.val + 1 :=
 262                  Fin.val_add_one_of_lt' (n := T) (i := k) hk
 263                have hk'1 : ((Fin.castAdd T k : Fin (T + T)) + 1).val =
 264                    (Fin.castAdd T k : Fin (T + T)).val + 1 :=
 265                  Fin.val_add_one_of_lt' (n := T + T) (i := Fin.castAdd T k) hk_big
 266                simpa [hk1] using hk'1
 267              -- adjacency comes from IH in dimension d+1, lifted through `snocBit`
 268              have hstep : OneBitDiff (brgcPath (d + 1) k) (brgcPath (d + 1) (k + 1)) := ih k
 269              have hstep' : OneBitDiff (left k) (left (k + 1)) :=
 270                oneBitDiff_snocBit_same false hstep
 271              -- rewrite the `append` evaluations
 272              simpa [Fin.append_left, hnext, left, right] using hstep'
 273            · -- boundary: last element of left half steps into the first element of right half
 274              have hkval : k.val = T - 1 := by
 275                have hle : k.val + 1 ≤ T := Nat.succ_le_of_lt k.isLt
 276                have hge : T ≤ k.val + 1 := Nat.le_of_not_gt hk
 277                have : k.val + 1 = T := Nat.le_antisymm hle hge
 278                exact Nat.eq_sub_of_add_eq this
 279              have hnext : (Fin.castAdd T k : Fin (T + T)) + 1 = Fin.natAdd T 0 := by
 280                apply Fin.ext
 281                -- both have value `T`
 282                have hT1 : 1 ≤ T := Nat.succ_le_of_lt hTpos
 283                have hkplus : (Fin.castAdd T k : Fin (T + T)).val + 1 = T := by
 284                  -- `(castAdd T k).val = k.val = T-1`
 285                  simpa [hkval, Nat.sub_add_cancel hT1]
 286                have hk_big : (Fin.castAdd T k : Fin (T + T)).val + 1 < T + T := by
 287                  -- `T < T+T` since `T>0`
 288                  have hT1 : 1 ≤ T := Nat.succ_le_of_lt hTpos
 289                  have hTlt : T < T + T := by
 290                    have hle : T + 1 ≤ T + T := Nat.add_le_add_left hT1 T
 291                    exact lt_of_lt_of_le (Nat.lt_succ_self T) hle
 292                  -- rewrite the LHS using `hkplus : (castAdd ...).val + 1 = T`
 293                  exact hkplus.symm ▸ hTlt
 294                have hk'1 : ((Fin.castAdd T k : Fin (T + T)) + 1).val =
 295                    (Fin.castAdd T k : Fin (T + T)).val + 1 :=
 296                  Fin.val_add_one_of_lt' (n := T + T) (i := Fin.castAdd T k) hk_big
 297                have hval : ((Fin.castAdd T k : Fin (T + T)) + 1).val = T := by
 298-- ... 128 more lines elided ...