Call by name untyped lambda calculus interpreter in Coq

I made a very simple interpreter of the untyped lambda calculus in Coq.

I’m still very new with formal methods and I’m sure I’m doing a lot of things very wrong.

The spec is also very very weak currently. For example, a bug with the stack fully permitted by the spec caused an infinite loop.

Fuller repository here that contains a bit of Haskell to actually run the interpreter:

https://github.com/sstewartgallus/experimenting-with-coq

Import IfNotations.

Class EqDec {v : Set} := {
  eq_decide (x y : v) : {x = y} + {x <> y}
}.

Section term.
(* I define terms in a parameteric higher order abstract style.
   As we go along variables become a sort of address/pointer.
 *)
Variable v : Set.

Inductive term :=
| var (_ : v)
| pass (_ : term) (_ : term)
| lam (_ : v -> term)
.

Declare Custom Entry lam.
Notation "_{ e }" := e (e custom lam at level 99).
Notation "x" := x (in custom lam at level 0, x constr at level 0).
Notation "f x" := (pass f x) (in custom lam at level 1, left associativity).
Notation "'fun' x => y" :=
  (lam (fun x => y)) (in custom lam at level 90,
                     x ident,
                     y custom lam at level 99,
                     left associativity).
Notation "( x )" := x (in custom lam, x at level 99).
Notation "${ x }" := x (in custom lam, x constr at level 0).

Coercion var : v >-> term.

(* My intuition is that a stack is kind of like a one hole context/evaluation context.
   An alternate representation might be:

   Definition term' := term -> term.
   Definition hole : term' := fun x => x.
   Definition lpass (k : term') (e : term) : term' := fun x =>
     pass (k x) e.

   I'm not totally sure which is better.
 *)
Inductive term' :=
| hole
| lpass (_ : term') (_ : term).

Record ck := { control : term ; kont : term' }. 
Notation " 'E' ( h | e )" := {| control := e ; kont := h |} (e custom lam).

(* We use a very simple model of the heap as a function.
   Note that this very simple model leaks memory.
*)
Definition heap := v -> term.

Record state := { store : heap ; local : ck }.
(*
I used the turnstile before while figuring things out but really this is a store not an environment.
I need to think up better notation/denotation.

fun store => E(kont|control) ?
*)
Notation "s |- ck" := {| store := s ; local := ck |} (at level 70).

Definition put `{EqDec v} old x e : heap:=
fun x' => if eq_decide x x' then e else old x'.

Reserved Notation "s0 ~> s1 " (at level 80).

Variant step: state -> state -> Prop := 
| step_var s (x: v) k :
   s |- E(k| x) ~> s |- E(k| ${s x})

| step_pass s k e0 e1 :
   s |- E(k| e0 e1) ~> s |- E(lpass k e1| e0)

| step_lam `{EqDec v} s k f x e:
   s |- E(lpass k e| ${lam f}) ~> put s x e |- E(k|${f x})
where "st ~> st'" := (step st st').

(* FIXME I need to think of a less misleading name, the spec is very weak currently *)
(*
  If an interpreter takes a step (and succeeds!) then that implies that must have been a valid state transition.
*)
Definition valid (tick : state -> option state) := forall c s k,
exists c' s' k',
(tick (s |- E(k|c)) = Some (s |- E(k|c))) -> (s |- E(k|c)) ~> (s' |- E(k'|c')).

(* We use an old trick of lazily threading through new variables *)
CoInductive font : Set := { head : v ; left : font ; right : font }.

Fixpoint go `{EqDec v} (fnt : font) s k c :=
match c with
| var x => Some (s |- E(k |${s x}))

| _{ c0 c1 } => Some (s |- E(lpass k c1 | c0))
| lam f =>
   if k is lpass k' e0
   then
     let x := head fnt in
     go (right fnt) (put s x e0) k' (f x)
   else None
end.

Definition go_valid `{EqDec v} fnt : valid (fun st => go fnt (store st) (kont (local st)) (control (local st))).
intros c s k.
cbn.
(* Perform induction over all possible cases of control, then all cases of the stack *)
induction c.
+ cbn.
  eexists (s v0).
  eexists s.
  eexists k.
  intro.
  apply (step_var s v0 k).
+ cbn.
  eexists c1.
  eexists s.
  eexists (lpass k c2).
  intro.
  apply (step_pass s k c1 c2).
+ cbn.
  induction k.
  * (* I'm not precisely sure why we have to introduce an arbitrary term here but identity works well enough. *)
    eexists _{ fun x => x }.
    eexists s.
    eexists hole.
    discriminate.
  * eexists (t (head fnt)).
    eexists (put s (head fnt) t0).
    eexists k.
    intro.
    eapply (step_lam s k t (head fnt) t0).
Qed.

End term.

(* My language of choice is Haskell but a runtime of Ocaml or Scheme might be preferable. Not sure. *)
Require Extraction.

Extraction Language Haskell.
Extract Inductive bool => "Prelude.Bool" ("Prelude.True" "Prelude.False").
Extract Inductive sumbool => "Prelude.Bool" ("Prelude.True" "Prelude.False").
Extract Inductive sumor => "Prelude.Maybe" ("Prelude.Just" "Prelude.Nothing").
Extract Inductive option => "Prelude.Maybe" ("Prelude.Just" "Prelude.Nothing").
Extract Inductive prod => "(,)" ("(,)").
Extract Inductive unit => "()" ("()").
Extract Inductive list => "()" ("()" "(:)").
Extraction "./Step.hs" go.
```