Theorem: ConsExp.decode_encode (Fine/Util/ConsExp.lean)

State before:
c : ConsExp
⊢ decode (encode c) = c
Tactic:
induction c
State after:
case nat
a✝ : ℕ
⊢ decode (encode (nat a✝)) = nat a✝

case cons
a✝¹ a✝ : ConsExp
a_ih✝¹ : decode (encode a✝¹) = a✝¹
a_ih✝ : decode (encode a✝) = a✝
⊢ decode (encode (cons a✝¹ a✝)) = cons a✝¹ a✝

State before:
case cons
a✝¹ a✝ : ConsExp
a_ih✝¹ : decode (encode a✝¹) = a✝¹
a_ih✝ : decode (encode a✝) = a✝
⊢ decode (encode (cons a✝¹ a✝)) = cons a✝¹ a✝
Tactic:
next hf hg =>
  rw [encode, decode]
  split
  next h => simp at h
  next h =>
    simp [Nat.div2_val] at h
    cases h
    simp [*]
State after:
no goals

State before:
a✝ m✝ : ℕ
h : Nat.boddDiv2 (2 * a✝) = (false, m✝)
⊢ nat m✝ = nat a✝
Tactic:
simp [Nat.div2_val] at h
State after:
a✝ m✝ : ℕ
h : a✝ = m✝
⊢ nat m✝ = nat a✝

State before:
a✝ m✝ : ℕ
h : a✝ = m✝
⊢ nat m✝ = nat a✝
Tactic:
simp [*]
State after:
no goals

State before:
a✝ m✝ : ℕ
h : Nat.boddDiv2 (2 * a✝) = (true, m✝)
⊢ (match hm : Nat.unpair m✝ with
    | (f, g) =>
      let_fun hn' := (_ : 1 ≤ 2 * a✝);
      let_fun this := (_ : m✝ < 2 * a✝);
      let_fun this_1 := (_ : f < 2 * a✝);
      let_fun this := (_ : g < 2 * a✝);
      cons (decode f) (decode g)) =
    nat a✝
Tactic:
simp at h
State after:
no goals

State before:
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
⊢ decode (encode (cons a✝¹ a✝)) = cons a✝¹ a✝
Tactic:
rw [encode, decode]
State after:
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
⊢ (match hn : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) with
    | (false, m) => nat m
    | (true, m) =>
      match hm : Nat.unpair m with
      | (f, g) =>
        let_fun hn' := (_ : 1 ≤ 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
        let_fun this := (_ : m < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
        let_fun this_1 := (_ : f < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
        let_fun this := (_ : g < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
        cons (decode f) (decode g)) =
    cons a✝¹ a✝

State before:
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
⊢ (match hn : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) with
    | (false, m) => nat m
    | (true, m) =>
      match hm : Nat.unpair m with
      | (f, g) =>
        let_fun hn' := (_ : 1 ≤ 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
        let_fun this := (_ : m < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
        let_fun this_1 := (_ : f < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
        let_fun this := (_ : g < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
        cons (decode f) (decode g)) =
    cons a✝¹ a✝
Tactic:
split
State after:
case h_1
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
m✝ : ℕ
heq✝ : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) = (false, m✝)
⊢ nat m✝ = cons a✝¹ a✝

case h_2
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
m✝ : ℕ
heq✝ : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) = (true, m✝)
⊢ (match hm : Nat.unpair m✝ with
    | (f, g) =>
      let_fun hn' := (_ : 1 ≤ 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : m✝ < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this_1 := (_ : f < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : g < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      cons (decode f) (decode g)) =
    cons a✝¹ a✝

State before:
case h_1
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
m✝ : ℕ
heq✝ : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) = (false, m✝)
⊢ nat m✝ = cons a✝¹ a✝

case h_2
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
m✝ : ℕ
heq✝ : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) = (true, m✝)
⊢ (match hm : Nat.unpair m✝ with
    | (f, g) =>
      let_fun hn' := (_ : 1 ≤ 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : m✝ < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this_1 := (_ : f < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : g < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      cons (decode f) (decode g)) =
    cons a✝¹ a✝
Tactic:
next h => simp at h
State after:
case h_2
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
m✝ : ℕ
heq✝ : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) = (true, m✝)
⊢ (match hm : Nat.unpair m✝ with
    | (f, g) =>
      let_fun hn' := (_ : 1 ≤ 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : m✝ < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this_1 := (_ : f < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : g < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      cons (decode f) (decode g)) =
    cons a✝¹ a✝

State before:
case h_2
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
m✝ : ℕ
heq✝ : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) = (true, m✝)
⊢ (match hm : Nat.unpair m✝ with
    | (f, g) =>
      let_fun hn' := (_ : 1 ≤ 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : m✝ < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this_1 := (_ : f < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : g < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      cons (decode f) (decode g)) =
    cons a✝¹ a✝
Tactic:
next h =>
  simp [Nat.div2_val] at h
  cases h
  simp [*]
State after:
no goals

State before:
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
m✝ : ℕ
h : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) = (false, m✝)
⊢ nat m✝ = cons a✝¹ a✝
Tactic:
simp at h
State after:
no goals

State before:
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
m✝ : ℕ
h : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) = (true, m✝)
⊢ (match hm : Nat.unpair m✝ with
    | (f, g) =>
      let_fun hn' := (_ : 1 ≤ 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : m✝ < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this_1 := (_ : f < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : g < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      cons (decode f) (decode g)) =
    cons a✝¹ a✝
Tactic:
simp [Nat.div2_val] at h
State after:
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
m✝ : ℕ
h✝ : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) = (true, m✝)
h : Nat.mkpair (encode a✝¹) (encode a✝) = m✝
⊢ (match hm : Nat.unpair m✝ with
    | (f, g) =>
      let_fun hn' := (_ : 1 ≤ 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : m✝ < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this_1 := (_ : f < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : g < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      cons (decode f) (decode g)) =
    cons a✝¹ a✝

State before:
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
m✝ : ℕ
h✝ : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) = (true, m✝)
h : Nat.mkpair (encode a✝¹) (encode a✝) = m✝
⊢ (match hm : Nat.unpair m✝ with
    | (f, g) =>
      let_fun hn' := (_ : 1 ≤ 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : m✝ < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this_1 := (_ : f < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : g < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      cons (decode f) (decode g)) =
    cons a✝¹ a✝
Tactic:
cases h
State after:
case refl
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
h : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) = (true, Nat.mkpair (encode a✝¹) (encode a✝))
⊢ (match hm : Nat.unpair (Nat.mkpair (encode a✝¹) (encode a✝)) with
    | (f, g) =>
      let_fun hn' := (_ : 1 ≤ 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : Nat.mkpair (encode a✝¹) (encode a✝) < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this_1 := (_ : f < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : g < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      cons (decode f) (decode g)) =
    cons a✝¹ a✝

State before:
case refl
a✝¹ a✝ : ConsExp
hf : decode (encode a✝¹) = a✝¹
hg : decode (encode a✝) = a✝
h : Nat.boddDiv2 (2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1) = (true, Nat.mkpair (encode a✝¹) (encode a✝))
⊢ (match hm : Nat.unpair (Nat.mkpair (encode a✝¹) (encode a✝)) with
    | (f, g) =>
      let_fun hn' := (_ : 1 ≤ 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : Nat.mkpair (encode a✝¹) (encode a✝) < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this_1 := (_ : f < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      let_fun this := (_ : g < 2 * Nat.mkpair (encode a✝¹) (encode a✝) + 1);
      cons (decode f) (decode g)) =
    cons a✝¹ a✝
Tactic:
simp [*]
State after:
no goals