Library CoLoR.Term.WithArity.ARelation

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Sebastien Hinderer, 2004-02-09
general definitions and results about relations on terms

Set Implicit Arguments.

Require Import SN.
Require Import ASubstitution.
Require Import ATerm.
Require Import RelUtil.
Require Import List.
Require Import AContext.
Require Import LogicUtil.

Section S.

Variable Sig : Signature.

Notation term := (term Sig).

basic definitions and properties

Section basic.

Variable succ : relation term.

Definition preserv_vars := t u, succ t uincl (vars u) (vars t).

Definition substitution_closed :=
   t1 t2 s, succ t1 t2succ (sub s t1) (sub s t2).

Definition context_closed :=
   t1 t2 c, succ t1 t2succ (fill c t1) (fill c t2).

Definition rewrite_ordering := substitution_closed context_closed.

Definition reduction_ordering := WF succ rewrite_ordering.

End basic.

Record Rewrite_ordering : Type := mkRewrite_ordering {
  rew_ord_rel :> relation term;
  rew_ord_subs : substitution_closed rew_ord_rel;
  rew_ord_cont : context_closed rew_ord_rel
}.

reduction pair
weak reduction pair
reflexive closure

Section clos_refl.

Variable succ : relation term.

Notation succ_eq := (clos_refl succ).

Lemma rc_context_closed :
  weak_context_closed succ succ_eqcontext_closed succ_eq.

Proof.
intro. unfold context_closed. intros. unfold clos_refl in H0. decomp H0.
subst t2. unfold clos_refl. auto. apply H. assumption.
Qed.

Lemma rc_substitution_closed :
  substitution_closed succsubstitution_closed succ_eq.

Proof.
intro. unfold substitution_closed, clos_refl. intros. decomp H0.
subst t2. auto. right. apply H. assumption.
Qed.

Lemma rc_rewrite_ordering :
  weak_rewrite_ordering succ succ_eqrewrite_ordering succ_eq.

Proof.
intros (Hsubs,Hcont). split. apply rc_substitution_closed. assumption.
apply rc_context_closed. assumption.
Qed.

End clos_refl.

when succ is the strict part of succ_eq

Section strict.

Variables (succ_eq : relation term)
  (succ_eq_trans : transitive succ_eq).

Notation succ := (strict_part succ_eq).

Lemma absorb_strict : absorb succ succ_eq.

Proof.
unfold absorb, inclusion, RelUtil.compose, strict_part.
intros; split; decomp H. eapply succ_eq_trans. apply H1. assumption.
unfold not; intro. ded (succ_eq_trans H H1). contradiction.
Qed.

End strict.

End S.

tactics

Ltac destruct_rp :=
  match goal with
    | h : Reduction_pair _ |- _destruct h
    | h : Weak_reduction_pair _ |- _destruct h
    | h : reduction_ordering _ |- _destruct h
    | h : rewrite_ordering _ |- _destruct h
  end.

Ltac WFtac := repeat destruct_rp; assumption.

Ltac rptac := repeat destruct_rp; try split; assumption.