search

leanprover / theorem_proving_in_lean4

Theorem Proving in Lean 4
https://leanprover.github.io/theorem_proving_in_lean4/
Apache License 2.0
164 stars 92 forks source link

Broken div example proof chapter 8 #139

Open ketilwright opened 5 days ago

ketilwright commented 5 days ago

This example generates errors

example (x y : Nat) : div x y = if 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 := by
  conv => lhs; unfold div -- unfold occurrence in the left-hand-side of the equation

In spite of the text saying "the defining example for div does not hold definitionally. . ", I was able to rw [div]; rfl

example (x y : Nat) : div x y = if 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 := by
  rw [div]; rfl

lean --version Lean (version 4.12.0, x86_64-apple-darwin22.6.0, commit dc2533473114, Release)