shttpd/coq/S/Lucid/Equivalence.v

(* SPDX-License-Identifier: GPL-2.0 or GPL-3.0
   Copyright © 2019 Ariadne Devos *)

Require Import S.Lucid.Arrow.
Require Import Coq.Sets.Ensembles.
Require Import Coq.Classes.Equivalence.

(* Define a notion of equivalence for arrow signatures *)
Section equivalence.

Variable World : Type.
Variable A B : Type.
Definition Domain := ArrowSig World A B.

Section definition.
Variable this that : Domain.

(* Equivalence of pre-conditions *)
Definition eqv_pre : Prop
  := forall p, pre this p <-> pre that p.

Definition eqv_rely : Prop
  := forall p w, rely this p w <-> rely that p w.

Definition eqv_guarantee : Prop
  := forall p w, guarantee this p w <-> guarantee that p w.

Definition eqv_post : Prop
  := forall p q, post this p q <-> post that p q.

(* (This probably says nothing about timing,
   cache access ...) *)
Definition eqv_sig : Prop
  := (eqv_pre /\ eqv_post) /\ (eqv_rely /\ eqv_guarantee).

End definition.

Ltac unfold_trans x y z :=
  match goal with
  | H : ?a x y, H1 : ?a y z |- ?a x z =>
    (unfold a; unfold a in H, H1)
  end.

Lemma eqv_sig_trans : Transitive eqv_sig.
Proof.
  intros x y z P Q.
  unfold_trans x y z.
  intuition.
  all : unfold_trans x y z.
  all : intros.
  + exact (transitivity (H3 p) (H0 p)).
  + exact (transitivity (H4 p q) (H6 p q)).
  + exact (transitivity (H p w) (H1 p w)).
  + exact (transitivity (H5 p w) (H7 p w)).
Qed.

Add Relation Domain eqv_sig
    reflexivity proved by ltac:(firstorder)
    symmetry proved by ltac:(firstorder)
    transitivity proved by eqv_sig_trans
    as eqv_sig_equiv.

End equivalence.

Arguments eqv_pre { _ _ _ } _ _.
Arguments eqv_rely { _ _ _ } _ _.
Arguments eqv_guarantee { _ _ _ } _ _.
Arguments eqv_post { _ _ _ } _ _.
Arguments eqv_sig { _ _ _ } _ _.