PADEC - Coq Library

Library Padec.Tools.SetoidUtil

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global imports

From Coq Require Import Relations.
From Coq Require Import RelationPairs.
From Coq Require Import SetoidClass.
From Coq Require Import Lia.
From Coq Require Sumbool.
From Coq Require List.
From Coq Require Import BinNums.

Open Scope signature_scope.
Set Implicit Arguments.

Basic Tactics

Ltac dup x x' := (assert (x':=x)).

Ltac proper_ := unfold Proper;etransitivity;
[eassumption || symmetry;eassumption|
assumption || symmetry;assumption] .

Induction scheme for Acc:

How to prove some property P by induction on Acc? Goal P generalize (property_about_Acc); intros W. induction W as n W IH using Acc_ind_dep. This creates two hypothesis W: forall y, y R n -> Acc R y IH: forall y, y R n -> P y

Scheme Acc_ind_dep := Induction for Acc Sort Prop.

(brute force!) tactic

Ltac blast :=
reflexivity || assumption ||
(symmetry; (reflexivity || assumption)) || tauto || auto.

tactic case_eqs: use it instead of cases to remember equality from which come the cases

Ltac case_eqs r t :=
  (cut (r t t); [|reflexivity]); pattern t at - 1; case t.

Ltac case_equiv t :=
  (generalize (@Equivalence_Reflexive _ equiv setoid_equiv t);
   pattern t at - 1;case t).

Setoid / Partial Setoid

A setoid is a set endowed with an equivalence relation. A: Type; SA: Setoid A nb: Setoid is type class; SA ensures that A is a setoid endowed with equivalence relation noted equiv

Any equivalence relation is compatible (w.r.t. itself).

Global Instance equiv_compat {A} `{SA: Setoid A}:
Proper (equiv ==> equiv ==> iff) (equiv (A := A)).

A partial setoid is a set endowed with an partial equivalence relation (no reflexivity) A: Type; SA: PartialSetoid A nb: PartialSetoid is type class; SA ensures that A is a setoid endowed with partial equivalence relation noted pequiv

Any partial equivalence relation is compatible (w.r.t. itself).

Global Instance pequiv_compat {A} `{SA: PartialSetoid A}:
Proper (pequiv ==> pequiv ==> iff) (pequiv (A := A)).

Equality from setoid or partial setoid is PER (Partial Equivalence Relation, from RelationClasses, type class)

Global Instance PER_SetoidClass_equiv {A} `{SA: Setoid A}:
RelationClasses.PER (SetoidClass.equiv (A := A)).

Global Instance PER_SetoidClass_pequiv {A} `{SA: PartialSetoid A}:
RelationClasses.PER (SetoidClass.pequiv (A := A)).

Builds the relation (as a type class) from the partial setoid equality Note the low priority of this rule (100)

Class Relation (A: Type) := { xequiv: relation A }.

Global Instance PartialSetoid_rel {A} `{SA: PartialSetoid A}: Relation A | 100 :=
{|xequiv := pequiv|}.

A setoid is also a partial setoid Note the low priority of this rule (100)

Global Instance Partial_Setoid {A} `{SA: Setoid A}: PartialSetoid A | 100 :=
{| pequiv:=equiv |}.

Lemma promote_pequiv A `{SA: Setoid A}:
@pequiv _ (@Partial_Setoid _ SA) = @equiv _ SA.

This lemma means that pequiv on a Setoid is the same relation as equiv

Setoids for basic datatypes:

nat, Z, N, pos, bool, unit, Empty_set, Prop, sumbool

> no generic instance for eq

Definition equiv_self {A} `{Setoid A} (a: A): a == a :=
  Equivalence_Reflexive a.

Global Hint Resolve equiv_self : core.

Global Hint Extern 5 (?X1 =~= ?X2) => proper_ : core.

Global Instance Setoid_nat: Setoid nat := {| equiv:=eq |}.
Global Instance Setoid_Z: Setoid Z := {| equiv:=eq |}.
Global Instance Setoid_N: Setoid N := {| equiv:=eq |}.
Global Instance Setoid_pos: Setoid positive := {| equiv:=eq |}.
Global Instance Setoid_bool: Setoid bool := {| equiv:=eq |}.
Global Instance Setoid_unit: Setoid unit := {| equiv:=eq |}.
Global Instance Setoid_empty: Setoid Empty_set := {| equiv:=eq |}.
Global Instance Setoid_Prop: Setoid Prop := {| equiv:=iff |}.

Definition sumbool_equiv (P Q: Prop): relation ({P } + {Q }) :=
  fun sb1 sb2 =>
    match sb1, sb2 with
    | left _, left _ | right _, right _ => True
    | left _, right _ | right _, left _ => False
    end.

Partial Setoid of Functions from A to B

with A (resp. B) being a setoid or a partial setoid

Notation to distinguish functional equivalence

Notation fequiv := (pequiv (A:= _ -> _)).

Setoid and Partial Setoid on product

Global Instance RelProd_Setoid {A: Type} `{SA: Setoid A} {B: Type}
         `{SB: Setoid B}: Setoid (A * B) :=
  {| equiv := (equiv (A := A) * equiv (A := B)) |}.

Global Instance RelProd_per {A} {eqA} `{PER A eqA} {B} {eqB} `{PER B eqB} :
  PER (eqA * eqB).

Global Instance RelProd_PartialSetoid {A: Type} `{SA: PartialSetoid A}
         {B: Type} `{SB: PartialSetoid B}: PartialSetoid (A * B) :=
  {| pequiv := (pequiv (A := A) * pequiv (A := B)) |}.

Global Instance fst_compat {A B: Type} (eqA: relation A) (eqB: relation B):
  Proper ( (eqA * eqB ) ==> eqA) fst.

Global Instance snd_compat {A B: Type} (eqA: relation A) (eqB: relation B):
  Proper ( (eqA * eqB ) ==> eqB ) snd.

Setoid and Partial Setoid on Subsets (dependant types)

Section Subsets.

  Context {A: Type} {eqA: relation A}.
  Context (P: A -> Prop) (M: A -> Type).

  Definition eqSig: relation (sig P) :=
    fun a1 a2 => eqA (proj1_sig a1) (proj1_sig a2).

  Definition eqSigT: relation (sigT M) :=
    fun a1 a2 => eqA (projT1 a1) (projT1 a2).

End Subsets.

Global Instance eqSig_equiv {A: Type} (eqA: relation A) `{EA: Equivalence _ eqA}
         (P: A -> Prop): Equivalence (@eqSig _ eqA P).

Global Instance sig_Setoid {A: Type} `{SA: Setoid A} (P: A -> Prop):
  Setoid (sig P):= {| equiv := (@eqSig _ equiv P) |}.

Global Instance eqSigT_equiv {A: Type} (eqA: relation A) `{EA: Equivalence _ eqA}
         (M: A -> Type): Equivalence (@eqSigT _ eqA M).

Global Instance sigT_Setoid {A: Type} `{SA: Setoid A} (M: A -> Type):
  Setoid (sigT M):= {| equiv := (@eqSigT _ equiv M) |}.

Global Instance eqSig_per {A: Type} (eqA: relation A) `{PA: PER _ eqA}
         (P: A -> Prop): PER (@eqSig _ eqA P).

Global Instance sig_PartialSetoid {A: Type} `{SA: PartialSetoid A}
         (P: A -> Prop): PartialSetoid (sig P)
  := {| pequiv := (@eqSig _ pequiv P) |}.

Global Instance eqSigT_per {A: Type} (eqA: relation A) `{PA: PER _ eqA}
         (M: A -> Type): PER (@eqSigT _ eqA M).

Global Instance sigT_PartialSetoid {A: Type} `{SA: PartialSetoid A}
         (M: A -> Type): PartialSetoid (sigT M)
  := {| pequiv := (@eqSigT _ pequiv M) |}.

Tools for proving Compatibility

Tools based on equality to prove compatibility

Global Instance equiv_to_Proper_l {A: Type} `{SA: Setoid A}:
  forall a1 a2, a1 == a2 -> Proper equiv a1.

Global Instance equiv_to_Proper_r {A: Type} `{SA: Setoid A}:
  forall a1 a2, a1 == a2 -> Proper equiv a2.

Global Instance pequiv_to_Proper_l {A: Type} `{SA: PartialSetoid A}:
  forall a1 a2, a1 =~= a2 -> Proper pequiv a1.

Global Instance pequiv_to_Proper_r {A: Type} `{SA: PartialSetoid A}:
  forall a1 a2, a1 =~= a2 -> Proper pequiv a2.

Tools based on comparison for proving compatibility

Global Instance le_compat: Proper fequiv le.

Global Instance ge_compat: Proper fequiv ge.

Global Instance lt_compat: Proper fequiv lt.

Global Instance gt_compat: Proper fequiv gt.

Tools based on logic connectors for proving compatibility

Lemma impl_iff_compat_ext A1 A2 B1 B2:
  (A1 <-> A2 ) -> (A1 -> (B1 <-> B2 )) ->
  ((A1 -> B1 ) <-> (A2 -> B2 )).

Lemma and_iff_compat_ext (A1 A2 B1 B2: Prop):
  (B2 -> (A1 <-> A2 )) -> (A1 -> (B1 <-> B2 )) ->
  ((A1 /\ B1 ) <-> (A2 /\ B2 )).

Global Instance iff_compat: Proper fequiv iff.

if then else

Global Instance ITE_compat1 {A: Type} `{SA: Setoid A}:
  Proper (fequiv) (fun (cond: bool) (iftrue iffalse: A) =>
                     if cond then iftrue else iffalse).

Global Instance ITE_compat2 {A: Type} `{SA: PartialSetoid A}:
  Proper (fequiv) (fun (cond: bool) (iftrue iffalse: A) =>
                     if cond then iftrue else iffalse).

Global Instance ITE_sumbool_compat1 {A: Type} `{SA: Setoid A}
       {P: Prop} {Q: Prop}:
  Proper (fequiv) (fun (cond: {P } + {Q }) (ifleft ifright: A) =>
                     if cond then ifleft else ifright).

Global Instance ITE_sumbool_compat2 {A: Type} `{SA: PartialSetoid A}
       {P: Prop} {Q: Prop}:
  Proper (fequiv) (fun (cond: {P } + {Q }) (ifleft ifright: A) =>
                     if cond then ifleft else ifright).

forall

Notation all_compat := Morphisms_Prop.all_iff_morphism.

exists

Notation ex_compat := Morphisms_Prop.ex_iff_morphism.

Notation impl_compat := Morphisms_Prop.iff_iff_iff_impl_morphism.

Notation or_compat:=Morphisms_Prop.or_iff_morphism.

Notation and_compat:=Morphisms_Prop.and_iff_morphism.

Notation not_compat:=Morphisms_Prop.not_iff_morphism.

Global Instance eq_compat A : Proper (eq ==> eq ==> iff) (@eq A).

Decidability of equality

Decider eq: means eq is decidable

Definition Decider {A: Type} (eqA: relation A) :=
  forall a a', {eqA a a'} + {~eqA a a'}.

Definition Weak_Dec {A: Type} (eqA: relation A) (P: A -> Prop) :=
  forall a, {Proper eqA a -> P a } + {~P a }.

Definition Weak_Dec_relation {A: Type} (eqA: relation A) :=
  forall a1 a2, {Proper eqA a1 -> Proper eqA a2 -> eqA a1 a2 } +
                {~eqA a1 a2 }.

Definition RelProd_dec {A B} {eqA: relation A} {eqB: relation B}
           (Adec:Decider eqA) (eqB_dec:Decider eqB):
  Decider (eqA *eqB).

Lemma eqSig_dec {A: Type} (eqA: relation A) (eqA_dec: Decider eqA)
      (P: A -> Prop): Decider (@eqSig _ eqA P).

Lemma eqSigT_dec {A: Type} (eqA: relation A) (eqA_dec: Decider eqA)
      (M: A -> Type): Decider (@eqSigT _ eqA M).

Respectful for dependent functions

Section Respectful_Dependent.

  Import List.

  Notation fun_type := (@fold_right Type Type (fun U V => U -> V)).

  Notation sfun_type := (@fold_right Type (Prop + Type)
                                     (fun U V => match U with
                                                 | inl pp => pp -> V
                                                 | inr pt => pt -> V
                                                 end)).

  Notation pred_type := (fun_type Type).

  Notation fun2_type := (@fold_right Type Type (fun U V => U -> U -> V)).

  Notation pred2_type := (fun2_type Prop).

  Notation vect_type := (fun (T: Type -> Type) =>
                           @fold_right Type Type (fun U V => (T U * V)%type)
                                       unit).

  Notation rel_type := (vect_type relation).

  Notation elt_type := (vect_type (fun x => x)).

  Notation Plist lA :=(list (fun_type Prop lA + fun_type Type lA)).

  Notation Papply := (fun T Q (t: T) =>
                        List.map (fun p =>
                                    match p with
                                    | inl pp => inl (pp t)
                                    | inr pt => inr (pt t)
                                    end): Plist (T ::Q) -> Plist Q).

End Respectful_Dependent.

Close Scope signature_scope.
Unset Implicit Arguments.