internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
case a
F h1_phi h1_psi : Formula
⊢ IsAxiom (h1_phi.imp_ (h1_psi.imp_ h1_phi))
Tactic:
apply IsAxiom.prop_1_
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F h1_phi h1_psi h1_chi : Formula
⊢ IsDeduct ∅ ((h1_phi.imp_ (h1_psi.imp_ h1_chi)).imp_ ((h1_phi.imp_ h1_psi).imp_ (h1_phi.imp_ h1_chi)))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a
F h1_phi h1_psi h1_chi : Formula
⊢ IsAxiom ((h1_phi.imp_ (h1_psi.imp_ h1_chi)).imp_ ((h1_phi.imp_ h1_psi).imp_ (h1_phi.imp_ h1_chi)))
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
case a
F h1_phi h1_psi h1_chi : Formula
⊢ IsAxiom ((h1_phi.imp_ (h1_psi.imp_ h1_chi)).imp_ ((h1_phi.imp_ h1_psi).imp_ (h1_phi.imp_ h1_chi)))
Tactic:
apply IsAxiom.prop_2_
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F h1_phi h1_psi : Formula
⊢ IsDeduct ∅ ((h1_phi.not_.imp_ h1_psi.not_).imp_ (h1_psi.imp_ h1_phi))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a
F h1_phi h1_psi : Formula
⊢ IsAxiom ((h1_phi.not_.imp_ h1_psi.not_).imp_ (h1_psi.imp_ h1_phi))
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
case a
F h1_phi h1_psi : Formula
⊢ IsAxiom ((h1_phi.not_.imp_ h1_psi.not_).imp_ (h1_psi.imp_ h1_phi))
Tactic:
apply IsAxiom.prop_3_
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F : Formula
h1_v : VarName
h1_phi h1_psi : Formula
⊢ IsDeduct ∅ ((forall_ h1_v (h1_phi.imp_ h1_psi)).imp_ ((forall_ h1_v h1_phi).imp_ (forall_ h1_v h1_psi)))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a
F : Formula
h1_v : VarName
h1_phi h1_psi : Formula
⊢ IsAxiom ((forall_ h1_v (h1_phi.imp_ h1_psi)).imp_ ((forall_ h1_v h1_phi).imp_ (forall_ h1_v h1_psi)))
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
case a
F : Formula
h1_v : VarName
h1_phi h1_psi : Formula
⊢ IsAxiom ((forall_ h1_v (h1_phi.imp_ h1_psi)).imp_ ((forall_ h1_v h1_phi).imp_ (forall_ h1_v h1_psi)))
Tactic:
apply IsAxiom.pred_1_
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F : Formula
h1_v h1_t : VarName
h1_phi h1_phi' : Formula
h1_1 : fastAdmits h1_v h1_t h1_phi
h1_ih_1 : fastReplaceFree h1_v h1_t h1_phi = h1_phi'
⊢ IsDeduct ∅ ((forall_ h1_v h1_phi).imp_ h1_phi')
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a
F : Formula
h1_v h1_t : VarName
h1_phi h1_phi' : Formula
h1_1 : fastAdmits h1_v h1_t h1_phi
h1_ih_1 : fastReplaceFree h1_v h1_t h1_phi = h1_phi'
⊢ IsAxiom ((forall_ h1_v h1_phi).imp_ h1_phi')
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
case a
F : Formula
h1_v h1_t : VarName
h1_phi h1_phi' : Formula
h1_1 : fastAdmits h1_v h1_t h1_phi
h1_ih_1 : fastReplaceFree h1_v h1_t h1_phi = h1_phi'
⊢ IsAxiom ((forall_ h1_v h1_phi).imp_ h1_phi')
Tactic:
exact IsAxiom.pred_2_ h1_v h1_t h1_phi h1_phi' h1_1 h1_ih_1
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : ¬isFreeIn h1_v h1_phi
⊢ IsDeduct ∅ (h1_phi.imp_ (forall_ h1_v h1_phi))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : ¬isFreeIn h1_v h1_phi
⊢ IsAxiom (h1_phi.imp_ (forall_ h1_v h1_phi))
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
case a
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : ¬isFreeIn h1_v h1_phi
⊢ IsAxiom (h1_phi.imp_ (forall_ h1_v h1_phi))
Tactic:
apply IsAxiom.pred_3_
Proof state after:
case a.a
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : ¬isFreeIn h1_v h1_phi
⊢ ¬isFreeIn h1_v h1_phi
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
case a.a
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : ¬isFreeIn h1_v h1_phi
⊢ ¬isFreeIn h1_v h1_phi
Tactic:
exact h1_1
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F : Formula
h1 : VarName
⊢ IsDeduct ∅ (forall_ h1 (eq_ h1 h1))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a
F : Formula
h1 : VarName
⊢ IsAxiom (forall_ h1 (eq_ h1 h1))
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
case a
F : Formula
h1 : VarName
⊢ IsAxiom (forall_ h1 (eq_ h1 h1))
Tactic:
apply IsAxiom.eq_1_
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F : Formula
h1_name : PredName
h1_n : ℕ
h1_xs h1_ys : Fin h1_n → VarName
⊢ IsDeduct ∅
    (Forall_ (List.ofFn h1_xs)
      (Forall_ (List.ofFn h1_ys)
        ((And_ (List.ofFn fun i => eq_ (h1_xs i) (h1_ys i))).imp_
          ((pred_const_ h1_name (List.ofFn h1_xs)).iff_ (pred_const_ h1_name (List.ofFn h1_ys))))))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a
F : Formula
h1_name : PredName
h1_n : ℕ
h1_xs h1_ys : Fin h1_n → VarName
⊢ IsAxiom
    (Forall_ (List.ofFn h1_xs)
      (Forall_ (List.ofFn h1_ys)
        ((And_ (List.ofFn fun i => eq_ (h1_xs i) (h1_ys i))).imp_
          ((pred_const_ h1_name (List.ofFn h1_xs)).iff_ (pred_const_ h1_name (List.ofFn h1_ys))))))
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
case a
F : Formula
h1_name : PredName
h1_n : ℕ
h1_xs h1_ys : Fin h1_n → VarName
⊢ IsAxiom
    (Forall_ (List.ofFn h1_xs)
      (Forall_ (List.ofFn h1_ys)
        ((And_ (List.ofFn fun i => eq_ (h1_xs i) (h1_ys i))).imp_
          ((pred_const_ h1_name (List.ofFn h1_xs)).iff_ (pred_const_ h1_name (List.ofFn h1_ys))))))
Tactic:
apply IsAxiom.eq_2_pred_const_
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F : Formula
h1_x_0 h1_y_0 h1_x_1 h1_y_1 : VarName
⊢ IsDeduct ∅
    (forall_ h1_x_0
      (forall_ h1_y_0
        (forall_ h1_x_1
          (forall_ h1_y_1
            (((eq_ h1_x_0 h1_x_1).and_ (eq_ h1_y_0 h1_y_1)).imp_ ((eq_ h1_x_0 h1_y_0).iff_ (eq_ h1_x_1 h1_y_1)))))))
Tactic:
apply IsDeduct.axiom_
Proof state after:
case a
F : Formula
h1_x_0 h1_y_0 h1_x_1 h1_y_1 : VarName
⊢ IsAxiom
    (forall_ h1_x_0
      (forall_ h1_y_0
        (forall_ h1_x_1
          (forall_ h1_y_1
            (((eq_ h1_x_0 h1_x_1).and_ (eq_ h1_y_0 h1_y_1)).imp_ ((eq_ h1_x_0 h1_y_0).iff_ (eq_ h1_x_1 h1_y_1)))))))
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
case a
F : Formula
h1_x_0 h1_y_0 h1_x_1 h1_y_1 : VarName
⊢ IsAxiom
    (forall_ h1_x_0
      (forall_ h1_y_0
        (forall_ h1_x_1
          (forall_ h1_y_1
            (((eq_ h1_x_0 h1_x_1).and_ (eq_ h1_y_0 h1_y_1)).imp_ ((eq_ h1_x_0 h1_y_0).iff_ (eq_ h1_x_1 h1_y_1)))))))
Tactic:
apply IsAxiom.eq_2_eq_
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : IsProofAlt h1_phi
h1_ih : IsDeduct ∅ h1_phi
⊢ IsDeduct ∅ (forall_ h1_v h1_phi)
Tactic:
apply generalization
Proof state after:
case h1
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : IsProofAlt h1_phi
h1_ih : IsDeduct ∅ h1_phi
⊢ IsDeduct ∅ h1_phi

case h2
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : IsProofAlt h1_phi
h1_ih : IsDeduct ∅ h1_phi
⊢ ∀ H ∈ ∅, ¬isFreeIn h1_v H
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
case h1
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : IsProofAlt h1_phi
h1_ih : IsDeduct ∅ h1_phi
⊢ IsDeduct ∅ h1_phi
Tactic:
exact h1_ih
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
case h2
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : IsProofAlt h1_phi
h1_ih : IsDeduct ∅ h1_phi
⊢ ∀ H ∈ ∅, ¬isFreeIn h1_v H
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
F h1_phi h1_psi : Formula
h1_1 : IsProofAlt (h1_phi.imp_ h1_psi)
h1_2 : IsProofAlt h1_phi
h1_ih_1 : IsDeduct ∅ (h1_phi.imp_ h1_psi)
h1_ih_2 : IsDeduct ∅ h1_phi
⊢ IsDeduct ∅ h1_psi
Tactic:
exact IsDeduct.mp_ h1_phi h1_psi h1_ih_1 h1_ih_2
Proof state after:
no goals
Theorem: FOL.NV.isProofAltImpIsDeduct
Proof state before:
case def_exists_
F : Formula
v✝ : VarName
phi✝ : Formula
⊢ IsDeduct ∅ ((exists_ v✝ phi✝).iff_ (forall_ v✝ phi✝.not_).not_)
Tactic:
sorry
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F : Formula
h1 : IsDeduct ∅ F
⊢ IsProofAlt F
Tactic:
induction h1
Proof state after:
case axiom_
F phi✝ : Formula
a✝ : IsAxiom phi✝
⊢ IsProofAlt phi✝

case assume_
F phi✝ : Formula
a✝ : phi✝ ∈ ∅
⊢ IsProofAlt phi✝

case mp_
F phi✝ psi✝ : Formula
a✝¹ : IsDeduct ∅ (phi✝.imp_ psi✝)
a✝ : IsDeduct ∅ phi✝
a_ih✝¹ : IsProofAlt (phi✝.imp_ psi✝)
a_ih✝ : IsProofAlt phi✝
⊢ IsProofAlt psi✝
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsProofAlt h1_phi
Tactic:
case axiom_ h1_phi h1_1 =>
  induction h1_1
  case prop_true_ =>
    apply IsProofAlt.prop_true_
  case prop_1_ h1_1_phi h1_1_psi =>
    apply IsProofAlt.prop_1_
  case prop_2_ h1_1_phi h1_1_psi h1_1_chi =>
    apply IsProofAlt.prop_2_
  case prop_3_ h1_1_phi h1_1_psi =>
    apply IsProofAlt.prop_3_
  case pred_1_ h1_1_v h1_1_phi h1_1_psi =>
    apply IsProofAlt.pred_1_
  case pred_2_ h1_1_v h1_1_t h1_1_phi h1_1_1 h1_1_ih_1 h1_1_ih_2 =>
    apply IsProofAlt.pred_2_ h1_1_v h1_1_t h1_1_phi h1_1_1 h1_1_ih_1 h1_1_ih_2
  case pred_3_ h1_1_v h1_1_phi h1_1_1 =>
    apply IsProofAlt.pred_3_
    exact h1_1_1
  case eq_1_ h1_1 =>
    apply IsProofAlt.eq_1_
  case eq_2_pred_const_ h1_1_name h1_1_n h1_1_xs h1_1_ys =>
    apply IsProofAlt.eq_2_pred_const_
  case eq_2_eq_ h1_1_x_0 h1_1_y_0 h1_1_x_1 h1_1_y_1 =>
    apply IsProofAlt.eq_2_eq_
  case gen_ h1_1_v h1_1_phi h1_1_1 h1_1_ih =>
    apply IsProofAlt.gen_
    exact h1_1_ih
  all_goals
    sorry
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1 : h1_phi ∈ ∅
⊢ IsProofAlt h1_phi
Tactic:
case assume_ h1_phi h1_1 =>
  simp at h1_1
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi h1_psi : Formula
h1_1 : IsDeduct ∅ (h1_phi.imp_ h1_psi)
h1_2 : IsDeduct ∅ h1_phi
h1_ih_1 : IsProofAlt (h1_phi.imp_ h1_psi)
h1_ih_2 : IsProofAlt h1_phi
⊢ IsProofAlt h1_psi
Tactic:
case mp_ h1_phi h1_psi h1_1 h1_2 h1_ih_1 h1_ih_2 =>
  exact IsProofAlt.mp_ h1_phi h1_psi h1_ih_1 h1_ih_2
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsProofAlt h1_phi
Tactic:
induction h1_1
Proof state after:
case prop_true_
F h1_phi : Formula
⊢ IsProofAlt true_

case prop_1_
F h1_phi phi✝ psi✝ : Formula
⊢ IsProofAlt (phi✝.imp_ (psi✝.imp_ phi✝))

case prop_2_
F h1_phi phi✝ psi✝ chi✝ : Formula
⊢ IsProofAlt ((phi✝.imp_ (psi✝.imp_ chi✝)).imp_ ((phi✝.imp_ psi✝).imp_ (phi✝.imp_ chi✝)))

case prop_3_
F h1_phi phi✝ psi✝ : Formula
⊢ IsProofAlt ((phi✝.not_.imp_ psi✝.not_).imp_ (psi✝.imp_ phi✝))

case pred_1_
F h1_phi : Formula
v✝ : VarName
phi✝ psi✝ : Formula
⊢ IsProofAlt ((forall_ v✝ (phi✝.imp_ psi✝)).imp_ ((forall_ v✝ phi✝).imp_ (forall_ v✝ psi✝)))

case pred_2_
F h1_phi : Formula
v✝ t✝ : VarName
phi✝ phi'✝ : Formula
a✝¹ : fastAdmits v✝ t✝ phi✝
a✝ : fastReplaceFree v✝ t✝ phi✝ = phi'✝
⊢ IsProofAlt ((forall_ v✝ phi✝).imp_ phi'✝)

case pred_3_
F h1_phi : Formula
v✝ : VarName
phi✝ : Formula
a✝ : ¬isFreeIn v✝ phi✝
⊢ IsProofAlt (phi✝.imp_ (forall_ v✝ phi✝))

case eq_1_
F h1_phi : Formula
v✝ : VarName
⊢ IsProofAlt (forall_ v✝ (eq_ v✝ v✝))

case eq_2_pred_const_
F h1_phi : Formula
name✝ : PredName
n✝ : ℕ
xs✝ ys✝ : Fin n✝ → VarName
⊢ IsProofAlt
    (Forall_ (List.ofFn xs✝)
      (Forall_ (List.ofFn ys✝)
        ((And_ (List.ofFn fun i => eq_ (xs✝ i) (ys✝ i))).imp_
          ((pred_const_ name✝ (List.ofFn xs✝)).iff_ (pred_const_ name✝ (List.ofFn ys✝))))))

case eq_2_eq_
F h1_phi : Formula
x_0✝ x_1✝ y_0✝ y_1✝ : VarName
⊢ IsProofAlt
    (forall_ x_0✝
      (forall_ x_1✝
        (forall_ y_0✝
          (forall_ y_1✝ (((eq_ x_0✝ y_0✝).and_ (eq_ x_1✝ y_1✝)).imp_ ((eq_ x_0✝ x_1✝).iff_ (eq_ y_0✝ y_1✝)))))))

case gen_
F h1_phi : Formula
v✝ : VarName
phi✝ : Formula
a✝ : IsAxiom phi✝
a_ih✝ : IsProofAlt phi✝
⊢ IsProofAlt (forall_ v✝ phi✝)

case def_false_
F h1_phi : Formula
⊢ IsProofAlt (false_.iff_ true_.not_)

case def_and_
F h1_phi phi✝ psi✝ : Formula
⊢ IsProofAlt ((phi✝.and_ psi✝).iff_ (phi✝.imp_ psi✝.not_).not_)

case def_or_
F h1_phi phi✝ psi✝ : Formula
⊢ IsProofAlt ((phi✝.or_ psi✝).iff_ (phi✝.not_.imp_ psi✝))

case def_iff_
F h1_phi phi✝ psi✝ : Formula
⊢ IsProofAlt
    (((phi✝.iff_ psi✝).imp_ ((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_).imp_
        (((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_.imp_ (phi✝.iff_ psi✝)).not_).not_

case def_exists_
F h1_phi : Formula
v✝ : VarName
phi✝ : Formula
⊢ IsProofAlt ((exists_ v✝ phi✝).iff_ (forall_ v✝ phi✝.not_).not_)
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
⊢ IsProofAlt true_
Tactic:
case prop_true_ =>
  apply IsProofAlt.prop_true_
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi h1_1_phi h1_1_psi : Formula
⊢ IsProofAlt (h1_1_phi.imp_ (h1_1_psi.imp_ h1_1_phi))
Tactic:
case prop_1_ h1_1_phi h1_1_psi =>
  apply IsProofAlt.prop_1_
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi h1_1_phi h1_1_psi h1_1_chi : Formula
⊢ IsProofAlt ((h1_1_phi.imp_ (h1_1_psi.imp_ h1_1_chi)).imp_ ((h1_1_phi.imp_ h1_1_psi).imp_ (h1_1_phi.imp_ h1_1_chi)))
Tactic:
case prop_2_ h1_1_phi h1_1_psi h1_1_chi =>
  apply IsProofAlt.prop_2_
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi h1_1_phi h1_1_psi : Formula
⊢ IsProofAlt ((h1_1_phi.not_.imp_ h1_1_psi.not_).imp_ (h1_1_psi.imp_ h1_1_phi))
Tactic:
case prop_3_ h1_1_phi h1_1_psi =>
  apply IsProofAlt.prop_3_
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1_v : VarName
h1_1_phi h1_1_psi : Formula
⊢ IsProofAlt ((forall_ h1_1_v (h1_1_phi.imp_ h1_1_psi)).imp_ ((forall_ h1_1_v h1_1_phi).imp_ (forall_ h1_1_v h1_1_psi)))
Tactic:
case pred_1_ h1_1_v h1_1_phi h1_1_psi =>
  apply IsProofAlt.pred_1_
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1_v h1_1_t : VarName
h1_1_phi h1_1_1 : Formula
h1_1_ih_1 : fastAdmits h1_1_v h1_1_t h1_1_phi
h1_1_ih_2 : fastReplaceFree h1_1_v h1_1_t h1_1_phi = h1_1_1
⊢ IsProofAlt ((forall_ h1_1_v h1_1_phi).imp_ h1_1_1)
Tactic:
case pred_2_ h1_1_v h1_1_t h1_1_phi h1_1_1 h1_1_ih_1 h1_1_ih_2 =>
  apply IsProofAlt.pred_2_ h1_1_v h1_1_t h1_1_phi h1_1_1 h1_1_ih_1 h1_1_ih_2
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1_v : VarName
h1_1_phi : Formula
h1_1_1 : ¬isFreeIn h1_1_v h1_1_phi
⊢ IsProofAlt (h1_1_phi.imp_ (forall_ h1_1_v h1_1_phi))
Tactic:
case pred_3_ h1_1_v h1_1_phi h1_1_1 =>
  apply IsProofAlt.pred_3_
  exact h1_1_1
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1 : VarName
⊢ IsProofAlt (forall_ h1_1 (eq_ h1_1 h1_1))
Tactic:
case eq_1_ h1_1 =>
  apply IsProofAlt.eq_1_
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1_name : PredName
h1_1_n : ℕ
h1_1_xs h1_1_ys : Fin h1_1_n → VarName
⊢ IsProofAlt
    (Forall_ (List.ofFn h1_1_xs)
      (Forall_ (List.ofFn h1_1_ys)
        ((And_ (List.ofFn fun i => eq_ (h1_1_xs i) (h1_1_ys i))).imp_
          ((pred_const_ h1_1_name (List.ofFn h1_1_xs)).iff_ (pred_const_ h1_1_name (List.ofFn h1_1_ys))))))
Tactic:
case eq_2_pred_const_ h1_1_name h1_1_n h1_1_xs h1_1_ys =>
  apply IsProofAlt.eq_2_pred_const_
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1_x_0 h1_1_y_0 h1_1_x_1 h1_1_y_1 : VarName
⊢ IsProofAlt
    (forall_ h1_1_x_0
      (forall_ h1_1_y_0
        (forall_ h1_1_x_1
          (forall_ h1_1_y_1
            (((eq_ h1_1_x_0 h1_1_x_1).and_ (eq_ h1_1_y_0 h1_1_y_1)).imp_
              ((eq_ h1_1_x_0 h1_1_y_0).iff_ (eq_ h1_1_x_1 h1_1_y_1)))))))
Tactic:
case eq_2_eq_ h1_1_x_0 h1_1_y_0 h1_1_x_1 h1_1_y_1 =>
  apply IsProofAlt.eq_2_eq_
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1_v : VarName
h1_1_phi : Formula
h1_1_1 : IsAxiom h1_1_phi
h1_1_ih : IsProofAlt h1_1_phi
⊢ IsProofAlt (forall_ h1_1_v h1_1_phi)
Tactic:
case gen_ h1_1_v h1_1_phi h1_1_1 h1_1_ih =>
  apply IsProofAlt.gen_
  exact h1_1_ih
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
case def_false_
F h1_phi : Formula
⊢ IsProofAlt (false_.iff_ true_.not_)

case def_and_
F h1_phi phi✝ psi✝ : Formula
⊢ IsProofAlt ((phi✝.and_ psi✝).iff_ (phi✝.imp_ psi✝.not_).not_)

case def_or_
F h1_phi phi✝ psi✝ : Formula
⊢ IsProofAlt ((phi✝.or_ psi✝).iff_ (phi✝.not_.imp_ psi✝))

case def_iff_
F h1_phi phi✝ psi✝ : Formula
⊢ IsProofAlt
    (((phi✝.iff_ psi✝).imp_ ((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_).imp_
        (((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_.imp_ (phi✝.iff_ psi✝)).not_).not_

case def_exists_
F h1_phi : Formula
v✝ : VarName
phi✝ : Formula
⊢ IsProofAlt ((exists_ v✝ phi✝).iff_ (forall_ v✝ phi✝.not_).not_)
Tactic:
all_goals
  sorry
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
⊢ IsProofAlt true_
Tactic:
apply IsProofAlt.prop_true_
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi h1_1_phi h1_1_psi : Formula
⊢ IsProofAlt (h1_1_phi.imp_ (h1_1_psi.imp_ h1_1_phi))
Tactic:
apply IsProofAlt.prop_1_
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi h1_1_phi h1_1_psi h1_1_chi : Formula
⊢ IsProofAlt ((h1_1_phi.imp_ (h1_1_psi.imp_ h1_1_chi)).imp_ ((h1_1_phi.imp_ h1_1_psi).imp_ (h1_1_phi.imp_ h1_1_chi)))
Tactic:
apply IsProofAlt.prop_2_
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi h1_1_phi h1_1_psi : Formula
⊢ IsProofAlt ((h1_1_phi.not_.imp_ h1_1_psi.not_).imp_ (h1_1_psi.imp_ h1_1_phi))
Tactic:
apply IsProofAlt.prop_3_
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1_v : VarName
h1_1_phi h1_1_psi : Formula
⊢ IsProofAlt ((forall_ h1_1_v (h1_1_phi.imp_ h1_1_psi)).imp_ ((forall_ h1_1_v h1_1_phi).imp_ (forall_ h1_1_v h1_1_psi)))
Tactic:
apply IsProofAlt.pred_1_
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1_v h1_1_t : VarName
h1_1_phi h1_1_1 : Formula
h1_1_ih_1 : fastAdmits h1_1_v h1_1_t h1_1_phi
h1_1_ih_2 : fastReplaceFree h1_1_v h1_1_t h1_1_phi = h1_1_1
⊢ IsProofAlt ((forall_ h1_1_v h1_1_phi).imp_ h1_1_1)
Tactic:
apply IsProofAlt.pred_2_ h1_1_v h1_1_t h1_1_phi h1_1_1 h1_1_ih_1 h1_1_ih_2
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1_v : VarName
h1_1_phi : Formula
h1_1_1 : ¬isFreeIn h1_1_v h1_1_phi
⊢ IsProofAlt (h1_1_phi.imp_ (forall_ h1_1_v h1_1_phi))
Tactic:
apply IsProofAlt.pred_3_
Proof state after:
case a
F h1_phi : Formula
h1_1_v : VarName
h1_1_phi : Formula
h1_1_1 : ¬isFreeIn h1_1_v h1_1_phi
⊢ ¬isFreeIn h1_1_v h1_1_phi
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
case a
F h1_phi : Formula
h1_1_v : VarName
h1_1_phi : Formula
h1_1_1 : ¬isFreeIn h1_1_v h1_1_phi
⊢ ¬isFreeIn h1_1_v h1_1_phi
Tactic:
exact h1_1_1
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1 : VarName
⊢ IsProofAlt (forall_ h1_1 (eq_ h1_1 h1_1))
Tactic:
apply IsProofAlt.eq_1_
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1_name : PredName
h1_1_n : ℕ
h1_1_xs h1_1_ys : Fin h1_1_n → VarName
⊢ IsProofAlt
    (Forall_ (List.ofFn h1_1_xs)
      (Forall_ (List.ofFn h1_1_ys)
        ((And_ (List.ofFn fun i => eq_ (h1_1_xs i) (h1_1_ys i))).imp_
          ((pred_const_ h1_1_name (List.ofFn h1_1_xs)).iff_ (pred_const_ h1_1_name (List.ofFn h1_1_ys))))))
Tactic:
apply IsProofAlt.eq_2_pred_const_
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1_x_0 h1_1_y_0 h1_1_x_1 h1_1_y_1 : VarName
⊢ IsProofAlt
    (forall_ h1_1_x_0
      (forall_ h1_1_y_0
        (forall_ h1_1_x_1
          (forall_ h1_1_y_1
            (((eq_ h1_1_x_0 h1_1_x_1).and_ (eq_ h1_1_y_0 h1_1_y_1)).imp_
              ((eq_ h1_1_x_0 h1_1_y_0).iff_ (eq_ h1_1_x_1 h1_1_y_1)))))))
Tactic:
apply IsProofAlt.eq_2_eq_
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1_v : VarName
h1_1_phi : Formula
h1_1_1 : IsAxiom h1_1_phi
h1_1_ih : IsProofAlt h1_1_phi
⊢ IsProofAlt (forall_ h1_1_v h1_1_phi)
Tactic:
apply IsProofAlt.gen_
Proof state after:
case a
F h1_phi : Formula
h1_1_v : VarName
h1_1_phi : Formula
h1_1_1 : IsAxiom h1_1_phi
h1_1_ih : IsProofAlt h1_1_phi
⊢ IsProofAlt h1_1_phi
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
case a
F h1_phi : Formula
h1_1_v : VarName
h1_1_phi : Formula
h1_1_1 : IsAxiom h1_1_phi
h1_1_ih : IsProofAlt h1_1_phi
⊢ IsProofAlt h1_1_phi
Tactic:
exact h1_1_ih
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
case def_exists_
F h1_phi : Formula
v✝ : VarName
phi✝ : Formula
⊢ IsProofAlt ((exists_ v✝ phi✝).iff_ (forall_ v✝ phi✝.not_).not_)
Tactic:
sorry
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi : Formula
h1_1 : h1_phi ∈ ∅
⊢ IsProofAlt h1_phi
Tactic:
simp at h1_1
Proof state after:
no goals
Theorem: FOL.NV.isDeductImpIsProofAlt
Proof state before:
F h1_phi h1_psi : Formula
h1_1 : IsDeduct ∅ (h1_phi.imp_ h1_psi)
h1_2 : IsDeduct ∅ h1_phi
h1_ih_1 : IsProofAlt (h1_phi.imp_ h1_psi)
h1_ih_2 : IsProofAlt h1_phi
⊢ IsProofAlt h1_psi
Tactic:
exact IsProofAlt.mp_ h1_phi h1_psi h1_ih_1 h1_ih_2
Proof state after:
no goals
Theorem: FOL.NV.T_17_10
Proof state before:
P : Formula
u v : VarName
⊢ IsProof ((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P)))
Tactic:
apply deduction_theorem
Proof state after:
case h1
P : Formula
u v : VarName
⊢ IsDeduct (∅ ∪ {forall_ u (forall_ v P)}) (forall_ v (forall_ u P))
Theorem: FOL.NV.T_17_10
Proof state before:
case h1
P : Formula
u v : VarName
⊢ IsDeduct (∅ ∪ {forall_ u (forall_ v P)}) (forall_ v (forall_ u P))
Tactic:
simp
Proof state after:
case h1
P : Formula
u v : VarName
⊢ IsDeduct {forall_ u (forall_ v P)} (forall_ v (forall_ u P))
Theorem: FOL.NV.T_17_10
Proof state before:
case h1
P : Formula
u v : VarName
⊢ IsDeduct {forall_ u (forall_ v P)} (forall_ v (forall_ u P))
Tactic:
apply generalization
Proof state after:
case h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {forall_ u (forall_ v P)} (forall_ u P)

case h1.h2
P : Formula
u v : VarName
⊢ ∀ H ∈ {forall_ u (forall_ v P)}, ¬isFreeIn v H
Theorem: FOL.NV.T_17_10
Proof state before:
case h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {forall_ u (forall_ v P)} (forall_ u P)
Tactic:
apply generalization
Proof state after:
case h1.h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {forall_ u (forall_ v P)} P

case h1.h1.h2
P : Formula
u v : VarName
⊢ ∀ H ∈ {forall_ u (forall_ v P)}, ¬isFreeIn u H
Theorem: FOL.NV.T_17_10
Proof state before:
case h1.h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {forall_ u (forall_ v P)} P
Tactic:
apply specId v P
Proof state after:
case h1.h1.h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {forall_ u (forall_ v P)} (forall_ v P)
Theorem: FOL.NV.T_17_10
Proof state before:
case h1.h1.h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {forall_ u (forall_ v P)} (forall_ v P)
Tactic:
apply specId u (forall_ v P)
Proof state after:
case h1.h1.h1.h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {forall_ u (forall_ v P)} (forall_ u (forall_ v P))
Theorem: FOL.NV.T_17_10
Proof state before:
case h1.h1.h1.h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {forall_ u (forall_ v P)} (forall_ u (forall_ v P))
Tactic:
apply IsDeduct.assume_
Proof state after:
case h1.h1.h1.h1.h1.a
P : Formula
u v : VarName
⊢ forall_ u (forall_ v P) ∈ {forall_ u (forall_ v P)}
Theorem: FOL.NV.T_17_10
Proof state before:
case h1.h1.h1.h1.h1.a
P : Formula
u v : VarName
⊢ forall_ u (forall_ v P) ∈ {forall_ u (forall_ v P)}
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.T_17_10
Proof state before:
case h1.h1.h2
P : Formula
u v : VarName
⊢ ∀ H ∈ {forall_ u (forall_ v P)}, ¬isFreeIn u H
Tactic:
simp
Proof state after:
case h1.h1.h2
P : Formula
u v : VarName
⊢ ¬isFreeIn u (forall_ u (forall_ v P))