rw matches wrong equation

Stream: new members

[Guilherme Espada]

Given the following mwe:

import tactic.suggest
import data.finset
import data.finmap
import data.list
import data.finmap
import tactic.linarith

@[derive decidable_eq]
inductive ttype
| ty_func (l r:ttype): ttype
| ty_bool : ttype

open ttype


instance : inhabited ttype := inhabited.mk ty_bool

@[derive decidable_eq]
inductive term
|t_var (idx:int) : term
|t_abs (T:ttype) (t:term) : term
|t_app (t1 t2: term) : term
|t_true : term
|t_false : term
|t_if (cond l r: term): term

open term

abbreviation ctxtype := list ttype

def lookup_list : ctxtype → int → option ttype
| (head :: tail) 0  := some head
| (head :: tail) n  := lookup_list tail (n-1)
| list.nil _ := none
@[simp]
def in_ctx (idx: int) (val: ttype) (ctx:ctxtype) := lookup_list ctx idx = (some val)


example {ctx : list ttype} {S T : ttype} (t_ᾰ : 0 ≥ 0)
  (inctx : lookup_list (T :: ctx) 0 = some S) :
  T = S :=
begin
  rw lookup_list at inctx, --here
end

I would expect the rewrite to produce a term in the context of the form some T = some S. However, it instead produces two goals, one of which is unprovable (¬ 0 = 0). What is happening here?

Thanks,

[Guilherme Espada]

It seems to be matching the second equation rather than the first?

[Guilherme Espada]

I'm guessing the unprovable goal comes from this lookup_list.equations._eqn_3 : ∀ (head : ttype) (tail : list ttype) (n : ℤ), ¬n = 0 → lookup_list (head :: tail) n = lookup_list tail (n - 1)

[Guilherme Espada]

But I'm not sure why it's matching the second one rather than the first.

[Horatiu Cheval]

I have no idea about the reasons, but in any case, to solve your goal, instead of rw you can do

example {ctx : list ttype} {S T : ttype} (t_ᾰ : 0 ≥ 0)
  (inctx : lookup_list (T :: ctx) 0 = some S) :
  T = S :=
begin
  simp only [lookup_list] at inctx,
  assumption,
end

or

example {ctx : list ttype} {S T : ttype} (t_ᾰ : 0 ≥ 0)
  (inctx : lookup_list (T :: ctx) 0 = some S) :
  T = S :=
begin
  unfold lookup_list at inctx,
  cases inctx,
  refl,
end

and it works.

[Guilherme Espada]

Thanks! I made a lemma with this workaround for now until I find the root cause.

[Horatiu Cheval]

On an unrelated note, is lookup_list intended to find the nth element in the context? If so, is there a reason for it to have an int argument instead of a nat one? I imagine for some proofs and defs it would be easier to work with nat. And also, if it helps, there exists list.nth which does precisely that.

[Guilherme Espada]

It has an int argument because I forgot to change it back while I was experimenting with different types.

list.nth is a great suggestion, and it doesn't have this issue! Thank you :smile: