Zulip Chat Archive

Stream: mathlib4

Topic: apply function to hypothesis


Jeremy Salwen (Jan 10 2023 at 22:05):

I want to add a function call to both sides of a hypothesis. I tried apply_fun at but it seems to be picky about how you call it:

import Std.Data.List.Basic
import Mathlib.Tactic.applyFun

open Lean

lemma foo (a b: List α) (P: a = b): True := by
  apply_fun List.length at P
  -- Error: Can not use `apply_fun` with a dependently typed function.

This does work if I replace List.length with @List.length α.

II feel like the same thing could be accomplished with just a lemma, but I can't seem to find an appropriate lemma.

Sky Wilshaw (Jan 10 2023 at 22:06):

docs4#congr_arg might help.

Heather Macbeth (Jan 10 2023 at 22:30):

@Jeremy Salwen If you have time, could you check whether it worked in mathlib3? This might be an accidental loss of functionality between the mathlib3 and mathlib4 versions of apply_fun.

Heather Macbeth (Jan 10 2023 at 22:30):

(@Sky Wilshaw The tactic apply_fun is a wrapper for the lemma congr_arg).

Jeremy Salwen (Jan 10 2023 at 22:34):

@Heather Macbeth

lemma foo {α} (a b: list α) (P: a = b): a = a := by
  apply_fun list.length at P

Works in lean 3.

Heather Macbeth (Jan 10 2023 at 22:35):

Thanks for checking! Would you mind opening an issue:
https://github.com/leanprover-community/mathlib4/issues
with the full code snippets (including imports) which work in mathlib3 and don't work in mathlib4?

Heather Macbeth (Jan 10 2023 at 22:36):

And let's also ping @Scott Morrison, who it seems wrote the mathlib4 apply_fun (mathlib4#475).

Jeremy Salwen (Jan 10 2023 at 23:23):

@Heather Macbeth done! https://github.com/leanprover-community/mathlib4/issues/1471

Scott Morrison (Jan 11 2023 at 02:47):

Fixed in mathlib4#1476, although I feel like the extra work being done there perhaps should be done in core in Lean.Meta.mkCongrArg.


Last updated: Dec 20 2023 at 11:08 UTC