internlm/Lean-Github huggingface dataset:
Theorem: LoopProgram.ofLen_contains_extendLenOne_image
Proof state before:
case h.h
p : LoopProgram
n : ℕ
p' : LoopProgram
h₁ : p ∈ ofLen n
h₂ : p' ∈ extendLenOne p
⊢ ∃
    x ∈
      (fun y a =>
          Acc.rec
            (fun x₁ h ih =>
              (fun a a_1 =>
                  (match (motive :=
                      (x : ℕ) →
                        ((y : ℕ) → (invImage (fun a => sizeOf 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 =>
                              match x_1 with
                              | { val := l, property := h } =>
                                let_fun this := ⋯;
                                Finset.image
                                  (fun x =>
                                    match x with
                                    | (a, b) => concat a b)
                                  (Finset.product (x l ⋯) (x (n - l) ⋯)))
                            (Finset.attach (Finset.range n)) ∪
                        baseProgram (n + 1))
                    a_1)
                x₁ ih)
            ⋯)
        (Nat.add n 0) ⋯,
    p' ∈ extendLenOne x
Tactic:
exists p
Proof state after:
no goals
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
x y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ stmt { index := x } { index := y } n ∈ ofLen (x + y + n + 1)
Tactic:
simp [ofLen]
Proof state after:
x y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ stmt { index := x } { index := y } n ∈ Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (x + y + n)) ∨
    stmt { index := x } { index := y } n ∈
        Finset.fold (fun x x_1 => x ∪ x_1) ∅
          (fun x_1 => Finset.image (fun x => concat x.1 x.2) (Finset.product (ofLen ↑x_1) (ofLen (x + y + n - ↑x_1))))
          (Finset.attach (Finset.range (x + y + n))) ∨
      stmt { index := x } { index := y } n ∈ baseProgram (x + y + n + 1)
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
x y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ stmt { index := x } { index := y } n ∈ Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (x + y + n)) ∨
    stmt { index := x } { index := y } n ∈
        Finset.fold (fun x x_1 => x ∪ x_1) ∅
          (fun x_1 => Finset.image (fun x => concat x.1 x.2) (Finset.product (ofLen ↑x_1) (ofLen (x + y + n - ↑x_1))))
          (Finset.attach (Finset.range (x + y + n))) ∨
      stmt { index := x } { index := y } n ∈ baseProgram (x + y + n + 1)
Tactic:
cases' x with x'
Proof state after:
case zero
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ stmt { index := Nat.zero } { index := y } n ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.zero + y + n)) ∨
    stmt { index := Nat.zero } { index := y } n ∈
        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 (Nat.zero + y + n - ↑x))))
          (Finset.attach (Finset.range (Nat.zero + y + n))) ∨
      stmt { index := Nat.zero } { index := y } n ∈ baseProgram (Nat.zero + y + n + 1)

case succ
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.succ x' + y + n)) ∨
    stmt { index := Nat.succ x' } { index := y } n ∈
        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 (Nat.succ x' + y + n - ↑x))))
          (Finset.attach (Finset.range (Nat.succ x' + y + n))) ∨
      stmt { index := Nat.succ x' } { index := y } n ∈ baseProgram (Nat.succ x' + y + n + 1)
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case zero.succ
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.succ y' } n ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.zero + Nat.succ y' + n)) ∨
    stmt { index := Nat.zero } { index := Nat.succ y' } n ∈
        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 (Nat.zero + Nat.succ y' + n - ↑x))))
          (Finset.attach (Finset.range (Nat.zero + Nat.succ y' + n))) ∨
      stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ baseProgram (Nat.zero + Nat.succ y' + n + 1)

case succ
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.succ x' + y + n)) ∨
    stmt { index := Nat.succ x' } { index := y } n ∈
        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 (Nat.succ x' + y + n - ↑x))))
          (Finset.attach (Finset.range (Nat.succ x' + y + n))) ∨
      stmt { index := Nat.succ x' } { index := y } n ∈ baseProgram (Nat.succ x' + y + n + 1)
Tactic:
. apply Or.inl ∘ Finset.mem_fold_union_iff.mpr
  refine' ⟨stmt (.mk 0) (.mk y') n, ⟨_, _⟩⟩
  rw [Nat.add_succ, Nat.succ_add, Nat.succ_eq_add_one]
  apply ofLen_stmt_complete _ h_stmt
  cases' h_stmt with h h <;> rw [h] <;> simp [extendLenOne]
Proof state after:
case succ
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.succ x' + y + n)) ∨
    stmt { index := Nat.succ x' } { index := y } n ∈
        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 (Nat.succ x' + y + n - ↑x))))
          (Finset.attach (Finset.range (Nat.succ x' + y + n))) ∨
      stmt { index := Nat.succ x' } { index := y } n ∈ baseProgram (Nat.succ x' + y + n + 1)
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case succ
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.succ x' + y + n)) ∨
    stmt { index := Nat.succ x' } { index := y } n ∈
        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 (Nat.succ x' + y + n - ↑x))))
          (Finset.attach (Finset.range (Nat.succ x' + y + n))) ∨
      stmt { index := Nat.succ x' } { index := y } n ∈ baseProgram (Nat.succ x' + y + n + 1)
Tactic:
. apply Or.inl ∘ Finset.mem_fold_union_iff.mpr
  refine' ⟨stmt (.mk x') (.mk y) n, ⟨_, _⟩⟩
  rw [Nat.succ_add, Nat.succ_add, Nat.succ_eq_add_one]
  apply ofLen_stmt_complete _ h_stmt
  cases' h_stmt with h h <;> rw [h] <;> simp [extendLenOne]
Proof state after:
no goals
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case zero.zero.zero
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ stmt { index := Nat.zero } { index := Nat.zero } Nat.zero ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.zero + Nat.zero + Nat.zero)) ∨
    stmt { index := Nat.zero } { index := Nat.zero } Nat.zero ∈
        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 (Nat.zero + Nat.zero + Nat.zero - ↑x))))
          (Finset.attach (Finset.range (Nat.zero + Nat.zero + Nat.zero))) ∨
      stmt { index := Nat.zero } { index := Nat.zero } Nat.zero ∈ baseProgram (Nat.zero + Nat.zero + Nat.zero + 1)
Tactic:
refine' .inr ∘ .inr $ lenOne_complete _ _
Proof state after:
case zero.zero.zero
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ len (stmt { index := Nat.zero } { index := Nat.zero } Nat.zero) = 1
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case zero.zero.zero
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
⊢ len (stmt { index := Nat.zero } { index := Nat.zero } Nat.zero) = 1
Tactic:
cases' h_stmt with h h <;> rw [h] <;> rfl
Proof state after:
no goals
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case zero.zero.succ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
n' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.zero + Nat.zero + Nat.succ n')) ∨
    stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈
        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 (Nat.zero + Nat.zero + Nat.succ n' - ↑x))))
          (Finset.attach (Finset.range (Nat.zero + Nat.zero + Nat.succ n'))) ∨
      stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈
        baseProgram (Nat.zero + Nat.zero + Nat.succ n' + 1)
Tactic:
apply Or.inl ∘ Finset.mem_fold_union_iff.mpr
Proof state after:
case zero.zero.succ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
n' : ℕ
⊢ ∃ x ∈ ofLen (Nat.zero + Nat.zero + Nat.succ n'),
    stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈ extendLenOne x
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case zero.zero.succ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
n' : ℕ
⊢ ∃ x ∈ ofLen (Nat.zero + Nat.zero + Nat.succ n'),
    stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈ extendLenOne x
Tactic:
refine' ⟨stmt (.mk 0) (.mk 0) n', ⟨ofLen_stmt_complete _ h_stmt, _⟩⟩
Proof state after:
case zero.zero.succ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
n' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈ extendLenOne (stmt { index := 0 } { index := 0 } n')
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case zero.zero.succ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
n' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.zero } (Nat.succ n') ∈ extendLenOne (stmt { index := 0 } { index := 0 } n')
Tactic:
cases' h_stmt with h h <;> rw [h] <;> simp [extendLenOne]
Proof state after:
no goals
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case zero.succ
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.succ y' } n ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.zero + Nat.succ y' + n)) ∨
    stmt { index := Nat.zero } { index := Nat.succ y' } n ∈
        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 (Nat.zero + Nat.succ y' + n - ↑x))))
          (Finset.attach (Finset.range (Nat.zero + Nat.succ y' + n))) ∨
      stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ baseProgram (Nat.zero + Nat.succ y' + n + 1)
Tactic:
apply Or.inl ∘ Finset.mem_fold_union_iff.mpr
Proof state after:
case zero.succ
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ ∃ x ∈ ofLen (Nat.zero + Nat.succ y' + n), stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ extendLenOne x
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case zero.succ
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ ∃ x ∈ ofLen (Nat.zero + Nat.succ y' + n), stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ extendLenOne x
Tactic:
refine' ⟨stmt (.mk 0) (.mk y') n, ⟨_, _⟩⟩
Proof state after:
case zero.succ.refine'_1
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := 0 } { index := y' } n ∈ ofLen (Nat.zero + Nat.succ y' + n)

case zero.succ.refine'_2
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ extendLenOne (stmt { index := 0 } { index := y' } n)
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case zero.succ.refine'_1
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := 0 } { index := y' } n ∈ ofLen (Nat.zero + Nat.succ y' + n)

case zero.succ.refine'_2
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ extendLenOne (stmt { index := 0 } { index := y' } n)
Tactic:
rw [Nat.add_succ, Nat.succ_add, Nat.succ_eq_add_one]
Proof state after:
case zero.succ.refine'_1
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := 0 } { index := y' } n ∈ ofLen (Nat.zero + y' + n + 1)

case zero.succ.refine'_2
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ extendLenOne (stmt { index := 0 } { index := y' } n)
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case zero.succ.refine'_1
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := 0 } { index := y' } n ∈ ofLen (Nat.zero + y' + n + 1)

case zero.succ.refine'_2
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ extendLenOne (stmt { index := 0 } { index := y' } n)
Tactic:
apply ofLen_stmt_complete _ h_stmt
Proof state after:
case zero.succ.refine'_2
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ extendLenOne (stmt { index := 0 } { index := y' } n)
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case zero.succ.refine'_2
n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
y' : ℕ
⊢ stmt { index := Nat.zero } { index := Nat.succ y' } n ∈ extendLenOne (stmt { index := 0 } { index := y' } n)
Tactic:
cases' h_stmt with h h <;> rw [h] <;> simp [extendLenOne]
Proof state after:
no goals
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case succ
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈
      Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (Nat.succ x' + y + n)) ∨
    stmt { index := Nat.succ x' } { index := y } n ∈
        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 (Nat.succ x' + y + n - ↑x))))
          (Finset.attach (Finset.range (Nat.succ x' + y + n))) ∨
      stmt { index := Nat.succ x' } { index := y } n ∈ baseProgram (Nat.succ x' + y + n + 1)
Tactic:
apply Or.inl ∘ Finset.mem_fold_union_iff.mpr
Proof state after:
case succ
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ ∃ x ∈ ofLen (Nat.succ x' + y + n), stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne x
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case succ
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ ∃ x ∈ ofLen (Nat.succ x' + y + n), stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne x
Tactic:
refine' ⟨stmt (.mk x') (.mk y) n, ⟨_, _⟩⟩
Proof state after:
case succ.refine'_1
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := x' } { index := y } n ∈ ofLen (Nat.succ x' + y + n)

case succ.refine'_2
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne (stmt { index := x' } { index := y } n)
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case succ.refine'_1
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := x' } { index := y } n ∈ ofLen (Nat.succ x' + y + n)

case succ.refine'_2
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne (stmt { index := x' } { index := y } n)
Tactic:
rw [Nat.succ_add, Nat.succ_add, Nat.succ_eq_add_one]
Proof state after:
case succ.refine'_1
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := x' } { index := y } n ∈ ofLen (x' + y + n + 1)

case succ.refine'_2
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne (stmt { index := x' } { index := y } n)
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case succ.refine'_1
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := x' } { index := y } n ∈ ofLen (x' + y + n + 1)

case succ.refine'_2
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne (stmt { index := x' } { index := y } n)
Tactic:
apply ofLen_stmt_complete _ h_stmt
Proof state after:
case succ.refine'_2
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne (stmt { index := x' } { index := y } n)
Theorem: LoopProgram.ofLen_stmt_complete
Proof state before:
case succ.refine'_2
y n : ℕ
stmt : Variable → Variable → ℕ → LoopProgram
h_stmt : stmt = add ∨ stmt = sub
x' : ℕ
⊢ stmt { index := Nat.succ x' } { index := y } n ∈ extendLenOne (stmt { index := x' } { index := y } n)
Tactic:
cases' h_stmt with h h <;> rw [h] <;> simp [extendLenOne]
Proof state after:
no goals
Theorem: LoopProgram.ofLen_complete
Proof state before:
⊢ ∀ (p : LoopProgram), p ∈ ofLen (len p)
Tactic:
intro p
Proof state after:
p : LoopProgram
⊢ p ∈ ofLen (len p)
Theorem: LoopProgram.ofLen_complete
Proof 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 _⟩
Proof state after:
no goals
Theorem: LoopProgram.ofLen_complete
Proof 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
Proof state after:
case h_stmt
p : LoopProgram
x y n : ℕ
⊢ add = add ∨ add = sub
Theorem: LoopProgram.ofLen_complete
Proof state before:
case h_stmt
p : LoopProgram
x y n : ℕ
⊢ add = add ∨ add = sub
Tactic:
apply Or.inl
Proof state after:
case h_stmt.h
p : LoopProgram
x y n : ℕ
⊢ add = add
Theorem: LoopProgram.ofLen_complete
Proof state before:
case h_stmt.h
p : LoopProgram
x y n : ℕ
⊢ add = add
Tactic:
rfl
Proof state after:
no goals
Theorem: LoopProgram.ofLen_complete
Proof 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
Proof state after:
case h_stmt
p : LoopProgram
x y m : ℕ
⊢ sub = add ∨ sub = sub
Theorem: LoopProgram.ofLen_complete
Proof state before:
case h_stmt
p : LoopProgram
x y m : ℕ
⊢ sub = add ∨ sub = sub
Tactic:
apply Or.inr
Proof state after:
case h_stmt.h
p : LoopProgram
x y m : ℕ
⊢ sub = sub
Theorem: LoopProgram.ofLen_complete
Proof state before:
case h_stmt.h
p : LoopProgram
x y m : ℕ
⊢ sub = sub
Tactic:
rfl
Proof state after:
no goals
Theorem: LoopProgram.ofLen_complete
Proof state before:
p✝ : LoopProgram
x : ℕ
p : LoopProgram
⊢ loop { index := x } p ∈ ofLen (len (loop { index := x } p))
Tactic:
dsimp [len]
Proof state after:
p✝ : LoopProgram
x : ℕ
p : LoopProgram
⊢ loop { index := x } p ∈ ofLen (len p + x + 1)
Theorem: LoopProgram.ofLen_complete
Proof state before:
p✝ : LoopProgram
x : ℕ
p : LoopProgram
⊢ loop { index := x } p ∈ ofLen (len p + x + 1)
Tactic:
cases' x with x'
Proof 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)
Theorem: LoopProgram.ofLen_complete
Proof 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]
Proof state after:
case succ
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ ofLen (len p + Nat.succ x' + 1)
Theorem: LoopProgram.ofLen_complete
Proof 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
Proof 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
Theorem: LoopProgram.ofLen_complete
Proof state before:
p✝ p : LoopProgram
x' : ℕ
⊢ LoopProgram
Tactic:
case p => exact loop (.mk x') p
Proof state after:
no goals
Theorem: LoopProgram.ofLen_complete
Proof 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
Proof 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)
Theorem: LoopProgram.ofLen_complete
Proof 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]
Proof 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)