Library CoLoR.Util.Relation.RedLength

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2005-02-17
  • Adam Koprowski and Hans Zantema, 2007-03
maximal reduction length of a term for a finitely branching well-founded relation

Set Implicit Arguments.

Require Import SN.
Require Import ListMax.
Require Import RelUtil.
Require Import ListUtil.
Require Import LogicUtil.
Require Import Arith.

Section S.

Variables (A : Type) (R : relation A) (FB : finitely_branching R) (WF : WF R).

Definition len_aux x (len : y, R x ynat) :=
  let f i (hi : i < length (sons FB x)) :=
    len (ith hi) (in_sons_R FB (ith_In hi))
  in S (lmax (pvalues f)).

Lemma len_aux_ext : x (f g : y, R x ynat),
  ( y (p : R x y), f y p = g y p) → len_aux f = len_aux g.

Proof.
intros. unfold len_aux. apply (f_equal (fun lS (lmax l))).
apply pvalues_eq. intros. apply H.
Qed.

Definition len : Anat := Fix (WF_wf_transp WF) _ len_aux.

Lemma len_eq : x, len x = S (lmax (map len (sons FB x))).

Proof.
intro. unfold len. rewrite Fix_eq. 2: exact len_aux_ext. fold len.
unfold len_aux. apply (f_equal (fun lS (lmax l))).
rewrite <- (@pvalues_ith_eq_map A nat). apply pvalues_eq. intros. refl.
Qed.

Lemma R_len : x y, R x ylen x > len y.

Proof.
intros. rewrite len_eq. unfold gt, lt. apply le_n_S. apply in_lmax.
apply in_map. apply R_in_sons. exact H.
Qed.

End S.