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

State before:
F : Formula
h1 : IsDeduct ∅ F
⊢ IsProofAlt F
Tactic:
induction h1
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✝

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
State after:
no goals

State before:
F h1_phi : Formula
h1_1 : h1_phi ∈ ∅
⊢ IsProofAlt h1_phi
Tactic:
case assume_ h1_phi h1_1 =>
  simp at h1_1
State after:
no goals

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
State after:
no goals

State before:
F h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsProofAlt h1_phi
Tactic:
induction h1_1
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_)

State before:
F h1_phi : Formula
⊢ IsProofAlt true_
Tactic:
case prop_true_ =>
  apply IsProofAlt.prop_true_
State after:
no goals

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_
State after:
no goals

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_
State after:
no goals

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_
State after:
no goals

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_
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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_
State after:
no goals

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_
State after:
no goals

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_
State after:
no goals

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
State after:
no goals

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
State after:
no goals

State before:
F h1_phi : Formula
⊢ IsProofAlt true_
Tactic:
apply IsProofAlt.prop_true_
State after:
no goals

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_
State after:
no goals

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_
State after:
no goals

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_
State after:
no goals

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_
State after:
no goals

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
State after:
no goals

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_
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

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
State after:
no goals

State before:
F h1_phi : Formula
h1_1 : VarName
⊢ IsProofAlt (forall_ h1_1 (eq_ h1_1 h1_1))
Tactic:
apply IsProofAlt.eq_1_
State after:
no goals

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_
State after:
no goals

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_
State after:
no goals

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_
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

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
State after:
no goals

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
State after:
no goals

State before:
F h1_phi : Formula
h1_1 : h1_phi ∈ ∅
⊢ IsProofAlt h1_phi
Tactic:
simp at h1_1
State after:
no goals

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
State after:
no goals