Library examples.cime_trace.rewriting
Require Import Omega.
Require Import term.
Require Import Relations.
Require Inclusion.
Require equational_theory.
Require Import Wellfounded.
Notation "'SN'" := Acc.
Notation "'termine'" := well_founded.
Section Inclusion.
Variable A : Set.
Variable R1 R2 : A->A->Prop.
Hypothesis Incl : inclusion _ R1 R2.
Theorem SN_incl : forall x : A , SN R2 x -> SN R1 x.
unfold transp.
intros.
eapply Inclusion.Acc_incl ; eauto.
Qed.
Theorem termine_incl : termine R2 -> termine R1.
unfold transp.
intros.
eapply Inclusion.wf_incl ; eauto.
Qed.
End Inclusion.
Section Terminaison.
Variable T:Type.
Variable R: T -> T -> Prop.
Notation "T -R> U" := (R U T) (at level 80) : rewriting.
Open Scope rewriting.
Definition Retoile := clos_refl_trans _ R.
Theorem no_infinite_sequence2 : forall x : T , SN R x ->
~(exists f : nat -> T , f 0 = x /\ forall i : nat , f i -R> f (i+1)) .
intros.
induction H.
intuition.
elim H1.
intros.
apply (H0 (x0 1)).
intuition.
subst.
apply (H4 0).
exists ( fun i => (x0 (i+1))).
intuition.
Qed.
Variable f : T -> nat.
Hypothesis H_compat : forall x y: T, x -R> y -> f y < f x.
Theorem termine_gt_compat : termine R.
Proof.
red .
cut (forall n a, f a < n -> Acc R a).
intros H a.
apply (H (S (f a))); auto with arith.
induction n.
intros; absurd (f a < 0); auto with arith.
intros a ltSma.
apply Acc_intro.
intros b ltfafb.
apply IHn.
assert (f b < f a).
apply H_compat.
trivial.
omega.
Qed.
Inductive R2 (y x: T) : Prop :=
R2_intro: forall (z:T), x -R> z -> z -R> y -> R2 y x.
Lemma termineR2aux :
termine R -> forall x, SN R2 x /\ (forall y, R y x -> SN R2 y).
intros.
apply Acc_ind
with (R:=R) (P:=fun x => (SN R2 x) /\ (forall y, R y x -> (SN R2 y))).
intuition.
apply Acc_intro.
intros.
elim H2.
intros.
generalize (H1 z H3).
intuition.
generalize (H1 y H2).
intuition.
apply H.
Qed.
Theorem termineR2 : termine R -> termine R2.
intros rtermine.
red.
intros a.
generalize (termineR2aux rtermine).
intros hyp.
decompose [and] (hyp a).
auto.
Qed.
End Terminaison.