PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.Tools.SetoidUtil

A Framework for Certified Self-Stabilization
PADEC Coq Library

Global imports

From Coq Require Import Relations.
From Coq Require Import RelationPairs.
From Coq Require Import SetoidClass.
From Coq Require Import Omega.
From Coq Require Sumbool.
From Coq Require List.

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).
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).
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)
Instance PER_SetoidClass_equiv {A} `{SA: Setoid A}:
  RelationClasses.PER (SetoidClass.equiv (A := A)).

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 }.

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)
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


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

Hint Resolve equiv_self.

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

Instance Setoid_nat: Setoid nat := {| equiv:=eq |}.
Instance Setoid_Z: Setoid Z := {| equiv:=eq |}.
Instance Setoid_N: Setoid N := {| equiv:=eq |}.
Instance Setoid_pos: Setoid positive := {| equiv:=eq |}.
Instance Setoid_bool: Setoid bool := {| equiv:=eq |}.
Instance Setoid_unit: Setoid unit := {| equiv:=eq |}.
Instance Setoid_empty: Setoid Empty_set := {| equiv:=eq |}.
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.

Program Instance sumbool_Setoid {P} {Q}: Setoid ({P} + {Q}) :=
  {| equiv := sumbool_equiv (P := P) (Q := Q) |}.

Partial Setoid of Functions from A to B

with A (resp. B) being a setoid or a partial setoid
Instance Fun_PartialSetoid0 {A} `{SA: Setoid A} {B} `{SB: Setoid B}:
  PartialSetoid (A -> B) | 0:=
  {| pequiv := (equiv ==> equiv) |}.

Instance Fun_PartialSetoid1 {A} `{SA: Setoid A} {B} `{SB: PartialSetoid B}:
  PartialSetoid (A -> B) | 1 :=
  {| pequiv := (equiv ==> pequiv) |}.

Instance Fun_PartialSetoid2 {A} `{SA: PartialSetoid A} {B} `{SB: Setoid B}:
  PartialSetoid (A -> B) | 1 :=
  {| pequiv := (pequiv ==> equiv) |}.

Instance Fun_PartialSetoid3 {A} `{SA: PartialSetoid A}
         {B} `{SB: PartialSetoid B}: PartialSetoid (A -> B)| 2 :=
  {| pequiv := (pequiv ==> pequiv) |}.

Notation to distinguish functional equivalence
Notation fequiv := (pequiv (A:= _ -> _)).

Setoid and Partial Setoid on product


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

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

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.

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

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

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

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

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

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

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

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

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

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

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

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.