rw/simp on value replaces it, existing refs are to old value

Stream: new members

[aron]

When I rw or simp a value that is referenced by a type, lean creates a new value instead of changing the old value in place. This means that the type now references the old, unchanged value. Why is this and how can I prevent this from happening?

/-- A list which you add items onto at the end -/
inductive Ctx (α : Type u)
  | nil : Ctx α
  | add (body : Ctx α) (tip : α) : Ctx α

@[reducible] def Ctx.length {α} (ctx : Ctx α) : Nat :=
  match ctx with
  | .nil => 0
  | .add ctx _ => ctx.length + 1

@[reducible] def Ctx.tryGet (ctx : Ctx α) (n : Nat) : Option α :=
  if hlen : n >= ctx.length then
    none
  else if hlen : n + 1 = ctx.length then
    match hctx : ctx with
    | .nil => by
      simp at hlen
    | .add _ tip => tip
  else
    match ctx with
    | .nil => by
      expose_names
      simp at hlen_1
    | .add inner _ =>
      inner.tryGet n



@[reducible] def Ctx.get {α : Type} (ctx : Ctx α) (n : Nat) (h : n < ctx.length) : α :=
  match ctx, n with
  | .add inner tip, _ =>
    -- since we know this index is in the list, the only way we would get a `none` here is if the index is exactly the last item in the list, i.e. the tip
    match inner.tryGet n with
    | none => tip
    | some item => item



/-- This is a type that proves that in this `ctx`, the item at index `n` is `a` -/
inductive HasItem {α : Type u} : (index : Nat) → (ctx : Ctx α) → (a : α) → Prop where
  | stop : HasItem 0 (.add .nil a) a
  | pop {ctx : Ctx α} : HasItem n ctx a → HasItem (n+1) (.add ctx other) a



theorem HasItem.from_ctx_get {ctx : Ctx α} {h : n < ctx.length} (prf : ctx.get n h = a) : HasItem n ctx a := by
    rcases ctx with _ | _ | _
    case nil => simp at h
    case _ tip =>
      simp only [Ctx.length] at h

      -- This makes `prf` reference `h✝` instead of `h`! How can I change `h` in-place?
      simp at h

      sorry

    case _ => sorry

[Aaron Liu]

Why do you want to do this?

[aron]

because i want to create a HasItem n ctx a

[aron]

and if we know ctx.get n h = a that should be sufficient to construct one

[Aaron Liu]

I guess you could subst h to replace n with 0 everywhere

[Aaron Liu]

Then you can start unfolding the definition of Ctx.get

[Aaron Liu]

But I don't think changing the proof that it is using will do anything.

[aron]

oh god :face_palm: yeah, if I just unfold Ctx.get then I get rid of h altogether and I don't need to worry about it anymore!

[aron]

thanks @Aaron Liu :folded_hands:

[aron]

Hm in addition to my original question, I think my HasItem type is actually malformed :thinking: I think it currently looks like it tells you the index from the start but in actuality it's impossible to make a HasItem ctx n a for any item that isn't at index 0

[aron]

I think in the original snippet I adapted this from, the index is from the end of the list, not the beginning