Local variables of function behavior differs vs arguments

Stream: lean4

[Pavel Klimov]

Here is some types

inductive Ty
| int
| str
deriving DecidableEq

def Ty.toType : Ty → Type
| .int => Int
| .str => String

structure TypedVal where
type : Ty
value : type.toType

(edit: changed "implicit" -> "explicit")
Following code doesn't work, it require explicit cast in many places with proofs

def TypedValue.eq (val1' val2' : TypedVal) : Bool :=
  if h : val1'.type = val2'.type then
    let type := val1'.type
    let val1 : type.toType := val1'.value
    let val2 : type.toType := cast (by rw [← h]) val2'.value
    match type with
    | .int => BEq.beq (α := Int) val1 val2
    | .str => BEq.beq (α := String) val1 val2
  else
    false

While following code works without proofs

def TypedValue.eqHelper (type : Ty) (val1 val2 : type.toType) : Bool :=
  match type with
  | .int => BEq.beq (α := Int) val1 val2
  | .str => BEq.beq (α := String) val1 val2

So, my current solution is using second function inside previous, like this:

def TypedValue.eq1 (val1 val2 : TypedVal) : Bool :=
  if h : val1.type = val2.type then
    TypedValue.eqHelper val1.type val1.value (cast (by rw [h]) val2.value)
  else
    false

But, I would like to inline it inside function, because I'm not planning to use this helper for anything else.

So, I wonder why inlining doesn't work while all types still the same? :thinking:

[Henrik Böving]

I don't see what you are getting at, both of your functions require the exact same amount of casts (namely 1)?

[Pavel Klimov]

@Henrik Böving have you tried to check my code? The first version is not working, and I have to add 4 explicit casts to make it work (some of them require proofs). (edit: changed "implicit" -> "explicit")

[Pavel Klimov]

Here is working version:

def TypedValue.eq (val1' val2' : TypedVal) : Bool :=
if h : val1'.type = val2'.type then
  let type := val1'.type
  let val1 : type.toType := val1'.value
  let val2 : type.toType := cast (by rw [← h]) val2'.value
  match h1 : type with
  | .int => BEq.beq (α := Int) (cast (by rw [h1]; rfl) val1) (cast (by rw [h1]; rfl) val2)
  | .str => BEq.beq (α := String) (cast (by rw [h1]; rfl) val1) (cast (by rw [h1]; rfl) val2)
else
  false

[Henrik Böving]

If I was doing it in a single function I'd probably do:

def TypedValue.eq (val1 val2 : TypedVal) : Bool :=
  if _h : val1.type = val2.type then
    match val1, val2 with
    | ⟨.int, val1⟩, ⟨.int, val2⟩ => BEq.beq (α := Int) val1 val2
    | ⟨.str, val1⟩, ⟨.str, val2⟩ => BEq.beq (α := String) val1 val2
  else
    false

[Henrik Böving]

Or I guess even

def TypedValue.eq (val1 val2 : TypedVal) : Bool :=
    match val1, val2 with
    | ⟨.int, val1⟩, ⟨.int, val2⟩ => BEq.beq (α := Int) val1 val2
    | ⟨.str, val1⟩, ⟨.str, val2⟩ => BEq.beq (α := String) val1 val2
    | _, _ => false

[Alfredo Moreira-Rosa]

Or even :grinning_face_with_smiling_eyes: :

def TypedValue.eq: TypedVal → TypedVal → Bool
    | ⟨.int, val1⟩, ⟨.int, val2⟩ => BEq.beq (α := Int) val1 val2
    | ⟨.str, val1⟩, ⟨.str, val2⟩ => BEq.beq (α := String) val1 val2
    | _, _ => false

[Pavel Klimov]

It's flaw of my example. Tag of type can be not so simple (without arguments), and comparing each argument of tag is cumbersome. So I want to avoid matching of both arguments because I would have to match arguments of constructors as well. (Constructors of inductive value)

[Pavel Klimov]

Also, it does not answer why arguments work differently in comparison with arguments of function.

[Alfredo Moreira-Rosa]

if you don't want to match constructor arguments, just use _ ?

[Pavel Klimov]

I have to match them, because it's tag of type. toType depends on them.

[Alfredo Moreira-Rosa]

you can extract before the match :

def TypedValue.eq (val1' val2' : TypedVal) : Bool :=
    let ⟨type1, val1⟩ := val1'
    let ⟨type2, val2⟩ := val2'
    match type1,type2 with
      | .int,.int => BEq.beq (α := Int) val1 val2
      | .str,.str => BEq.beq (α := String) val1 val2
      | _, _ => false

[Alfredo Moreira-Rosa]

And as for why it works for the separate functions ? it's because you have done the cast once when calling the function to say that the values are of the same type.

[Pavel Klimov]

@ecyrbe Here is closer to my actual case types:

inductive Ty
| fin (n : Nat)
| pos2d (n : Nat) (m : Nat)
deriving DecidableEq

def Ty.toType : Ty → Type
| .fin n => Fin n
| .pos2d n m => Prod (BitVec n) (BitVec m)

structure TypedVal where
type : Ty
value : type.toType

I hope you'll figure out why I dislike paired matching approach.

[Pavel Klimov]

ecyrbe писал/а:

And as for why it works for the separate functions ? it's because you have done the cast once when calling the function to say that the values are of the same type.

Haven't I set local variables with the same types in my first example?

[Alfredo Moreira-Rosa]

so here an alternative to make lean understand they are of the same type and is way shorter :

def TypedVal.eq (a b : TypedVal) : Bool :=
  if h : a.type = b.type then
    have same_type : b.type.toType = a.type.toType := by rw [h]
    let bVal : a.type.toType := cast same_type b.value
    a.value == bVal
  else
    false

[Alfredo Moreira-Rosa]

or even :

def TypedVal.eq (a b : TypedVal) : Bool :=
  if h : a.type = b.type then
    a.value == cast (by rw [h]) b.value
  else
    false

[Pavel Klimov]

it complains about line:

a.value == bVal

It says

failed to synthesize
BEq a.type.toType

And following:

def TypedVal.eq (a b : TypedVal) : Bool :=
  if h : a.type = b.type then
    have same_type : b.type.toType = a.type.toType := by rw [h]
    let bVal : a.type.toType := cast same_type b.value
    match a.type with
    | .fin n => BEq.beq (α := Fin n) a.value bVal
    | .pos2d n m => BEq.beq (α := Prod (BitVec n) (BitVec m)) a.value bVal
  else
    false

complains about both cases.

[Alfredo Moreira-Rosa]

add this :

private instance (t : Ty) : DecidableEq t.toType :=
by
  cases t <;> dsimp [Ty.toType] <;> infer_instance

[Aaron Liu]

don't use tactics to construct data

[Aaron Liu]

DecidableEq is data

[Alfredo Moreira-Rosa]

i use it all the time, why is this rule ?

[Aaron Liu]

you can sometimes get stuff that doesn't reduce well

[Aaron Liu]

or stuff that's really hard to prove it's equal to what you want it to be

[Aaron Liu]

or stuff that's just ugly when you unfold it

[Alfredo Moreira-Rosa]

i guess it's ok for my code then ? not mathlib ?

[Aaron Liu]

or stuff that has poor performance when compiled

[Aaron Liu]

ecyrbe said:

i guess it's ok for my code then ? not mathlib ?

well it's bad practice but if you really want to then

[Pavel Klimov]

It's amazing :+1:
I didn't know that you can do that.
But it doesn't answer my initial question :(

[Alfredo Moreira-Rosa]

just in case, you want to put it on mathlib, without tactics:

private instance (t : Ty) : DecidableEq t.toType :=
  match t with
  | .fin n => (inferInstance : DecidableEq (Fin n))
  | .pos2d n m => (inferInstance : DecidableEq (Prod (BitVec n) (BitVec m)))

[Alfredo Moreira-Rosa]

But personnally i prefer tactics automation, so i could change my types and it still would work :)