Library ExprSemantics.eval_exp

Author: Jean-François Monin, Verimag, Université Grenoble Alpes

Require Import Utf8.

Toy language of expressions
Inductive te : Type :=
  | Te_const : nat → te
  | Te_plus : te → te → te
  | Te_div0 : te → te.

Inductive val : Type :=
  | Nval : nat → val
  | Bval : bool → val.

Evaluation
Inductive eval : te → val → Prop :=
  | E_Const n :
      eval (Te_const n) (Nval n)
  | E_Plus {t1 t2 n1 n2} :
      eval t1 (Nval n1) →
      eval t2 (Nval n2) →
      eval (Te_plus t1 t2) (Nval (n1 + n2)).

Inversion when the 1st arg only is constructed
Inductive is_E_Const n : ∀v, eval (Te_const n) v → Prop :=
  | is_E_Const_intro : is_E_Const n (Nval n) (E_Const n).
Inductive is_E_Plus t1 t2 : ∀v, eval (Te_plus t1 t2) v → Prop :=
  | is_E_Plus_intro n1 n2 :
      ∀ (e1 : eval t1 (Nval n1))
        (e2 : eval t2 (Nval n2)),
      is_E_Plus t1 t2 (Nval (n1 + n2)) (E_Plus e1 e2).
Inductive is_nothing_Div0 (t: te) : ∀v, eval (Te_div0 t) v → Prop :=.

Definition eval_inv {t v} (e : eval t v) :
    match t with
    | Te_const n ⇒ is_E_Const n
    | Te_plus t1 t2 ⇒ is_E_Plus t1 t2
    | Te_div0 t1 ⇒ is_nothing_Div0 t1
    end v e.
Proof. destruct e; constructor; assumption. Defined.

Inversion when arg 1 is constructed and arg 2 is partly constructed

Inductive is_E_Const2 c : ∀n, eval (Te_const c) (Nval n) → Prop :=
  | is_E_Const2_intro : is_E_Const2 c c (E_Const c).
Inductive is_E_Plus2 t1 t2 : ∀n, eval (Te_plus t1 t2) (Nval n) → Prop :=
  | is_E_Plus2_intro n1 n2 :
      ∀ (e1 : eval t1 (Nval n1))
        (e2 : eval t2 (Nval n2)),
        is_E_Plus2 t1 t2 (n1 + n2) (E_Plus e1 e2).
Inductive is_other2 t v : eval t v → Prop :=.

Definition eval_inv2 {t v} (e : eval t v) :
    match t,v with
    | Te_const c, Nval n ⇒ is_E_Const2 c n
    | Te_plus t1 t2, Nval n ⇒ is_E_Plus2 t1 t2 n
    | t, v ⇒ is_other2 t v
    end e.
Proof. destruct e; constructor; assumption. Defined.

Section varP.

Variable P : val → Prop.

Lemma test_ev1 :
  ∀ v , P v → eval (Te_plus (Te_const 1) (Te_const 0)) v → v = Nval 1.
Proof.
  intros v p e.
  destruct (eval_inv e) as [n1 n2 e1 e2].
  destruct (eval_inv2 e1).
  destruct (eval_inv2 e2).
  reflexivity.
Qed.

Lemma test_ev2:
  eval (Te_plus (Te_const 1) (Te_const 0)) (Bval true) → False.
Proof.
intro e. destruct (eval_inv2 e).
Qed.

Lemma test_ev3:
  ∀ n, n < 5 → eval (Te_plus (Te_const 1) (Te_const 0)) (Nval n) → n = 1.
Proof.
  intros n l e.
  destruct (eval_inv2 e) as [n1 n2 e1 e2].
  destruct (eval_inv2 e1).
  destruct (eval_inv2 e2).
  reflexivity.
Qed.

End varP.

Non-deterministic evaluation, in order to illustrate several cases matching an "input"

Section varQ.

Variable Q : te → Prop.

Inductive eval_nd: te → val → Prop :=
  | E_Const_nd : ∀ n,
      eval_nd (Te_const n) (Nval n)
  | E_Plus_nd1 : ∀ t1 t2 n1 n2,
      eval_nd t1 (Nval n1) →
      eval_nd t2 (Nval n2) →
      eval_nd (Te_plus t1 t2) (Nval (n1 + n2))
  | E_Plus_nd2 : ∀ t1 t2 n2,
      Q t1 →
      eval_nd t2 (Nval n2) →
      eval_nd (Te_plus t1 t2) (Nval n2).

Auxiliary inductive definitions
Inductive eval_nd_Const_1 n : val → Prop :=
  | E_Const_nd_1 : eval_nd_Const_1 n (Nval n).
Inductive eval_nd_Plus_1 t1 t2 : val → Prop :=
  | E_Plus_nd1_1 : ∀ n1 n2,
      eval_nd t1 (Nval n1) →
      eval_nd t2 (Nval n2) →
      eval_nd_Plus_1 t1 t2 (Nval (n1 + n2))
  | E_Plus_nd2_1 : ∀ n2,
      Q t1 →
      eval_nd t2 (Nval n2) →
      eval_nd_Plus_1 t1 t2 (Nval n2).
Inductive eval_Div0_1_2 (t1 : te) : val → Prop :=.

Definition eval_nd_1 : te → val → Prop :=
  fun t ⇒
    match t with
    | Te_const n ⇒ eval_nd_Const_1 n
    | Te_plus t1 t2 ⇒ eval_nd_Plus_1 t1 t2
    | Te_div0 t1 ⇒ eval_Div0_1_2 t1
    end.

Definition eval_nd_eval_nd_1 {t v} : eval_nd t v → eval_nd_1 t v :=
  fun e ⇒
    match e with
    | E_Const_nd n ⇒ E_Const_nd_1 n
    | E_Plus_nd1 t1 t2 n1 n2 e1 e2 ⇒ E_Plus_nd1_1 t1 t2 n1 n2 e1 e2
    | E_Plus_nd2 t1 t2 n2 q e2 ⇒ E_Plus_nd2_1 t1 t2 n2 q e2
    end.

Inductive eval_nd_Const_Nval_1_2 n : nat → Prop :=
  | E_Const_nd_Nval_1_2 : eval_nd_Const_Nval_1_2 n n.
Inductive eval_nd_Plus_Nval_1_2 t1 t2 : nat → Prop :=
  | E_Plus_nd_Nval1_1_2 : ∀ n1 n2,
      eval_nd t1 (Nval n1) →
      eval_nd t2 (Nval n2) →
      eval_nd_Plus_Nval_1_2 t1 t2 (n1 + n2)
  | E_Plus_nd_Nval2_1_2 : ∀ n2,
      Q t1 →
      eval_nd t2 (Nval n2) →
      eval_nd_Plus_Nval_1_2 t1 t2 n2.

Definition eval_nd_1_2 : te → val → Prop :=
  fun t v ⇒
    match t, v with
    | Te_const c, Nval n ⇒ eval_nd_Const_Nval_1_2 c n
    | Te_plus t1 t2, Nval n ⇒ eval_nd_Plus_Nval_1_2 t1 t2 n
    | _, _ ⇒ False
    end.

Definition eval_nd_eval_nd_1_2 {t v} : eval_nd t v → eval_nd_1_2 t v :=
  fun e ⇒
    match e with
    | E_Const_nd n ⇒ E_Const_nd_Nval_1_2 n
    | E_Plus_nd1 t1 t2 n1 n2 e1 e2 ⇒ E_Plus_nd_Nval1_1_2 t1 t2 n1 n2 e1 e2
    | E_Plus_nd2 t1 t2 n2 q e2 ⇒ E_Plus_nd_Nval2_1_2 t1 t2 n2 q e2
    end.

Lemma test_ev_nd2:
  ∀ t, eval_nd (Te_plus (Te_const 0) (Te_const 1)) t→ t = Nval 1.
Proof.
  intros t e.
  destruct (eval_nd_eval_nd_1 e) as [n1 n2 e1 e2 | n2 q e2].
  - destruct (eval_nd_eval_nd_1_2 e1). destruct (eval_nd_eval_nd_1_2 e2). reflexivity.
  - destruct (eval_nd_eval_nd_1_2 e2). reflexivity.
Qed.

Lemma test_ev_nd3:
  ∀ n, eval_nd (Te_plus (Te_const 0) (Te_const 1)) (Nval n) → n = 1.
Proof.
  intros n e.
  destruct (eval_nd_eval_nd_1_2 e) as [n1 n2 e1 e2 | n2 q e2].
  - destruct (eval_nd_eval_nd_1_2 e1). destruct (eval_nd_eval_nd_1_2 e2). reflexivity.
  - destruct (eval_nd_eval_nd_1_2 e2). reflexivity.
Qed.

End varQ.