Theorem: LoopProgram.ofLen_complete (FormalSystems/Computability/Loop.lean)

State before:
⊢ ∀ (p : LoopProgram), p ∈ ofLen (len p)
Tactic:
intro p
State after:
p : LoopProgram
⊢ p ∈ ofLen (len p)

State before:
p : LoopProgram
⊢ p ∈ ofLen (len p)
Tactic:
match p with
| add (.mk x) (.mk y) n =>
  apply ofLen_stmt_complete
  apply Or.inl; rfl
| sub (.mk x) (.mk y) m =>
  apply ofLen_stmt_complete
  apply Or.inr; rfl
| loop (.mk x) p =>
  dsimp [len]
  cases' x with x'
  match h: p.len with
  | 0 => exact False.elim $ Nat.ne_of_gt p.len_gt_zero h
  | 1 =>
    dsimp [ofLen, baseProgram]
    apply Finset.mem_union_right
    apply Finset.mem_image_of_mem
    exact lenOne_complete _ h
  | n + 1 =>
    apply ofLen_contains_extendLenOne_image
    rw [<- Nat.succ_eq_add_one, <- h]
    apply ofLen_complete
    cases p <;> simp [extendLenOne]
  apply ofLen_contains_extendLenOne_image
  case p => exact loop (.mk x') p
  have : p.len + x'.succ = (loop (.mk x') p).len := by rfl
  rw [this]
  apply ofLen_complete
  simp [extendLenOne]
| concat a b =>
  simp [len, ofLen]
  refine' .inr $ .inl (Finset.mem_fold_union_iff.mpr ⟨⟨a.len, _⟩, _⟩)
  rw [Finset.mem_range]; simp [len_gt_zero]
  simp; apply Finset.mem_product.mpr
  exact ⟨ofLen_complete _, ofLen_complete _⟩
State after:
no goals

State before:
p : LoopProgram
x y n : ℕ
⊢ add { index := x } { index := y } n ∈ ofLen (len (add { index := x } { index := y } n))
Tactic:
apply ofLen_stmt_complete
State after:
case h_stmt
p : LoopProgram
x y n : ℕ
⊢ add = add ∨ add = sub

State before:
case h_stmt
p : LoopProgram
x y n : ℕ
⊢ add = add ∨ add = sub
Tactic:
apply Or.inl
State after:
case h_stmt.h
p : LoopProgram
x y n : ℕ
⊢ add = add

State before:
case h_stmt.h
p : LoopProgram
x y n : ℕ
⊢ add = add
Tactic:
rfl
State after:
no goals

State before:
p : LoopProgram
x y m : ℕ
⊢ sub { index := x } { index := y } m ∈ ofLen (len (sub { index := x } { index := y } m))
Tactic:
apply ofLen_stmt_complete
State after:
case h_stmt
p : LoopProgram
x y m : ℕ
⊢ sub = add ∨ sub = sub

State before:
case h_stmt
p : LoopProgram
x y m : ℕ
⊢ sub = add ∨ sub = sub
Tactic:
apply Or.inr
State after:
case h_stmt.h
p : LoopProgram
x y m : ℕ
⊢ sub = sub

State before:
case h_stmt.h
p : LoopProgram
x y m : ℕ
⊢ sub = sub
Tactic:
rfl
State after:
no goals

State before:
p✝ : LoopProgram
x : ℕ
p : LoopProgram
⊢ loop { index := x } p ∈ ofLen (len (loop { index := x } p))
Tactic:
dsimp [len]
State after:
p✝ : LoopProgram
x : ℕ
p : LoopProgram
⊢ loop { index := x } p ∈ ofLen (len p + x + 1)

State before:
p✝ : LoopProgram
x : ℕ
p : LoopProgram
⊢ loop { index := x } p ∈ ofLen (len p + x + 1)
Tactic:
cases' x with x'
State after:
case zero
p✝ p : LoopProgram
⊢ loop { index := Nat.zero } p ∈ ofLen (len p + Nat.zero + 1)

case succ
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ ofLen (len p + Nat.succ x' + 1)

State before:
case zero
p✝ p : LoopProgram
⊢ loop { index := Nat.zero } p ∈ ofLen (len p + Nat.zero + 1)

case succ
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ ofLen (len p + Nat.succ x' + 1)
Tactic:
match h: p.len with
| 0 => exact False.elim $ Nat.ne_of_gt p.len_gt_zero h
| 1 =>
  dsimp [ofLen, baseProgram]
  apply Finset.mem_union_right
  apply Finset.mem_image_of_mem
  exact lenOne_complete _ h
| n + 1 =>
  apply ofLen_contains_extendLenOne_image
  rw [<- Nat.succ_eq_add_one, <- h]
  apply ofLen_complete
  cases p <;> simp [extendLenOne]
State after:
case succ
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ ofLen (len p + Nat.succ x' + 1)

State before:
case succ
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ ofLen (len p + Nat.succ x' + 1)
Tactic:
apply ofLen_contains_extendLenOne_image
State after:
case succ.h₁
p✝ p : LoopProgram
x' : ℕ
⊢ ?succ.p ∈ ofLen (len p + Nat.succ x')

case succ.h₂
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ extendLenOne ?succ.p

case succ.p
p✝ p : LoopProgram
x' : ℕ
⊢ LoopProgram

State before:
p✝ p : LoopProgram
x' : ℕ
⊢ LoopProgram
Tactic:
case p => exact loop (.mk x') p
State after:
no goals

State before:
case succ.h₁
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := x' } p ∈ ofLen (len p + Nat.succ x')

case succ.h₂
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ extendLenOne (loop { index := x' } p)
Tactic:
have : p.len + x'.succ = (loop (.mk x') p).len := by rfl
State after:
case succ.h₁
p✝ p : LoopProgram
x' : ℕ
this : len p + Nat.succ x' = len (loop { index := x' } p)
⊢ loop { index := x' } p ∈ ofLen (len p + Nat.succ x')

case succ.h₂
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ extendLenOne (loop { index := x' } p)

State before:
case succ.h₁
p✝ p : LoopProgram
x' : ℕ
this : len p + Nat.succ x' = len (loop { index := x' } p)
⊢ loop { index := x' } p ∈ ofLen (len p + Nat.succ x')

case succ.h₂
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ extendLenOne (loop { index := x' } p)
Tactic:
rw [this]
State after:
case succ.h₁
p✝ p : LoopProgram
x' : ℕ
this : len p + Nat.succ x' = len (loop { index := x' } p)
⊢ loop { index := x' } p ∈ ofLen (len (loop { index := x' } p))

case succ.h₂
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ extendLenOne (loop { index := x' } p)

State before:
case succ.h₁
p✝ p : LoopProgram
x' : ℕ
this : len p + Nat.succ x' = len (loop { index := x' } p)
⊢ loop { index := x' } p ∈ ofLen (len (loop { index := x' } p))

case succ.h₂
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ extendLenOne (loop { index := x' } p)
Tactic:
apply ofLen_complete
State after:
case succ.h₂
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ extendLenOne (loop { index := x' } p)

State before:
case succ.h₂
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ extendLenOne (loop { index := x' } p)
Tactic:
simp [extendLenOne]
State after:
no goals

State before:
p✝ p : LoopProgram
h : len p = 0
⊢ loop { index := Nat.zero } p ∈ ofLen (0 + Nat.zero + 1)
Tactic:
exact False.elim $ Nat.ne_of_gt p.len_gt_zero h
State after:
no goals

State before:
p✝ p : LoopProgram
h : len p = 1
⊢ loop { index := Nat.zero } p ∈ ofLen (1 + Nat.zero + 1)
Tactic:
dsimp [ofLen, baseProgram]
State after:
p✝ p : LoopProgram
h : len p = 1
⊢ loop { index := 0 } p ∈
    WellFounded.fix ofLen.proof_1
      (fun a a_1 =>
        (match (motive :=
            (x : ℕ) →
              ((y : ℕ) → (invImage (fun a => a) instWellFoundedRelation).1 y x → Finset LoopProgram) →
                Finset LoopProgram)
            a with
          | 0 => fun x => ∅
          | Nat.succ n => fun x =>
            Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                Finset.fold (fun x x_1 => x ∪ x_1) ∅
                  (fun x_1 => Finset.image (fun x => concat x.1 x.2) (Finset.product (x ↑x_1 ⋯) (x (n - ↑x_1) ⋯)))
                  (Finset.attach (Finset.range n)) ∪
              match n + 1 with
              | 0 => ∅
              | 1 => lenOne
              | 2 => Finset.image (loop { index := 0 }) lenOne
              | x => ∅)
          a_1)
      (1 + 1)

State before:
p✝ p : LoopProgram
h : len p = 1
⊢ loop { index := 0 } p ∈
    WellFounded.fix ofLen.proof_1
      (fun a a_1 =>
        (match (motive :=
            (x : ℕ) →
              ((y : ℕ) → (invImage (fun a => a) instWellFoundedRelation).1 y x → Finset LoopProgram) →
                Finset LoopProgram)
            a with
          | 0 => fun x => ∅
          | Nat.succ n => fun x =>
            Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                Finset.fold (fun x x_1 => x ∪ x_1) ∅
                  (fun x_1 => Finset.image (fun x => concat x.1 x.2) (Finset.product (x ↑x_1 ⋯) (x (n - ↑x_1) ⋯)))
                  (Finset.attach (Finset.range n)) ∪
              match n + 1 with
              | 0 => ∅
              | 1 => lenOne
              | 2 => Finset.image (loop { index := 0 }) lenOne
              | x => ∅)
          a_1)
      (1 + 1)
Tactic:
apply Finset.mem_union_right
State after:
case h
p✝ p : LoopProgram
h : len p = 1
⊢ loop { index := 0 } p ∈
    match 1 + 1 with
    | 0 => ∅
    | 1 => lenOne
    | 2 => Finset.image (loop { index := 0 }) lenOne
    | x => ∅

State before:
case h
p✝ p : LoopProgram
h : len p = 1
⊢ loop { index := 0 } p ∈
    match 1 + 1 with
    | 0 => ∅
    | 1 => lenOne
    | 2 => Finset.image (loop { index := 0 }) lenOne
    | x => ∅
Tactic:
apply Finset.mem_image_of_mem
State after:
case h.h
p✝ p : LoopProgram
h : len p = 1
⊢ p ∈ lenOne

State before:
case h.h
p✝ p : LoopProgram
h : len p = 1
⊢ p ∈ lenOne
Tactic:
exact lenOne_complete _ h
State after:
no goals

State before:
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ loop { index := Nat.zero } p ∈ ofLen (n + 1 + Nat.zero + 1)
Tactic:
apply ofLen_contains_extendLenOne_image
State after:
case h₁
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ ?p ∈ ofLen (n + 1)

case h₂
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ loop { index := Nat.zero } p ∈ extendLenOne ?p

case p
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ LoopProgram

State before:
case h₁
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ ?p ∈ ofLen (n + 1)

case h₂
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ loop { index := Nat.zero } p ∈ extendLenOne ?p

case p
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ LoopProgram
Tactic:
rw [<- Nat.succ_eq_add_one, <- h]
State after:
case h₁
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ ?p ∈ ofLen (len p)

case p
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ LoopProgram

case p
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ LoopProgram

case h₂
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ loop { index := Nat.zero } p ∈ extendLenOne ?p

case p
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ LoopProgram

State before:
case h₁
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ ?p ∈ ofLen (len p)

case p
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ LoopProgram

case p
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ LoopProgram

case h₂
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ loop { index := Nat.zero } p ∈ extendLenOne ?p

case p
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ LoopProgram
Tactic:
apply ofLen_complete
State after:
case h₂
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ loop { index := Nat.zero } p ∈ extendLenOne p

State before:
case h₂
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ loop { index := Nat.zero } p ∈ extendLenOne p
Tactic:
cases p <;> simp [extendLenOne]
State after:
no goals

State before:
p✝ p : LoopProgram
x' : ℕ
⊢ LoopProgram
Tactic:
exact loop (.mk x') p
State after:
no goals

State before:
p✝ p : LoopProgram
x' : ℕ
⊢ len p + Nat.succ x' = len (loop { index := x' } p)
Tactic:
rfl
State after:
no goals

State before:
p a b : LoopProgram
⊢ concat a b ∈ ofLen (len (concat a b))
Tactic:
simp [len, ofLen]
State after:
p a b : LoopProgram
⊢ concat a b ∈ Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (len a + len b)) ∨
    concat a b ∈
        Finset.fold (fun x x_1 => x ∪ x_1) ∅
          (fun x => Finset.image (fun x => concat x.1 x.2) (Finset.product (ofLen ↑x) (ofLen (len a + len b - ↑x))))
          (Finset.attach (Finset.range (len a + len b))) ∨
      concat a b ∈ baseProgram (len a + len b + 1)

State before:
p a b : LoopProgram
⊢ concat a b ∈ Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (len a + len b)) ∨
    concat a b ∈
        Finset.fold (fun x x_1 => x ∪ x_1) ∅
          (fun x => Finset.image (fun x => concat x.1 x.2) (Finset.product (ofLen ↑x) (ofLen (len a + len b - ↑x))))
          (Finset.attach (Finset.range (len a + len b))) ∨
      concat a b ∈ baseProgram (len a + len b + 1)
Tactic:
refine' .inr $ .inl (Finset.mem_fold_union_iff.mpr ⟨⟨a.len, _⟩, _⟩)
State after:
case refine'_1
p a b : LoopProgram
⊢ len a ∈ Finset.range (len a + len b)

case refine'_2
p a b : LoopProgram
⊢ { val := len a, property := ?refine'_1 } ∈ Finset.attach (Finset.range (len a + len b)) ∧
    concat a b ∈
      Finset.image (fun x => concat x.1 x.2)
        (Finset.product (ofLen ↑{ val := len a, property := ?refine'_1 })
          (ofLen (len a + len b - ↑{ val := len a, property := ?refine'_1 })))

State before:
case refine'_1
p a b : LoopProgram
⊢ len a ∈ Finset.range (len a + len b)

case refine'_2
p a b : LoopProgram
⊢ { val := len a, property := ?refine'_1 } ∈ Finset.attach (Finset.range (len a + len b)) ∧
    concat a b ∈
      Finset.image (fun x => concat x.1 x.2)
        (Finset.product (ofLen ↑{ val := len a, property := ?refine'_1 })
          (ofLen (len a + len b - ↑{ val := len a, property := ?refine'_1 })))
Tactic:
rw [Finset.mem_range]
State after:
case refine'_1
p a b : LoopProgram
⊢ len a < len a + len b

case refine'_2
p a b : LoopProgram
⊢ { val := len a, property := ⋯ } ∈ Finset.attach (Finset.range (len a + len b)) ∧
    concat a b ∈
      Finset.image (fun x => concat x.1 x.2)
        (Finset.product (ofLen ↑{ val := len a, property := ⋯ })
          (ofLen (len a + len b - ↑{ val := len a, property := ⋯ })))

State before:
case refine'_1
p a b : LoopProgram
⊢ len a < len a + len b

case refine'_2
p a b : LoopProgram
⊢ { val := len a, property := ⋯ } ∈ Finset.attach (Finset.range (len a + len b)) ∧
    concat a b ∈
      Finset.image (fun x => concat x.1 x.2)
        (Finset.product (ofLen ↑{ val := len a, property := ⋯ })
          (ofLen (len a + len b - ↑{ val := len a, property := ⋯ })))
Tactic:
simp [len_gt_zero]
State after:
case refine'_2
p a b : LoopProgram
⊢ { val := len a, property := ⋯ } ∈ Finset.attach (Finset.range (len a + len b)) ∧
    concat a b ∈
      Finset.image (fun x => concat x.1 x.2)
        (Finset.product (ofLen ↑{ val := len a, property := ⋯ })
          (ofLen (len a + len b - ↑{ val := len a, property := ⋯ })))

State before:
case refine'_2
p a b : LoopProgram
⊢ { val := len a, property := ⋯ } ∈ Finset.attach (Finset.range (len a + len b)) ∧
    concat a b ∈
      Finset.image (fun x => concat x.1 x.2)
        (Finset.product (ofLen ↑{ val := len a, property := ⋯ })
          (ofLen (len a + len b - ↑{ val := len a, property := ⋯ })))
Tactic:
simp
State after:
case refine'_2
p a b : LoopProgram
⊢ (a, b) ∈ Finset.product (ofLen (len a)) (ofLen (len b))

State before:
case refine'_2
p a b : LoopProgram
⊢ (a, b) ∈ Finset.product (ofLen (len a)) (ofLen (len b))
Tactic:
apply Finset.mem_product.mpr
State after:
case refine'_2
p a b : LoopProgram
⊢ (a, b).1 ∈ ofLen (len a) ∧ (a, b).2 ∈ ofLen (len b)

State before:
case refine'_2
p a b : LoopProgram
⊢ (a, b).1 ∈ ofLen (len a) ∧ (a, b).2 ∈ ofLen (len b)
Tactic:
exact ⟨ofLen_complete _, ofLen_complete _⟩
State after:
no goals