Hi !

I recently found out about encoding relations as inductives. I am currently experimenting with these. I tried to create a simple stack automaton with two operations : Const a, which puts the value a on top of the stack, and Plus, which takes two values from the top of the stack and puts back their sum.

I encoded a relation that says that an operation is legal on a given stack :

```
Require Import List.
Inductive Op := Constant : nat -> Op | Plus.
Inductive OpAllowed : Op -> list nat -> Prop :=
| plus_allowed : forall (a : list nat) (e1 e2 : nat), OpAllowed Plus (e1 :: e2 :: a)
| const_allowed : forall (a : list nat) (e : nat), OpAllowed (Constant e) a.
```

This states that plus is allowed on all stacks with >= 2 elements, and const is always allowed.

I am now wondering how to use this fact in an interpreter step :

```
Definition step (op : Op)(stack : list nat) : OpAllowed op stack -> list nat :=
match op with
| Plus => fun p => ???
| Constant k => fun p => ???
end.
```

I do not know how to use the fact that there is an OpAllowed in context to construct the stack after the operation. I am probably using these wrong, but I am not familiar enough with them to understand where.

Would you have any pointers ?

Best,

MRandl