simp only puzzle

Stream: lean4

[Joachim Breitner]

namespace Puzzle1
opaque foo : Nat → Prop
theorem foo_eq (h : x = 5 → False) : foo x := sorry
theorem puzzle (h : ¬ x = 5) : foo x := by  simp only [foo_eq] -- does it rewrite or not?
end Puzzle1

namespace Puzzle2
opaque foo : Nat → Prop
theorem foo_eq (h : ¬ x = 5) : foo x := sorry
theorem puzzle (h : ¬ x = 5) : foo x := by  simp only [foo_eq] -- does it rewrite or not?
end Puzzle2

namespace Puzzle3
opaque foo : Nat → Prop
theorem foo_eq (h : ¬ x = 5) : foo x := sorry
theorem puzzle (h : x = 5 → False) : foo x := by  simp only [foo_eq] -- does it rewrite or not?
end Puzzle3

namespace Puzzle4
opaque foo : Nat → Prop
theorem foo_eq (h : x = 5 → False) : foo x := sorry
theorem puzzle (h : x = 5 → False) : foo x := by  simp only [foo_eq] -- does it rewrite or not?
end Puzzle4

[Johan Commelin]

Some Puzzle3s should be Puzzle4s... :wink:

[Joachim Breitner]

Ok, first cookie given, and puzzle fixed :-)

[Joachim Breitner]

NB: It says simp only [foo_eq], not simp only [foo_eq, h].