Equality between type and constructor indices

Stream: general

[Patrick Johnson]

What is the recommended way to deal with this?

inductive T {α : Type} (s : set α) : list α → Prop
| mk₁ : T []
| mk₂ {xs x} : T xs → x ∈ s → T (xs ++ [x])

example {α : Type} {s : set α} {x xs} (h : T s (xs ++ [x])) : T s xs :=
begin
  cases h, -- cases tactic failed, unsupported equality between type and constructor indices
  assumption,
end

It can be solved by replacing xs ++ [x] with another variable and then substituting it back.
For example:

example {α : Type} {s : set α} {x xs} (h : T s (xs ++ [x])) : T s xs :=
begin
  revert h, generalize h₁ : xs ++ [x] = ys, intro h, cases h,
  { cases (list.append_eq_nil.mp h₁).2 },
  { have h₁ : _ = list.reverse (_ ++ _) := congr_arg _ h₁,
    simp at h₁, rcases h₁ with ⟨rfl, rfl⟩, assumption },
end

Is there a better way?

[Floris van Doorn]

cases can automatically deal with goals that cannot apply because they are different constructors to an inductive type. To explain, let's consider the easier case of nat:

• nat.succ n and nat.zero are different constructors, so cases can prove this:

example (n : ℕ) : nat.succ n ≠ nat.zero := by { intro h, cases h }

• n + 1 and 0 reduce to different constructors (after unfolding definitions this is the same problem as before - addition on natural numbers is defined by recursion on the second argument), so cases can also deal with this:

example (n : ℕ) : n + 1 ≠ 0 := by { intro h, cases h }

• 1 + n and 0 do not reduce to different constructors. In fact, since + is defined by recursion on the second argument, 1 + n doesn't reduce at all. Of course the terms are unequal, but cases cannot find this for you. So this doesn't work:

example (n : ℕ) : 1 + n ≠ 0 := by { intro h, cases h }

How this applies to your example is that xs ++ [x] is not a different constructor from [], since ++ is defined by recursion on the first argument. One way to solve this, is to replace xs ++ [x] by x :: xs:

inductive T {α : Type} (s : set α) : list α → Prop
| mk₁ : T []
| mk₂ {xs x} : T xs → x ∈ s → T (x :: xs)

example {α : Type} {s : set α} {x xs} (h : T s (x :: xs)) : T s xs :=
begin
  cases h, -- works!
  assumption,
end

I don't know if this works in your actual use case.

[Patrick Johnson]

I know how cases work, I didn't expect from cases,assumption to solve the goal. My question was, if you already have a type defined like T which uses append singleton instead of cons, and you need to prove T xs from T (xs ++ [x]), how would you do it?

Is there a tactic similar to cases that fallbacks to eq whenever it fails to unify using defeq? I would like a tactic that can transform this:

example {α : Type} {s : set α} {x xs} (h : T s (xs ++ [x])) : T s xs :=
begin
  cases' h,
end

Into this:

Two goals:

α: Type
s: set α
x: α
xs: list α
h: xs ++ [x] = []
⊢ T s xs

α: Type
s: set α
x: α
xs ys: list α
y: α
h₁: T s ys
h₂: y ∈ s
h₃: xs ++ [x] = ys ++ [y]
⊢ T s xs

And then we could easily prove it:

example {α : Type} {s : set α} {x xs} (h : T s (xs ++ [x])) : T s xs :=
begin
  cases' h,
  { cases (list.append_eq_nil.mp h).2 },
  { have h₃ := congr_arg list.reverse h₃, simp at h₃, simpa [h₃] },
end

[Floris van Doorn]

Try import tactic.induction: it will provide the cases' tactic that will does what you want (it does not support custom induction principles though).