## 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 ids 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