Reusing values from inductive relation

Using Coq
1

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

2

something like this

Definition step (op : Op)(stack : list nat) : OpAllowed op stack -> list nat :=
  match op with
  | Plus =>
      match stack with
      | nil | _ :: nil => ltac:(intro H;exfalso;inversion H)
      | a :: b :: rest => fun _ => (a + b) :: rest
      end
  | Constant k => fun _ => k :: stack
  end.

or perhaps


Definition step (op : Op)(stack : list nat) : OpAllowed op stack -> list nat.
Proof.
  refine (match op with
  | Plus =>
      match stack with
      | nil | _ :: nil => _
      | a :: b :: rest => fun _ => (a + b) :: rest
      end
  | Constant k => fun _ => k :: stack
  end).
  all: intro H;exfalso;abstract inversion H.
Defined.

so that the ugly term produced by inversion is hidden behind the lemma produced by abstract (compare the output of Print step in each case) (using abstract in a ltac:() doesn’t produce a definition so doesn’t work for this purpose).

3

I didn’t know about this refine tactic, it seems useful. I will investigate this further.
Thanks a lot!