Zulip Chat Archive

Stream: maths

Topic: constructe proof


Jakub Kądziołka (Mar 04 2022 at 12:57):

If I have a constructive proof of a ∃!, can I extract a witness and use it to define a function? It seems that the answer is no, since it's in Prop, and you can't eliminate out of Prop. Is there a constructive variant of ∃!, then?

Anne Baanen (Mar 04 2022 at 13:00):

No, once something is in Prop you can't get it back out into Type (unless the codomain is a (syntactic) subsingleton, in which case there is not much to get out anyway). A good constructive equivalent for ∃! might be unique { x // p x }, like subtype is the equivalent of .

Eric Wieser (Mar 04 2022 at 13:01):

I assume the context of this is #12443, where I suggested that instead of ∃! (S : finset ℕ), is_zeckendorf_rep S ∧ S.sum fib = n you define something like ℕ ≃ {f : finset ℕ // is_zeckendorf_rep f} where the forward direction of the equiv is finset.sum S fib (or at least, I suggested something analogous)

Jakub Kądziołka (Mar 04 2022 at 13:08):

yeah, though ℕ ≃ {f : finset ℕ // is_zeckendorf_rep f} doesn't really look induction-friendly

Jakub Kądziołka (Mar 04 2022 at 13:12):

If we want to make it computable, though, we might as well make it efficient, though. Does Lean support code extraction, BTW? That's where algorithmic complexity of such a construction would be most important, I think

Eric Wieser (Mar 04 2022 at 13:14):

Lean4 transpiles to C code, lean3 only "extracts" code to the VM. There are advantages to constructive approaches even if the construction isn't efficient, as often they make things easier to prove

Eric Wieser (Mar 04 2022 at 13:15):

For instance, it likely makes it easier to prove that the largest fibonacci number smaller than n is in the set, as its likely true by definition

Jakub Kądziołka (Mar 04 2022 at 13:16):

well you don't need to prove that for the solution you pick, you need to prove it for an arbitrary solution to prove uniqueness

Eric Wieser (Mar 04 2022 at 13:30):

You get uniqueness for free by proving zeckendorf_rep (l.map fib).sum = l and ((zeckendorf_rep n).map fib).sum = n, although perhaps the fist is harder to prove than proving uniqueness first (the second is easy)


Last updated: Dec 20 2023 at 11:08 UTC