Zulip Chat Archive

Stream: mathlib4

Topic: noob issue/bug when using congrArg

Andre Popovitch (Jan 11 2024 at 05:22):

So this simple example does what I would expect:

example (h3: -a * d = 0) : False := by
    simp at h3
    sorry

But when I use congrArg, I get a weird type error

example (h3: -a * d = 0) : False := by
    apply (congrArg (fun x => x / 1)) at h3
    simp at h3 -- ← error here
    sorry

The error is:

application type mismatch
  Eq.mp (congrFun (congrArg Eq (congrFun (congrArg HDiv.hDiv (neg_mul a d)) 1)) (0 / 1))
argument
  congrFun (congrArg Eq (congrFun (congrArg HDiv.hDiv (neg_mul a d)) 1)) (0 / 1)
has type
  (-a * d / 1 = 0 / 1) = (-(a * d) / 1 = 0 / 1) : Prop
but is expected to have type
  ?α = ?β : Prop

Kyle Miller (Jan 11 2024 at 05:25):

Zulip hints: #backticks and #mwe

This seems to be a mwe:

import Mathlib.Data.Real.Basic

variable (a d : ℝ)

example (h3: -a * d = 0) : False := by
    apply (congrArg (fun x => x / 1)) at h3
    simp at h3 -- ← error here
    sorry

Kyle Miller (Jan 11 2024 at 05:25):

There seems to be a bug in apply ... at ... itself, where it's forgetting to synthesize synthetic metavariables. Here's a workaround:

example (h3: -a * d = 0) : False := by
    apply (congrArg (fun x => x / 1)) at h3
    have := 1
    simp at h3 -- ← no more error
    sorry

Notification Bot (Jan 11 2024 at 05:26):

This topic was moved here from #lean4 > noob issue/bug when using congrArg by Kyle Miller.

Kyle Miller (Jan 11 2024 at 05:28):

@Adam Topaz apply ... at ... appears to be missing docs#Lean.Elab.Term.synthesizeSyntheticMVars or something equivalent. Maybe wrap it in withSynthesize?

Kyle Miller (Jan 11 2024 at 05:29):

@Andre Popovitch Here's another way to write this:

example (h3: -a * d = 0) : False := by
  have h3 := congr(1 / $h3)
  simp at h3
  sorry

Kyle Miller (Jan 11 2024 at 05:30):

Here's another:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic.ApplyFun

variable (a d : ℝ)

example (h3: -a * d = 0) : False := by
  apply_fun (1 / ·) at h3
  simp at h3
  sorry