Evaluation to a value distributes over binops proven for small-step without relying on equivalence to big-step

step.v

Set Implicit Arguments.
From Stdlib Require Import ZArith.
Inductive simple_expr :=
| SLit : Z  -> simple_expr
| SDiv : simple_expr -> simple_expr -> simple_expr
| SCrash : simple_expr
.
Inductive simple_ctx :=
| Shole : simple_ctx
| SLDiv : simple_ctx -> simple_expr -> simple_ctx
| SRDiv : Z -> simple_ctx -> simple_ctx
.
Fixpoint simple_fill c e :=
  match c with
  | Shole => e
  | SLDiv K e' => SDiv (simple_fill K e) e'
  | SRDiv v K  => SDiv (SLit v) (simple_fill K e)
  end
.
Inductive prim_step : simple_expr -> simple_expr -> Prop :=
| PSdiv : forall n1 n2, n2 <> 0%Z -> prim_step (SDiv (SLit n1) (SLit n2)) (SLit (n1 / n2))
| PSfail : forall n1, prim_step (SDiv (SLit n1) (SLit 0%Z)) SCrash
.
Infix "~>" := (prim_step) (at level 80, right associativity).
Inductive ctx_step : simple_expr -> simple_expr -> Prop :=
| ctx_do_step : forall e1 e2 e1' e2' K,
    e1 = simple_fill K e1' ->
    e2 = simple_fill K e2' ->
    prim_step e1' e2' ->
    ctx_step e1 e2
| ctx_do_crash : forall e1 e1' K,
    e1 = simple_fill K e1' ->
    prim_step e1' SCrash ->
    ctx_step e1 SCrash
.
Infix "=>" := (ctx_step) (at level 80, right associativity).
Inductive rtc {A : Type} (R : A -> A -> Prop) : A -> A -> Prop :=
| rtc_refl  : forall a, rtc R a a
| rtc_trans : forall a b c, R a b -> rtc R b c -> rtc R a c
.
Infix "=>*" := (rtc ctx_step) (at level 80, right associativity).

Lemma val_inj n m :
  SLit n =>* SLit m ->
  n = m
.
Proof.
  remember (SLit n) as e; remember (SLit m) as e'; intros H;
  revert n m Heqe Heqe'; induction H; intros; subst; try now inversion Heqe'.
  inversion H; subst. induction K; inversion H1; cbn in *.
  rewrite <- H1 in H3; inversion H3. 
  destruct K; inversion H1; inversion H2; cbn in *; congruence.
Qed.
Lemma crash_nostep e :
  e <> SCrash ->
  SCrash =>* e ->
  False
.
Proof.
  remember (SCrash) as e0; intros H Ht;
  revert H Heqe0; induction Ht; intros; subst; try now inversion Heqe'.
  now apply H.
  inversion H; subst. destruct K; inversion H1; cbn in *; subst. 
  inversion H3. eauto.
Qed.
Lemma binop_inversion e1 e2 n :
  SDiv e1 e2 =>* SLit n ->
  exists n1 n2, (e1 =>* SLit n1) /\
           (e2 =>* SLit n2) /\
           (n = n1 / n2)%Z
.
Proof.
  (** We want an induction hypothesis that is as general as possible.
      For this, we essentially change the shape of `SDiv e1 e2 =>* SLit n`
      into `e =>* e'` for some `e` and `e'` s.t. `e = SDiv e1 e2` and `e' = SLit n` *)
  remember (SDiv e1 e2) as e; remember (SLit n) as e'; intros H;
  revert e1 e2 n Heqe Heqe'. 
  (** Observe the proof context, this is most general to induce on `=>*` *)
  induction H as [x|x y z Hxy Hyz IH]; intros; subst;
  (** Base case will have `SDiv e1 e2 = SLit n` as assumption, which we
      can resolve immediately by congruence *)
    try congruence.

  (** Now, we need to unpack the ordinary step relation in order to learn 
      something about y. Intuitively, there should be three cases:
       - SPLus (SLit _) (SLit _) => SLit _ = y
       - SDiv e1 e2 => SDiv e1' e2 = y
       - SDiv e1 e2 => SDiv e1 e2' = y
      But, due to crash, there can be more cases.
      *)
  inversion Hxy; subst; clear Hxy;
  (** We get these three cases by destructuring `K` and looking at our assumption
      of shape `SDiv e1 e2 = simple_fill K e1'`, which restricts `K` to be 
      just `_`, `_+e` or `n+_`. *)
  destruct K; cbn in *; inversion H;
  (** immediately resolve cases where one of the exprs is a crash *)
    try now apply crash_nostep in Hyz.
  - (** context is just the hole *)
    (** unpack the primitive step `e1' ~> e2'` *)
    rewrite <- H in H1; inversion H1; subst.
    (** the unpacking gave us two numbers `n1`, `n2` s.t. `SLit (n1+n2) =>* Slit n`,
        so simply instantiate the goal *)
    do 2 eexists; repeat split; eauto using rtc_refl.
    (** Now use that for values `v`, `v'`, if `v =>* v'`, then `v = v'` *)
    now apply val_inj in Hyz.
    (** crash does not step *)
    now eapply crash_nostep in Hyz.
  - (** context is of the form `_ + s` *)
    (** unpack the induction hypothesis... *)
    specialize (IH _ s n Logic.eq_refl Logic.eq_refl) as [n1 [n2 [IHa [IHb IHc]]]].
    (** and use the extracted values as witnesses in the goal *)
    exists n1, n2; repeat split; eauto. 
    (** what is left to argue is that the lefthandside of the plus op evals to `n1` *)
    (** This follows from transitivity of the star step relation *)
    rewrite <- H2; eapply rtc_trans; try eapply ctx_do_step with (K:=K) (e2':=e2'); eauto.
  - (** context is of the form `n0 + _` *)
    (** unpack the induction hypothesis... *)
    specialize (IH _ _ n Logic.eq_refl Logic.eq_refl) as [n1 [n2 [IHa [IHb IHc]]]].
    (** now, note that `n0 =>* n1` means that `n0 = n1`  *)
    apply val_inj in IHa as ->.
    (** and use the extracted values as witnesses in the goal *)
    exists n1, n2; repeat split; eauto using rtc_refl. 
    (** what is left to argue is that the righthandside of the plus op evals to `n2` *)
    (** This follows from transitivity of the star step relation *)
    rewrite <- H3; eapply rtc_trans; try eapply ctx_do_step with (K:=K) (e2':=e2'); eauto.
Qed.