ite_then_ite

Stream: Is there code for X?

[Scott Morrison]

Do we have lemmas like

lemma ite_then_dite {P Q : Prop} [decidable P] [decidable Q] {α : Type*} (a : α) (b : Q → α) (c : ¬Q → α) :
  (if P then (if h : Q then b h else c h) else a) = if h : Q then (if P then b h else a) else (if P then c h else a) :=
by split_ifs; refl

lemma ite_else_dite {P Q : Prop} [decidable P] [decidable Q] {α : Type*} (a : α) (b : Q → α) (c : ¬Q → α) :
  (if P then a else (if h : Q then b h else c h)) = if h : Q then (if P then a else b h) else (if P then a else c h) :=
by split_ifs; refl

in the library somewhere? I guess there are further variants change ite and dite.

[Yaël Dillies]

I had those lemmas on a branch then I noticed those were just applications of ite_apply and apply_ite

[Yaël Dillies]

If you really want them as standalone lemmas, I can PR them.

[Scott Morrison]

I'd like to rewrite by them, so yes I think I want them not just as ite_apply.

[Scott Morrison]

That would be lovely if you wanted to PR them. :-)

[Scott Morrison]

Ping me and I'll hit merge!

[Yaël Dillies]

Will do!

[Eric Wieser]

Is docs#if_assoc similar?

[Eric Wieser]

Hmm, I was sure that existed

[Yaël Dillies]

No, it doesn't because the branches don't really work out.

[Yaël Dillies]

I'm a bit mad at myself because I deleted the branch both on my local git and on Github :angry_cat:

[Mauricio Collares]

git reflog? And then git cherry-pick it onto a new branch if you find the missing commit

[Yaël Dillies]

Even if it was a month ago?

[Eric Wieser]

If it hasn't done a GC, then it should still be there

[Yaël Dillies]

Yeah I found it :smiley:

[Yaël Dillies]

#14146