Add Unary operators to expression semantics

coq/Expressions.v

@@ -23,13 +23,36 @@ Definition binop_eq_bool (b1:binop) (b2:binop) :=
   Next define an evaluation function for binary operators on reals.
   Errors are added on the expression evaluation level later.
  **)
-Fixpoint eval_binop (o:binop) (v1:R) (v2:R) :=
+Definition eval_binop (o:binop) (v1:R) (v2:R) :=
   match o with
   | Plus => Rplus v1 v2
   | Sub => Rminus v1 v2
   | Mult => Rmult v1 v2
   | Div => Rdiv v1 v2
   end.
+
+(**
+   Expressions will use unary operators.
+   Define them first
+ **)
+Inductive unop: Type := Neg | Inv.
+
+Definition unop_eq_bool (o1:unop) (o2:unop) :=
+  match o1 with
+  |Neg => match o2 with |Neg => true |_=> false end
+  |Inv => match o2 with |Inv => true |_ => false end
+  end.
+
+(**
+   Define evaluation for unary operators on reals.
+   Errors are added on the expression evaluation level later.
+ **)
+Definition eval_unop (o:unop) (v:R):=
+  match o with
+  |Neg => (- v)%R
+  |Inv => (/ v)%R
+  end .
+
 (**
   Define expressions parametric over some value type V.
   Will ease reasoning about different instantiations later.
@@ -41,6 +64,7 @@ Inductive exp (V:Type): Type :=
   Var: nat -> exp V
 | Param: nat -> exp V
 | Const: V -> exp V
+| Unop: unop -> exp V -> exp V
 | Binop: binop -> exp V -> exp V -> exp V.
 
 
@@ -61,9 +85,14 @@ Fixpoint exp_eq_bool (e1:exp Q) (e2:exp Q) :=
    |Const n2 => Qeq_bool n1 n2
    | _=> false
    end
-  |Binop b1 e11 e12 =>
+  |Unop o1 e11 =>
+   match e2 with
+   |Unop o2 e22 => andb (unop_eq_bool o1 o2) (exp_eq_bool e11 e22)
+   |_ => false
+   end
+  |Binop o1 e11 e12 =>
    match e2 with
-   |Binop b2 e21 e22 => andb (binop_eq_bool b1 b2) (andb (exp_eq_bool e11 e21) (exp_eq_bool e12 e22))
+   |Binop o2 e21 e22 => andb (binop_eq_bool o1 o2) (andb (exp_eq_bool e11 e21) (exp_eq_bool e12 e22))
    |_ => false
    end
   end.
@@ -89,8 +118,13 @@ Inductive eval_exp (eps:R) (env:env_ty) : (exp R) -> R -> Prop :=
 | Const_dist n delta:
     Rle (Rabs delta) eps ->
     eval_exp eps env (Const n) (perturb n delta)
-|Binop_dist op e1 e2 v1 v2 delta:
-   Rle (Rabs delta) eps ->
+(** Unary negation is special! We do not have a new error here since IEE 754 gives us a sign bit **)
+| Unop_neg e1 v1: eval_exp eps env e1 v1 -> eval_exp eps env (Unop Neg e1) (eval_unop Neg v1)
+| Unop_inv e1 v1 delta: Rle (Rabs delta) eps ->
+                        eval_exp eps env e1 v1 ->
+                        eval_exp eps env (Unop Inv e1) (perturb (eval_unop Inv v1) delta)
+| Binop_dist op e1 e2 v1 v2 delta:
+    Rle (Rabs delta) eps ->
                 eval_exp eps env e1 v1 ->
                 eval_exp eps env e2 v2 ->
                 eval_exp eps env (Binop op e1 e2) (perturb (eval_binop op v1 v2) delta).
@@ -120,11 +154,14 @@ Lemma eval_0_det (e:exp R) (env:env_ty):
   v1 = v2.
 Proof.
   induction e; intros v1 v2 eval_v1 eval_v2;
-    inversion eval_v1; inversion eval_v2; [ auto | | | ];
-      repeat try rewrite perturb_0_val; auto.
-  subst.
-  rewrite (IHe1 v0 v4); auto.
-  rewrite (IHe2 v3 v5); auto.
+    inversion eval_v1; inversion eval_v2; [ auto | | | | | | | ];
+      repeat try rewrite perturb_0_val; subst; auto.
+  - rewrite (IHe v0 v3); auto.
+  - inversion H3.
+  - inversion H4.
+  - rewrite (IHe v0 v3); auto.
+  - rewrite (IHe1 v0 v4); auto.
+    rewrite (IHe2 v3 v5); auto.
 Qed.
 
 (**
@@ -134,7 +171,7 @@ evaluating the subexpressions and then binding the result values to different
 variables in the environment.
 This needs the property that variables are not perturbed as opposed to parameters
 **)
-Lemma existential_rewriting (b:binop) (e1:exp R) (e2:exp R) (eps:R) (cenv:env_ty) (v:R):
+Lemma existential_rewriting_binary (b:binop) (e1:exp R) (e2:exp R) (eps:R) (cenv:env_ty) (v:R):
   (eval_exp eps cenv (Binop b e1 e2) v <->
    exists v1 v2,
      eval_exp eps cenv e1 v1 /\
@@ -157,6 +194,28 @@ Proof.
     constructor; auto.
 Qed.
 
+
+Lemma existential_rewriting_unary (e:exp R) (eps:R) (cenv:env_ty) (v:R):
+  (eval_exp eps cenv (Unop Inv e) v <->
+   exists v1,
+     eval_exp eps cenv e v1 /\
+     eval_exp eps (updEnv 1 v1 cenv) (Unop Inv (Var R 1)) v).
+Proof.
+  split.
+  - intros eval_un.
+    inversion eval_un; subst.
+    exists v1.
+    repeat split; try auto.
+    constructor; try auto.
+    constructor; auto.
+  - intros exists_val.
+    destruct exists_val as [v1 [eval_e1 eval_e_env]].
+    inversion eval_e_env; subst.
+    inversion H1; subst.
+    unfold updEnv in *; simpl in *.
+    constructor; auto.
+Qed.
+
 (**
   Using the parametric expressions, define boolean expressions for conditionals
 **)