Theorem: HMem.Encoding.encodeSource_inj (HMem/Encoding/Emulator.lean)

State before:
s₀ s₁ : Source
⊢ encodeSource s₀ = encodeSource s₁ → s₀ = s₁
Tactic:
cases h₀:s₀ <;> cases h₁:s₁
State after:
case nil.nil
s₀ s₁ : Source
h₀ : s₀ = Source.nil
h₁ : s₁ = Source.nil
⊢ encodeSource Source.nil = encodeSource Source.nil → Source.nil = Source.nil

case nil.imm
s₀ s₁ : Source
h₀ : s₀ = Source.nil
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource Source.nil = encodeSource (Source.imm hd✝ tl✝) → Source.nil = Source.imm hd✝ tl✝

case nil.idx
s₀ s₁ : Source
h₀ : s₀ = Source.nil
hd✝ tl✝ : Source
h₁ : s₁ = Source.idx hd✝ tl✝
⊢ encodeSource Source.nil = encodeSource (Source.idx hd✝ tl✝) → Source.nil = Source.idx hd✝ tl✝

case imm.nil
s₀ s₁ : Source
hd✝ : Bool
tl✝ : Source
h₀ : s₀ = Source.imm hd✝ tl✝
h₁ : s₁ = Source.nil
⊢ encodeSource (Source.imm hd✝ tl✝) = encodeSource Source.nil → Source.imm hd✝ tl✝ = Source.nil

case imm.imm
s₀ s₁ : Source
hd✝¹ : Bool
tl✝¹ : Source
h₀ : s₀ = Source.imm hd✝¹ tl✝¹
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource (Source.imm hd✝¹ tl✝¹) = encodeSource (Source.imm hd✝ tl✝) → Source.imm hd✝¹ tl✝¹ = Source.imm hd✝ tl✝

case imm.idx
s₀ s₁ : Source
hd✝¹ : Bool
tl✝¹ : Source
h₀ : s₀ = Source.imm hd✝¹ tl✝¹
hd✝ tl✝ : Source
h₁ : s₁ = Source.idx hd✝ tl✝
⊢ encodeSource (Source.imm hd✝¹ tl✝¹) = encodeSource (Source.idx hd✝ tl✝) → Source.imm hd✝¹ tl✝¹ = Source.idx hd✝ tl✝

case idx.nil
s₀ s₁ hd✝ tl✝ : Source
h₀ : s₀ = Source.idx hd✝ tl✝
h₁ : s₁ = Source.nil
⊢ encodeSource (Source.idx hd✝ tl✝) = encodeSource Source.nil → Source.idx hd✝ tl✝ = Source.nil

case idx.imm
s₀ s₁ hd✝¹ tl✝¹ : Source
h₀ : s₀ = Source.idx hd✝¹ tl✝¹
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource (Source.idx hd✝¹ tl✝¹) = encodeSource (Source.imm hd✝ tl✝) → Source.idx hd✝¹ tl✝¹ = Source.imm hd✝ tl✝

case idx.idx
s₀ s₁ hd✝¹ tl✝¹ : Source
h₀ : s₀ = Source.idx hd✝¹ tl✝¹
hd✝ tl✝ : Source
h₁ : s₁ = Source.idx hd✝ tl✝
⊢ encodeSource (Source.idx hd✝¹ tl✝¹) = encodeSource (Source.idx hd✝ tl✝) → Source.idx hd✝¹ tl✝¹ = Source.idx hd✝ tl✝

State before:
s₀ s₁ : Source
hd✝¹ : Bool
tl✝¹ : Source
h₀ : s₀ = Source.imm hd✝¹ tl✝¹
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource (Source.imm hd✝¹ tl✝¹) = encodeSource (Source.imm hd✝ tl✝) → Source.imm hd✝¹ tl✝¹ = Source.imm hd✝ tl✝
Tactic:
case imm.imm => simpa [encodeSource] using λ hhd htl ↦ ⟨hhd, encodeSource_inj htl⟩
State after:
no goals

State before:
s₀ s₁ hd✝¹ tl✝¹ : Source
h₀ : s₀ = Source.idx hd✝¹ tl✝¹
hd✝ tl✝ : Source
h₁ : s₁ = Source.idx hd✝ tl✝
⊢ encodeSource (Source.idx hd✝¹ tl✝¹) = encodeSource (Source.idx hd✝ tl✝) → Source.idx hd✝¹ tl✝¹ = Source.idx hd✝ tl✝
Tactic:
case idx.idx => simpa [encodeSource] using λ hhd htl ↦ ⟨encodeSource_inj hhd, encodeSource_inj htl⟩
State after:
no goals

State before:
case nil.nil
s₀ s₁ : Source
h₀ : s₀ = Source.nil
h₁ : s₁ = Source.nil
⊢ encodeSource Source.nil = encodeSource Source.nil → Source.nil = Source.nil

case nil.imm
s₀ s₁ : Source
h₀ : s₀ = Source.nil
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource Source.nil = encodeSource (Source.imm hd✝ tl✝) → Source.nil = Source.imm hd✝ tl✝

case nil.idx
s₀ s₁ : Source
h₀ : s₀ = Source.nil
hd✝ tl✝ : Source
h₁ : s₁ = Source.idx hd✝ tl✝
⊢ encodeSource Source.nil = encodeSource (Source.idx hd✝ tl✝) → Source.nil = Source.idx hd✝ tl✝

case imm.nil
s₀ s₁ : Source
hd✝ : Bool
tl✝ : Source
h₀ : s₀ = Source.imm hd✝ tl✝
h₁ : s₁ = Source.nil
⊢ encodeSource (Source.imm hd✝ tl✝) = encodeSource Source.nil → Source.imm hd✝ tl✝ = Source.nil

case imm.idx
s₀ s₁ : Source
hd✝¹ : Bool
tl✝¹ : Source
h₀ : s₀ = Source.imm hd✝¹ tl✝¹
hd✝ tl✝ : Source
h₁ : s₁ = Source.idx hd✝ tl✝
⊢ encodeSource (Source.imm hd✝¹ tl✝¹) = encodeSource (Source.idx hd✝ tl✝) → Source.imm hd✝¹ tl✝¹ = Source.idx hd✝ tl✝

case idx.nil
s₀ s₁ hd✝ tl✝ : Source
h₀ : s₀ = Source.idx hd✝ tl✝
h₁ : s₁ = Source.nil
⊢ encodeSource (Source.idx hd✝ tl✝) = encodeSource Source.nil → Source.idx hd✝ tl✝ = Source.nil

case idx.imm
s₀ s₁ hd✝¹ tl✝¹ : Source
h₀ : s₀ = Source.idx hd✝¹ tl✝¹
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource (Source.idx hd✝¹ tl✝¹) = encodeSource (Source.imm hd✝ tl✝) → Source.idx hd✝¹ tl✝¹ = Source.imm hd✝ tl✝
Tactic:
all_goals simp[encodeSource]
State after:
no goals

State before:
s₀ s₁ : Source
hd✝¹ : Bool
tl✝¹ : Source
h₀ : s₀ = Source.imm hd✝¹ tl✝¹
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource (Source.imm hd✝¹ tl✝¹) = encodeSource (Source.imm hd✝ tl✝) → Source.imm hd✝¹ tl✝¹ = Source.imm hd✝ tl✝
Tactic:
simpa [encodeSource] using λ hhd htl ↦ ⟨hhd, encodeSource_inj htl⟩
State after:
no goals

State before:
s₀ s₁ hd✝¹ tl✝¹ : Source
h₀ : s₀ = Source.idx hd✝¹ tl✝¹
hd✝ tl✝ : Source
h₁ : s₁ = Source.idx hd✝ tl✝
⊢ encodeSource (Source.idx hd✝¹ tl✝¹) = encodeSource (Source.idx hd✝ tl✝) → Source.idx hd✝¹ tl✝¹ = Source.idx hd✝ tl✝
Tactic:
simpa [encodeSource] using λ hhd htl ↦ ⟨encodeSource_inj hhd, encodeSource_inj htl⟩
State after:
no goals

State before:
case idx.imm
s₀ s₁ hd✝¹ tl✝¹ : Source
h₀ : s₀ = Source.idx hd✝¹ tl✝¹
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource (Source.idx hd✝¹ tl✝¹) = encodeSource (Source.imm hd✝ tl✝) → Source.idx hd✝¹ tl✝¹ = Source.imm hd✝ tl✝
Tactic:
simp[encodeSource]
State after:
no goals