A proof checker meant for education
jsiek.github.io
jsiek.github.io
import List
import Nathttps://docs.github.com/en/repositories/managing-your-reposi...
"You're under no obligation to choose a license. However, without a license, the default copyright laws apply, meaning that you retain all rights to your source code and no one may reproduce, distribute, or create derivative works from your work."
If I'm looking at everything else on the internet with the purpose of trying to transform it in some way, that's definitely a potential copyright issue.
Your last sentence basically admits that the fundamental legal situation of code and prose, independent of usage, is the same. If your only possible interest in code is to "transform it in some way", that's your problem, not ours.
On Github I don't just want to give that permission to github, but to everyone who clones my repo.
One thing I didn't see here is the ability to header-like file which declares the type of proofs... the syntax of deduce looks very nice though.
Files with only proofs would Compile to something akin to main = nil
ext
exact ⟨
λ p ↦ ⟨p.left.left, p.left.right, p.right⟩,
λ p ↦ ⟨⟨p.left, p.right.left⟩, p.right.right⟩
⟩
Or a maybe simpler example, for this level[1], you can use `exact λ _ xBComp xA ↦ xBComp (h1 xA)` as a one-liner. The proof here is a lambda function. It's an actual value, not unit. Moreover, within that proof, you use e.g. h1: A⊆B as a function that you can call on xA: x∈A to get a proof of x∈B. Proofs are tangible values that you can build, pull apart, pass around, and (often) call.
A lot of the set theory levels can be solved with one-liners by thinking about what the proposition actually means as a programming language construct, and then making some clever use of λ and ∘ (compose). e.g. [2] is starting to get into a complicated statement, but has a short proof where you build a pair of lambdas that each require 3 function calls. To some extent, you can even figure it out without knowing about sets and intersections by just "following the types":
exact ⟨
λ hASubIntF s hsF a haA ↦ hASubIntF haA s hsF,
λ hASubsF a haA s hsF ↦ hASubsF s hsF haA
⟩
[0] https://adam.math.hhu.de/#/g/djvelleman/stg4/world/Intersect...
[1] https://adam.math.hhu.de/#/g/djvelleman/stg4/world/Complemen...
[2] https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamInter/...
Programmers tend to call it something different because the goal is not to prove mathematical propositions but to prove static guarantees of your program.
0 = ∅
1 = Successor(0) = {0} ∪ 0 = {∅}
2 = Successor(1) = {1} ∪ 1 = {{∅}} ∪ {∅} = {{∅}, ∅} = {1, 0}
If you don't like the meaning of equality here, that is exactly my point.
My point is not that you cannot make sense of 2 = {0, 1}. You can, and this is a corner stone of encoding numbers is set theory, and it certainly describes an aspect of numbers (the set theoretic aspect). But it is not how we understand numbers usually.
And the same is true for the "Curry-Howard" way of understanding proofs.
If you want to prove to me that `A => B`, what other way is there to do so besides giving me logical steps to get from `A` to `B`? If you had a proof-of-A, would that not then be a function that takes your proof-of-A and returns a proof-of-B?
A proof is already logical steps to get from proposition A to proposition B. What you're requesting is that it should be replaced with logical steps to get from a value of type A to a value of type B, where types A and B aren't ordinary object-class types suck as "pencil" or "employee" or "goblin", nor ordinary data-structure types such as "pair(int, list(string))", but (in most cases) some completely abstract labels that you made up in order for this mapping to work. You have a cool demonstration of disjunction elimination, which of course is no simpler than actual disjunction elimination, but how will you prove something non-constructive like "x mod 2 = 0 → not (x mod 4 = 1)" in your system, and how will it not be more complicated than proving it without your system?
You mentioned passing in axioms as extra assumptions, like the law of the excluded middle. In programming terms, the law of the excluded middle is a magical function that, for every type T, returns an Either<T,Not<T>> - Not<T> being one of those made up types that only exist to make the correspondence work and don't actually mean anything. If you're working with Not you presumably also want a function that takes any Not<Not<T>> and returns a T. In programming terms this is completely unimplementable and meaningless so I'm not really sure why you think it would be useful.
It seems like you might be suffering from fuckarounditis: https://news.ycombinator.com/item?id=43466252
import Mathlib.Data.Nat.ModEq
example (h: x ≡ 0 [MOD 2]): ¬(x≡1[MOD4]) := λ xeq1mod4 ↦ by
have h24 : 2 ∣ 4 := ⟨2,by tauto⟩
have h' := (h.congr (xeq1mod4.of_dvd h24)).mp (by rfl)
contradiction
The whole thing is a proof that if you give me a proof that x=0 mod2 and x=1 mod4, I can build you a contradiction. Exactly like you'd expect in a proofs class. Since I'm a programmer, I wrote the whole thing as a big lambda function.
Note that Not[T] is also not some arcane thing. It's just Function[T,Void]. Essentially, it's a function you could never possibly call (because the whole point is that you can't get a T to call it), but if you did, it would just crash the program/throw an exception. It has an obvious purpose if you're trying to formally prove a negative.
The use of a reader monad to get a constructive-ish proof of things that need AC or LEM is just what programmers might call dependency injection. It's a normal pattern (in programming). It only "doesn't mean" something if you don't believe in those axioms at all, but even then many proofs don't need the full axiom and will work if you can bring your own choice function (e.g. you already have a basis for your vector space). Just like many (most?) real world programs basically don't need a turing machine, and actually work fine as a DFA with a trivial event loop or something.
Fwiw, you can easily construct a ¬¬T from a t: T: `λ f↦f(t)` (so make a closure that remembers your t:T and passes it into any ¬T someone gives it). LEM essentially says all ¬¬T are of this form, so you can extract the T that's hidden inside. Sort of like how functionals in finite dimensions are all secretly hiding a vector to do a dot product.
It is also useful to think like a mathematician to do programming, and I find that e.g. scala's ecosystem is a lot easier to work with for business problems than others like go or php because things tend to have more structure and predictable design, but that's a separate issue.
Another comparison you won't like: Insisting to phrase everything in terms of electrical engineering is quite useless for most applications running on a computer.
My original reply was to someone who thought proofs are all unit valued, which is the sort of confusion you get when these systems try to shy away from the programming part. The point was that proofs are things that a programmer ought to feel to be concrete, not just some trickery with type aliases of unit.
That is the danger if you get too married to the idea of proofs as programs, and think about it like a programmer, not a mathematician.
Listen, if thinking about proofs as programs helps you, great! Personally, I never found it helpful, and it never helped me solve anything.
I don't know what strategies they're using, but mathlib in Lean has formalizations for measure theory for example: https://github.com/leanprover-community/mathlib4/blob/master...
For very practical programming work (like business software), I'd be surprised if there were any useful programs that can't be boiled down to `while True: f(x)` where f(x) is some finite terminating program that you can prove stuff about. When you do a bunch of work in a language/ecosystem like Scala's, you get used to the idea that if your function says it returns an A, then it returns an A; there's generally no failure modes to consider if they're not in the type (ignoring realities like a datacenter catching on fire that are outside of the programming model). Passing a B to a `Function[B,A]` is an actual proof that you now have an `A` in your hand.
Is there any standard curriculum course for... this? (Actually, I don't know if it's a good idea to use this for learning, instead of learning Lean, because I imagine that 95% of learning Lean would be Learning its library anyway. But I never actually tried to use these kind of tools for anything.)
What makes it for education? Why can't it be used as a general purpose proof checker?
In a general purpose theorem proving environment, such as with Lean, there is a different attitude about what level of abstraction to expose by default. It's less intuitive to a child to have a tutor need to explain what it means for a function to be `unsafe` than it is to explain what it means to `print` an expression.
By creating a separate platform, you can set these defaults to curate different kinds of engagement with users. Take the `processing` language as an example. While it's Java under the hood, the careful curation of the programming environment incentivizes learners to play with it like a toy, increasing creative expression and fault-less experimentation.
This repo is closer to an intro to automated theorem proving than "Proof Designer" is (imo). Less math, more programming.
Note: Proof Designer has an excellent list of problems to try to prove. [1]