Oooh, bikeshedding! To me your `import math with x as y` reads like "import all of math, making all of its symbols visible, just renaming some of them". That's different from the intended "from math, import only x (maybe with a renaming)".
This is someone's private project for their own amusement. It's clearly not in a state where it would be "useful" to "users". Nor is it meant to be. At the moment it's meant for compiler geeks to look at.
Not every readme is a sales pitch for Enterprise Quality(tm) software.
> It would be like if I were helping you get to work in the morning, and I said, "Okay, you're current [sub]goal is that you're done brushing your teeth." No. That's not a goal. That's progress toward a goal.
Interesting. Let's say our overall goal is to get to work showered, wearing clean clothes, and having brushed our teeth. After we showered and put on clean clothes, wouldn't you say that the remaining goal is to brush our teeth and get to work? And if we then do brush our teeth, wouldn't you say that the remaining goal is to get to work? In this scenario, if anything can be called progress, it is what's in the past (the showering etc.), not what is still to be done.
>Let's say our overall goal is to get to work showered, wearing clean clothes, and having brushed our teeth. After we showered and put on clean clothes, wouldn't you say that the remaining goal is to brush our teeth and get to work?
Yes, I agree! My issue is not with the reality of having reduced the problem to a different one, but with the "goal" metaphor, which is counterintuitive to how that term is normally used, especially since it connotes that each step is some brand new thing, rather than progress.
And sure, like any technical jargon, you can learn to accept some specialized term-of-art usage, but I'd prefer it be conducive to developing a correct ontology of what is going on in an assisted Lean proof.
While "subgoal" is better, I think the issue even goes back to calling the original theorem a "goal". Really, the goal is to prove the theorem. So a better term, more conducive to intuiting the Lean ontology, would be something like "[remaining] unresolved proof state", even though it's more verbose. (Perhaps you could get the best of both worlds with some kind of footnote for new users that clarifies that this is what "goal" means here.)
With that said, I appreciate the pushback, as your comment forced me to more carefully think about what I was objecting to.
Gotcha. I've never had a problem with this usage. I guess I see the objection of "the goal is to prove the theorem" vs. "the (initial) goal is the theorem". It strikes me as overly pedantic, but we're talking about formal methods, so I guess pedanticism is warranted.
I do want to note that systems usually use terms like "current goal" or "active goal", which do imply a sense of progress. I never felt that they imply that the current goal is a brand-new thing. It's a transformed version of the previous goal, hopefully made up of simpler parts that eventually become so simple as to be trivial, which then completes the overall proof.
Nitpick, but it's a bit strange to say that the two_eq_two theorem looks like a function. It looks more like a constant, since it has no arguments. (Yes I know that constants are nullary functions.)
I would find the following a more convincing presentation:
theorem x_eq_x (x:nat) : x = x := by
rfl
theorem 2_eq_2 : 2 = 2 := by
exact (x_eq_x 2)
Here x_eq_x looks like a function, and in 2_eq_2's proof we apply it like a function.
Fair! I decided not to do that because the way arguments work (and dependent types in general — like being able to return a proof of `x = x` given x) is unusual for people like me, and deserves an article of its own. So I’m kicking that to one of the next articles.
Rocq used to have a "mathematical proof language". It's hard to find examples, but this shows the flavor (https://stackoverflow.com/a/40739190):
Lemma foo:
forall b: bool, b = true -> (if b then 0 else 1) = 0.
proof.
let b : bool.
per cases on b.
suppose it is true. thus thesis.
suppose it is false. thus thesis.
end cases.
end proof.
Qed.
So the idea was to make proofs read more like "manual" proofs as you would find them in math papers. Apparently nobody used this, so it was removed.
lemma "map f xs = map f ys ==> length xs = length ys"
proof (induct ys arbitrary: xs)
case Nil thus ?case by simp
next
case (Cons y ys) note Asm = Cons
show ?case
proof (cases xs)
case Nil
hence False using Asm(2) by simp
thus ?thesis ..
next
case (Cons x xs’)
with Asm(2) have "map f xs’ = map f ys" by simp
from Asm(1)[OF this] ‘xs = x#xs’‘ show ?thesis by simp
qed
qed
You spell out the structure and intermediate results you want, and the "by ..." blocks allow you to specify concrete tactics for parts where the detains don't matter and the tactic does what you want. In this proof, "simp" (a kind of simplify/reflexivity tactic) is enough for all the intermediate steps.
I don't know if there is anything like this for Lean, but maybe this provides some keywords for a web search. Or inspiration for a post in some Lean forum.
You can structure your proofs in Lean to reason forward, but proofs in Mathlib still primarily do backward proof, because it is more compact and performant.
Declarative proof languages support backward proof, typically phrased as: "suffices <statement> by ... " i.e. it suffices to show <statement>, and the current goal follows.
Yes, there is a prelude that defines natural numbers and an addition function on them. As the post notes, the reflexivity tactic "unfolds" the addition, meaning that it applies the addition function to the constants it is given, to arrive at a constant. This is not specific to addition, it unfolds other function definitions too. So addition doesn't have to come first, you are right that reflexivity is more fundamental.
Author here — this is correct. I’ve added a paragraph on this in an edit btw so it’s possible the parent poster hasn’t seen it yet. Reproducing the paragraph:
(Here, rfl closes ⊢ 3 + 3 = 6, but for a different reason than one might think. It doesn’t really “know” that 3 + 3 is 6. Rather, rfl unfolds the definitions on both sides before comparing them. As 3, 6, and + get unfolded, both sides turn into something like Nat.zero.succ.succ.succ.succ.succ.succ. That’s why it actually is a something = something situation, and rfl is able to close it.)
Zero being even is not contentious. Contention is when there is strong disagreement whereas people who are misinformed can be mathematically proven to be incorrect.
By your reasoning you could call all higher mathematics "contentious" because laypeople would come to wrong conclusions due to inexperience. It devalues the word.
OK, if you're going to be prescriptive, I'm going to be prescriptive too.
https://en.wiktionary.org/wiki/contentious
"1. Marked by heated arguments or controversy."
There are heated arguments about this (among laypeople). The people arguing heatedly happen to be wrong, but the dictionary doesn't say that the heated arguments must have merit, only that they happen.
BTW, your "There is literally no credible argument why 0 would be considered odd." suggests that you didn't read the linked Wikipedia page and didn't look at the results of the Mastodon poll. Take a look what actual laypeople self-report about their position on this issue.
I can, yes. Laypeople might not be able to, or be aware of the various (equivalent) accepted definitions.
And yes, this means that many laypeople are not effective at doing mathematics. Does this surprise you? If yes, then the linked article and Mastodon thread may be interesting to you. Which is why I submitted them.
Many subway systems have displays showing that the next train is right behind the current one, and yet many people still insist on getting on the current overcrowded one.
Certainly with buses people have been burned where they are told that another bus will be along in 2 minutes only for that to evaporate and the next bus actually takes 15+ minutes. If that happens to you then you'll squeeze onto the first bus you can physically fit.
It takes quite a long period of good service to undo one bad interaction.
I'd argue that that's not bunching, it's the entire system being overloaded. A characteristic of bunching is that you have a pair of vehicles which together carry an average manageable load of passengers, but that load is unevenly distributed between them.
