Proof of inverse

Stream: lean4

[Scott Godwin]

I'm trying to prove that a function is an inverse of another one, but I'm getting stuck trying to do a rw or simplifying the goal. What I have is:

inductive Foo where
  | foo₁
  | foo₂

inductive Bar : List Foo → Foo → Type where
  | here {fs : List Foo} {f : Foo} : Bar (f :: fs) f
  | there {fs : List Foo} {f₁ f₂ : Foo} : Bar fs f₂ → Bar (f₁ :: fs) f₂

def from_fin : (fs : List Foo) → Fin fs.length → Σ f : Foo, Bar fs f
  | f :: _, ⟨0, _⟩ => ⟨f, Bar.here⟩
  | _ :: fs, ⟨Nat.succ n, lt⟩ =>
      let ⟨f, b⟩ := from_fin fs ⟨n, Nat.lt_of_succ_lt_succ lt⟩
      ⟨f, Bar.there b⟩

def to_fin {fs : List Foo} {f : Foo} : (Bar fs f) → Fin fs.length
  | .here => ⟨0, Nat.zero_lt_succ _⟩
  | .there b => (to_fin b).succ

theorem inverse {fs : List Foo} {f : Foo} (b : Bar fs f) : from_fin fs (to_fin b) = ⟨f, b⟩ := by
  cases b with
  | here => rfl
  | there b =>
      have h := inverse b

      simp [to_fin, Fin.succ, from_fin]

      -- This is what I want to do, but it causes `tactic 'rewrite' failed, motive is not type correct`
      -- rw [Nat.add_zero (to_fin b).val]
      -- rw [h]

      -- Tried a different approach
      congr
      . simp; rw [h]
      . simp; rw [h]
      . -- `simp` doesn't work here nor does a direct `rw` or `subst`
        rw [Nat.add_zero (to_fin b).val]
        sorry

The goal seems trivially true, but I don't know how I can do the rewrite (since it says it's not "type correct") to use the inductive hypothesis. Any suggestions?

[Mario Carneiro]

kind of a silly solution, but this works:

theorem inverse {fs : List Foo} {f : Foo} (b : Bar fs f) : from_fin fs (to_fin b) = ⟨f, b⟩ := by
  cases b with
  | here => rfl
  | @there fs f₁ _ b =>
    show (let ⟨f, b⟩ := from_fin fs ⟨to_fin b, _⟩; (⟨f, Bar.there b⟩ : Sigma _)) = _
    rw [inverse b]

[Scott Godwin]

Thanks! I'll admit I'm a bit confused why that works but the other approaches didn't. If I understand it correctly, show normalizes both the goal and the given term and unifies them. But that would require it to normalize (to_fin b).val + 0 to (to_fin b).val which, while obvious, isn't being normalized when using simp, rw, and subst

[Mario Carneiro]

show doesn't normalize anything, it changes the goal to a specified term and unifies it with the goal. The key advantage it has over dsimp and unfold and the like is that you are giving explicitly where you want to end up, rather than what procedure you want to apply. The issue with those other methods is that they don't produce a goal which has the LHS of inverse b syntactically within them

[Mario Carneiro]

note that it is important to use only definitional rewriting tactics here (like dsimp over simp), because your goal has a dependent function and so non-definitional rewrites are either not going to apply or will result in a type incorrect term

[Mario Carneiro]

the presence of the let ⟨f, b⟩ := ...; ⟨f, Bar.there b⟩ in the definition is messing up dsimp and making it try the wrong thing