Zulip Chat Archive

Stream: new members

Topic: Syntax sugar for `dite`


view this post on Zulip 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

view this post on Zulip Reid Barton (Jul 04 2020 at 03:04):

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

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

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

view this post on Zulip Pedro Minicz (Jul 04 2020 at 03:09):

Thank you very much!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jul 05 2020 at 03:51):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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