Unfold instance definition in a proof

Stream: lean4

[Pavel Klimov]

Is it possible to unfold definition of instance in a proof?

inductive Node
| leaf
| node (children : List Node)

mutual

def Node.beq : Node → Node → Bool
| .leaf, .leaf => true
| .node children1, .node children2 => Node.listBeq children1 children2
| _, _ => false

def Node.listBeq : List Node → List Node → Bool
| .nil, .nil => true
| x1 :: xs1, x2 :: xs2 => Node.beq x1 x2 && Node.listBeq xs1 xs2
| _, _ => false

end

instance nodeBEqInst : BEq Node where
  beq := Node.beq

in proofs, rw [BEq.beq] will translate == into nodeBEqInst.1 and then, is there way to convert it into Node.beq and use its definition?

[Kenny Lau]

@Pavel Klimov keep unfolding:

example (a b : Node) : a == b := by
  rw [BEq.beq, nodeBEqInst]
  dsimp only

[Jovan Gerbscheid]

In this case, simp only [BEq.beq] does the job, because simp only also expands projections.

[Jovan Gerbscheid]

You can also spell it like this: simp only [(· == ·)]

[Pavel Klimov]

@Kenny Lau Thanks! I tried only rw [nodeBEqInst.1] which didn't work. I didn't know about dsimp existence.
@Jovan Gerbscheid nice one!

Sad, though, it doesn't work if BEq instance is given by deriving statement :frown:

[Kenny Lau]

@Pavel Klimov that's because nodeBEqInst.1 is actually two things: the nodeBEqInst, and the .1.

[Jovan Gerbscheid]

Yes, if you want to prove anything about the instance, you shouldn't use deriving. I would have suggested trying deriving DecidableEq, but that doesn't seem to work here.

[Markus Himmel]

Jovan Gerbscheid said:

Yes, if you want to prove anything about the instance, you shouldn't use deriving

This is (slowly) changing! In the latest nightly, there is now a reduceBEq simproc which will unfold derived BEq instances. Sadly, for now this only works for non-nested inductives, so it's not useful for Pavel Klimov's example yet.

[Pavel Klimov]

@Kenny Lau what is .1 then? First element of what? Can I specify in rw or simp exactly .1 part of nodeBEqInst?

[Kenny Lau]

@Pavel Klimov it's some built-in notation that means "the first part of the structure"

[Kenny Lau]

I'm getting a bit meta here, but the corresponding Lean.Expr is docs#Lean.Expr.proj (ignore the meta stuff if it confuses you); the point here is that it's a separate atomic notation and not based on anything else

[Robin Arnez]

Well, nodeBEqInst is of type BEq Node and BEq is a structure with the first field BEq.beq; usually you'd have nodeBEqInst.beq a b (which gets the a == b) notation but you unfolded that so you get what's called a primitive projection which is a detail of how projections are supported in Lean.

[Kenny Lau]

for example, a ↔ b is another structure with the first field being a → b and the second field being b → a, so if you have h : a ↔ b, then you have access to h.1 : a → b and h.2 : b → a.
(https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Iff)

[Robin Arnez]

If you write .1 or .2 etc. yourself, you're usually not going to get a primitive projection but a projection function; these projection functions are implemented using primitive projections though. Primitive projections exist for inductives with exactly one constructor (e.g. structures) and are basically equivalent to a match that extracts the nth element:

inductive ABC where
  | xyz (x : Nat) (y : Bool)

example (x : ABC) :
    x.1 =
      match x with
      | .xyz a _ => a := rfl

example (x : ABC) :
    x.2 =
      match x with
      | .xyz _ b => b := rfl

[Kenny Lau]

so somehow nobody here provided the correct answer, which I only discovered recently thanks to @Aaron Liu :

@Pavel Klimov the way to do it is by unfold_projs

import Mathlib.Data.Set.Defs
import Mathlib.Tactic.DefEqTransformations

example (X : Set Nat) : X ⊆ X := by
  unfold_projs
  guard_target =ₛ Set.Subset X X
  exact fun x hx ↦ hx

(which I now realise is in mathlib not core)

[Aaron Liu]

I didn't realize it was the "correct" answer

[Ruben Van de Velde]

It's not a great idea to use that in code you want to maintain, I wouldn't say

[Ruben Van de Velde]

The correct answer is rw [Set.subset_def]