3 ms·

I'm not seeing how those are at all the same, or how it's convoluted to think of/require a proof to be an actual demonstration of the thing you are setting out

I'm not seeing how those are at all the same, or how it's convoluted to think of/require a proof to be an actual demonstration of the thing you are setting out to prove. 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?

immibis 2y ago
Nobody else is seeing how it is not convoluted. 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 https://news.ycombinator.com/item?id=43466252
- ndriscoll 2y ago
  They are values though! That's my whole point! These languages are constructed and written about in a way that often obscures that. A lot of them are simple things like tuple(x: int, y: int, h: x<y). Here's a constructive proof of your proposition: 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 You can see at one point, I make a proof that 2|4, which is a data structure that needs to remember that 2 is the solution to 2*n=4 as the proof. Then I pass that to a couple functions (lemmas) that require that assumption, and get an Iff, which is a pair of implications (lambda functions) going each direction. I pull out one of them and call it on a trivial proof of `x=x`. This all gives me a proof that 0=1 mod 2. Finally I can ask it to expand that definition until it reaches a 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.
  - immibis 2y ago
    Still sounds like a lot of programming that's not useful for programming but rather just adds extra complexity to proving by pretending it is programming. I don't need a function that returns undefined if I pass it an object that's 0 mod 2 and 1 mod 4 at the same time.
    - ndriscoll 2y ago
      You're in a thread about proof assistants. I'm not saying it's useful to prove number theory facts in your business code. I'm saying it's useful to embrace programming and intentionally think like a programmer to do proofs. You're the one who asked about number theory proofs. 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.
      - auggierose 2y ago
        I have contributed to proof assistants, and while programming is part of mathematics, it is not all of it. Obviously, a proof assistant is a program, but its concepts don't need to be all about programming. If they are, that is to the detriment of the mathematics done in the proof assistant. 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.
        ndriscoll 2y ago
        I didn't say you always need to phrase things in those terms, merely that it can be useful to not try to avoid them (and I wish tutorials wouldn't obscure it). It's like how geometers use d/dx as an element of the tangent space, but they don't treat it as some quirk to ignore. They actually use the fact that it's an operator too. It makes things easier. Obviously you don't need to do that with every vector space you'll ever encounter. 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.

immibis 2y ago

Nobody else is seeing how it is not convoluted. 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 https://news.ycombinator.com/item?id=43466252

ndriscoll 2y ago
They are values though! That's my whole point! These languages are constructed and written about in a way that often obscures that. A lot of them are simple things like tuple(x: int, y: int, h: x<y). Here's a constructive proof of your proposition: 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 You can see at one point, I make a proof that 2|4, which is a data structure that needs to remember that 2 is the solution to 2*n=4 as the proof. Then I pass that to a couple functions (lemmas) that require that assumption, and get an Iff, which is a pair of implications (lambda functions) going each direction. I pull out one of them and call it on a trivial proof of `x=x`. This all gives me a proof that 0=1 mod 2. Finally I can ask it to expand that definition until it reaches a 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.
- immibis 2y ago
  Still sounds like a lot of programming that's not useful for programming but rather just adds extra complexity to proving by pretending it is programming. I don't need a function that returns undefined if I pass it an object that's 0 mod 2 and 1 mod 4 at the same time.
  - ndriscoll 2y ago
    You're in a thread about proof assistants. I'm not saying it's useful to prove number theory facts in your business code. I'm saying it's useful to embrace programming and intentionally think like a programmer to do proofs. You're the one who asked about number theory proofs. 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.
    - auggierose 2y ago
      I have contributed to proof assistants, and while programming is part of mathematics, it is not all of it. Obviously, a proof assistant is a program, but its concepts don't need to be all about programming. If they are, that is to the detriment of the mathematics done in the proof assistant. 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.
      - ndriscoll 2y ago
        I didn't say you always need to phrase things in those terms, merely that it can be useful to not try to avoid them (and I wish tutorials wouldn't obscure it). It's like how geometers use d/dx as an element of the tangent space, but they don't treat it as some quirk to ignore. They actually use the fact that it's an operator too. It makes things easier. Obviously you don't need to do that with every vector space you'll ever encounter. 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.