rewrite failure

Stream: lean4

[Kevin Buzzard]

Me and several other people on the discord are completely bewildered about why rw [ih] fails below. This is as minimal as I can get it. This all came from doing Exercise sheet 5 from @Sebastian Ullrich 's course. Help!

def filter (p : α → Prop) [DecidablePred p] (as : List α) : List α :=
  match as with
  | [] => []
  | b :: bs => if p b then b :: filter p bs else filter p bs

variable {p : α → Prop} [DecidablePred p] {as : List α} {bs : List α}

@[simp] theorem filter_cons_true (h : p a) : filter p (a :: as) = a :: filter p as :=
  by simp [filter, h]

inductive Mem (a : α) : List α → Prop where
  | head {as} : Mem a (a::as)
  | tail {as} : Mem a as → Mem a (a'::as)

infix:50 " ∈ " => Mem

@[simp] theorem MemConsIff (a c : α) (cs : List α) : a ∈ c :: cs ↔ a = c ∨ a ∈ cs := sorry

theorem mem_filter : a ∈ filter p as ↔ a ∈ as ∧ p a := by
  induction as with
  | nil => admit
  | cons c cs ih =>
    byCases h : p c
    focus
      rw [filter_cons_true h, MemConsIff]
      rw [ih]
/-
tactic 'rewrite' failed, equality or iff proof expected
  a ∈ filter p cs ↔ a ∈ cs ∧ p a
case cons.inl
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
as bs : List α
a c : α
cs : List α
ih : a ∈ filter p cs ↔ a ∈ cs ∧ p a
h : p c
⊢ a = c ∨ a ∈ filter p cs ↔ a ∈ c :: cs ∧ p a
-/

[Marc Huisinga]

simp only [ih] and rw [propext ih] work. funny.

[Gabriel Ebner]

Ah so rw just doesn't know what to do with ↔ yet.

[Marc Huisinga]

Gabriel Ebner said:

Ah so rw just doesn't know what to do with ↔ yet.

sometimes it does.

example (h1 : a ↔ b) (h2 : b ↔ c) : a ↔ c := by
  rw [h1]
  assumption

works

[Gabriel Ebner]

It's just the usual missing instantiateMVars:

diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean
index f057ee311d..d605f7634c 100644
--- a/src/Lean/Meta/Tactic/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Rewrite.lean
@@ -20,7 +20,7 @@ def rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
     (symm : Bool := false) (occs : Occurrences := Occurrences.all) (mode := TransparencyMode.reducible) : MetaM RewriteResult :=
   withMVarContext mvarId do
     checkNotAssigned mvarId `rewrite
-    let heqType ← inferType heq
+    let heqType ← instantiateMVars (← inferType heq)
     let (newMVars, binderInfos, heqType) ← forallMetaTelescopeReducing heqType
     let heq := mkAppN heq newMVars
     let cont (heq heqType : Expr) : MetaM RewriteResult := do

[Daniel Fabian]

on an only vaguely related note, I have really come to love the fact that even when the meta programs are buggy, it doesn't cause soundness bugs. Given how much compiler magic is going on, having to trust the meta programs would make feel quite uneasy by now ;-)

[Gabriel Ebner]

https://github.com/leanprover/lean4/pull/524