## Stream: new members

### Topic: failed to synthesize instance

#### Jeremy Tan (Mar 15 2023 at 06:50):

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 (Mar 15 2023 at 07:40):

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 (Mar 15 2023 at 07:44):

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

#### Mario Carneiro (Mar 15 2023 at 07:45):

resetI should not be necessary

#### Mario Carneiro (Mar 15 2023 at 07:45):

it happens automatically and transparently now

#mwe

#### Jeremy Tan (Mar 15 2023 at 08:06):

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 (Mar 15 2023 at 14:53):

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 (Mar 15 2023 at 15:00):

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

#### Kevin Buzzard (Mar 15 2023 at 15:01):

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

#### Andrew Wells (Mar 28 2023 at 23:28):

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 (Mar 28 2023 at 23:35):

Do you want Record to be

Attr -> Value -> Value


#### Newell Jensen (Mar 28 2023 at 23:36):

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

#### Newell Jensen (Mar 28 2023 at 23:38):

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 (Mar 28 2023 at 23:42):

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 (Mar 29 2023 at 00:04):

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

#### Newell Jensen (Mar 29 2023 at 00:06):

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

#### Andrew Wells (Mar 29 2023 at 00:08):

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

#### Newell Jensen (Mar 29 2023 at 00:14):

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 (Mar 29 2023 at 00:15):

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 (Mar 29 2023 at 05:54):

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 (Mar 29 2023 at 18:24):

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!

Last updated: Dec 20 2023 at 11:08 UTC