Zulip Chat Archive

Stream: new members

Topic: by_cases in term mode definition?


view this post on Zulip ROCKY KAMEN-RUBIO (Jul 04 2020 at 19:30):

Is there a way to do the equivalent of by_cases in term mode? Specifically, I mean check whether a given condition is met so we can call another definition/theorem that requires it, else give some other value. Here's an example

def h (a b : ) (h : a  b) : Prop := 1 / (a - b) > 0

def g' (a b : ) : Prop :=
begin
  by_cases hab : a = b,
  {exact tt},
  exact h a b hab,
end

def g (a b : ) : Prop := a = b  h a b _,

view this post on Zulip Mario Carneiro (Jul 04 2020 at 20:02):

if hab : a = b then tt else h a b hab

view this post on Zulip Mario Carneiro (Jul 04 2020 at 20:03):

That's the direct translation, but in this case you can use \forall hab : a != b, h a b hab


Last updated: May 15 2021 at 00:39 UTC