Syntax sugar for `dite`

Stream: new members

[Pedro Minicz]

Is there syntax sugar for dite? It would be nice to have a "dependent if" or maybe if could add the hypothesis to the context and generate ite or dite based on whether or not it was used.

example {n : ℕ} (f : fin (n + 2)) : fin (n + 1) :=
if f = 0 then 0 else f.pred _

example {n : ℕ} (f : fin (n + 2)) : fin (n + 1) :=
dite (f = 0) (λ _, 0) f.pred

[Reid Barton]

if h : f = 0 then 0 else f.pred h

[Mario Carneiro]

if h : p then t else e = dite p (\lam h, t) (\lam h, e)

[Pedro Minicz]

Thank you very much!

[Pedro Minicz]

Is there an equivalent for match? I want a proof of equality with (e.g. cmp x y = lt) in each branch like I would have with the cases tactic.

  match cmp x y with
  | ordering.lt := sorry -- I want a hypothesis `h : cmp x y = lt` here!
  | ordering.eq := sorry
  | ordering.gt := sorry
  end

[Pedro Minicz]

I came up with the following, which is horribly ugly.

  @ordering.cases_on (λ o, cmp x y = o → term Γ) (cmp x y)
    (λ h, sorry)
    (λ h, sorry)
    (λ h, sorry) rfl

[Pedro Minicz]

I am trying to define a function that lives on Type. I remember seeing here a while ago that tactics should only be used to generate proof and not definitions of function.

[Yury G. Kudryashov]

You should not use tactics for definitions if you care about details of the generated term (e.g., presence of unneeded ids etc). If you don't care, then you can use tactics.

[Yury G. Kudryashov]

You can also define mydef using tactics, then #print mydef.

[Yury G. Kudryashov]

I don't know how to deal with match but you can use something like this (from algebra/order):

/-- `compares o a b` means that `a` and `b` have the ordering relation
  `o` between them, assuming that the relation `a < b` is defined -/
@[simp] def compares [has_lt α] : ordering → α → α → Prop
| lt a b := a < b
| eq a b := a = b
| gt a b := a > b

theorem compares.eq_lt [preorder α] :
  ∀ {o} {a b : α}, compares o a b → (o = lt ↔ a < b)
| lt a b h := ⟨λ _, h, λ _, rfl⟩
| eq a b h := ⟨λ h, by injection h, λ h', (ne_of_lt h' h).elim⟩
| gt a b h := ⟨λ h, by injection h, λ h', (lt_asymm h h').elim⟩

theorem compares.eq_eq [preorder α] :
  ∀ {o} {a b : α}, compares o a b → (o = eq ↔ a = b)
| lt a b h := ⟨λ h, by injection h, λ h', (ne_of_lt h h').elim⟩
| eq a b h := ⟨λ _, h, λ _, rfl⟩
| gt a b h := ⟨λ h, by injection h, λ h', (ne_of_gt h h').elim⟩

[Yury G. Kudryashov]

Now I know:

lemma ordering.compares.symm {α} [has_lt α] {x y : α} (o : ordering) (h : o.compares x y) :
  o.swap.compares y x :=
match o, h with
| ordering.lt, h := h
| ordering.eq, h := h.symm
| ordering.gt, h := h
end

[Pedro Minicz]

Yury G. Kudryashov said:

Now I know:

lemma ordering.compares.symm {α} [has_lt α] {x y : α} (o : ordering) (h : o.compares x y) :
  o.swap.compares y x :=
match o, h with
| ordering.lt, h := h
| ordering.eq, h := h.symm
| ordering.gt, h := h
end

I ended up setting for a solution using algebra/order. This lemma is very elegant, thank you!