Zulip Chat Archive

Stream: new members

Topic: forall vs input

Dax Fohl (Jul 24 2023 at 08:44):

I'm trying to prove

theorem test (n: Nat):
   (m : Fin n),
  Vector.get (Vector.replicate n 0) m = 0 := by
  rw [Vector.get_replicate] -- did not find instance of the pattern in the target expression

but it doesn't find the instance. However the following works fine, even though AFAICT it is the same thing.

theorem test1 (n: Nat) (m : Fin n):
  Vector.get (Vector.replicate n 0) m = 0 := by
  rw [Vector.get_replicate]

Why does it behave differently? How do I get the first one to compile?

Martin Dvořák (Jul 24 2023 at 08:45):

You must start the proof with intro m in the first one.

Last updated: Dec 20 2023 at 11:08 UTC