Theorem: LO.FirstOrder.Derivation.ProofList.isProper_primrec (Logic/FirstOrder/Computability/Calculus.lean)

State before:
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
⊢ Primrec isProper
Tactic:
have : Primrec₂ (fun _ p => p.2.2 && F p.1.2 (sequents p.2.1) p.1.1
  : ProofList L → (Code L × List (SyntacticFormula L)) × (List (Code L × List (SyntacticFormula L))) × Bool → Bool) :=
  (dom_bool₂ _).comp₂ (snd.comp₂ $ snd.comp₂ Primrec₂.right)
  (F_primrec.comp₂
      ((Primrec₂.pair.comp (snd.comp fst) (list_map (fst.comp snd) (snd.comp₂ Primrec₂.right))).comp₂ Primrec₂.right)
      (fst.comp₂ $ fst.comp₂ Primrec₂.right))
State after:
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
⊢ Primrec isProper

State before:
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
⊢ Primrec isProper
Tactic:
have : Primrec (fun l => l.rec true (fun c l' ih => ih && F c.2 (sequents l') c.1) : ProofList L → Bool) :=
  list_rec Primrec.id (const true) this
State after:
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
⊢ Primrec isProper

State before:
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
⊢ Primrec isProper
Tactic:
exact this.of_eq <| by
  intro l; induction' l with c l ih <;> simp[isProper]
  rw[ih]; rcases c with ⟨⟨⟩, Γ⟩ <;> simp[isProper, F, Code.equiv, Bool.and_assoc]
State after:
no goals

State before:
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
⊢ ∀ (n : ProofList L),
    List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) n = n.isProper
Tactic:
intro l
State after:
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
l : ProofList L
⊢ List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l = l.isProper

State before:
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
l : ProofList L
⊢ List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l = l.isProper
Tactic:
induction' l with c l ih <;> simp[isProper]
State after:
case cons
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
c : Code L × List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
ih : List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l = isProper l
⊢ (List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l &&
      LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l) c.1) =
    isProper (c :: l)

State before:
case cons
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
c : Code L × List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
ih : List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l = isProper l
⊢ (List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l &&
      LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l) c.1) =
    isProper (c :: l)
Tactic:
rw[ih]
State after:
case cons
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
c : Code L × List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
ih : List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l = isProper l
⊢ (isProper l && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l) c.1) = isProper (c :: l)

State before:
case cons
μ : Type ?u.175455
L : Language
inst✝⁶ : (k : ℕ) → DecidableEq (L.Func k)
inst✝⁵ : (k : ℕ) → DecidableEq (L.Rel k)
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this✝ : Primrec₂ fun x p => p.2.2 && LO.FirstOrder.Derivation.ProofList.F p.1.2 (sequents p.2.1) p.1.1
this :
  Primrec fun l => List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l
c : Code L × List (SyntacticFormula L)
l : List (Code L × List (SyntacticFormula L))
ih : List.rec true (fun c l' ih => ih && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l') c.1) l = isProper l
⊢ (isProper l && LO.FirstOrder.Derivation.ProofList.F c.2 (sequents l) c.1) = isProper (c :: l)
Tactic:
rcases c with ⟨⟨⟩, Γ⟩ <;> simp[isProper, F, Code.equiv, Bool.and_assoc]
State after:
no goals