Definition by cases on logical or?

Stream: new members

[Nicholas Dyson]

If I understand logical OR in the context of constructive logic correctly (which I may not), if we have a proof of (a \/ b) then by definition we "know" whether it's a proof of a or a proof of b. Can I write a function definition that takes a proof of (a \/ b) as one of its arguments and then has two different evaluation paths, one of which uses a proof of a to create the return value and one of which uses a proof of b to create it?

I know this is a simple question but I've been reviewing the documentation and can't find anything. Thanks a lot for any advice!

[Eric Wieser]

No, because that would be logically inconsistent, and allow you to prove false

[Eric Wieser]

You can inspect it with #reduce though to find out how the proof was constructed

[Nicholas Dyson]

Why's that inconsistent? The cases tactic allows us to say "if the left-hand-side of the OR is true, do this; if the right-hand-side of the OR is true, do this". How is it different doing that in a function definition than in a proof? I'm very curious now.

[Eric Wieser]

The contradiction:

variables {P Q : Prop}

constant is_from_inl (a : P ∨ Q) : bool
axiom is_from_inl_inl (p : P) (Q) : is_from_inl (or.inl p : P ∨ Q) = tt
axiom is_from_inl_inr (P) (q : Q) : is_from_inl (or.inr q : P ∨ Q) = ff

example : false := begin
  have hl := is_from_inl_inl trivial true,
  have hr := is_from_inl_inr true trivial,
  exact bool.ff_ne_tt (hr.symm.trans hl)
end

[Eric Wieser]

Here I'm using axiom / constant as a quick way to say "imagine such a function existed"

[Eric Wieser]

It's inconsistent because of docs#proof_irrel - two proofs of the same proposition are always equal, which means any function of those proofs must always be equal

[Eric Wieser]

If you want to compute based on which side is true, you can use docs#psum instead of docs#or, as:

def foo {P Q : Prop} : psum P Q → bool
| (psum.inr x) := tt
| (psum.inl x) := ff

[Nicholas Dyson]

Ah, I think I get it now. Thanks for the information.