# Zulip Chat Archive

## Stream: new members

### Topic: Syntax sugar for `dite`

#### Pedro Minicz (Jul 04 2020 at 03:04):

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 (Jul 04 2020 at 03:04):

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

#### Mario Carneiro (Jul 04 2020 at 03:05):

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

#### Pedro Minicz (Jul 04 2020 at 03:09):

Thank you very much!

#### Pedro Minicz (Jul 05 2020 at 02:24):

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 (Jul 05 2020 at 02:45):

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 (Jul 05 2020 at 02:47):

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 (Jul 05 2020 at 03:51):

You should not use tactics for definitions if you care about details of the generated term (e.g., presence of unneeded `id`

s etc). If you don't care, then you can use tactics.

#### Yury G. Kudryashov (Jul 05 2020 at 03:51):

You can also define `mydef`

using tactics, then `#print mydef`

.

#### Yury G. Kudryashov (Jul 05 2020 at 03:53):

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 (Jul 05 2020 at 03:55):

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 (Jul 06 2020 at 03:03):

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!

Last updated: May 14 2021 at 22:15 UTC