internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Model.PropForm.eval_ofFun
Proof state before:
case cons.true
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
hhead : τ head = true
⊢ (true && eval τ (ofFun.aux p tail fun v' h' => if h : v' = head then true else passn v' ⋯) ||
      !true && eval τ (ofFun.aux p tail fun v' h' => if h : v' = head then false else passn v' ⋯)) =
    p τ
Tactic:
simp
Proof state after:
case cons.true
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
hhead : τ head = true
⊢ eval τ (ofFun.aux p tail fun v' h' => if h : v' = head then true else passn v' ⋯) = p τ
Theorem: LeanSAT.Model.PropForm.eval_ofFun
Proof state before:
case cons.true
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
hhead : τ head = true
⊢ eval τ (ofFun.aux p tail fun v' h' => if h : v' = head then true else passn v' ⋯) = p τ
Tactic:
apply ih
Proof state after:
case cons.true.ht
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
hhead : τ head = true
⊢ ∀ (v : V) (h : v ∉ tail), (if h : v = head then true else passn v ⋯) = τ v
Theorem: LeanSAT.Model.PropForm.eval_ofFun
Proof state before:
case cons.true.ht
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
hhead : τ head = true
⊢ ∀ (v : V) (h : v ∉ tail), (if h : v = head then true else passn v ⋯) = τ v
Tactic:
intro v h
Proof state after:
case cons.true.ht
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
hhead : τ head = true
v : V
h : v ∉ tail
⊢ (if h : v = head then true else passn v ⋯) = τ v
Theorem: LeanSAT.Model.PropForm.eval_ofFun
Proof state before:
case cons.true.ht
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
hhead : τ head = true
v : V
h : v ∉ tail
⊢ (if h : v = head then true else passn v ⋯) = τ v
Tactic:
split <;> simp [*]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.entails_ofFun
Proof state before:
V : Type u_1
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ τ ⊨ ofFun p L hc ↔ p τ = true
Tactic:
simp [SemanticEntails.entails, satisfies]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.entails_ofFun
Proof state before:
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ τ ⊨ ofFun p ↔ p τ = true
Tactic:
simp [SemanticEntails.entails, satisfies, ofFun]
Proof state after:
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ eval τ (Fintype.elim_elems (fun L h1 x => ⟦PropForm.ofFun p L h1⟧) ⋯) = p τ
Theorem: LeanSAT.Model.PropFun.entails_ofFun
Proof state before:
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ eval τ (Fintype.elim_elems (fun L h1 x => ⟦PropForm.ofFun p L h1⟧) ⋯) = p τ
Tactic:
apply Fintype.elim_elems_eq_forall (V := V)
Proof state after:
case h'
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L),
    Fintype.elim_elems ?f ?h = ?f L h1 h2 → eval τ (Fintype.elim_elems (fun L h1 x => ⟦PropForm.ofFun p L h1⟧) ⋯) = p τ

case f
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → ?m.15443

case h
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), ?f L1 h1 h11 = ?f L2 h2 h22

V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ Type ?u.15442
Theorem: LeanSAT.Model.PropFun.entails_ofFun
Proof state before:
case h'
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L),
    Fintype.elim_elems ?f ?h = ?f L h1 h2 → eval τ (Fintype.elim_elems (fun L h1 x => ⟦PropForm.ofFun p L h1⟧) ⋯) = p τ

case f
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → ?m.15443

case h
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), ?f L1 h1 h11 = ?f L2 h2 h22

V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ Type ?u.15442
Tactic:
intro L h1 h2 h'
Proof state after:
case h'
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
L : List V
h1 : ∀ (v : V), v ∈ L
h2 : List.Nodup L
h' : Fintype.elim_elems ?f ?h = ?f L h1 h2
⊢ eval τ (Fintype.elim_elems (fun L h1 x => ⟦PropForm.ofFun p L h1⟧) ⋯) = p τ

case f
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → ?m.15443

case h
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), ?f L1 h1 h11 = ?f L2 h2 h22

V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ Type ?u.15442
Theorem: LeanSAT.Model.PropFun.entails_ofFun
Proof state before:
case h'
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
L : List V
h1 : ∀ (v : V), v ∈ L
h2 : List.Nodup L
h' : Fintype.elim_elems ?f ?h = ?f L h1 h2
⊢ eval τ (Fintype.elim_elems (fun L h1 x => ⟦PropForm.ofFun p L h1⟧) ⋯) = p τ

case f
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → ?m.15443

case h
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), ?f L1 h1 h11 = ?f L2 h2 h22

V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ Type ?u.15442
Tactic:
rw [h']
Proof state after:
case h'
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
L : List V
h1 : ∀ (v : V), v ∈ L
h2 : List.Nodup L
h' : Fintype.elim_elems (fun L h1 x => ⟦PropForm.ofFun p L h1⟧) ⋯ = ⟦PropForm.ofFun p L h1⟧
⊢ eval τ ⟦PropForm.ofFun p L h1⟧ = p τ
Theorem: LeanSAT.Model.PropFun.entails_ofFun
Proof state before:
case h'
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
L : List V
h1 : ∀ (v : V), v ∈ L
h2 : List.Nodup L
h' : Fintype.elim_elems (fun L h1 x => ⟦PropForm.ofFun p L h1⟧) ⋯ = ⟦PropForm.ofFun p L h1⟧
⊢ eval τ ⟦PropForm.ofFun p L h1⟧ = p τ
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.Model.PropFun.satisfies_ofSet
Proof state before:
V : Type u_1
τ : PropAssignment V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
S : Set (PropAssignment V)
inst✝ : DecidablePred fun x => x ∈ S
⊢ τ ⊨ ofSet S ↔ τ ∈ S
Tactic:
simp [ofSet]
Proof state after:
no goals
Theorem: sterbenz
Proof state before:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ 2 * b
⊢ trunc n (a - b) = a - b
Tactic:
rewrite [Nat.two_mul] at hab
Proof state after:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ trunc n (a - b) = a - b
Theorem: sterbenz
Proof state before:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ trunc n (a - b) = a - b
Tactic:
apply trunc_eq_of_le_of_ulp_dvd b
Proof state after:
case hle
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ a - b ≤ b

case hdvd
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a - b
Theorem: sterbenz
Proof state before:
case hle
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ a - b ≤ b

case hdvd
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a - b
Tactic:
. exact tsub_le_iff_right.mpr hab
Proof state after:
case hdvd
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a - b
Theorem: sterbenz
Proof state before:
case hdvd
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a - b
Tactic:
. apply Nat.dvd_sub'
  . trans ulp n a
    . exact ulp_dvd_ulp n hba
    . exact ulp_dvd_of_trunc_eq hfa
  . exact ulp_dvd_of_trunc_eq hfb
Proof state after:
no goals
Theorem: sterbenz
Proof state before:
case hle
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ a - b ≤ b
Tactic:
exact tsub_le_iff_right.mpr hab
Proof state after:
no goals
Theorem: sterbenz
Proof state before:
case hdvd
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a - b
Tactic:
apply Nat.dvd_sub'
Proof state after:
case hdvd.h₁
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a

case hdvd.h₂
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ b
Theorem: sterbenz
Proof state before:
case hdvd.h₁
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a

case hdvd.h₂
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ b
Tactic:
. trans ulp n a
  . exact ulp_dvd_ulp n hba
  . exact ulp_dvd_of_trunc_eq hfa
Proof state after:
case hdvd.h₂
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ b
Theorem: sterbenz
Proof state before:
case hdvd.h₂
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ b
Tactic:
. exact ulp_dvd_of_trunc_eq hfb
Proof state after:
no goals
Theorem: sterbenz
Proof state before:
case hdvd.h₁
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ a
Tactic:
trans ulp n a
Proof state after:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ ulp n a

n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n a ∣ a
Theorem: sterbenz
Proof state before:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ ulp n a

n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n a ∣ a
Tactic:
. exact ulp_dvd_ulp n hba
Proof state after:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n a ∣ a
Theorem: sterbenz
Proof state before:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n a ∣ a
Tactic:
. exact ulp_dvd_of_trunc_eq hfa
Proof state after:
no goals
Theorem: sterbenz
Proof state before:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ ulp n a
Tactic:
exact ulp_dvd_ulp n hba
Proof state after:
no goals
Theorem: sterbenz
Proof state before:
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n a ∣ a
Tactic:
exact ulp_dvd_of_trunc_eq hfa
Proof state after:
no goals
Theorem: sterbenz
Proof state before:
case hdvd.h₂
n a b : ℕ
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab : a ≤ b + b
⊢ ulp n b ∣ b
Tactic:
exact ulp_dvd_of_trunc_eq hfb
Proof state after:
no goals
Theorem: s₁'
Proof state before:
n a b x : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
h : 2 * a < b - x
⊢ trunc n (trunc n (b - x) - a) = trunc n (b - x) - a
Tactic:
induction x with
| zero =>
  rewrite [Nat.sub_zero]
  rewrite [hfb]
  exact hf
| succ w ih =>
  replace ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a := by
    apply ih
    apply Nat.lt_of_lt_of_le h
    apply tsub_le_tsub_left
    exact Nat.le_succ w
  rewrite [Nat.sub_succ, Nat.pred_eq_sub_one]
  cases eq_or_ne (trunc n (b - w)) (b - w) with
  | inr ne =>
    rewrite [trunc_pred_eq_trunc_of_trunc_ne_self npos ne]
    exact ih
  | inl hfb₁ =>
    have bpos : 0 < b - w :=
      Nat.zero_lt_of_lt $ Nat.lt_pred_iff.mp $ Nat.sub_succ _ _ ▸ h
    rewrite [trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq bpos hfb₁]
    rewrite [tsub_right_comm]
    rewrite [trunc_eq_iff_ulp_dvd]
    apply Nat.dvd_sub'
    . calc ulp n (b - w - a - ulp n (b - w - 1))
        _ ∣ ulp n (b - w - a) := ulp_dvd_ulp n tsub_le_self
        _ ∣ b - w - a         := ulp_dvd_of_trunc_eq $ hfb₁ ▸ ih
    . apply ulp_dvd_ulp
      calc b - w - a - ulp n (b - w - 1)
        _ ≤ b - w - a - 1 := tsub_le_tsub_left (Nat.one_le_of_lt $ ulp_pos n _) _
        _ ≤ b - w - 1     := tsub_le_tsub_right tsub_le_self _
Proof state after:
no goals
Theorem: s₁'
Proof state before:
case zero
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
h : 2 * a < b - Nat.zero
⊢ trunc n (trunc n (b - Nat.zero) - a) = trunc n (b - Nat.zero) - a
Tactic:
rewrite [Nat.sub_zero]
Proof state after:
case zero
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
h : 2 * a < b - Nat.zero
⊢ trunc n (trunc n b - a) = trunc n b - a
Theorem: s₁'
Proof state before:
case zero
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
h : 2 * a < b - Nat.zero
⊢ trunc n (trunc n b - a) = trunc n b - a
Tactic:
rewrite [hfb]
Proof state after:
case zero
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
h : 2 * a < b - Nat.zero
⊢ trunc n (b - a) = b - a
Theorem: s₁'
Proof state before:
case zero
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
h : 2 * a < b - Nat.zero
⊢ trunc n (b - a) = b - a
Tactic:
exact hf
Proof state after:
no goals
Theorem: s₁'
Proof state before:
case succ
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
ih : 2 * a < b - w → trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
h : 2 * a < b - Nat.succ w
⊢ trunc n (trunc n (b - Nat.succ w) - a) = trunc n (b - Nat.succ w) - a
Tactic:
replace ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a := by
  apply ih
  apply Nat.lt_of_lt_of_le h
  apply tsub_le_tsub_left
  exact Nat.le_succ w
Proof state after:
case succ
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
⊢ trunc n (trunc n (b - Nat.succ w) - a) = trunc n (b - Nat.succ w) - a
Theorem: s₁'
Proof state before:
case succ
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
⊢ trunc n (trunc n (b - Nat.succ w) - a) = trunc n (b - Nat.succ w) - a
Tactic:
rewrite [Nat.sub_succ, Nat.pred_eq_sub_one]
Proof state after:
case succ
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
⊢ trunc n (trunc n (b - w - 1) - a) = trunc n (b - w - 1) - a
Theorem: s₁'
Proof state before:
case succ
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
⊢ trunc n (trunc n (b - w - 1) - a) = trunc n (b - w - 1) - a
Tactic:
cases eq_or_ne (trunc n (b - w)) (b - w) with
| inr ne =>
  rewrite [trunc_pred_eq_trunc_of_trunc_ne_self npos ne]
  exact ih
| inl hfb₁ =>
  have bpos : 0 < b - w :=
    Nat.zero_lt_of_lt $ Nat.lt_pred_iff.mp $ Nat.sub_succ _ _ ▸ h
  rewrite [trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq bpos hfb₁]
  rewrite [tsub_right_comm]
  rewrite [trunc_eq_iff_ulp_dvd]
  apply Nat.dvd_sub'
  . calc ulp n (b - w - a - ulp n (b - w - 1))
      _ ∣ ulp n (b - w - a) := ulp_dvd_ulp n tsub_le_self
      _ ∣ b - w - a         := ulp_dvd_of_trunc_eq $ hfb₁ ▸ ih
  . apply ulp_dvd_ulp
    calc b - w - a - ulp n (b - w - 1)
      _ ≤ b - w - a - 1 := tsub_le_tsub_left (Nat.one_le_of_lt $ ulp_pos n _) _
      _ ≤ b - w - 1     := tsub_le_tsub_right tsub_le_self _
Proof state after:
no goals
Theorem: s₁'
Proof state before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
ih : 2 * a < b - w → trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
h : 2 * a < b - Nat.succ w
⊢ trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
Tactic:
apply ih
Proof state after:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
ih : 2 * a < b - w → trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
h : 2 * a < b - Nat.succ w
⊢ 2 * a < b - w
Theorem: s₁'
Proof state before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
ih : 2 * a < b - w → trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
h : 2 * a < b - Nat.succ w
⊢ 2 * a < b - w
Tactic:
apply Nat.lt_of_lt_of_le h
Proof state after:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
ih : 2 * a < b - w → trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
h : 2 * a < b - Nat.succ w
⊢ b - Nat.succ w ≤ b - w
Theorem: s₁'
Proof state before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
ih : 2 * a < b - w → trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
h : 2 * a < b - Nat.succ w
⊢ b - Nat.succ w ≤ b - w
Tactic:
apply tsub_le_tsub_left
Proof state after:
case h
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
ih : 2 * a < b - w → trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
h : 2 * a < b - Nat.succ w
⊢ w ≤ Nat.succ w
Theorem: s₁'
Proof state before:
case h
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
ih : 2 * a < b - w → trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
h : 2 * a < b - Nat.succ w
⊢ w ≤ Nat.succ w
Tactic:
exact Nat.le_succ w
Proof state after:
no goals
Theorem: s₁'
Proof state before:
case succ.inr
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
ne : trunc n (b - w) ≠ b - w
⊢ trunc n (trunc n (b - w - 1) - a) = trunc n (b - w - 1) - a
Tactic:
rewrite [trunc_pred_eq_trunc_of_trunc_ne_self npos ne]
Proof state after:
case succ.inr
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
ne : trunc n (b - w) ≠ b - w
⊢ trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
Theorem: s₁'
Proof state before:
case succ.inr
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
ne : trunc n (b - w) ≠ b - w
⊢ trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
Tactic:
exact ih
Proof state after:
no goals
Theorem: s₁'
Proof state before:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
⊢ trunc n (trunc n (b - w - 1) - a) = trunc n (b - w - 1) - a
Tactic:
have bpos : 0 < b - w :=
  Nat.zero_lt_of_lt $ Nat.lt_pred_iff.mp $ Nat.sub_succ _ _ ▸ h
Proof state after:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ trunc n (trunc n (b - w - 1) - a) = trunc n (b - w - 1) - a
Theorem: s₁'
Proof state before:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ trunc n (trunc n (b - w - 1) - a) = trunc n (b - w - 1) - a
Tactic:
rewrite [trunc_pred_eq_sub_ulp_of_pos_of_trunc_eq bpos hfb₁]
Proof state after:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ trunc n (b - w - ulp n (b - w - 1) - a) = b - w - ulp n (b - w - 1) - a
Theorem: s₁'
Proof state before:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ trunc n (b - w - ulp n (b - w - 1) - a) = b - w - ulp n (b - w - 1) - a
Tactic:
rewrite [tsub_right_comm]
Proof state after:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ trunc n (b - w - a - ulp n (b - w - 1)) = b - w - a - ulp n (b - w - 1)
Theorem: s₁'
Proof state before:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ trunc n (b - w - a - ulp n (b - w - 1)) = b - w - a - ulp n (b - w - 1)
Tactic:
rewrite [trunc_eq_iff_ulp_dvd]
Proof state after:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ b - w - a - ulp n (b - w - 1)