oneBitDiff_snocBit_same

formal source

 120
 121/-! ## One-bit adjacency -/
 122
 123private theorem oneBitDiff_snocBit_same {d : Nat} {p q : Pattern d} (b : Bool) :
 124    OneBitDiff p q → OneBitDiff (snocBit p b) (snocBit q b) := by
 125  intro h
 126  classical
 127  rcases h with ⟨k, hk, hkuniq⟩
 128  refine ⟨k.castSucc, ?_, ?_⟩
 129  · simpa using hk
 130  · intro j hj
 131    -- any differing coordinate cannot be the new last coordinate (since it is fixed to `b`)
 132    induction j using Fin.lastCases with
 133    | last =>
 134        have : False := by
 135          simpa [snocBit] using hj
 136        exact this.elim
 137    | cast j =>
 138        have hj' : p j ≠ q j := by
 139          simpa [snocBit] using hj
 140        have : j = k := hkuniq j hj'
 141        simpa [this]
 142
 143private theorem oneBitDiff_snocBit_flip {d : Nat} (p : Pattern d) :
 144    OneBitDiff (snocBit p false) (snocBit p true) := by
 145  classical
 146  refine ⟨Fin.last d, ?_, ?_⟩
 147  · simp
 148  · intro j hj
 149    induction j using Fin.lastCases with
 150    | last => rfl
 151    | cast j =>
 152        have : False := by
 153          -- on old coordinates the patterns are equal