Rewriting/simplifying through Fin

Stream: new members

[pandaman]

Hi! I'm trying to better architect intermediate data and proofs that appear in my proofs by grouping them in a struct and proving theorems about them (inspired by this ProofData technique). However, I got stuck when rewriting Fin due to a "motive is not type correct" error. Usually simp can resolve the issue, but it didn't work either. The following snippet is a minimized example of the issue. Can someone help unstuck the last sorry? Or any advice about structuring proof-related data is welcome. Thanks!

structure Node

structure NFA where
  nodes : Array Node
  start : Fin nodes.size

def append (nfa : NFA) : { nfa' : NFA // nfa.nodes.size < nfa'.nodes.size } :=
  let nfa' := {
    nodes := nfa.nodes ++ [Node.mk, Node.mk, Node.mk],
    start := ⟨nfa.nodes.size + 1, by simp⟩,
  }
  ⟨nfa', by simp [nfa']; omega⟩

structure ProofData (nfa : NFA) where
  nfa' : NFA
  nfa'_property : nfa.nodes.size < nfa'.nodes.size
  eq : nfa' = (append nfa).val

def intro (eq : append nfa = result) : ProofData nfa :=
  {
    nfa' := result.val,
    nfa'_property := result.property,
    eq := by simp [eq],
  }

def ProofData.start (self : ProofData nfa) : Fin self.nfa'.nodes.size := ⟨nfa.nodes.size + 1, by simp [self.eq, append]⟩

theorem ProofData.start_eq (self : ProofData nfa) : self.nfa'.start = self.start := by
  -- Q1. How can I make this simp progress?
  -- simp [self.eq]
  -- Q2. Or, how can I work around the "motive is not type correct" error?
  --   I guess the type error comes from different arguments to `Fin`.
  -- rw [self.eq]
  sorry

[Matt Diamond]

One suggestion I would make is to add set_option autoImplicit false at the top, as it's possible that you're relying on autoImplicit accidentally

[Matt Diamond]

actually, on second glance that might be irrelevant

[pandaman]

Yes, I omitted in this example, but I disable autoImplicit in my code.

[Matt Diamond]

I got this to work:

apply Fin.ext
change _ = nfa.nodes.size + 1
rw [self.eq]

[Matt Diamond]

I think the key is using Fin.ext to get out of the Fin context

[pandaman]

Thanks! rw [self.eq] still fails right after Fin.ext though. Why could change replace the self.start.val to nfa.nodes.size + 1 (which is less dependent on self I guess)?

[Matt Diamond]

honestly not sure... I was kind of surprised, as I was trying to rewrite it using docs#Fin.val_mk and it didn't seem to work, which is why I resorted to change

[Matt Diamond]

(btw, simp [append] closes the goal after those 3 lines)

[Matt Diamond]

also weird: if you replace rw [self.eq] with simp [self.eq], simp still makes no progress

[pandaman]

Yeah, simp often work better with Fin, but it's not the case here :(. I wonder if I can add some simp lemmas to make it go smoothly...

[pandaman]

I ended up not using Fin, carrying proofs around when necessary.