Can't use proof that list contains item to prove l[n] = v

Stream: new members

[aron]

I've tried to write HasType.at_ctx_index so many different ways but there always seems to be some sort of problem preventing me from doing it. This is the closest I've come (it was a good idea to do cases ht before doing induction on ctx) but now I'm getting a totally inscrutable error that I've never seen before and don't understand. All I want to do is use HasType n ctx ty to prove that ctx[n] = ty. Which should be trivial

inductive HasType {α : Type u} : (index : Nat) → List α → α → Prop where
  | stop : HasType 0 (ty :: ctx) ty
  | pop {ctx : List α} : HasType n ctx ty → HasType (n+1) (otherTy :: ctx) ty

@[reducible] def HasType.lte_ctxLen {α} {ctx : List α} {ty : α} (h : HasType n ctx ty) : n < ctx.length :=
  match ctx, h with
  | _ :: [], .stop => by simp
  | head :: tail, @HasType.pop _ n _ _ _ h => by
    simp
    exact h.lte_ctxLen
  | head :: tail, .stop => by simp [List.length]

theorem HasType.at_ctx_index (ht : HasType n ctx ty) : ctx[n]'ht.lte_ctxLen = ty := by
  cases ht with
  | stop => simp
  | pop htt =>
    expose_names
    induction ctx with
    | nil => cases htt
    | cons head tail ih =>
      have := HasType.at_ctx_index htt
      trivial

[aron]

Actually it would be amazing if I could do this both ways:

HasType n ctx ty ↔ ctx[n] = ty

which should also be totally possible just by looking at their definitions. I just can't actually work out how to do it without running into errors :big_frown:

[Aaron Liu]

This is a bug

[Aaron Liu]

This way seems to avoid it

theorem HasType.at_ctx_index (ht : HasType n ctx ty) : ctx[n]'ht.lte_ctxLen = ty := by
  induction ht with
  | stop => simp
  | @pop _ _ _ ctx htt ih =>
    cases ctx with
    | nil => cases htt
    | cons head tail => exact ih

[aron]

oh whoa. that's so so much simpler than any of the things i tried. how does ih : (head :: tail)[n✝] = ty✝ fulfil the goal of (otherTy✝ :: head :: tail)[n✝ + 1] = ty✝ here?

[aron]

it's not even using simp, so this wouldn't even reduce definitions marked with reducible, as far as i understand

[aron]

also, here's my attempt at creating a HasType. I get stuck at the end bc the goal has become HasType (nn + 1) ctx ctx[nn + 1] but i think it should be HasType (nn + 1) (other :: ctx) (other :: ctx)[nn + 1], no?

def HasType.from_prf {ctx : List α} (dblLtCtxLen : dbl < ctx.length) : HasType dbl ctx ctx[dbl] := by
  let ty := ctx[dbl]'dblLtCtxLen
  have tyIsAtIndex : ty = ctx[dbl]'dblLtCtxLen := by trivial

  induction dbl with
  | zero =>
    have : ∀ x, ctx[0] = x → ctx ≠ [] := by
      (expose_names; exact fun x a => List.ne_nil_of_length_pos dblLtCtxLen)

    cases ctx with
    | nil => contradiction
    | cons head tail =>
      have : ty = (head :: tail)[0] := by (expose_names; exact tyIsAtIndex)
      exact @HasType.stop _ ty tail
  | succ nn ih =>
    expose_names
    have : nn < ctx.length := by exact Nat.lt_of_succ_lt dblLtCtxLen
    have := ih this rfl
    refine HasType.pop this
    sorry

[aron]

but i think it should be HasType (nn + 1) (other :: ctx) (other :: ctx)[nn + 1]

ah no the last type index is fine to still be ctx[nn] because you only need the + 1 here if it was (other :: ctx)[n + 1] but since we're putting this in terms of ctx that's fine.

but yeah, i still think it should be HasType (nn + 1) (other :: ctx) ctx[nn], not HasType (nn + 1) ctx ctx[nn]

[aron]

More streamlined attempt of HasType.from_prf:

def HasType.from_prf {ctx : List α} (dblLtCtxLen : dbl < ctx.length) : HasType dbl ctx ctx[dbl] := by
  induction dbl with
  | zero =>
    have : ∀ x, ctx[0] = x → ctx ≠ [] := by
      (expose_names; exact fun x a => List.ne_nil_of_length_pos dblLtCtxLen)
    cases ctx with
    | nil => contradiction
    | cons head tail =>
      exact @HasType.stop _ head tail
  | succ nn ih =>
    expose_names
    have : nn < ctx.length := by exact Nat.lt_of_succ_lt dblLtCtxLen
    have := ih this
    refine @HasType.pop α nn ctx[nn] ?head ctx ?_
    sorry

[aron]

Woohoo I managed to prove construction of a HasType n ctx ctx[n] using only a proof that n < ctx.length:

theorem HasType.from_prf (ctx : List α) (h : n < ctx.length) : HasType n ctx ctx[n] := by
  cases ctx with
  | nil => contradiction
  | cons head tail =>
    cases tail with
    | nil =>
      have unwrap: [head][n] = head := by exact List.getElem_singleton h
      have n_eq_0: n = 0 := by exact Nat.lt_one_iff.mp h
      rw [unwrap, n_eq_0]
      exact .stop
    | cons neck taill =>
      cases n with
      | zero => exact .stop
      | succ nn =>
        refine .pop ?_
        exact HasType.from_prf (neck :: taill) _

[aron]

And now the whole thing together, including a function to convert to and from HasType n ctx ty ↔ ctx[n] = ty:

inductive HasType {α : Type u} : (index : Nat) → List α → α → Prop where
  | stop : HasType 0 (ty :: ctx) ty
  | pop {ctx : List α} : HasType n ctx ty → HasType (n+1) (otherTy :: ctx) ty

@[reducible] def HasType.lte_ctxLen {α} {ctx : List α} {ty : α} (h : HasType n ctx ty) : n < ctx.length :=
  match ctx, h with
  | _ :: [], .stop => by simp
  | head :: tail, @HasType.pop _ n _ _ _ h => by
    simp
    exact h.lte_ctxLen
  | head :: tail, .stop => by simp [List.length]

theorem HasType.at_ctx_index {ctx : List α} (ht : HasType n ctx ty) : ctx[n]'ht.lte_ctxLen = ty := by
  induction ht with
  | stop => simp
  | @pop _ _ _ ctx htt ih =>
    cases ctx with
    | nil => cases htt
    | cons head tail => exact ih

theorem HasType.from_prf (ctx : List α) (h : n < ctx.length) : HasType n ctx ctx[n] := by
  cases ctx with
  | nil => contradiction
  | cons head tail =>
    cases tail with
    | nil =>
      have unwrap: [head][n] = head := by exact List.getElem_singleton h
      have n_eq_0: n = 0 := by exact Nat.lt_one_iff.mp h
      rw [unwrap, n_eq_0]
      exact .stop
    | cons neck taill =>
      cases n with
      | zero => exact .stop
      | succ nn =>
        refine .pop ?_
        exact HasType.from_prf (neck :: taill) _

theorem HasType.ctx_both_ways {α n ty} (ctx : List α) {lenPrf : n < ctx.length} : ctx[n] = ty ↔ HasType n ctx ty := by
  apply Iff.intro
  intro h
  rw [←h]
  refine HasType.from_prf ctx ?_
  intro h
  refine HasType.at_ctx_index h