Module Qcert.Common.Operators.OperatorsEq



Section OperatorsEq.
  Require Import Equivalence.
  Require Import Morphisms.
  Require Import Setoid.
  Require Import EquivDec.
  Require Import Program.
  Require Import List.
  Require Import String.
  Require Import Utils.
  Require Import BrandRelation.
  Require Import ForeignData.
  Require Import Data.
  Require Import DataNorm.
  Require Import Iterators.
  Require Import OperatorsUtils.
  Require Import BinaryOperatorsSem.
  Require Import UnaryOperatorsSem.
  Require Import ForeignOperators.

  Context {fdata:foreign_data}.
  Context {fuop:foreign_unary_op}.
  Context {fbop:foreign_binary_op}.


  Definition unary_op_eq (uop1 uop2:unary_op) : Prop :=
    forall (h:list (string*string)),
    forall (x:data),
      data_normalized h x ->
      (unary_op_eval h uop1) x = (unary_op_eval h uop2) x.

  Global Instance unary_op_equiv : Equivalence unary_op_eq.
Proof.
    constructor.
    - unfold Reflexive, unary_op_eq.
      intros; reflexivity.
    - unfold Symmetric, unary_op_eq.
      intros; rewrite H by trivial; reflexivity.
    - unfold Transitive, unary_op_eq.
      intros; rewrite H, H0 by trivial; reflexivity.
  Qed.

  Definition binary_op_eq (bop1 bop2:binary_op) : Prop :=
    forall (h:list (string*string)),
    forall (x:data),
      data_normalized h x ->
      forall (y:data),
        data_normalized h x ->
        (binary_op_eval h bop1) x y = (binary_op_eval h bop2) x y.

  Global Instance binary_op_equiv : Equivalence binary_op_eq.
Proof.
    constructor.
    - unfold Reflexive, binary_op_eq.
      intros; reflexivity.
    - unfold Symmetric, binary_op_eq.
      intros; rewrite (H h) by trivial; reflexivity.
    - unfold Transitive, binary_op_eq.
      intros; rewrite (H h), (H0 h) by trivial; reflexivity.
  Qed.

End OperatorsEq.