max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: avoid unnecessary h :s

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-19 11:21:37 -07:00
parent f29319647f
commit 72b6f4d528
1 changed files with 8 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Init/Data/Nat/Div.lean
View file

@ -14,7 +14,7 @@ private def div_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=
@[extern "lean_nat_div"]
protected def div (x y : @& Nat) : Nat :=
if h : 0 < y ∧ y ≤ x then
if 0 < y ∧ y ≤ x then
Nat.div (x - y) y + 1
else
0
@ -23,8 +23,9 @@ decreasing_by apply div_rec_lemma; assumption
instance : Div Nat := ⟨Nat.div⟩
theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 := by
simp [Nat.div] -- hack to force eq theorem to be generated. We don't have `conv` yet.
apply Nat.div._eq_1
show Nat.div x y = _
rw [Nat.div]
rfl
theorem div.inductionOn.{u}
{motive : Nat → Nat → Sort u}
@ -40,7 +41,7 @@ decreasing_by apply div_rec_lemma; assumption
@[extern "lean_nat_mod"]
protected def mod (x y : @& Nat) : Nat :=
if h : 0 < y ∧ y ≤ x then
if 0 < y ∧ y ≤ x then
Nat.mod (x - y) y
else
x
@ -49,8 +50,9 @@ decreasing_by apply div_rec_lemma; assumption
instance : Mod Nat := ⟨Nat.mod⟩
theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x := by
simp [Nat.mod] -- hack to force eq theorem to be generated. We don't have `conv` yet.
apply Nat.mod._eq_1
show Nat.mod x y = _
rw [Nat.mod]
rfl
theorem mod.inductionOn.{u}
{motive : Nat → Nat → Sort u}