Theorem: FOL.NV.Forall_spec_id (FOL/NV/Margaris/Fol.lean)

State before:
xs : List VarName
P : Formula
⊢ IsProof ((Forall_ xs P).imp_ P)
Tactic:
induction xs
State after:
case nil
P : Formula
⊢ IsProof ((Forall_ [] P).imp_ P)

case cons
P : Formula
head✝ : VarName
tail✝ : List VarName
tail_ih✝ : IsProof ((Forall_ tail✝ P).imp_ P)
⊢ IsProof ((Forall_ (head✝ :: tail✝) P).imp_ P)

State before:
P : Formula
⊢ IsProof ((Forall_ [] P).imp_ P)
Tactic:
case nil =>
  simp only [Forall_]
  apply prop_id
State after:
no goals

State before:
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsProof ((Forall_ (xs_hd :: xs_tl) P).imp_ P)
Tactic:
case cons xs_hd xs_tl xs_ih =>
  simp only [Forall_]
  apply deduction_theorem
  simp
  apply IsDeduct.mp_ (Forall_ xs_tl P)
  apply proof_imp_deduct
  exact xs_ih
  apply specId xs_hd
  apply IsDeduct.assume_
  simp
  rfl
State after:
no goals

State before:
P : Formula
⊢ IsProof ((Forall_ [] P).imp_ P)
Tactic:
simp only [Forall_]
State after:
P : Formula
⊢ IsProof ((List.foldr forall_ P []).imp_ P)

State before:
P : Formula
⊢ IsProof ((List.foldr forall_ P []).imp_ P)
Tactic:
apply prop_id
State after:
no goals

State before:
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsProof ((Forall_ (xs_hd :: xs_tl) P).imp_ P)
Tactic:
simp only [Forall_]
State after:
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsProof ((List.foldr forall_ P (xs_hd :: xs_tl)).imp_ P)

State before:
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsProof ((List.foldr forall_ P (xs_hd :: xs_tl)).imp_ P)
Tactic:
apply deduction_theorem
State after:
case h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct (∅ ∪ {List.foldr forall_ P (xs_hd :: xs_tl)}) P

State before:
case h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct (∅ ∪ {List.foldr forall_ P (xs_hd :: xs_tl)}) P
Tactic:
simp
State after:
case h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} P

State before:
case h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} P
Tactic:
apply IsDeduct.mp_ (Forall_ xs_tl P)
State after:
case h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} ((Forall_ xs_tl P).imp_ P)

case h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} (Forall_ xs_tl P)

State before:
case h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} ((Forall_ xs_tl P).imp_ P)

case h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} (Forall_ xs_tl P)
Tactic:
apply proof_imp_deduct
State after:
case h1.a.h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsProof ((Forall_ xs_tl P).imp_ P)

case h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} (Forall_ xs_tl P)

State before:
case h1.a.h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsProof ((Forall_ xs_tl P).imp_ P)

case h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} (Forall_ xs_tl P)
Tactic:
exact xs_ih
State after:
case h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} (Forall_ xs_tl P)

State before:
case h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} (Forall_ xs_tl P)
Tactic:
apply specId xs_hd
State after:
case h1.a.h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} (forall_ xs_hd (Forall_ xs_tl P))

State before:
case h1.a.h1
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ IsDeduct {forall_ xs_hd (List.foldr forall_ P xs_tl)} (forall_ xs_hd (Forall_ xs_tl P))
Tactic:
apply IsDeduct.assume_
State after:
case h1.a.h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ forall_ xs_hd (Forall_ xs_tl P) ∈ {forall_ xs_hd (List.foldr forall_ P xs_tl)}

State before:
case h1.a.h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ forall_ xs_hd (Forall_ xs_tl P) ∈ {forall_ xs_hd (List.foldr forall_ P xs_tl)}
Tactic:
simp
State after:
case h1.a.h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ Forall_ xs_tl P = List.foldr forall_ P xs_tl

State before:
case h1.a.h1.a
P : Formula
xs_hd : VarName
xs_tl : List VarName
xs_ih : IsProof ((Forall_ xs_tl P).imp_ P)
⊢ Forall_ xs_tl P = List.foldr forall_ P xs_tl
Tactic:
rfl
State after:
no goals