simp reduce ite didn't work

Stream: new members

[Jakub Nowak]

Why split_ifs didn't work in this case? It added two subgoals with correct hypotheses, but it seems like for some reason simp cannot reduce this ite expression.

import Mathlib

open SimpleGraph

universe u
variable {V : Type u} {G : SimpleGraph V}

private def odd_cycle_of_odd_walk_step [DecidableEq V] {u v : V}
    (pref : G.Walk u v) (suf : G.Walk v u) :
    Σ w : V, G.Walk w w :=
  match suf with
  | .nil => ⟨u, Walk.nil⟩ -- unreachable
  | .cons' v w u hAdj suf' =>
    if h : w ∈ pref.support then
      let pref_pre_part : G.Walk u w := pref.takeUntil w h
      let pref_cycle_part : G.Walk w v := pref.dropUntil w h
      let cycle : G.Walk v v := .cons hAdj pref_cycle_part
      if cycle.length.bodd then
        ⟨v, cycle⟩
      else
        odd_cycle_of_odd_walk_step pref_pre_part suf'
    else
      odd_cycle_of_odd_walk_step (pref.concat hAdj) suf'

private theorem odd_cycle_of_odd_walk_step.is_cycle [DecidableEq V] {u v : V}
    (pref : G.Walk u v) (suf : G.Walk v u)
    (hPref : pref.IsPath) (hOdd : (pref.append suf).length.bodd) :
    (odd_cycle_of_odd_walk_step pref suf).snd.IsCycle := by
  cases suf with
  | nil =>
    exfalso
    simp_all
  | cons hAdj suf' =>
    rename_i w
    delta odd_cycle_of_odd_walk_step
    simp_all
    split_ifs with h

[Aaron Liu]

that's so weird

[Robin Arnez]

It's because the type changes: The type of ⋯.snd is before:

G.Walk (if ⋯¹ then ⋯² else ⋯³).fst (if ⋯¹ then ⋯² else ⋯³).fst

and then

G.Walk ⋯² ⋯²

and simp can't rewrite with type changes

[Jakub Nowak]

I see, but than, what can I do? I don't know any other way to reduce ite, other than the reduce implement in simp and split_ifs.

[Aaron Liu]

you can rw with docs#dif_pos and docs#dif_neg and docs#if_pos and docs#if_neg

[Jakub Nowak]

Robin Arnez said:

It's because the type changes: The type of ⋯.snd is before:

G.Walk (if ⋯¹ then ⋯² else ⋯³).fst (if ⋯¹ then ⋯² else ⋯³).fst

and then

G.Walk ⋯² ⋯²

and simp can't rewrite with type changes

Should I report this as an issue on github or is it already known?

[Jakub Nowak]

mwe of the issue:

import Mathlib


def ok (n : Nat) : List Nat :=
  if n = 0 then
    []
  else
    []

example (n : Nat) : ok n = [] := by
  unfold ok
  split
  -- `split` successfully split ite


def not_ok (n : Nat) : Σ α : Type, List α :=
  if n = 0 then
    ⟨Nat, []⟩
  else
    ⟨Nat, []⟩

example (n : Nat) : (not_ok n).snd = [] := by
  unfold not_ok
  split
  -- `split` didn't split ite

example (n : Nat) : (not_ok n).snd = [] := by
  unfold not_ok
  split_ifs
  -- `split_ifs` did `by_cases` but didn't manage to simplify ite
  simp_all
  -- `simp` also cannot simplify ite

example (n : Nat) : (not_ok n).snd = [] := by
  unfold not_ok
  by_cases n = 0
  · rw [if_pos]
    sorry
  · rw [if_neg]
    sorry
  -- `rw` with `if_pos`/`if_neg`/`dif_pos`/`dif_neg` works