What does it mean when you have multiple lines defining the action of an inductive constructor?

Question

I was looking at:

Inductive aevalR : aexp -> nat -> Prop :=
  | E_ANum  : forall (n: nat),
      aevalR (ANum n) n
  | E_APlus : forall (e1 e2: aexp) (n1 n2: nat),
      aevalR e1 n1 ->
      aevalR e2 n2 ->
      aevalR (APlus e1 e2) (n1 + n2)
  | E_AMinus: forall (e1 e2: aexp) (n1 n2: nat),
      aevalR e1 n1 ->
      aevalR e2 n2 ->
      aevalR (AMinus e1 e2) (n1 - n2)
  | E_AMult : forall (e1 e2: aexp) (n1 n2: nat),
      aevalR e1 n1 ->
      aevalR e2 n2 ->
      aevalR (AMult e1 e2) (n1 * n2).

and trying to understand what it meant. I understand that it takes an arithmetic exp. maps that to a function that maps to a nat that maps to a prop. But what confuses me is what is inside the | A_AOp clauses. They have no period at the end and the plus and minus ones have an arrow pointing to another arrow.

What type of syntax is this and what is it suppose to be saying? What is the input to this inductive type? Like usually I see in python:

def f(a,b,*args):

so I know what I am suppose to give as input (more or less). But This one is confusing me. How do I use this and what does the definition mean?

idk if its suppose to be an easy functional programming question or not since I'm just learning Coq and functional programming and this part wasn't in the functional programming intro of the course I was looking at:

https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html

Arthur Azevedo De Amorim Arthur Azevedo De Amorim · Accepted Answer · 2018-12-13T13:20:58

This snippet defines a predicate aevalR inductively. The predicate is a relation between expressions e : aexp and numbers n : nat: aevalR e n holds when e evaluates to n. Each clause introduced by a vertical bar describes one of the possibilities for evaluating an expression. For instance, E_APlus says that when e1 evaluates to n1 and e2 evaluates to n2, we know that APlus e1 e2 evaluates to n1 + n2.

Inductive propositions are one of the most used tools in Coq. There is a chapter in the Software Foundations book that introduces the concept. I advise you to familiarize yourself with that concept there before trying to attack the Imp chapter -- it should make the reading much easier.

What does it mean when you have multiple lines defining the action of an inductive constructor?

1 Answers