Proof irrelevance ignored?

Stream: new members

[aron]

My attempt to prove a goal fails with this error:

type mismatch
  this
has type
  (@set' α len tail j' ⋯ a)[n'] = tail[n'] : Prop
but is expected to have type
  (@set' α len tail j' ⋯ a)[n'] = tail[n'] : Prop

The only difference between these two is the proof. The former has proof:

?m.67165 tail n' j' (Nat.succ_lt_succ_iff.mp jlt) nneqj : j' < len

And the latter:

Nat.succ_lt_succ_iff.mp jlt : j' < len

But why is this causing an issue if proofs are irrelevant anyway?

import Mathlib

section Vec

inductive Vec (α : Type u) : Nat → Type u
  | nil : Vec α 0
  | cons : α → Vec α n → Vec α (n + 1)


@[match_pattern] infixr:67 " :: " => Vec.cons
@[match_pattern] notation "[]" => Vec.nil
@[match_pattern] notation "[" t "]" => Vec.cons t []

example : Vec Nat 3 := 1 :: 2 :: 3 :: []

def Vec.map (vec : Vec α n) (f : α → β) : Vec β n :=
  match vec with
  | [] => []
  | head :: tail => f head :: tail.map f

instance : Functor (Vec · n) where
  map f a := Vec.map a f

def Vec.mem [DecidableEq α] (vec : Vec α n) (item : α) : Prop :=
  match vec with
  | [] => False
  | head :: tail => if head = item then True else mem tail item


instance [DecidableEq α] : Membership α (Vec α n) where
  mem := Vec.mem





@[reducible] def Vec.length (_vec : Vec α n) : Nat := n

@[reducible,simp] def Vec.set' (vec : Vec α n) (i : Nat) {h : i < n} (newItem : α) : Vec α n :=
  match vec, i with
  | .cons head tail, 0 => .cons newItem tail
  | .cons head tail, n+1 => by
    refine .cons head (tail.set' (h:= ?_) n newItem)
    exact Nat.succ_lt_succ_iff.mp h

@[reducible,simp] def Vec.set (vec : Vec α n) (index : Fin n) (newItem : α) : Vec α n :=
  vec.set' index (h:=index.prop) newItem


@[reducible,simp] def Vec.setIndexPrf (vec : Vec α n) (index : Nat) (h : index < n) (newItem : α) : Vec α n :=
  vec.set ⟨index,h⟩ newItem

theorem Vec.sets_eq {vec : Vec α n} : vec.set ⟨index,h⟩ = vec.setIndexPrf index h := by simp


@[reducible,simp] def Vec.get (vec : Vec α n) (index : Fin n) : α :=
  match vec, index with
  | .cons head tail, ⟨ 0, _ ⟩ => head
  | .cons head tail, ⟨ n+1, _ ⟩ => by
    refine tail.get ⟨ n, ?_ ⟩
    expose_names
    exact Nat.succ_lt_succ_iff.mp isLt


@[reducible,simp] def Vec.getIndexPrf (vec : Vec α n) (index : Nat) (h : index < n) : α :=
  vec.get ⟨index,h⟩

theorem Vec.gets_eq {vec : Vec α n} : vec.get ⟨index,h⟩ = vec.getIndexPrf index h := by simp


@[simp,reducible] instance : GetElem (Vec α n) Nat α (valid := fun _ i => i < n) where
  getElem as i h := as.get ⟨i,h⟩

@[simp,reducible] instance : GetElem (Vec α n) (Fin n) α (valid := fun _ _ => True) where
  getElem as i _ := as.get i




theorem Vec.get_at_zero {tail : Vec α len} {h : 0 < len+1} : (head :: tail)[0] = head := by simp only [instGetElemVecNatLt]





theorem Vec.get_at_zero_prf {tail : Vec α len} {index : Fin (len+1)} {h : index.val = 0} : (head :: tail)[index] = head := by
  simp
  let ⟨inner,prf⟩ := index
  have : inner = 0 := h
  simp_rw [this]

theorem Vec.get_elem {vec : Vec α len} {h : index < len} : vec[index] = vec.get ⟨index,h⟩ := by simp
theorem Vec.get_elem_to_prf {vec : Vec α len} {h : index < len} : vec[index] = vec[Fin.mk index h] := by simp





theorem Vec.get_prf_succ {tail : Vec α n} {i : Nat} {hlt : i < n} : (head :: tail : Vec α (n+1))[i + 1]'(by simp; exact hlt) = tail[i] := by
  simp

theorem Vec.get_succ {tail : Vec α n} {i : Fin n} : (head :: tail : Vec α (n+1))[Fin.mk (i.val + 1) (by simp : i.val + 1 < n+1)] = tail[i] := by
  simp


theorem Vec.cons_uncons {vec : Vec α len} {n : Nat} {h : n < len} : (head :: vec)[n+1] = vec[n] := by simp [instGetElemVecNatLt,Vec.get]



theorem Vec.get_nat_fin_eq {α len index h} {vec : Vec α len} : vec.get ⟨index, h⟩ = vec[index]'h := by
  cases vec <;> simp [instGetElemVecNatLt]


theorem Vec.set_at_zero {tail : Vec α len} {h : 0 < len+1} : (head :: tail).set ⟨0, h⟩ newThing = newThing :: tail := by simp

theorem Vec.set_at_succ {tail : Vec α len} {i : Nat} {h : i < len+1} {hsucc : i = i' + 1} : (head :: tail).set ⟨i, h⟩ newThing = (head :: tail.set ⟨i', by omega⟩ newThing : Vec _ _) := by
  simp only [Vec.set]
  subst_eqs
  simp

theorem Vec.set'_at_succ {tail : Vec α len} {i : Nat} {h : i < len+1} {hsucc : i = i' + 1} : (head :: tail).set' (h:=h) i newThing = (head :: tail.set' i' (h:=by omega) newThing : Vec _ _) := by
  subst_eqs
  simp


theorem Vec.set_has_at {ctx : Vec α len} : (ctx.set index newThing)[index] = newThing := by
  simp only [Vec.set]
  exact Vec.set'.induct ctx index.val (h:=index.prop)
    (motive := fun {len} ctx i {h} => (ctx.set' i (h:=h) newThing)[i] = newThing)
    (case1 := fun a head tail isLt => by simp)
    (case2 := fun a b c d e f => f)


theorem Vec.set_other_unchanged {ctx : Vec α len} (j : Nat) (hj : j < len) (i : Nat) (hi : i < len) (hneq : i ≠ j) : (ctx.set' (h:=hj) j a)[i] = ctx[i] := by
  revert i
  have :=
    Vec.set'.induct
      (motive := fun {len} vec i => ∀ (j : Nat) (hj : j < len) (jneq : i ≠ j), (vec.set' j a)[i] = vec[i])
      (case1 :=
        by
        intro len head tail isLt j jlt jneq
        rw [Vec.get_at_zero]
        cases j with
        | zero => contradiction
        | succ j' =>
          have : ((head :: tail).set' (h:=?_) (j' + 1) a) = (head :: (tail.set' (h:=?_) j' a)) := Vec.set'_at_succ (i:=j'+1) (hsucc:=rfl)
          rw [this]
          rw [Vec.get_at_zero]
          exact Nat.succ_lt_succ_iff.mp jlt
          exact jlt)
      (case2 :=
        by
        intro len head tail n' hn ih
        have pl1 : n'.succ = n'+1 := by exact rfl
        simp only [pl1]
        intro j jlt jneq
        cases j with
        | zero => simp
        | succ j' =>
          have : ((head :: tail).set' (h:= jlt) (j' + 1) a) = (head :: (tail.set' (h:=Nat.succ_lt_succ_iff.mp jlt) j' a)) := Vec.set'_at_succ (i:=j'+1) (hsucc:=rfl)
          rw [this]
          have := Vec.get_prf_succ (i:=n') (n:=len) (hlt:= Nat.succ_lt_succ_iff.mp hn) (head:=head) (tail:=tail)
          rw [this]
          have := Vec.get_prf_succ (i:=n') (n:=len) (hlt:= Nat.succ_lt_succ_iff.mp hn) (head:=head) (tail:=tail.set' (h:=Nat.succ_lt_succ_iff.mp jlt) j' a)
          rw [this]
          have jlen : j' < len := by exact Nat.succ_lt_succ_iff.mp jlt
          have nneqj : n' ≠ j' := by exact fun a => jneq (congrFun (congrArg HAdd.hAdd a) 1)
          have := ih j' (Nat.succ_lt_succ_iff.mp jlt) nneqj
          -- simp at this ⊢
          -- rw [←this]
          refine this)

  refine this

[Aaron Liu]

On one side the proof is a metavariable that defeq can't figure out how to assign and I'm guessing this is blocking it from applying proof irrelevance

[Aaron Liu]

in particular if you go to that metavariable and sorry it the refine this goes through but you get more "failed to infer" problems elsewhere

[aron]

how do i "go" to that metavariable?

[aron]

but why can't it figure out how to assign it? i'm literally providing it with Nat.succ_lt_succ_iff.mp jlt

[Aaron Liu]

  have :=
    Vec.set'.induct
      (motive := fun {len} vec i => ∀ (j : Nat) (hj : j < len) (jneq : i ≠ j), (vec.set' j a (h := sorry))[i] = vec[i])

is what I did and it got me a bunch of new errors

[Aaron Liu]

By the way, why are you taking the proof implicitly?

[aron]

idk, why not? ease of use

[aron]

right so it looks like all I needed to do was

    Vec.set'.induct (n:=len) (vec:=ctx)
      (motive := fun {len} vec i => ∀ (j : Nat) (hj : j < len) (jneq : i ≠ j), (vec.set' (h:=hj) j a)[i] = vec[i])

Then all that was left was massaging the params a bit and it worked

theorem Vec.set_other_unchanged {ctx : Vec α len} (j : Nat) (hj : j < len) (i : Nat) (hi : i < len) (hneq : i ≠ j) : (ctx.set' (h:=hj) j a)[i] = ctx[i] := by
  revert i
  have this :=
    Vec.set'.induct (n:=len) (vec:=ctx)
      (motive := fun {len} vec i => ∀ (j : Nat) (hj : j < len) (jneq : i ≠ j), (vec.set' (h:=hj) j a)[i] = vec[i])
      (case1 :=
        by
        intro len head tail isLt j jlt jneq
        rw [Vec.get_at_zero]
        cases j with
        | zero => contradiction
        | succ j' =>
          have : ((head :: tail).set' (h:=?_) (j' + 1) a) = (head :: (tail.set' (h:=?_) j' a)) := Vec.set'_at_succ (i:=j'+1) (hsucc:=rfl)
          rw [this]
          rw [Vec.get_at_zero]
          exact Nat.succ_lt_succ_iff.mp jlt
          exact jlt)
      (case2 :=
        by
        intro len head tail n' hn ih
        have pl1 : n'.succ = n'+1 := by exact rfl
        simp only [pl1]
        intro j jlt jneq
        induction j with
        | zero => simp
        | succ j' iih =>
          have : ((head :: tail).set' (h:= jlt) (j' + 1) a) = (head :: (tail.set' (h:=Nat.succ_lt_succ_iff.mp jlt) j' a)) := Vec.set'_at_succ (i:=j'+1) (hsucc:=rfl)
          rw [this]
          have := Vec.get_prf_succ (i:=n') (n:=len) (hlt:= Nat.succ_lt_succ_iff.mp hn) (head:=head) (tail:=tail)
          rw [this]
          have := Vec.get_prf_succ (i:=n') (n:=len) (hlt:= Nat.succ_lt_succ_iff.mp hn) (head:=head) (tail:=tail.set' (h:=Nat.succ_lt_succ_iff.mp jlt) j' a)
          rw [this]
          have jlen : j' < len := by exact Nat.succ_lt_succ_iff.mp jlt
          have nneqj : n' ≠ j' := by exact fun a => jneq (congrFun (congrArg HAdd.hAdd a) 1)
          have this : (tail.set' j' a)[n'] = tail[n'] := ih j' (Nat.succ_lt_succ_iff.mp jlt) nneqj
          refine this)

  exact fun i hi hneq => this i j hj hneq

[Aaron Liu]

aron said:

idk, why not? ease of use

It only seems harder to use so far, since it can rarely actually be inferred so you always have to specify it