Zulip Chat Archive

Stream: new members

Topic: cases tactic failed, unexpected failure when introducing aux


Horatiu Cheval (Jun 22 2021 at 11:40):

In the following, var is a constructor depending on a natural index and a proof of a statement about it. I believe I am not mistaken in thinking that var i hi = var j hj -> i = j, as I am trying to show below. However, my go-to approach of using cases on var i hi = var j hj fails.
What's happening here? Any ideas on how to solve this?

import tactic

inductive type
| zero : type
| arrow : type  type  type

def context := list type

inductive term : context  type  Type
| var {ctx : context} {σ : type} (i : ) : ctx.nth i = some σ  term ctx σ

open term

example {ctx : context} {σ : type} {i j : } {hi} {hj} :
  @var ctx σ i hi = @var ctx σ j hj  i = j :=
begin
  intros h,
  cases h,
    /-
  cases tactic failed, unexpected failure when introducing auxiliary equalities
  state:
  ctx : context,
  σ : type,
  i : ℕ,
  hi hj : list.nth ctx i = some σ,
  h : var i hi = var i hj
  ⊢ i = i
  -/
end

Kevin Buzzard (Jun 22 2021 at 11:42):

example {ctx : context} {σ : type} {i j : } {hi} {hj} :
  @var ctx σ i hi = @var ctx σ j hj  i = j :=
begin
  intros h,
  injection h,
end

Horatiu Cheval (Jun 22 2021 at 11:46):

Thanks, I didn't know about injection

Kevin Buzzard (Jun 22 2021 at 11:46):

Shing Tak Lam told me about it last week :-)

Eric Wieser (Jun 22 2021 at 12:14):

A shorter proof:

example {ctx : context} {σ : type} {i j : } {hi} {hj} :
  @var ctx σ i hi = @var ctx σ j hj  i = j :=
var.inj

Last updated: Dec 20 2023 at 11:08 UTC