From b8cdcecd1a814e4cfa336b45efc42a0ae148a9db Mon Sep 17 00:00:00 2001 From: Heiko Becker Date: Sun, 18 Sep 2016 18:50:04 +0200 Subject: [PATCH] Add equality on booleans for expressions --- coq/Expressions.v | 35 ++++++++++++++++++++++++++++++++++- 1 file changed, 34 insertions(+), 1 deletion(-) diff --git a/coq/Expressions.v b/coq/Expressions.v index 008ecea..961242a 100644 --- a/coq/Expressions.v +++ b/coq/Expressions.v @@ -1,7 +1,7 @@ (** Formalization of the base expression language for the daisy framework **) -Require Import Coq.Reals.Reals Coq.micromega.Psatz. +Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith. Require Import Daisy.Infra.RealSimps Daisy.Infra.Abbrevs. Set Implicit Arguments. (** @@ -9,6 +9,15 @@ Set Implicit Arguments. Define them first **) Inductive binop : Type := Plus | Sub | Mult | Div. + +Definition binop_eq_bool (b1:binop) (b2:binop) := + match b1 with + Plus => match b2 with Plus => true |_ => false end + | Sub => match b2 with Sub => true |_ => false end + | Mult => match b2 with Mult => true |_ => false end + | Div => match b2 with Div => true |_ => false end + end. + (** Next define an evaluation function for binary operators on reals. Errors are added on the expression evaluation level later. @@ -33,6 +42,30 @@ Inductive exp (V:Type): Type := | Const: V -> exp V | Binop: binop -> exp V -> exp V -> exp V. + +Fixpoint exp_eq_bool (e1:exp Q) (e2:exp Q) := + match e1 with + |Var _ v1 => + match e2 with + |Var _ v2 => v1 =? v2 + | _=> false + end + |Param _ v1 => + match e2 with + |Param _ v2 => v1 =? v2 + | _=> false + end + |Const n1 => + match e2 with + |Const n2 => Qeq_bool n1 n2 + | _=> false + end + |Binop b1 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)) + |_ => false + end + end. (** Define a perturbation function to ease writing of basic definitions **) -- GitLab