diff --git a/coq/Expressions.v b/coq/Expressions.v index 128bf2603331462f29996750b2fe5c825a03af73..f4b238997162fb7173d5e2add9625d56a3778404 100644 --- a/coq/Expressions.v +++ b/coq/Expressions.v @@ -91,6 +91,40 @@ Definition evalUnop (o:unop) (v:R):= |Inv => (/ v)%R end . +(** + Expressions will use ternary operators + Define them first +**) +Inductive terop: Type := Fma. + +Definition teropEq (o1: terop) (o2: terop) := + match o1, o2 with + | Fma, Fma => true + end. + +Lemma teropEq_refl b: + teropEq b b = true. +Proof. + now destruct b. +Qed. + +Lemma teropEq_compat_eq b1 b2: + teropEq b1 b2 = true <-> b1 = b2. +Proof. + now destruct b1, b2. +Qed. + +Lemma teropEq_compat_eq_false b1 b2: + teropEq b1 b2 = false <-> ~ (b1 = b2). +Proof. + now destruct b1, b2. +Qed. + +Definition evalTerop (o: terop) (v1: R) (v2: R) (v3: R) := + match o with + | Fma => Rplus v1 (Rmult v2 v3) + end. + (** Define expressions parametric over some value type V. Will ease reasoning about different instantiations later. @@ -100,6 +134,7 @@ Inductive exp (V:Type): Type := | Const: mType -> V -> exp V | Unop: unop -> exp V -> exp V | Binop: binop -> exp V -> exp V -> exp V +| Terop: terop -> exp V -> exp V -> exp V -> exp V | Downcast: mType -> exp V -> exp V. (** @@ -115,6 +150,8 @@ Fixpoint expEq (e1:exp Q) (e2:exp Q) := (unopEq o1 o2) && (expEq e11 e22) | Binop o1 e11 e12, Binop o2 e21 e22 => (binopEq o1 o2) && (expEq e11 e21) && (expEq e12 e22) + | Terop o1 e11 e12 e13, Terop o2 e21 e22 e23 => + (teropEq o1 o2) && (expEq e11 e21) && (expEq e12 e22) && (expEq e13 e23) | Downcast m1 f1, Downcast m2 f2 => (mTypeEq m1 m2) && (expEq f1 f2) | _, _ => false @@ -129,6 +166,7 @@ Proof. - apply Qeq_bool_iff; lra. - case u; auto. - case b; auto. + - case t. firstorder. - apply mTypeEq_refl. Qed. @@ -149,6 +187,11 @@ Proof. * destruct b; auto. * apply IHe1. + apply IHe2. + - f_equal. + + f_equal. + * destruct t, t0. simpl. apply IHe1. + * apply IHe2. + + apply IHe3. - f_equal. + apply mTypeEq_sym; auto. + apply IHe. @@ -180,6 +223,13 @@ Proof. rewrite binopEq_refl; simpl. apply andb_true_iff. split; [eapply IHe1; eauto | eapply IHe2; eauto]. + - andb_to_prop eq1; + andb_to_prop eq2. + rewrite teropEq_compat_eq in *; subst. + rewrite teropEq_refl; simpl. + rewrite andb_true_iff. + rewrite andb_true_iff. + firstorder. - andb_to_prop eq1; andb_to_prop eq2. rewrite mTypeEq_compat_eq in *; subst. @@ -189,11 +239,12 @@ Qed. Fixpoint toRExp (e:exp Q) := match e with - |Var _ v => Var R v - |Const m n => Const m (Q2R n) - |Unop o e1 => Unop o (toRExp e1) - |Binop o e1 e2 => Binop o (toRExp e1) (toRExp e2) - |Downcast m e1 => Downcast m (toRExp e1) + | Var _ v => Var R v + | Const m n => Const m (Q2R n) + | Unop o e1 => Unop o (toRExp e1) + | Binop o e1 e2 => Binop o (toRExp e1) (toRExp e2) + | Terop o e1 e2 e3 => Terop o (toRExp e1) (toRExp e2) (toRExp e3) + | Downcast m e1 => Downcast m (toRExp e1) end. Fixpoint toREval (e:exp R) := @@ -202,6 +253,7 @@ Fixpoint toREval (e:exp R) := | Const _ n => Const M0 n | Unop o e1 => Unop o (toREval e1) | Binop o e1 e2 => Binop o (toREval e1) (toREval e2) + | Terop o e1 e2 e3 => Terop o (toREval e1) (toREval e2) (toREval e3) | Downcast _ e1 => Downcast M0 (toREval e1) end. @@ -493,4 +545,4 @@ Qed. *) (* Simplify arithmetic later by making > >= only abbreviations *) (* **) *) (* Definition gr := fun (V:Type) (f1: exp V) (f2: exp V) => less f2 f1. *) -(* Definition greq := fun (V:Type) (f1:exp V) (f2: exp V) => leq f2 f1. *) \ No newline at end of file +(* Definition greq := fun (V:Type) (f1:exp V) (f2: exp V) => leq f2 f1. *)