4 ms·

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 thi

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.
      - auggierose 2y ago
        > My original reply was to someone who thought proofs are all unit valued 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.

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.
    - auggierose 2y ago
      > My original reply was to someone who thought proofs are all unit valued 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.