Lean4 : Repr in parameterized inductive types

Stream: new members

[Shubham Kumar 🦀 (he/him)]

  inductive Op Nat where
  | Add : Nat → Nat → Op Nat
  | Sub : Nat → Nat → Op Nat
  deriving Repr

Repr seems to have issues with the inductive type, I'm not sure why?

This is the error message
Screenshot-from-2022-10-26-09-50-06.png file:///home/sk/Pictures/Screenshots/Screenshot%20from%202022-10-26%2009-50-06.png

[Reid Barton]

What is Nat in inductive Op Nat where supposed to mean?

[Reid Barton]

Is Nat a variable for the whole declaration?

[Reid Barton]

I'm unsure about both what you intended and how Lean interprets this definition and even if they are the same, this probably isn't the clearest way to write the definition.

[Shubham Kumar 🦀 (he/him)]

good question
Reid Barton said:

What is Nat in inductive Op Nat where supposed to mean?

I'm not sure if I was doing it the right way but I wanted Op to be parameterized with a Natural Number.
And Add and Sub are 2 operations on Natural numbers that I am trying to define inductively.

I'm pretty sure I didn't represent it correctly

[Johan Commelin]

You might want (n : Nat) in that case. But I still don't understand what your are trying to do exactly.

[Johan Commelin]

It seems like you want to do at the same time:

• state that Add is a binary operation? (I guess you want it to be an Op 2, maybe?
• given an actual definition of Add, because it eats (x : Nat) and (y : Nat).

[Johan Commelin]

But if that is what you want to do, then you shouldn't do them at the same time.

[Johan Commelin]

Can you #xy your question?

[Shubham Kumar 🦀 (he/him)]

Johan Commelin said:

Can you #xy your question?

sure I want to build a inductive type that essentially does addition, multiplication, division and subtraction.

I don't know how to represent that in lean4

[Shubham Kumar 🦀 (he/him)]

when I say "does" I mean generate constructors for doing those operations if that makes any sense

[Johan Commelin]

Are you trying to build your own copy of the natural numbers? Or are you trying to define what a (semi)ring is? Or are you trying to do some sort of model theory?

[Shubham Kumar 🦀 (he/him)]

I'm trying to write semantics of a stack machine that does the four operations, it can be only add and multiply just to make things work

[Shubham Kumar 🦀 (he/him)]

nothing too complex

[Shubham Kumar 🦀 (he/him)]

I am trying to learn how to encode operational semantics, very much a beginner

[Shubham Kumar 🦀 (he/him)]

in lean and expressing semantics in lean

[Reid Barton]

The simplest option is

inductive Op where
| Add : Op
| Sub : Op

[Johan Commelin]

Shubham Kumar 🦀 (he/him) said:

I'm trying to write semantics of a stack machine that does the four operations, it can be only add and multiply just to make things work

Ok, that's a much better #xy.

[Shubham Kumar 🦀 (he/him)]

Johan Commelin said:

Shubham Kumar 🦀 (he/him) said:

I'm trying to write semantics of a stack machine that does the four operations, it can be only add and multiply just to make things work

Ok, that's a much better #xy.

Sorry for making it too complex, thanks for bearing with me :-)