Zulip Chat Archive

Stream: lean4

Topic: symmetry tactic

Chris Lovett (Oct 13 2022 at 20:26):

Is there another symmetry tactic besides this one symmetry? I'm trying to use it for NNG Advanced Addition World Level 9, but it is failing and the trace.Meta.synthInstance trace is not super useful

set_option trace.Meta.synthInstance true
set_option pp.all true
theorem succ_ne_zero (a : Nat) : Nat.succ a ≠ 0 := by
  symmetry
  exact zero_ne_succ a

The error is:

failed to synthesize
  @Symmetric.{1, 0} Nat (@Ne.{1} Nat)

[Meta.synthInstance] ❌ @Symmetric.{1, 0} Nat (@Ne.{1} Nat) ▼
  [] no instances for @Symmetric.{1, 0} Nat (@Ne.{1} Nat) ▼
    [instances] #[]

Any ideas on how to debug this?

Adam Topaz (Oct 13 2022 at 20:32):

Does it work if you add the following?

instance  : symmetric (λ x y : α => x ≠ y) :=
λ _ _ h c => h c.symm

Adam Topaz (Oct 13 2022 at 20:33):

If so, then it seems like a missing instance.

Adam Topaz (Oct 13 2022 at 20:33):

I can't get the symmetry tactic to work at all on my machine for some reason...

Adam Topaz (Oct 13 2022 at 20:36):

wait, I'm just not using this ground_zero repo at all... that's my problem.

Mario Carneiro (Oct 13 2022 at 20:59):

the symmetry tactic is in mathlib4, it's called symm now

Chris Lovett (Oct 13 2022 at 21:10):

that's why I couldn't find it, thanks. But I don't see it listed in https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/Tactic.
I do see this in Mathlib/Mathport/Syntax.lean? /- E -/ syntax (name := symm) "symm" : tactic. I also checked https://github.com/leanprover/std4 ?

Chris Lovett (Oct 13 2022 at 21:16):

Perhaps I need to import Mathlib.Mathport.Syntax to connect all the .symm functions on to a tactic, but this gives me an error import failed, environment already contains 'Lean.Expr.withAppAux._at.Lean.Expr.getAppFnArgs._spec_1._cstage2' ? Oh, but I just realized I can do this instead for now as a workaround: apply Ne.symm

Newell Jensen (Oct 13 2022 at 21:17):

I will claim that tactic...looks like it is on the list of tactics that still need to be ported to mathlib4

Newell Jensen (Oct 13 2022 at 21:18):

nm, those are already in there...weird that the syntax line is still there

Chris Lovett (Oct 13 2022 at 21:19):

those are already in there
what are you looking at?

Newell Jensen (Oct 13 2022 at 21:21):

Sorry, I jumped in on this conversation and am basically mumbling to myself. Here is what I was referring to.
https://github.com/leanprover-community/mathlib4/issues/430

symm and trans have been PR'd but haven't been committed yet.

Chris Lovett (Oct 13 2022 at 21:23):

Ah, thanks.

Chris Lovett (Oct 13 2022 at 21:42):

I got it working with that mathlib symm tactic, thanks:

@[symm] def neqSymm{α : Type} (a b: α) : a ≠ b → b ≠ a := Ne.symm

theorem succ_ne_zero (a : MyNat) : succ a ≠ 0 := by
  symm
  exact (zero_ne_succ a)

Chris Lovett (Oct 13 2022 at 23:18):

Rats the symm tactic can't seem to rewrite hypotheses. Is there are way to work around that somehow? NNG advanced multiplication world level 4 uses symmetry at hb?

Mario Carneiro (Oct 13 2022 at 23:21):

the workaround is have hb : _ = _ := by symmetry; exact hb but it would be better to not bother and just fix the tactic

Mario Carneiro (Oct 13 2022 at 23:22):

or just have hb := hb.symm

Kevin Buzzard (Oct 14 2022 at 00:53):

symmetry in Lean 3 can't rewrite hypotheses either. I hacked NNG symmetry so it worked on hypotheses but the lean tactic was in core so at the time I couldn't touch it. There's a mathlib3 tactic symmetry' which works on hypotheses.

Mario Carneiro (Oct 14 2022 at 00:55):

The symmetry' tactic was skipped because it was in the category "tactics that are the same as lean tactics + apply bug fix"

Last updated: Dec 20 2023 at 11:08 UTC