internlm/Lean-Github huggingface dataset:
Theorem: HMem.Trace.CostedProgram.splitTimeCost
Proof state before:
α : Type u_1
inst✝⁵ : Complexity.Coding α Memory
β : Type u_2
inst✝⁴ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
γ δ : Type
inst✝³ : Complexity.Coding γ Memory
inst✝² : Complexity.Encoding δ Memory
fs : γ → δ
cs : Complexity.CostFunction γ ℕ
inst✝¹ : Complexity.Computable Encoding.Model fs
inst✝ : Complexity Encoding.Model fs cs
size : α → ℕ
fm : α → Option Memory
fcp : CostedProgram
hf : Program.sound (TracedProgram.toProgram (toTracedProgram fcp)) f size
dst✝ src✝ : Source
next✝ : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (recurse dst✝ src✝ next✝)) fm
x✝¹ : α
x✝ : Memory
hm : x✝ ∈ fm x✝¹
⊢ Stack.timeCost
      (Stack.execution
        {
          state :=
            Complexity.encode
              (Option.get (Complexity.decode α (Memory.getms x✝ src✝))
                (_ : Option.isSome (Complexity.decode α (Memory.getms x✝ src✝)) = true)),
          current := toProgram fcp, function := toProgram fcp }
        [])
      (_ :
        Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp))
          (Complexity.encode
            (Option.get (Complexity.decode α (Memory.getms x✝ src✝))
              (_ : Option.isSome (Complexity.decode α (Memory.getms x✝ src✝)) = true)))) ≤
    Program.timeCost (TracedProgram.toProgram (toTracedProgram fcp))
      (_ :
        Program.haltsOn (TracedProgram.toProgram (toTracedProgram fcp))
          (Complexity.encode
            (Option.get ((Complexity.decode α ∘ flip Memory.getms src✝) x✝)
              (_ : Option.isSome (Complexity.decode α (Memory.getms x✝ src✝)) = true))))
Tactic:
apply le_refl
Proof state after:
no goals
Theorem: HMem.Program.splitTimeCost
Proof state before:
TracedProgram : Sort ?u.211566
α : Type u_1
inst✝⁶ : Complexity.Coding α Memory
β : Type u_2
inst✝⁵ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
γ δ : Type
inst✝⁴ : Complexity.Coding γ Memory
inst✝³ : Complexity.Encoding δ Memory
fs : γ → δ
cs : Complexity.CostFunction γ ℕ
inst✝² : Complexity.Computable Encoding.Model fs
inst✝¹ : Complexity Encoding.Model fs cs
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
⊢ timeCost' p h ≤ subroutineTimeCost h + recurseTimeCost h + localTimeCost h
Tactic:
intro a
Proof state after:
TracedProgram : Sort ?u.211566
α : Type u_1
inst✝⁶ : Complexity.Coding α Memory
β : Type u_2
inst✝⁵ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
γ δ : Type
inst✝⁴ : Complexity.Coding γ Memory
inst✝³ : Complexity.Encoding δ Memory
fs : γ → δ
cs : Complexity.CostFunction γ ℕ
inst✝² : Complexity.Computable Encoding.Model fs
inst✝¹ : Complexity Encoding.Model fs cs
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ timeCost' p h a ≤ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a
Theorem: HMem.Program.splitTimeCost
Proof state before:
TracedProgram : Sort ?u.211566
α : Type u_1
inst✝⁶ : Complexity.Coding α Memory
β : Type u_2
inst✝⁵ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
γ δ : Type
inst✝⁴ : Complexity.Coding γ Memory
inst✝³ : Complexity.Encoding δ Memory
fs : γ → δ
cs : Complexity.CostFunction γ ℕ
inst✝² : Complexity.Computable Encoding.Model fs
inst✝¹ : Complexity Encoding.Model fs cs
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ timeCost' p h a ≤ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a
Tactic:
apply le_trans
Proof state after:
case a
TracedProgram : Sort ?u.211566
α : Type u_1
inst✝⁶ : Complexity.Coding α Memory
β : Type u_2
inst✝⁵ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
γ δ : Type
inst✝⁴ : Complexity.Coding γ Memory
inst✝³ : Complexity.Encoding δ Memory
fs : γ → δ
cs : Complexity.CostFunction γ ℕ
inst✝² : Complexity.Computable Encoding.Model fs
inst✝¹ : Complexity Encoding.Model fs cs
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ timeCost' p h a ≤ ?b

case a
TracedProgram : Sort ?u.211566
α : Type u_1
inst✝⁶ : Complexity.Coding α Memory
β : Type u_2
inst✝⁵ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
γ δ : Type
inst✝⁴ : Complexity.Coding γ Memory
inst✝³ : Complexity.Encoding δ Memory
fs : γ → δ
cs : Complexity.CostFunction γ ℕ
inst✝² : Complexity.Computable Encoding.Model fs
inst✝¹ : Complexity Encoding.Model fs cs
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ ?b ≤ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a

case b
TracedProgram : Sort ?u.211566
α : Type u_1
inst✝⁶ : Complexity.Coding α Memory
β : Type u_2
inst✝⁵ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
γ δ : Type
inst✝⁴ : Complexity.Coding γ Memory
inst✝³ : Complexity.Encoding δ Memory
fs : γ → δ
cs : Complexity.CostFunction γ ℕ
inst✝² : Complexity.Computable Encoding.Model fs
inst✝¹ : Complexity Encoding.Model fs cs
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ ℕ
Theorem: HMem.Program.splitTimeCost
Proof state before:
case a
TracedProgram : Sort ?u.211566
α : Type u_1
inst✝⁶ : Complexity.Coding α Memory
β : Type u_2
inst✝⁵ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
γ δ : Type
inst✝⁴ : Complexity.Coding γ Memory
inst✝³ : Complexity.Encoding δ Memory
fs : γ → δ
cs : Complexity.CostFunction γ ℕ
inst✝² : Complexity.Computable Encoding.Model fs
inst✝¹ : Complexity Encoding.Model fs cs
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ timeCost' p h a ≤ ?b

case a
TracedProgram : Sort ?u.211566
α : Type u_1
inst✝⁶ : Complexity.Coding α Memory
β : Type u_2
inst✝⁵ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
γ δ : Type
inst✝⁴ : Complexity.Coding γ Memory
inst✝³ : Complexity.Encoding δ Memory
fs : γ → δ
cs : Complexity.CostFunction γ ℕ
inst✝² : Complexity.Computable Encoding.Model fs
inst✝¹ : Complexity Encoding.Model fs cs
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ ?b ≤ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a

case b
TracedProgram : Sort ?u.211566
α : Type u_1
inst✝⁶ : Complexity.Coding α Memory
β : Type u_2
inst✝⁵ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
γ δ : Type
inst✝⁴ : Complexity.Coding γ Memory
inst✝³ : Complexity.Encoding δ Memory
fs : γ → δ
cs : Complexity.CostFunction γ ℕ
inst✝² : Complexity.Computable Encoding.Model fs
inst✝¹ : Complexity Encoding.Model fs cs
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ ℕ
Tactic:
exact (Stack.timeCost_le_iff _ (Program.halts_of_sound h _)).mp (p.costedMatches ▸ p.costed.splitTimeCost (costed_sound h) (costed_sound' h) a _ (Option.mem_some_iff.mpr rfl))
Proof state after:
case a
TracedProgram : Sort ?u.211566
α : Type u_1
inst✝⁶ : Complexity.Coding α Memory
β : Type u_2
inst✝⁵ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
γ δ : Type
inst✝⁴ : Complexity.Coding γ Memory
inst✝³ : Complexity.Encoding δ Memory
fs : γ → δ
cs : Complexity.CostFunction γ ℕ
inst✝² : Complexity.Computable Encoding.Model fs
inst✝¹ : Complexity Encoding.Model fs cs
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ (Trace.CostedProgram.subroutineTimeCost
            (_ :
              Trace.TracedProgram.sound' f sz (Trace.CostedProgram.toTracedProgram (costed p))
                (some ∘ Complexity.encode)) +
          Trace.CostedProgram.recurseTimeCost
            (_ : sound (Trace.TracedProgram.toProgram (Trace.CostedProgram.toTracedProgram (costed p))) f sz)
            (_ :
              Trace.TracedProgram.sound' f sz (Trace.CostedProgram.toTracedProgram (costed p))
                (some ∘ Complexity.encode)) +
        Trace.CostedProgram.localTimeCost
          (_ :
            Trace.TracedProgram.sound' f sz (Trace.CostedProgram.toTracedProgram (costed p))
              (some ∘ Complexity.encode)))
      a ≤
    (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a
Theorem: HMem.Program.splitTimeCost
Proof state before:
case a
TracedProgram : Sort ?u.211566
α : Type u_1
inst✝⁶ : Complexity.Coding α Memory
β : Type u_2
inst✝⁵ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
γ δ : Type
inst✝⁴ : Complexity.Coding γ Memory
inst✝³ : Complexity.Encoding δ Memory
fs : γ → δ
cs : Complexity.CostFunction γ ℕ
inst✝² : Complexity.Computable Encoding.Model fs
inst✝¹ : Complexity Encoding.Model fs cs
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ (Trace.CostedProgram.subroutineTimeCost
            (_ :
              Trace.TracedProgram.sound' f sz (Trace.CostedProgram.toTracedProgram (costed p))
                (some ∘ Complexity.encode)) +
          Trace.CostedProgram.recurseTimeCost
            (_ : sound (Trace.TracedProgram.toProgram (Trace.CostedProgram.toTracedProgram (costed p))) f sz)
            (_ :
              Trace.TracedProgram.sound' f sz (Trace.CostedProgram.toTracedProgram (costed p))
                (some ∘ Complexity.encode)) +
        Trace.CostedProgram.localTimeCost
          (_ :
            Trace.TracedProgram.sound' f sz (Trace.CostedProgram.toTracedProgram (costed p))
              (some ∘ Complexity.encode)))
      a ≤
    (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a
Tactic:
exact le_refl _
Proof state after:
no goals
Theorem: HMem.Encoding.encode_sum_getm_t
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : Encoding α Memory
inst✝ : Encoding β Memory
v : α ⊕ β
⊢ Memory.getm (encode v) true = 0
Tactic:
cases v <;> simp
Proof state after:
no goals
Theorem: HMem.Encoding.encodeList_inj
Proof state before:
α : Type u_1
inst✝ : Encoding α Memory
head✝ : α
tail✝ : List α
⊢ encodeList [] = encodeList (head✝ :: tail✝) → [] = head✝ :: tail✝
Tactic:
simp[encodeList]
Proof state after:
no goals
Theorem: HMem.Encoding.encodeList_inj
Proof state before:
α : Type u_1
inst✝ : Encoding α Memory
head✝ : α
tail✝ : List α
⊢ encodeList (head✝ :: tail✝) = encodeList [] → head✝ :: tail✝ = []
Tactic:
simp[encodeList]
Proof state after:
no goals
Theorem: HMem.Encoding.encodeList_inj
Proof state before:
α : Type u_1
inst✝ : Encoding α Memory
head✝¹ : α
lhs : List α
head✝ : α
rhs : List α
⊢ encodeList (head✝¹ :: lhs) = encodeList (head✝ :: rhs) → head✝¹ :: lhs = head✝ :: rhs
Tactic:
simp[encodeList, Iff.intro (encodeList_inj lhs rhs) λ h ↦ h ▸ rfl]
Proof state after:
no goals
Theorem: HMem.Encoding.rawDecodeList_inv
Proof state before:
α : Type u_1
inst✝ : Coding α Memory
head✝ : α
tl : List α
⊢ decodeList (encodeList (head✝ :: tl)) = some (head✝ :: tl)
Tactic:
simpa [encodeList, decodeList, rawDecodeList] using rawDecodeList_inv tl
Proof state after:
no goals
Theorem: HMem.Encoding.tupleInj_eq
Proof state before:
α : Type u_1
inst✝ : Encoding α Memory
N₀ N₁ : ℕ
f₀ : Fin N₀ → α
f₁ : Fin N₁ → α
⊢ (encode f₀ = encode f₁) = (N₀ = N₁ ∧ HEq f₀ f₁)
Tactic:
simp [encodeFinTuple_def, List.ofFn_inj']
Proof state after:
no goals
Theorem: HMem.Encoding.encodeOp_inj
Proof state before:
α : Type u_1
inst✝ : Encoding α Memory
f₀ f₁ : (Fin 0 → Bool) → α
⊢ encodeOp f₀ = encodeOp f₁ → f₀ = f₁
Tactic:
simpa [encodeOp] using λ h ↦ funext λ x ↦ Subsingleton.elim _ x ▸ h
Proof state after:
no goals
Theorem: HMem.Encoding.encodeOp_inj
Proof state before:
α : Type u_1
inst✝ : Encoding α Memory
N : ℕ
f₀ f₁ : (Fin (N + 1) → Bool) → α
⊢ encodeOp f₀ = encodeOp f₁ → f₀ = f₁
Tactic:
simpa [encodeOp,
  λ b ↦ Iff.intro
    (encodeOp_inj
      (f₀ ∘ (Fin.cons (α := λ _ ↦ Bool) b))
      (f₁ ∘ (Fin.cons (α := λ _ ↦ Bool) b)))
    (λ h ↦ h ▸ rfl)]
  using λ hf ht ↦ funext λ y ↦ Fin.cons_self_tail y ▸
    match y 0 with
    | false => congrFun hf (Fin.tail y)
    | true => congrFun ht (Fin.tail y)
Proof state after:
no goals
Theorem: HMem.Encoding.decodeOp_inv
Proof state before:
α : Type u_1
inst✝ : Coding α Memory
x✝ : (Fin 0 → Bool) → α
⊢ decodeOp (encodeOp x✝) = some x✝
Tactic:
simpa [decodeOp, encodeOp]
using funext λ _ ↦ congrArg _ (funext finZeroElim)
Proof state after:
no goals
Theorem: HMem.Encoding.decodeOp_inv
Proof state before:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
⊢ decodeOp (encodeOp g) = some g
Tactic:
simp [decodeOp, encodeOp, decodeOp_inv (N := N)]
Proof state after:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
⊢ (fun g_1 =>
      match g_1 0 with
      | false => g (Fin.cons false (Fin.tail g_1))
      | true => g (Fin.cons true (Fin.tail g_1))) =
    g
Theorem: HMem.Encoding.decodeOp_inv
Proof state before:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
⊢ (fun g_1 =>
      match g_1 0 with
      | false => g (Fin.cons false (Fin.tail g_1))
      | true => g (Fin.cons true (Fin.tail g_1))) =
    g
Tactic:
apply funext
Proof state after:
case h
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
⊢ ∀ (x : Fin (N + 1) → Bool),
    (match x 0 with
      | false => g (Fin.cons false (Fin.tail x))
      | true => g (Fin.cons true (Fin.tail x))) =
      g x
Theorem: HMem.Encoding.decodeOp_inv
Proof state before:
case h
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
⊢ ∀ (x : Fin (N + 1) → Bool),
    (match x 0 with
      | false => g (Fin.cons false (Fin.tail x))
      | true => g (Fin.cons true (Fin.tail x))) =
      g x
Tactic:
intro x
Proof state after:
case h
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
x : Fin (N + 1) → Bool
⊢ (match x 0 with
    | false => g (Fin.cons false (Fin.tail x))
    | true => g (Fin.cons true (Fin.tail x))) =
    g x
Theorem: HMem.Encoding.decodeOp_inv
Proof state before:
case h
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
x : Fin (N + 1) → Bool
⊢ (match x 0 with
    | false => g (Fin.cons false (Fin.tail x))
    | true => g (Fin.cons true (Fin.tail x))) =
    g x
Tactic:
match h:x 0 with
| true =>
  apply congrArg g
  exact h ▸ Fin.cons_self_tail _
| false =>
  apply congrArg g
  exact h ▸ Fin.cons_self_tail _
Proof state after:
no goals
Theorem: HMem.Encoding.decodeOp_inv
Proof state before:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
x : Fin (N + 1) → Bool
h : x 0 = true
⊢ (match true with
    | false => g (Fin.cons false (Fin.tail x))
    | true => g (Fin.cons true (Fin.tail x))) =
    g x
Tactic:
apply congrArg g
Proof state after:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
x : Fin (N + 1) → Bool
h : x 0 = true
⊢ Fin.cons true (Fin.tail x) = x
Theorem: HMem.Encoding.decodeOp_inv
Proof state before:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
x : Fin (N + 1) → Bool
h : x 0 = true
⊢ Fin.cons true (Fin.tail x) = x
Tactic:
exact h ▸ Fin.cons_self_tail _
Proof state after:
no goals
Theorem: HMem.Encoding.decodeOp_inv
Proof state before:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
x : Fin (N + 1) → Bool
h : x 0 = false
⊢ (match false with
    | false => g (Fin.cons false (Fin.tail x))
    | true => g (Fin.cons true (Fin.tail x))) =
    g x
Tactic:
apply congrArg g
Proof state after:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
x : Fin (N + 1) → Bool
h : x 0 = false
⊢ Fin.cons false (Fin.tail x) = x
Theorem: HMem.Encoding.decodeOp_inv
Proof state before:
α : Type u_1
inst✝ : Coding α Memory
N : ℕ
g : (Fin (N + 1) → Bool) → α
x : Fin (N + 1) → Bool
h : x 0 = false
⊢ Fin.cons false (Fin.tail x) = x
Tactic:
exact h ▸ Fin.cons_self_tail _
Proof state after:
no goals
Theorem: HMem.Encoding.encodeOp_injN
Proof state before:
α : Type u_1
inst✝ : Encoding α Memory
N₁ : ℕ
x✝¹ : (Fin 0 → Bool) → α
x✝ : (Fin N₁ → Bool) → α
⊢ encode x✝¹ = encode x✝ → 0 = N₁
Tactic:
cases N₁ <;> simp [encodeOp_zeroDef, encodeOp_succDef]
Proof state after:
no goals
Theorem: HMem.Encoding.encodeOp_injN
Proof state before:
α : Type u_1
inst✝ : Encoding α Memory
N₀ : ℕ
x✝¹ : (Fin (N₀ + 1) → Bool) → α
x✝ : (Fin 0 → Bool) → α
⊢ encode x✝¹ = encode x✝ → N₀ + 1 = 0
Tactic:
simp [encodeOp_zeroDef, encodeOp_succDef]
Proof state after:
no goals
Theorem: HMem.Encoding.encodeOp_injN
Proof state before:
α : Type u_1
inst✝ : Encoding α Memory
N₀ N₁ : ℕ
f₀ : (Fin (N₀ + 1) → Bool) → α
f₁ : (Fin (N₁ + 1) → Bool) → α
⊢ encode f₀ = encode f₁ → N₀ + 1 = N₁ + 1
Tactic:
simpa [encodeOp_succDef] using λ _ ↦ encodeOp_injN
Proof state after:
no goals
Theorem: HMem.Encoding.encodeOp_injEq
Proof state before:
α : Type u_1
inst✝ : Encoding α Memory
N₀ N₁ : ℕ
f₀ : (Fin N₀ → Bool) → α
f₁ : (Fin N₁ → Bool) → α
h : encode f₀ = encode f₁
⊢ N₀ = N₁ ∧ HEq f₀ f₁
Tactic:
cases (encodeOp_injN h)
Proof state after:
case refl
α : Type u_1
inst✝ : Encoding α Memory
N₀ : ℕ
f₀ f₁ : (Fin N₀ → Bool) → α
h : encode f₀ = encode f₁
⊢ N₀ = N₀ ∧ HEq f₀ f₁
Theorem: HMem.Encoding.encodeOp_injEq
Proof state before:
case refl
α : Type u_1
inst✝ : Encoding α Memory
N₀ : ℕ
f₀ f₁ : (Fin N₀ → Bool) → α
h : encode f₀ = encode f₁
⊢ N₀ = N₀ ∧ HEq f₀ f₁
Tactic:
simp [h, ← encodeInjEq]
Proof state after:
no goals
Theorem: HMem.Encoding.encodeOp_injEq
Proof state before:
α : Type u_1
inst✝ : Encoding α Memory
N₀ N₁ : ℕ
f₀ : (Fin N₀ → Bool) → α
f₁ : (Fin N₁ → Bool) → α
h : N₀ = N₁ ∧ HEq f₀ f₁
⊢ encode f₀ = encode f₁
Tactic:
cases h.left
Proof state after:
case refl
α : Type u_1
inst✝ : Encoding α Memory
N₀ : ℕ
f₀ f₁ : (Fin N₀ → Bool) → α
h : N₀ = N₀ ∧ HEq f₀ f₁
⊢ encode f₀ = encode f₁
Theorem: HMem.Encoding.encodeOp_injEq
Proof state before:
case refl
α : Type u_1
inst✝ : Encoding α Memory
N₀ : ℕ
f₀ f₁ : (Fin N₀ → Bool) → α
h : N₀ = N₀ ∧ HEq f₀ f₁
⊢ encode f₀ = encode f₁
Tactic:
cases h.right
Proof state after:
case refl.refl
α : Type u_1
inst✝ : Encoding α Memory
N₀ : ℕ
f₀ : (Fin N₀ → Bool) → α
h : N₀ = N₀ ∧ HEq f₀ f₀
⊢ encode f₀ = encode f₀
Theorem: HMem.Encoding.encodeOp_injEq
Proof state before:
case refl.refl
α : Type u_1
inst✝ : Encoding α Memory
N₀ : ℕ
f₀ : (Fin N₀ → Bool) → α
h : N₀ = N₀ ∧ HEq f₀ f₀
⊢ encode f₀ = encode f₀
Tactic:
rfl
Proof state after:
no goals
Theorem: HMem.Encoding.encode_nat_def
Proof state before:
n : ℕ
⊢ encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
Tactic:
refine Nat.binaryRec' (n := n) Memory.zero_def'.symm ?hi
Proof state after:
case hi
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    (n = 0 → b = true) →
      encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2)) →
        encode (Nat.bit b n) =
          Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))
Theorem: HMem.Encoding.encode_nat_def
Proof state before:
case hi
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    (n = 0 → b = true) →
      encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2)) →
        encode (Nat.bit b n) =
          Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))
Tactic:
intro b n hn _
Proof state after:
case hi
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode (Nat.bit b n) =
    Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))
Theorem: HMem.Encoding.encode_nat_def
Proof state before:
case hi
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode (Nat.bit b n) =
    Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))
Tactic:
apply Eq.trans
Proof state after:
case hi.h₁
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode (Nat.bit b n) = ?hi.b

case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ ?hi.b = Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))

case hi.b
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ Memory
Theorem: HMem.Encoding.encode_nat_def
Proof state before:
case hi.h₁
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode (Nat.bit b n) = ?hi.b

case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ ?hi.b = Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))

case hi.b
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ Memory
Tactic:
apply congrArg (encode (α := List Bool))
Proof state after:
case hi.h₁
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ Nat.bits (Nat.bit b n) = ?m.80295

n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ List Bool

case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode ?m.80295 =
    Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))
Theorem: HMem.Encoding.encode_nat_def
Proof state before:
case hi.h₁
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ Nat.bits (Nat.bit b n) = ?m.80295

n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ List Bool

case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode ?m.80295 =
    Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))
Tactic:
apply Nat.bits_append_bit _ _ hn
Proof state after:
case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode (b :: Nat.bits n) =
    Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))
Theorem: HMem.Encoding.encode_nat_def
Proof state before:
case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode (b :: Nat.bits n) =
    Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))
Tactic:
apply Memory.mk_inj_iff.mpr
Proof state after:
case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ true = decide (Nat.bit b n ≠ 0) ∧
    encode b = encode (decide (Nat.bit b n % 2 = 1)) ∧ encodeList (Nat.bits n) = encode (Nat.bit b n / 2)
Theorem: HMem.Encoding.encode_nat_def
Proof state before:
case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ true = decide (Nat.bit b n ≠ 0) ∧
    encode b = encode (decide (Nat.bit b n % 2 = 1)) ∧ encodeList (Nat.bits n) = encode (Nat.bit b n / 2)
Tactic:
apply And.intro
Proof state after:
case hi.h₂.left
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ true = decide (Nat.bit b n ≠ 0)

case hi.h₂.right
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode b = encode (decide (Nat.bit b n % 2 = 1)) ∧ encodeList (Nat.bits n) = encode (Nat.bit b n / 2)