fix: Update examples to work with latest Lean nightly #107
Conversation
github-actions
bot
temporarily deployed
to
lean-lang.org/theorem_proving_in_lean4
david-christiansen
force-pushed
the
nightly-update
branch
from
a28a8cf to
1bf8c57
Compare
github-actions
bot
temporarily deployed
to
lean-lang.org/theorem_proving_in_lean4
| @@ -1100,10 +1100,11 @@ theorem linv_comp_self {f : α → β} [Inhabited α] | |||
| have ex : ∃ a₁ : α, f a₁ = f a := ⟨a, rfl⟩ | |||
| have feq : f (choose ex) = f a := choose_spec ex | |||
| calc linv f (f a) | |||
| _ = choose ex := dif_pos ex | |||
| _ = choose ex := by simp | |||
There was a problem hiding this comment.
This fixes an error where dif_pos's implicit arguments were not being found (namely the Decidable instance and the else branch). This lemma is really designed to be used with simp rather than directly, and simp solves the goal.
| @@ -43,10 +43,10 @@ constant of such a type. | |||
| # proof : p | |||
| #check Proof -- Proof : Prop → Type | |||
|
|
|||
| axiom and_comm (p q : Prop) : Proof (Implies (And p q) (And q p)) | |||
| axiom and_commutative (p q : Prop) : Proof (Implies (And p q) (And q p)) | |||
There was a problem hiding this comment.
We now have and_comm in scope by default. I chose to rename it here, rather than secretly stick it in a namespace, because I want code bits to work if people type them in.
On the other hand, the hidden Proof structure is not present, so this is a very weak argument for this solution. Happy to do the other one if you'd prefer.
| calc | ||
| x ∣ y := h₁ | ||
| _ = z := h₂ | ||
| _ ∣ 2*z := divides_mul .. |
There was a problem hiding this comment.
This notation is now built-in, and they were conflicting. It didn't seem to be worth a longer aside in the text to save this, so I deleted it.
| def Divides (x y : Nat) : Prop := | ||
| ∃ k, k*x = y | ||
|
|
||
| def divides_trans (h₁ : divides x y) (h₂ : divides y z) : divides x z := | ||
| def Divides_trans (h₁ : Divides x y) (h₂ : Divides y z) : Divides x z := | ||
| let ⟨k₁, d₁⟩ := h₁ | ||
| let ⟨k₂, d₂⟩ := h₂ | ||
| ⟨k₁ * k₂, by rw [Nat.mul_comm k₁ k₂, Nat.mul_assoc, d₁, d₂]⟩ | ||
|
|
||
| def divides_mul (x : Nat) (k : Nat) : divides x (k*x) := | ||
| def Divides_mul (x : Nat) (k : Nat) : Divides x (k*x) := | ||
| ⟨k, rfl⟩ | ||
|
|
||
| instance : Trans divides divides divides where | ||
| trans := divides_trans | ||
| instance : Trans Divides Divides Divides where | ||
| trans := Divides_trans | ||
|
|
||
| example (h₁ : divides x y) (h₂ : y = z) : divides x (2*z) := | ||
| example (h₁ : Divides x y) (h₂ : y = z) : Divides x (2*z) := | ||
| calc | ||
| divides x y := h₁ | ||
| Divides x y := h₁ | ||
| _ = z := h₂ | ||
| divides _ (2*z) := divides_mul .. | ||
| Divides _ (2*z) := Divides_mul .. |
There was a problem hiding this comment.
This is just a rename to more closely follow Lean 4 conventions while I was here
|
@avigad - I believe you're the right one to approve these changes. If not, let me know, and I'll start working down the list of co-authors. Thanks! |
These changes allow the tests to pass with the latest Lean nightly again.