constructe proof

Stream: maths

[Jakub Kądziołka]

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]

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]

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]

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

[Jakub Kądziołka]

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]

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]

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]

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]

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)