if then else in Prop

Stream: Is there code for X?

[Ka Wing Li]

Is there a way to use if-then-else in Prop? Aka, not decidable.

def bar_prop : A -> B -> Prop := fun a b => exists i, i < a, i \in b
def foo_prop : A -> B -> Prop :=
 fun a b => if bar_prop a b then sorry else sorry

[Adam Topaz]

You're missing a decidable instance.

[Ka Wing Li]

I am not sure how to make it decidable. Like the bar_prop has an existential quantifier or complex stuff.

[Robin Arnez]

You can always open Classical in before the if

[Eric Wieser]

Or you can use a conjunction of two implications

[Robin Arnez]

Yeah right the obvious (P → Q) ∧ (¬P → R) and P ∧ Q ∨ ¬P ∧ R translations work too (although they duplicate the condition term)

[Ka Wing Li]

Let me see if I can simplify stuff when translating.

[Jakub Nowak]

You could also try using inductive, something like this:

def bar_prop : A -> B -> Prop := fun a b => exists i, i < a, i ∈ b

inductive foo_prop (a : A) (b : B) : Prop
| bar_prop_ : bar_prop a b → sorry
| bar_prop_false : ¬ bar_prop a b → sorry