10
$\begingroup$

I am trying to prove the following example in Lean 4:

-- defining my own version of List.contains, because I could not figure out how 
-- to use the equality type class used in the existing one
def List.contains' (x: A): List A → Prop
  | [] => False
  | (y::ys) => x = y ∨ ys.contains' x

example
  {l: List Nat}
  {f: Nat → Nat}
  (h: ∀ (x: Nat), l.contains' x → (f (f x) = f x))
  : l.map (λx => f (f x)) = l.map (λx => f x)
  := by
    simp [h] -- fails

This example works without the l.contains' x precondition in h, but with the precondition it seems the context is missing.

My question is how I can teach Lean to do this rewrite automatically?

For context:

I am coming from Isabelle, where this example is simply:

theorem example: 
  assumes ‹∀x∈set l. f (f x) = f x›
  shows ‹map (λx. f (f x)) l = map (λx. f x) l›
  using assms by simp

What I tried so far:

Try 1

Since Isabelle uses congruence rules to guide the simplifier for nested terms, I tried to define a congruence rule in Lean as well:

@[congr]
def map_congr'
  {f g : A → B}
  {xs ys : List A}
  (h1: xs = ys)
  (h2: ∀(x: A), xs.contains' x → f x = g x)
  : xs.map f = ys.map g
  := sorry

However, this rule was not picked up by the simp, rw, or conv tactic.

Only manually applying worked:

example
  {l: List Nat}
  {f: Nat → Nat}
  (h: ∀ (x: Nat), l.contains' x → (f (f x) = f x))
  : l.map (λx => f (f x)) = l.map (λx => f x)
  := by
    apply map_congr' (xs := l)
    · exact show l = l from rfl
    · exact h

Try 2

Next, I tried to define a version of map that makes the fact that l.contains' x available in the function f:

def List.map' : (l: List A) → (f: (x: A) → l.contains' x → B) → List B
  | [], f => []
  | (x::xs), f =>
      have c1: (x::xs).contains' x := by simp [List.contains']
      f x c1 :: map' xs (fun y p =>
        have c2: (x::xs).contains' y := by simp [List.contains', p]
        f y c2)

I was expecting that this lets me use the rw or simp tactic, but again it failed:


example
  {l: List Nat}
  {f: Nat → Nat}
  (h: ∀ (x: Nat), l.contains' x → (f (f x) = f x))
  : l.map' (λx p => f (f x)) = l.map' (λx p => f x)
  := by
      rw [h] -- tactic 'rewrite' failed, did not find instance of the pattern in the target expression

It worked with the conv tactic, but my feeling is that there is an easier way to do this.


example
  {l: List Nat}
  {f: Nat → Nat}
  (h: ∀ (x: Nat), l.contains' x → (f (f x) = f x))
  : l.map' (λx p => f (f x)) = l.map' (λx p => f x)
  := by
      conv =>
        pattern (λx p => f (f x))
        intro x
        intro p
        rw [h x p]
$\endgroup$
0

1 Answer 1

4
$\begingroup$

You can see your congruence theorem is being applied using set_option trace.Debug.Meta.Tactic.simp true, but by default simp does not dynamically extend the context during traversal with local facts such as from xs.contains' x → _. You can tell it to do so via

by simp (config := { contextual := true }) [h]

or you can use the "heavy-weight" by simp_all that does both contextual simplification as well as simplification of assumptions via other assumptions.

$\endgroup$
2
  • $\begingroup$ Thanks, that worked. Is there a way to set this as a default? I would also like to use this congruence in a termination proof. Are there similar options on termination_by? (the termination proof is for a function on a tree, where the recursive call is inside a map over the children of a node). $\endgroup$ Feb 14, 2022 at 20:23
  • 1
    $\begingroup$ There is no option to change the default currently, though you could wrap that in a new tactic like in gist.github.com/Kha/91614b6149561750d77ba5ad0739c7ba. Well-founded termination does not have a concept of something like these congr rules yet, the usual workaround is to make it an explicit mutual recursion github.com/Kha/lean4/blob/…. $\endgroup$ Feb 15, 2022 at 15:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.