failed to synthesize instance

Stream: new members

[Jeremy Tan]

image.png how do I fix this error in Lean 4? It shouldn't be one since the required instance is in a hypothesis

[Kevin Buzzard]

What happens if you do resetI before the failing command? I don't know if that got ported yet but it would solve the problem in lean 3. Here I don't know whether the problem is the one solved by resetI (instance cache needs resetting) or lean4#2074

[Jeremy Tan]

resetI is not ported yet, and neither are the other I versions of tactics

[Mario Carneiro]

resetI should not be necessary

[Mario Carneiro]

it happens automatically and transparently now

[Mario Carneiro]

#mwe

[Jeremy Tan]

Mario Carneiro said:

#mwe

import Mathlib.Algebra.CharP.Basic
import Mathlib.Data.Nat.Prime

universe u

variable (R : Type u)

variable [Semiring R] [Nontrivial R] [NoZeroDivisors R]

class inductive ExpChar (R : Type u) [Semiring R] : ℕ → Prop
  | zero [CharZero R] : ExpChar R 1
  | Prime {q : ℕ} (hprime : q.Prime) [hchar : CharP R q] : ExpChar R q

theorem char_eq_expChar_iff (p q : ℕ) [hp : CharP R p] [hq : ExpChar R q] : p = q ↔ p.Prime :=
  sorry

theorem expChar_is_prime_or_one (q : ℕ) [hq : ExpChar R q] : Nat.Prime q ∨ q = 1 :=
  or_iff_not_imp_right.mpr fun h => by
    cases' CharP.exists R with p hp
    have p_eq_q : p = q := (char_eq_expChar_iff R p q).mpr -- here

[Adam Topaz]

if you use obtain instead of cases' then the error disappears (well, it changes to a type error, which is expected given char_eq_expChar_iff)

[Kevin Buzzard]

Somehow there are two threads about this, there's also a discussion in #mathlib4

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.232894

[Andrew Wells]

Hi, I'm trying my first programming project in Lean and I've run into the following difficulty:

import Init.Data.Repr

inductive Primitive where
  | Bool (b: Bool): Primitive
  | Int (i: Int): Primitive
  | String (s: String): Primitive
deriving Repr

abbrev Attr := String

inductive Value where
  | Primitive (p: Primitive) : Value
  | Record (r: Attr → Value): Value
deriving Repr -- fails with "failed to synthesize instance Repr (Attr -> Value)"

Where I'd like to use r: Attr → Value as a Map from Attrs to Values. The definition seem to work, but in order to print I'd like to derive Repr for Value. When I try I get the error:

failed to synthesize instance
    Repr (Attr -> Value)

I assume because Value is recursive. Is there a way I can derive Repr for Value (possibly by writing my own function to print Values)? Sorry for the noob question, I couldn't seem to find documentation for this.

[Newell Jensen]

Do you want Record to be

Attr -> Value -> Value

[Newell Jensen]

I could be wrong here but you could do Record : Attr -> Value if that is what you were intending.

[Newell Jensen]

import Init.Data.Repr

inductive Primitive where
  | Bool (b: Bool): Primitive
  | Int (i: Int): Primitive
  | String (s: String): Primitive
deriving Repr

abbrev Attr := String

inductive Value where
  | Primitive (p: Primitive) : Value
  | Record : Attr → Value
deriving Repr -- fails with "failed to synthesize instance Repr (Attr -> Value)"

Doesn't error out is what I am alluding to.

[Andrew Wells]

My intention is to be able to pass in structured data as <key, value> pairs where ultimately values will be primitives, but maybe not initially. So I could have:

def my_record (a : Attr) : Value := match a with
  | "foo" => Value.Primitive (Primitive.Bool false)

or

def inner_record (a : Attr) : Value := match a with
  | "foo" => Value.Primitive (Primitive.Bool false)
  | _ => Value.Wrong
def my_record (a : Attr) : Value := match a with
  | "foo" => inner_record
  | _ => Value.Wrong

to represent what would be

{"foo": false}

and

{"foo":{"foo":false}}

in python/json/whatever

[Newell Jensen]

The book Functional Programming for Lean 4 has section on JSON which might be helpful.

[Newell Jensen]

On mobile with one hand tied up throwing ball for my dogs so hard to look into it more at the moment.

[Andrew Wells]

Thanks for the help! I'll take a look.

[Newell Jensen]

import Init.Data.Repr

inductive Primitive where
  | Bool (b: Bool): Primitive
  | Int (i: Int): Primitive
  | String (s: String): Primitive
deriving Repr

abbrev Attr := String

inductive Value where
  | Primitive (p: Primitive) : Value
  | Record : Attr → Value → Value
deriving Repr -- fails with "failed to synthesize instance Repr (Attr -> Value)"

So the -> is right associative

[Newell Jensen]

At any rate, that doesn't error out (note to self: change the comments on someone's code block with your own comments)

[Reid Barton]

Andrew Wells said:

Is there a way I can derive Repr for Value (possibly by writing my own function to print Values)? Sorry for the noob question, I couldn't seem to find documentation for this.

You would need a way to print functions, since the argument r of the Record constructor is a function. And in general there's not an obvious way.

[Andrew Wells]

A co-worker gave the following solution, which I like:

import Init.Data.Repr
import Lean.Data.AssocList
open Lean

-- Derive Repr for AssocList
-- From https://leanprover-community.github.io/archive/stream/270676-lean4/topic/AssocList.20.22failed.20to.20synthesize.22.html
instance [Repr α] [Repr β] : Repr (AssocList α β) where
  reprPrec f _ := repr f.toList

inductive Primitive where
  | Bool (b: Bool): Primitive
  | Int (i: Int): Primitive
  | String (s: String): Primitive
deriving Repr

abbrev Attr := String

inductive Value where
  | Primitive (p: Primitive) : Value
  | Record (r: AssocList Attr Value): Value
deriving Repr

Thanks for the help!