Library hydras.Prelude.WfVariant

Pierre Casteran, LaBRI, University of Bordeaux Definition of termination variants

Set Implicit Arguments.

From Coq Require Import Relations Basics
     Wellfounded.Inverse_Image Wellfounded.Inclusion.

Section Variants.
Variable E: Type.
Variable tr : relation E.
Definition terminates := well_founded (flip tr).

Variables (T: Type)
           (lt : relation T)
           (m : E → T).

Infix "<" := lt.

Class WfVariant :=
   {
     wf : well_founded lt;
     decr : ∀ x y, tr x y → m y < m x
   }.

Lemma Variant_termination (Var : WfVariant ) : terminates .

End Variants.

Arguments decr {E tr T lt m} _ _ _ _.
Arguments wf {E tr T lt m} _ _ .