internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
case intro.inl.intro.inr.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : limplies (PosFin n) pivot c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pf : p ⊨ f
p' : PosFin n → Bool := fun a => if a = pivot.fst then pivot.snd else p a
p'_rw : p' = fun a => if a = pivot.fst then pivot.snd else p a
p'_entails_c : p' ⊨ c
c' : DefaultClause n
p'_not_entails_c' : ¬(p' ⊨ c')
c'_in_f : c' ∈ f.toList
pc' : p ⊨ c'
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin ratHints.size
hc' : f.clauses[ratHints[i].fst]! = some c'
h_performRupCheck_res :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.ratUnits = #[] ∧
    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.assignments.size = n
performRatCheck_success :
  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.performRatCheck pivot.negateLiteral ratHints[i]).snd =
    true
performRupCheck_res_satisfies_assignments_invariant :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.assignments_invariant
h✝ :
  ∀ (c_1 : DefaultClause n),
    f.clauses[ratHints[↑i].fst]! = some c_1 →
      limplies (PosFin n) ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
        (c_1.delete pivot.negateLiteral)
c'' : DefaultClause n
hc'' : c'' ∈ (f.insertRupUnits c.negate).fst.toList
pc : ∀ (x : PosFin n), ((x, false) ∈ c.clause → ¬p x = false) ∧ ((x, true) ∈ c.clause → ¬p x = true)
l : PosFin n
l_in_negc : (l, true) ∈ c.clause
l_def : Clause.unit (l, false) = c''
h : p l = false
⊢ p l = false
Tactic:
assumption
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRatCheck_fold_success_entails_safe_insert
Proof state before:
case intro.inr.a
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_in_c : limplies (PosFin n) pivot c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
p : PosFin n → Bool
pc : ¬(p ⊨ c)
p' : PosFin n → Bool := fun a => if a = pivot.fst then pivot.snd else p a
p'_rw : p' = fun a => if a = pivot.fst then pivot.snd else p a
p'_entails_c : p' ⊨ c
c' : DefaultClause n
p'_not_entails_c' : ¬(p' ⊨ c')
c'_in_f : c' ∈ f.toList
pc' : p ⊨ c'
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin ratHints.size
hc' : f.clauses[ratHints[i].fst]! = some c'
h_performRupCheck_res :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.ratUnits = #[] ∧
    ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.assignments.size = n
performRatCheck_success :
  (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.performRatCheck pivot.negateLiteral ratHints[i]).snd =
    true
performRupCheck_res_satisfies_assignments_invariant :
  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst.assignments_invariant
h :
  ∀ (c_1 : DefaultClause n),
    f.clauses[ratHints[↑i].fst]! = some c_1 →
      limplies (PosFin n) ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
        (c_1.delete pivot.negateLiteral)
c'' : DefaultClause n
hc'' : c'' ∈ (f.insertRupUnits c.negate).fst.toList
c''_in_f : c'' ∈ f.toList
pf :
  ∀ (x : DefaultClause n),
    x ∈ f.toList → ∃ a, (a, false) ∈ Clause.toList x ∧ p a = false ∨ (a, true) ∈ Clause.toList x ∧ p a = true
⊢ c'' ∈ f.toList
Tactic:
assumption
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ratAdd_sound
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
ratAddSuccess : f.performRatAdd c pivot rupHints ratHints = (f', true)
⊢ equisat (PosFin n) f f'
Tactic:
have f'_def := ratAdd_result f c pivot rupHints ratHints f' f_readyForRatAdd pivot_in_c ratAddSuccess
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
ratAddSuccess : f.performRatAdd c pivot rupHints ratHints = (f', true)
f'_def : f' = f.insert c
⊢ equisat (PosFin n) f f'
Theorem: LRAT.DefaultFormula.ratAdd_sound
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
ratAddSuccess : f.performRatAdd c pivot rupHints ratHints = (f', true)
f'_def : f' = f.insert c
⊢ equisat (PosFin n) f f'
Tactic:
rw [performRatAdd] at ratAddSuccess
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
ratAddSuccess :
  (if f.ratHintsExhaustive pivot ratHints = true then
      let negC := c.negate;
      match f.insertRupUnits negC with
      | (f, contradictionFound) =>
        if contradictionFound = true then (f, false)
        else
          match f.performRupCheck rupHints with
          | (f, derivedLits, derivedEmpty, encounteredError) =>
            if encounteredError = true then (f, false)
            else
              if derivedEmpty = true then (f, false)
              else
                let fold_fn := fun x ratHint =>
                  match x with
                  | (f, allChecksPassed) =>
                    if allChecksPassed = true then f.performRatCheck pivot.negateLiteral ratHint else (f, false);
                match Array.foldl fold_fn (f, true) ratHints 0 with
                | (f, allChecksPassed) =>
                  if (!allChecksPassed) = true then (f, false)
                  else
                    match f with
                    | { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =>
                      let assignments := restoreAssignments assignments derivedLits;
                      let f :=
                        { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits,
                            assignments := assignments }.clearRupUnits;
                      (f.insert c, true)
    else (f, false)) =
    (f', true)
f'_def : f' = f.insert c
⊢ equisat (PosFin n) f f'
Theorem: LRAT.DefaultFormula.ratAdd_sound
Proof state before:
case isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
h✝ : ¬f.ratHintsExhaustive pivot ratHints = true
ratAddSuccess : (f, false) = (f', true)
⊢ equisat (PosFin n) f f'
Tactic:
. simp at ratAddSuccess
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ratAdd_sound
Proof state before:
case isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
h✝ : (f.insertRupUnits c.negate).snd = true
ratAddSuccess : ((f.insertRupUnits c.negate).fst, false) = (f', true)
⊢ equisat (PosFin n) f f'
Tactic:
simp at ratAddSuccess
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ratAdd_sound
Proof state before:
case isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
ratAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ equisat (PosFin n) f f'
Tactic:
simp at ratAddSuccess
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ratAdd_sound
Proof state before:
case isFalse.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ equisat (PosFin n) f f'
Tactic:
simp at ratAddSuccess
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ratAdd_sound
Proof state before:
case isFalse.isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
h✝³ : ¬(f.insertRupUnits c.negate).snd = true
h✝² : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
h✝ :
  ¬(Array.foldl
          (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
      false
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
⊢ equisat (PosFin n) f f'
Tactic:
. next performRatCheck_fold_success =>
  simp only [Bool.not_eq_false] at performRatCheck_fold_success
  rw [f'_def]
  exact performRatCheck_fold_success_entails_safe_insert f f_readyForRatAdd c pivot rupHints ratHints pivot_in_c
    ratHintsExhaustive_eq_true performRatCheck_fold_success
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ratAdd_sound
Proof state before:
case isFalse.isFalse.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
h✝³ : ¬(f.insertRupUnits c.negate).snd = true
h✝² : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
h✝ :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    false
ratAddSuccess :
  ((Array.foldl
          (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
      false) =
    (f', true)
⊢ equisat (PosFin n) f f'
Tactic:
simp at ratAddSuccess
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ratAdd_sound
Proof state before:
case isFalse.isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
h✝³ : ¬(f.insertRupUnits c.negate).snd = true
h✝² : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
h✝ :
  ¬(Array.foldl
          (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
      false
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
⊢ equisat (PosFin n) f f'
Tactic:
next performRatCheck_fold_success =>
simp only [Bool.not_eq_false] at performRatCheck_fold_success
rw [f'_def]
exact performRatCheck_fold_success_entails_safe_insert f f_readyForRatAdd c pivot rupHints ratHints pivot_in_c
  ratHintsExhaustive_eq_true performRatCheck_fold_success
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ratAdd_sound
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
performRatCheck_fold_success :
  (Array.foldl
        (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
⊢ equisat (PosFin n) f (f.insert c)
Tactic:
exact performRatCheck_fold_success_entails_safe_insert f f_readyForRatAdd c pivot rupHints ratHints pivot_in_c
  ratHintsExhaustive_eq_true performRatCheck_fold_success
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ratAdd_sound
Proof state before:
case isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
h✝ : ¬f.ratHintsExhaustive pivot ratHints = true
ratAddSuccess : (f, false) = (f', true)
⊢ equisat (PosFin n) f f'
Tactic:
simp at ratAddSuccess
Proof state after:
no goals
Theorem: Sat.liff.symm
Proof state before:
α : Type u
σ1 : Type v
σ2 : Type 2
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ liff α f1 f2 → liff α f2 f1
Tactic:
intros h p
Proof state after:
α : Type u
σ1 : Type v
σ2 : Type 2
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 ↔ p ⊨ f1
Theorem: Sat.liff.symm
Proof state before:
α : Type u
σ1 : Type v
σ2 : Type 2
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
p : α → Bool
⊢ p ⊨ f2 ↔ p ⊨ f1
Tactic:
rw [h p]
Proof state after:
no goals
Theorem: Sat.liff.trans
Proof state before:
α : Type u
σ1 : Type v
σ2 : Type w
σ3 : Type x
inst✝² : HSat α σ1
inst✝¹ : HSat α σ2
inst✝ : HSat α σ3
f1 : σ1
f2 : σ2
f3 : σ3
⊢ liff α f1 f2 → liff α f2 f3 → liff α f1 f3
Tactic:
intros f1_eq_f2 f2_eq_f3 p
Proof state after:
α : Type u
σ1 : Type v
σ2 : Type w
σ3 : Type x
inst✝² : HSat α σ1
inst✝¹ : HSat α σ2
inst✝ : HSat α σ3
f1 : σ1
f2 : σ2
f3 : σ3
f1_eq_f2 : liff α f1 f2
f2_eq_f3 : liff α f2 f3
p : α → Bool
⊢ p ⊨ f1 ↔ p ⊨ f3
Theorem: Sat.liff.trans
Proof state before:
α : Type u
σ1 : Type v
σ2 : Type w
σ3 : Type x
inst✝² : HSat α σ1
inst✝¹ : HSat α σ2
inst✝ : HSat α σ3
f1 : σ1
f2 : σ2
f3 : σ3
f1_eq_f2 : liff α f1 f2
f2_eq_f3 : liff α f2 f3
p : α → Bool
⊢ p ⊨ f1 ↔ p ⊨ f3
Tactic:
rw [f1_eq_f2 p, f2_eq_f3 p]
Proof state after:
no goals
Theorem: Sat.limplies.trans
Proof state before:
α : Type u
σ1 : Type v
σ2 : Type w
σ3 : Type x
inst✝² : HSat α σ1
inst✝¹ : HSat α σ2
inst✝ : HSat α σ3
f1 : σ1
f2 : σ2
f3 : σ3
⊢ limplies α f1 f2 → limplies α f2 f3 → limplies α f1 f3
Tactic:
intros f1_implies_f2 f2_implies_f3 p p_entails_f1
Proof state after:
α : Type u
σ1 : Type v
σ2 : Type w
σ3 : Type x
inst✝² : HSat α σ1
inst✝¹ : HSat α σ2
inst✝ : HSat α σ3
f1 : σ1
f2 : σ2
f3 : σ3
f1_implies_f2 : limplies α f1 f2
f2_implies_f3 : limplies α f2 f3
p : α → Bool
p_entails_f1 : p ⊨ f1
⊢ p ⊨ f3
Theorem: Sat.limplies.trans
Proof state before:
α : Type u
σ1 : Type v
σ2 : Type w
σ3 : Type x
inst✝² : HSat α σ1
inst✝¹ : HSat α σ2
inst✝ : HSat α σ3
f1 : σ1
f2 : σ2
f3 : σ3
f1_implies_f2 : limplies α f1 f2
f2_implies_f3 : limplies α f2 f3
p : α → Bool
p_entails_f1 : p ⊨ f1
⊢ p ⊨ f3
Tactic:
exact f2_implies_f3 p $ f1_implies_f2 p p_entails_f1
Proof state after:
no goals
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ liff α f1 f2 ↔ limplies α f1 f2 ∧ limplies α f2 f1
Tactic:
constructor
Proof state after:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ liff α f1 f2 → limplies α f1 f2 ∧ limplies α f2 f1

case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ limplies α f1 f2 ∧ limplies α f2 f1 → liff α f1 f2
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ liff α f1 f2 → limplies α f1 f2 ∧ limplies α f2 f1

case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ limplies α f1 f2 ∧ limplies α f2 f1 → liff α f1 f2
Tactic:
. intro h
  constructor
  . intro p
    rw [h p]
    exact id
  . intro p
    rw [h p]
    exact id
Proof state after:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ limplies α f1 f2 ∧ limplies α f2 f1 → liff α f1 f2
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mpr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ limplies α f1 f2 ∧ limplies α f2 f1 → liff α f1 f2
Tactic:
. intros h p
  constructor
  . exact h.1 p
  . exact h.2 p
Proof state after:
no goals
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
⊢ liff α f1 f2 → limplies α f1 f2 ∧ limplies α f2 f1
Tactic:
intro h
Proof state after:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ limplies α f1 f2 ∧ limplies α f2 f1
Theorem: Sat.liff_iff_limplies_and_limplies
Proof state before:
case mp
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ limplies α f1 f2 ∧ limplies α f2 f1
Tactic:
constructor
Proof state after:
case mp.left
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ limplies α f1 f2

case mp.right
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : HSat α σ1
inst✝ : HSat α σ2
f1 : σ1
f2 : σ2
h : liff α f1 f2
⊢ limplies α f2 f1