# Library term_algebra.equational_theory

``` Add LoadPath "basis". Add LoadPath "list_extensions". ```

# Equational theory on a term algebra

``` Require Import List. Require Import Relations. Require Import Wellfounded. Require Import Arith. Require Import closure. Require Import more_list. Require Import list_permut. Require Import dickson. Require Import term. Notation " T '-[' R ']->' U " := (R U T) (at level 80) : term_scope . ```

## Module Type EqTh, an equational theory over a term algebra.

``` Module Type EqTh.   Declare Module T : term.Term.   Import T. Inductive defined (R : relation term) : symbol -> Prop :=   | Def : forall f l t, R t (Term f l) -> defined R f. Inductive constructor (R : relation term) : symbol -> Prop :=   | Const : forall f, (forall l t, ~ (R t (Term f l))) -> constructor R f. Inductive module (R1 R2 : relation term) : Prop :=   | Mod : (forall f2 s t, defined R2 f2 ->                     R1 s t -> symb_in_term_list f2 (s :: t :: nil) = false) ->              module R1 R2. ```

### One step at top.

``` Inductive axiom (R : relation term) : term -> term -> Prop :=   | instance : forall t1 t2 sigma,        R t1 t2 -> axiom R (apply_subst sigma t1) (apply_subst sigma t2). ```

### One step at any position.

``` Inductive one_step (R : relation term) : term -> term -> Prop :=   | at_top : forall t1 t2, axiom R t1 t2 -> one_step R t1 t2   | in_context : forall f l1 l2,       one_step_list R l1 l2 -> one_step R (Term f l1) (Term f l2) with one_step_list (R : relation term) : list term -> list term -> Prop :=   | head_step : forall t1 t2 l,        one_step R t1 t2 -> one_step_list R (t1 :: l) (t2 :: l)  | tail_step : forall t l1 l2,      one_step_list R l1 l2 -> one_step_list R (t :: l1) (t :: l2). ```

### Rewriting Theory as transitive closure of an equational step.

``` Definition rwr (R : relation term) t1 t2 := trans_clos (one_step R) t1 t2. Notation " T '-[' R '+]->' U " := (rwr R T U) (at level 80) : term_scope . Hint Constructors axiom one_step one_step_list. Axiom one_step_list_length_eq :   forall R l1 l2, one_step_list R l1 l2 -> length l1 = length l2. Axiom R_axiom : forall (R : relation term) t1 t2, R t1 t2 -> axiom R t1 t2. Axiom R_one_step : forall (R : relation term) t1 t2, R t1 t2 -> one_step R t1 t2. Axiom R_rwr : forall t1 t2 (R : relation term), R t1 t2 -> rwr R t1 t2. ```

### Generalization over lists of terms.

``` Fixpoint rwr_list (R : relation term) (l1 l2 : list term) {struct l1} : Prop :=    match l1, l2 with    | nil, nil => False    | nil, _ :: _ => False    | _ :: _, nil => False    | h1::tl1, h2::tl2 => (rwr R h1 h2 /\ tl1 = tl2) \/                                       (h1 = h2 /\ rwr_list R tl1 tl2) \/                                       (rwr R h1 h2 /\ rwr_list R tl1 tl2)    end. Axiom rwr_list_length_eq : forall R l1 l2, rwr_list R l1 l2 -> length l1 = length l2. Axiom one_step_list_rwr_list : forall R l1 l2, one_step_list R l1 l2 -> rwr_list R l1 l2. Axiom rwr_list_is_trans :   forall R l1 l2 l3, rwr_list R l1 l2 -> rwr_list R l2 l3 -> rwr_list R l1 l3. Axiom rwr_list_trans_clos_one_step_list :   forall R l1 l2, rwr_list R l1 l2 <-> trans_clos (one_step_list R) l1 l2. ```

### Rewriting is a congruence.

``` Axiom context_cons :   forall R f t1 t2 l, rwr R t1 t2 -> rwr R (Term f (t1 :: l)) (Term f (t2 :: l)). Axiom one_step_context_in :   forall R t1 t2 f l l', one_step R t1 t2 ->    one_step R (Term f (l ++ t1 :: l')) (Term f (l ++ t2 :: l')). Axiom context_in :   forall R t1 t2, rwr R t1 t2 ->   forall f l l', rwr R (Term f (l ++ t1 :: l')) (Term f (l ++ t2 :: l')). Axiom general_context_aux :   forall R f l1 l2 l' l'', rwr_list R l1 l2 ->   rwr R (Term f (l' ++ l1 ++ l'')) (Term f (l' ++ l2 ++ l'')). Axiom general_context :   forall R f l1 l2, rwr_list R l1 l2 -> rwr R (Term f l1) (Term f l2). Axiom one_step_in_list :   forall R l l', one_step_list R l' l ->   exists t, exists t', exists l1, exists l2, one_step R t' t /\ l = l1 ++ t :: l2 /\ l' = l1 ++ t' :: l2. ```

### Compatibility with substitutions.

``` Axiom one_step_apply_subst :   forall R t1 t2 sigma , one_step R t1 t2 -> one_step R (apply_subst sigma t1) (apply_subst sigma t2). Axiom rwr_apply_subst :   forall R t1 t2 sigma, rwr R t1 t2 -> rwr R (apply_subst sigma t1) (apply_subst sigma t2). ```

### Inclusion of relations and associated equational theories.

``` Axiom rwr_inv :   forall A R (eq : A -> A -> Prop) (f : term -> A),   (forall a1 a2 a3, eq a1 a2 -> eq a2 a3 -> eq a1 a3) ->   (forall t1 t2, one_step R t1 t2 -> eq (f t1) (f t2)) ->   forall t1 t2, rwr R t1 t2 -> eq (f t1) (f t2). Axiom R1_included_in_R2_axiom :   forall (R1 R2 : term -> term -> Prop) ,   (forall t1 t2, R1 t1 t2 -> R2 t1 t2) ->   forall t1 t2, axiom R1 t1 t2 -> axiom R2 t1 t2. Axiom R1_included_in_R2_one_step :   forall (R1 R2 : term -> term -> Prop) ,   (forall t1 t2, R1 t1 t2 -> R2 t1 t2) ->   forall t1 t2, one_step R1 t1 t2 -> one_step R2 t1 t2. Axiom R1_included_in_R2_rwr :   forall (R1 R2 : term -> term -> Prop),   (forall t1 t2, R1 t1 t2 -> R2 t1 t2) ->   forall t1 t2, rwr R1 t1 t2 -> rwr R2 t1 t2. Axiom R1_included_in_R2_rwr_list :   forall (R1 R2 : term -> term -> Prop),   (forall t1 t2, R1 t1 t2 -> R2 t1 t2) ->   forall l1 l2, rwr_list R1 l1 l2 -> rwr_list R2 l1 l2. Axiom rwr_R1_included_in_R2 :   forall (R1 R2 : term -> term -> Prop),   (forall t1 t2, rwr R1 t1 t2 -> R2 t1 t2) ->   forall t1 t2, rwr R1 t1 t2 -> rwr R2 t1 t2. Axiom rwr_closure_one_step :   forall (R : term -> term -> Prop),   forall t1 t2, one_step (rwr R) t1 t2 -> rwr R t1 t2. Axiom rwr_closure :   forall t1 t2 (R : term -> term -> Prop),   rwr (rwr R) t1 t2 -> rwr R t1 t2. Axiom split_rel :   forall R1 R2 s t, one_step (union _ R1 R2) t s <->   (one_step R1 t s \/ one_step R2 t s). Axiom rwr_or_eq :   forall R ll, (forall s t, In (s,t) ll -> s = t \/ rwr R s t) ->             map (@fst term term) ll = map (@snd term term) ll \/             rwr_list R (map (@fst term term) ll) (map (@snd term term) ll). Axiom rwr_or_eq_subst :   forall R t sigma tau, (forall x, In x (var_list t) ->                                apply_subst sigma (Var x) = apply_subst tau (Var x) \/                                rwr R (apply_subst sigma (Var x)) (apply_subst tau (Var x))) ->             apply_subst sigma t = apply_subst tau t \/             rwr R (apply_subst sigma t) (apply_subst tau t). Axiom no_need_of_instance_is_modular :   forall (R1 R2 : term -> term -> Prop),   (forall t1 t2, axiom R1 t1 t2 -> R1 t1 t2) ->   (forall t1 t2, axiom R2 t1 t2 -> R2 t1 t2) ->   (forall t1 t2, axiom (union term R1 R2) t1 t2 -> (union term R1 R2) t1 t2). ```

### Rewriting at a defined position.

``` Axiom one_step_at_pos :  forall R p t sigma u v t', subterm_at_pos t p = Some (apply_subst sigma u) ->   one_step R u v -> t' = (replace_at_pos t (apply_subst sigma v) p) -> one_step R t t'. Axiom rwr_at_pos :  forall R p t sigma u v t', subterm_at_pos t p = Some (apply_subst sigma u) ->   rwr R u v -> t' = (replace_at_pos t (apply_subst sigma v) p) -> rwr R t t'. ```

### Accessibility of the rewriting relation.

``` Axiom acc_one_step : forall R t, Acc (one_step R) t <-> Acc (rwr R) t. Axiom acc_one_step_list :  forall R l, (forall t, In t l -> Acc (one_step R) t) <-> Acc (one_step_list R) l. Axiom acc_subterms :   forall R, (forall x t, ~ (R t (Var x))) ->   forall f l, (forall t, In t l -> Acc (one_step R) t) -> constructor R f ->   Acc (one_step R) (Term f l). Axiom acc_subterms_1 :    forall R t s, Acc (one_step R) t -> direct_subterm s t -> Acc (one_step R) s. Axiom acc_subterms_3 :    forall R p t s, Acc (one_step R) t -> subterm_at_pos t p = Some s ->    Acc (one_step R) s. Axiom acc_with_subterm_subterms :   forall R t, Acc (union _ (one_step R) direct_subterm) t ->                  forall s, direct_subterm s t ->                    Acc (union _ (one_step R) direct_subterm) s. Axiom acc_with_subterm :   forall R t, Acc (one_step R) t <-> Acc (union _ (one_step R) direct_subterm) t. Axiom var_acc :    forall R l x sigma, In x (var_list_list l) ->    (forall t, In t (map (apply_subst sigma) l) -> Acc (one_step R) t) ->    Acc (one_step R) (apply_subst sigma (Var x)). Axiom term_acc_subst :   forall R t sigma, Acc (one_step R) (apply_subst sigma t) -> Acc (one_step R) t. Axiom nf_one_step_subterm:   forall R t, nf (one_step R) t -> forall s, direct_subterm s t -> nf (one_step R) s. Axiom nf_rwr_subterm :   forall R t, nf (one_step R) t -> forall p s, subterm_at_pos t p = Some s -> nf (one_step R) s. Axiom compute_red : list (term * term) -> term -> list term. Axiom compute_red_is_correct :    forall rule_list : list (term * term),    (forall l r : term, In (l, r) rule_list -> forall v : variable, In v (var_list r) -> In v (var_list l)) ->    forall R : term -> term -> Prop,    (forall l r : term, R r l <-> In (l, r) rule_list) ->    forall t s : term, In s (compute_red rule_list t) <-> one_step R s t. Axiom FB_nf_dec :   forall R FB, (forall t s, one_step R s t <-> In s (FB t)) ->   forall t, {nf (one_step R) t}+{~ nf (one_step R) t}. Declare Module VT : decidable_set.S with Definition A := (variable * term)%type. Module D := dickson.Make (VT). Definition non_overlapping (R : relation term) :=   forall l1 r1 l2 r2 sigma tau, R r1 l1 -> R r2 l2 ->   forall f l p, subterm_at_pos l1 p = Some (Term f l) ->   apply_subst sigma (Term f l) = apply_subst tau l2 -> p = nil /\ l1 = l2 /\ r1 = r2. Definition overlay (R : relation term) :=   forall l1 r1 l2 r2 sigma tau, R r1 l1 -> R r2 l2 ->   forall f l p, subterm_at_pos l1 p = Some (Term f l) ->   apply_subst sigma (Term f l) = apply_subst tau l2 -> p = nil. Definition sym_refl R (t1 t2 : term) := R t1 t2 \/ R t2 t1 \/ t1 = t2. Definition th_eq R := rwr (sym_refl R). Notation " T '<-[' R '*]->' U " := (th_eq R T U) (at level 80) : term_scope . Axiom th_refl : forall R t, th_eq R t t. Axiom th_sym : forall R t1 t2, th_eq R t1 t2 -> th_eq R t2 t1. End EqTh. ```

## A functor building a Module EqTh from a term algebra.

``` Module Make (T1 : term.Term) <: EqTh with Module T:=T1. Module T := T1. Import T.  Inductive defined (R : relation term) : symbol -> Prop :=   | Def : forall f l t, R t (Term f l) -> defined R f. Inductive constructor (R : relation term) : symbol -> Prop :=   | Const : forall f, (forall l t, ~ (R t (Term f l))) -> constructor R f. Inductive module (R1 R2 : relation term) : Prop :=   | Mod : (forall f2 s t, defined R2 f2 ->                     R1 s t -> symb_in_term_list f2 (s :: t :: nil) = false) ->              module R1 R2. ```

### One step at top.

``` Inductive axiom (R : relation term) : term -> term -> Prop :=   | instance : forall t1 t2 sigma,        R t1 t2 -> axiom R (apply_subst sigma t1) (apply_subst sigma t2). ```

### One step at any position.

``` Inductive one_step (R : relation term) : term -> term -> Prop :=   | at_top : forall t1 t2, axiom R t1 t2 -> one_step R t1 t2   | in_context : forall f l1 l2,       one_step_list R l1 l2 -> one_step R (Term f l1) (Term f l2) with one_step_list (R : relation term) : list term -> list term -> Prop :=   | head_step : forall t1 t2 l,        one_step R t1 t2 -> one_step_list R (t1 :: l) (t2 :: l)  | tail_step : forall t l1 l2,      one_step_list R l1 l2 -> one_step_list R (t :: l1) (t :: l2). ```

### Rewriting Theory as transitive closure of an equational step.

``` Definition rwr (R : relation term) t1 t2 := trans_clos (one_step R) t1 t2. Notation " T '-[' R '+]->' U " := (rwr R T U) (at level 80) : term_scope . Hint Constructors axiom one_step one_step_list. Lemma one_step_list_length_eq :   forall R l1 l2, one_step_list R l1 l2 -> length l1 = length l2. Proof. intros R l1 l2 H; induction H as [t1 t2 l H' | t k1 k2 H']; subst. trivial. simpl; rewrite IHH'; trivial. Qed. Lemma R_axiom : forall (R : relation term) t1 t2, R t1 t2 -> axiom R t1 t2. Proof. intros R t1 t2 H. replace t1 with (apply_subst nil t1); [idtac | apply empty_subst_is_id]. replace t2 with (apply_subst nil t2); [idtac | apply empty_subst_is_id]. apply instance; trivial. Qed. Lemma R_one_step : forall (R : relation term) t1 t2, R t1 t2 -> one_step R t1 t2. Proof. intros R t1 t2 H; apply at_top; apply R_axiom; trivial. Qed. Lemma R_rwr :   forall t1 t2 (R : relation term), R t1 t2 -> rwr R t1 t2. Proof. intros t1 t2 R H; unfold rwr; apply t_step; apply R_one_step; trivial. Qed. ```

### Generalization over lists of terms.

``` Fixpoint rwr_list (R : relation term) (l1 l2 : list term) {struct l1} : Prop :=    match l1, l2 with    | nil, nil => False    | nil, _ :: _ => False    | _ :: _, nil => False    | h1::tl1, h2::tl2 => (rwr R h1 h2 /\ tl1 = tl2) \/                                       (h1 = h2 /\ rwr_list R tl1 tl2) \/                                       (rwr R h1 h2 /\ rwr_list R tl1 tl2)    end. Lemma rwr_list_length_eq :   forall R l1 l2, rwr_list R l1 l2 -> length l1 = length l2. Proof. intros R l1; induction l1 as [ | t1 l1]; intros [ | t2 l2] H; simpl in H; try contradiction; intuition. subst; simpl; trivial. simpl; rewrite (IHl1 l2); trivial. simpl; rewrite (IHl1 l2); trivial. Qed. Lemma one_step_list_rwr_list :     forall R l1 l2, one_step_list R l1 l2 -> rwr_list R l1 l2. Proof. intros R l1; induction l1 as [ | a1 l1]; intros l2 H; inversion H as [t1 t2 l H' | t k1 k2 H']; subst. left; split; trivial; unfold rwr; apply t_step; trivial. simpl; right; left; split; trivial; apply IHl1; trivial. Qed. Lemma rwr_list_is_trans :   forall R l1 l2 l3, rwr_list R l1 l2 -> rwr_list R l2 l3 -> rwr_list R l1 l3. Proof. intros R l1; induction l1 as [ | t1 l1]; intros [ | t2 l2] [ | t3 l3] H1 H2; trivial. contradiction. simpl in H1; destruct H1 as [[H1 H1'] | [[H1 H1'] | [H1 H1']]]; simpl in H2; destruct H2 as [[H2 H2'] | [[H2 H2'] | [H2 H2']]]; subst; simpl. left; split; trivial; unfold rwr; apply trans_clos_is_trans with t2; trivial. right; right; split; trivial. right; right; split; trivial; unfold rwr; apply trans_clos_is_trans with t2; trivial. right; right; split; trivial. right; left; split; trivial; apply IHl1 with l2; trivial. right; right; split; trivial; apply IHl1 with l2; trivial. right; right; split; trivial; unfold rwr; apply trans_clos_is_trans with t2; trivial. right; right; split; trivial; apply IHl1 with l2; trivial. right; right; split. unfold rwr; apply trans_clos_is_trans with t2; trivial. apply IHl1 with l2; trivial. Qed. Lemma rwr_list_trans_clos_one_step_list :   forall R l1 l2, rwr_list R l1 l2 <-> trans_clos (one_step_list R) l1 l2. Proof. intros R l1 l2; split; intro H. generalize l2 H; clear l2 H; induction l1 as [ | a1 l1]; intros l2 H. destruct l2; contradiction. destruct l2 as [ | a2 l2]. contradiction. simpl in H; destruct H as [[H H'] | [[H H'] | [H H']]]; subst. apply (@incl_trans2 term (list term) (fun a => a :: l2) (one_step R) (one_step_list R)); trivial. intros; apply head_step; trivial. apply (@incl_trans2 (list term) (list term) (fun l => a2 :: l) (one_step_list R) (one_step_list R)); trivial. intros; apply tail_step; trivial. apply IHl1; trivial. apply trans_clos_is_trans with (a2 :: l1). apply (@incl_trans2 term (list term) (fun a => a :: l1) (one_step R) (one_step_list R)); trivial. intros; apply head_step; trivial. apply (@incl_trans2 (list term) (list term) (fun l => a2 :: l) (one_step_list R) (one_step_list R)); trivial. intros; apply tail_step; trivial. apply IHl1; trivial. induction H. apply one_step_list_rwr_list; trivial. apply rwr_list_is_trans with y; trivial; apply one_step_list_rwr_list; trivial. Qed. ```

### Rewriting is a congruence.

``` Lemma context_cons :   forall R f t1 t2 l, rwr R t1 t2 -> rwr R (Term f (t1 :: l)) (Term f (t2 :: l)). Proof. unfold rwr; intros R f t1 t2 l H. induction H as [ t1 t2 H' | t1 t2 t3 H' H'']. apply t_step; apply in_context; left; trivial. apply t_trans with (Term f (t2 :: l)); trivial; apply in_context; left; trivial. Qed. Lemma one_step_context_in :   forall R t1 t2 f l l', one_step R t1 t2 ->    one_step R (Term f (l ++ t1 :: l')) (Term f (l ++ t2 :: l')). Proof. intros R t1 t2 f l l' H; apply in_context; induction l as [ | t l ]; simpl; [ apply head_step | apply tail_step ]; trivial. Qed. Lemma context_in :   forall R t1 t2, rwr R t1 t2 ->   forall f l l', rwr R (Term f (l ++ t1 :: l')) (Term f (l ++ t2 :: l')). Proof. unfold rwr; intros R t1 t2 H; induction H as [ t1 t2 H' | t1 t2 t3 H' H'']; subst. intros f l l'; apply t_step; apply one_step_context_in; trivial. intros f l l'; apply t_trans with (Term f (l ++ t2 :: l')); trivial. apply one_step_context_in; trivial. Qed. Lemma general_context_aux :   forall R f l1 l2 l' l'', rwr_list R l1 l2 ->   rwr R (Term f (l' ++ l1 ++ l'')) (Term f (l' ++ l2 ++ l'')). Proof. unfold rwr; intros R f l1; induction l1 as [ | t1 l1]; intros [ | t2 l2] l' l'' l1_R_l2; simpl in l1_R_l2; try contradiction. destruct l1_R_l2 as [[t1_R_t2 l1_eq_l2] | [[t1_eq_t2 l1_R_l2] | [t1_R_t2 l1_R_l2]]]. subst; do 2 rewrite <- app_comm_cons; apply context_in; trivial. assert (H:= IHl1 l2 (l' ++ t2 :: nil) l'' l1_R_l2). do 2 rewrite app_ass in H; simpl in H; subst; do 2 rewrite <- app_comm_cons; trivial. apply trans_clos_is_trans with (Term f (l' ++ (t2 :: l1) ++ l'')). do 2 rewrite <- app_comm_cons; apply context_in; trivial. assert (H:= IHl1 l2 (l' ++ t2 :: nil) l'' l1_R_l2). do 2 rewrite app_ass in H; simpl in H; subst; do 2 rewrite <- app_comm_cons; trivial. Qed. Lemma general_context :   forall R f l1 l2, rwr_list R l1 l2 -> rwr R (Term f l1) (Term f l2). Proof. unfold rwr; intros R f l1 l2 l1_R_l2; assert (H:= general_context_aux R f l1 l2 nil nil l1_R_l2); simpl in H; do 2 rewrite <- app_nil_end in H; exact H. Qed. Lemma one_step_in_list :   forall R l l', one_step_list R l' l ->   exists t, exists t', exists l1, exists l2, one_step R t' t /\ l = l1 ++ t :: l2 /\ l' = l1 ++ t' :: l2. Proof. intros R l l' H'; induction H'. exists t2; exists t1; exists (@nil term); exists l; repeat split; trivial. destruct IHH' as [u [u' [l3 [l4 [H1 [H2 H3]]]]]]; subst. exists u; exists u'; exists (t :: l3); exists l4; repeat split; trivial. Qed. ```

### Compatibility with substitutions.

``` Lemma one_step_apply_subst :   forall R t1 t2 sigma , one_step R t1 t2 -> one_step R (apply_subst sigma t1) (apply_subst sigma t2). Proof. intros R t; pattern t; apply term_rec3; clear t. intros x1 t2 sigma H; inversion_clear H as [ t1' t2' H'|]; inversion_clear H' as [ t1' t2' tau H'']; do 2 (rewrite <- subst_comp_is_subst_comp); auto. intros f1 l1 Hrec t2 sigma H; inversion_clear H as [ t1' t2' H'| f l1' l2 H'']. inversion_clear H' as [ t1' t2' tau H'']; do 2 (rewrite <- subst_comp_is_subst_comp); auto. simpl; apply in_context; generalize l2 H''; clear l2 H''; induction l1 as [ | a1 l1]. intros l2 H; inversion_clear H. intros l2' H; inversion_clear H as [ t1' a2 l H' | t' l1' l2 H']. simpl; apply head_step; apply Hrec; trivial; left; trivial. simpl; apply tail_step; apply IHl1; trivial; intros; apply Hrec; trivial; right; trivial. Qed. Lemma rwr_apply_subst :   forall R t1 t2 sigma, rwr R t1 t2 -> rwr R (apply_subst sigma t1) (apply_subst sigma t2). Proof. unfold rwr; intros R t1 t2 sigma H; induction H as [ | t1 t2 t3 H1 Hrec1 H2 Hrec2]. apply t_step; apply one_step_apply_subst; trivial. apply trans_clos_is_trans with (apply_subst sigma t2); trivial; apply t_step; apply one_step_apply_subst; trivial. Qed. ```

### Inclusion of relations and associated equational theories.

``` Lemma rwr_inv :   forall A R (eq : A -> A -> Prop) (f : term -> A),   (forall a1 a2 a3, eq a1 a2 -> eq a2 a3 -> eq a1 a3) ->   (forall t1 t2, one_step R t1 t2 -> eq (f t1) (f t2)) ->   forall t1 t2, rwr R t1 t2 -> eq (f t1) (f t2). Proof. unfold rwr; intros A R eq f eq_trans Step_inv t1 t2 H; induction H as [t1 t2 H' | t1 t2 t3 H' H'']; subst; auto. apply eq_trans with (f t2); auto. Qed. Lemma R1_included_in_R2_axiom :   forall (R1 R2 : term -> term -> Prop) ,   (forall t1 t2, R1 t1 t2 -> R2 t1 t2) ->   forall t1 t2, axiom R1 t1 t2 -> axiom R2 t1 t2. Proof. intros R1 R2 Incl t1 t2 H; inversion H; auto. Qed. Lemma R1_included_in_R2_one_step :   forall (R1 R2 : term -> term -> Prop) ,   (forall t1 t2, R1 t1 t2 -> R2 t1 t2) ->   forall t1 t2, one_step R1 t1 t2 -> one_step R2 t1 t2. Proof. intros R1 R2 Incl t1; pattern t1; apply term_rec3; clear t1. intros x1 t2 H; inversion H; apply at_top; apply R1_included_in_R2_axiom with R1; trivial. intros f1 l1 Hrec t2 H; inversion_clear H as [| f l1' l2 H']. apply at_top; apply R1_included_in_R2_axiom with R1; trivial. apply in_context; generalize l2 H'; clear l2 H'; induction l1 as [ | a1 l1 ]; intros l2 H; inversion_clear H. apply head_step; apply Hrec; trivial; left; trivial. apply tail_step; apply IHl1; trivial; intros; apply Hrec; trivial; right; trivial. Qed. Lemma R1_included_in_R2_rwr :   forall (R1 R2 : term -> term -> Prop),   (forall t1 t2, R1 t1 t2 -> R2 t1 t2) ->   forall t1 t2, rwr R1 t1 t2 -> rwr R2 t1 t2. Proof. unfold rwr; intros R1 R2 Incl t1 t2 H; induction H as [t1 t2 H' | t1 t2 t3 H' H'']. apply t_step; apply R1_included_in_R2_one_step with R1; trivial. apply t_trans with t2; auto. apply R1_included_in_R2_one_step with R1; trivial. Qed. Lemma R1_included_in_R2_rwr_list :   forall (R1 R2 : term -> term -> Prop),   (forall t1 t2, R1 t1 t2 -> R2 t1 t2) ->   forall l1 l2, rwr_list R1 l1 l2 -> rwr_list R2 l1 l2. Proof. intros R1 R2 Incl l1; induction l1 as [ | t1 l1]; intros [ | t2 l2] H. inversion H. inversion H. inversion H. simpl in H; destruct H as [[Hh H'] | [[H' Ht] | [Hh Ht]]]; subst. left; split; trivial. apply R1_included_in_R2_rwr with R1; trivial. right; left; split; trivial; apply IHl1; trivial. right; right; split. apply R1_included_in_R2_rwr with R1; trivial. apply IHl1; trivial. Qed. Lemma rwr_R1_included_in_R2 :   forall (R1 R2 : term -> term -> Prop),   (forall t1 t2, rwr R1 t1 t2 -> R2 t1 t2) ->   forall t1 t2, rwr R1 t1 t2 -> rwr R2 t1 t2. Proof. unfold rwr; intros R1 R2 Incl t1 t2 H; apply R1_included_in_R2_rwr with (rwr R1); auto. unfold rwr; apply t_step; apply at_top; generalize (instance (rwr R1) t1 t2 nil H); do 2 rewrite empty_subst_is_id; trivial. Qed. Lemma rwr_closure_one_step :   forall (R : term -> term -> Prop),   forall t1 t2, one_step (rwr R) t1 t2 -> rwr R t1 t2. Proof. intros R t1; pattern t1; apply term_rec3; clear t1. intros x1 t2 H; inversion_clear H as [ t1' t2' H' | ]; inversion_clear H'; apply rwr_apply_subst; trivial. intros f1 l1 Hrec t2 H; inversion_clear H as [ t1' t2' H' | f' l1' l2 H']. inversion_clear H'; apply rwr_apply_subst; trivial. apply general_context; generalize l2 H'; clear l2 H'. induction l1 as [ | a1 l1 ]; intros l2 H; inversion H as [ H1 a2 H3 a1_R_a2 H5 H6 | H1 H2 l2' l1_R_l2' H5 H6]; subst. left; split; [ apply Hrec; [left | idtac] | idtac]; trivial. right; left; split; [idtac | apply IHl1; [ intros; apply Hrec | idtac]]; trivial. right; trivial. Qed. Lemma rwr_closure :   forall t1 t2 (R : term -> term -> Prop),   rwr (rwr R) t1 t2 -> rwr R t1 t2. Proof. unfold rwr; intros t1 t2 R H. induction H as [t1 t2 H' | t1 t2 t3 H' H'']. apply rwr_closure_one_step; trivial. apply trans_clos_is_trans with t2; auto. apply rwr_closure_one_step; trivial. Qed. Lemma rwr_or_eq :   forall R ll, (forall s t, In (s,t) ll -> s = t \/ rwr R s t) ->             map (@fst term term) ll = map (@snd term term) ll \/             rwr_list R (map (@fst term term) ll) (map (@snd term term) ll). Proof. intros R ll; induction ll as [ | [s t] ll]; intro H. left; trivial. destruct (H s t (or_introl _ (refl_equal _))) as [H1 | H1]. simpl; subst s; destruct IHll as [H2 | H2]. intros; apply H; right; trivial. left; rewrite H2; trivial. do 2 right; left; split; trivial. simpl; destruct IHll as [H2 | H2]. intros; apply H; right; trivial. right; left; split; trivial. do 3 right; split; trivial. Qed. Lemma rwr_or_eq_subst :   forall R t sigma tau, (forall x, In x (var_list t) ->                                apply_subst sigma (Var x) = apply_subst tau (Var x) \/                                rwr R (apply_subst sigma (Var x)) (apply_subst tau (Var x))) ->             apply_subst sigma t = apply_subst tau t \/             rwr R (apply_subst sigma t) (apply_subst tau t). Proof. intros R t; pattern t; apply term_rec3; clear t. intros v sigma tau H; apply H; left; trivial. intros f l IH sigma tau H; simpl. assert (H' : map (apply_subst sigma) l = map (apply_subst tau) l \/             rwr_list R (map (apply_subst sigma) l) (map (apply_subst tau) l)). rewrite var_list_unfold in H. induction l as [ | t l]. left; trivial. simpl; destruct (IH t (or_introl _ (refl_equal _)) sigma tau) as [H1 | H1]. intros x x_in_t; apply H; simpl; apply in_or_app; left; trivial. destruct IHl as [H2 | H2]. intros s s_in_t sigma' tau' H'; apply IH; trivial; right; trivial. intros x x_in_l; apply H; simpl; apply in_or_app; right; trivial. left; rewrite H1; rewrite H2; trivial. do 2 right; left; split; trivial. destruct IHl as [H2 | H2]. intros s s_in_t sigma' tau' H'; apply IH; trivial; right; trivial. intros x x_in_l; apply H; simpl; apply in_or_app; right; trivial. right; left; rewrite H2; split; trivial. do 3 right; split; trivial. destruct H' as [H' | H']. left; rewrite H'; trivial. right; apply general_context; trivial. Qed. Lemma split_rel :   forall R1 R2 s t, one_step (union _ R1 R2) t s <->   (one_step R1 t s \/ one_step R2 t s). Proof. intros R1 R2 s; pattern s; apply term_rec2; clear s. intro n; induction n as [ | n]; intros s Size_s. absurd (1 <= 0); auto with arith; apply le_trans with (size s); trivial; apply size_ge_one. intros t; split; intro H. inversion H as [s' t' H' | f' lt ls H']; subst. inversion H' as [t' s' sigma H'']; subst. destruct H'' as [K1 | K2]. left; apply at_top; apply instance; trivial. right; apply at_top; apply instance; trivial. assert (Size_ls : forall s, In s ls -> size s <= n). intros s s_in_ls; apply le_S_n. apply le_trans with (size (Term f' ls)); trivial. apply size_direct_subterm; trivial. clear H Size_s; assert (H'' : one_step_list R1 lt ls \/                   one_step_list R2 lt ls). induction H' as [t' s' l H'' | s lt' ls' H'']; subst. rewrite (IHn s' (Size_ls s' (or_introl _ (refl_equal _))) t') in H''. destruct H'' as [H1 | H2]. left; apply head_step; trivial. right; apply head_step; trivial. destruct IHH'' as [H1 | H2]. intros; apply Size_ls; right; trivial. left; apply tail_step; trivial. right; apply tail_step; trivial. destruct H'' as [H1 | H2]; [left | right]; apply in_context; trivial. destruct H as [H1 | H2]. apply R1_included_in_R2_one_step with R1; trivial. intros; left; trivial. apply R1_included_in_R2_one_step with R2; trivial. intros; right; trivial. Qed. Lemma no_need_of_instance_is_modular :   forall (R1 R2 : term -> term -> Prop),   (forall t1 t2, axiom R1 t1 t2 -> R1 t1 t2) ->   (forall t1 t2, axiom R2 t1 t2 -> R2 t1 t2) ->   (forall t1 t2, axiom (union term R1 R2) t1 t2 -> (union term R1 R2) t1 t2). Proof. intros R1 R2 H1 H2 t1 t2 H; inversion H as [t1' t2' sigma H']; subst; inversion H'; [left; apply H1 | right; apply H2]; apply instance; trivial. Qed. ```

### Rewriting at a defined position.

``` Lemma one_step_at_pos :  forall R p t sigma u v t', subterm_at_pos t p = Some (apply_subst sigma u) ->   one_step R u v -> t' = (replace_at_pos t (apply_subst sigma v) p) -> one_step R t t'. Proof. intros R p; induction p as [ | i p]; intros t sigma u v t' Sbt H H'; simpl in Sbt. injection Sbt; intros; subst; simpl. apply one_step_apply_subst; trivial. destruct t as [x | f l]. discriminate. subst t'; simpl; apply in_context. generalize l Sbt; clear l Sbt; induction i as [ | i]; intros [ | s l] Sbt; simpl. discriminate. simpl in Sbt. left; apply (IHp s sigma u v); trivial. discriminate. right; simpl in Sbt; apply (IHi _ Sbt). Qed. Lemma rwr_at_pos :  forall R p t sigma u v t', subterm_at_pos t p = Some (apply_subst sigma u) ->   rwr R u v -> t' = (replace_at_pos t (apply_subst sigma v) p) -> rwr R t t'. Proof. intros R p; induction p as [ | i p]; intros t sigma u v t' Sbt H H'; simpl in Sbt. injection Sbt; clear Sbt; intros; subst; simpl; trivial. apply rwr_apply_subst; trivial. destruct t as [x | f l]. discriminate. subst t'; rewrite replace_at_pos_unfold; apply general_context. assert (H' := nth_error_ok_in i l). destruct (nth_error l i) as [ti | ]. destruct (H' _ (refl_equal _)) as [l1 [l2 [L H'']]]. subst l i; rewrite replace_at_pos_list_replace_at_pos_in_subterm; trivial. clear H'; induction l1 as [ | a1 l1]; simpl. left; split; trivial; apply IHp with sigma u v; trivial. right; left; split; trivial. discriminate. Qed. ```

### Accessibility of the rewriting relation.

``` Lemma acc_one_step :   forall R t, Acc (one_step R) t <-> Acc (rwr R) t. Proof. unfold rwr; intros R t; split; intro H. apply Acc_incl with (trans_clos (one_step R)). intros t1 t2; simpl; trivial. apply acc_trans; trivial. induction H as [t H IH]. apply Acc_intro; intros; apply IH; apply t_step; trivial. Qed. Lemma acc_one_step_list :  forall R l, (forall t, In t l -> Acc (one_step R) t) <-> Acc (one_step_list R) l. Proof. assert (H : forall R t, Acc (one_step R) t ->                       (forall l, Acc (one_step_list R) l -> Acc (one_step_list R) (t :: l))). intros R t Acc_t; pattern t; refine (@Acc_ind _ (one_step R) _ _ t Acc_t). clear t Acc_t; intros t Acc_t IHt l Acc_l. pattern l; refine (@Acc_ind _ (one_step_list R) _ _ l Acc_l). clear l Acc_l; intros l Acc_l IHl. apply Acc_intro; intros [ | t' l'] H. inversion H. inversion H as [u' u l'' | u k k'' ]; subst. apply IHt; trivial; apply Acc_intro; assumption. apply IHl; trivial. intros R l; split. induction l as [ | t l]. intros _; apply Acc_intro; intros [ | t' l'] H'; inversion H'. intros H'; apply H. apply H'; left; trivial. apply IHl; intros; apply H'; right; trivial. intros Acc_l; induction Acc_l as [l Acc_l IH]. intros t t_in_l; apply Acc_intro; intros s H'; destruct (In_split _ _ t_in_l) as [l' [l'' H'']]; subst l; apply (IH (l' ++ s :: l'')). clear Acc_l IH t_in_l; induction l' as [ | s' l']. simpl; apply head_step; trivial. simpl; apply tail_step; trivial. apply in_or_app; right; left; trivial. Qed. Lemma acc_subterms :   forall R, (forall x t, ~ (R t (Var x))) ->   forall f l, (forall t, In t l -> Acc (one_step R) t) -> constructor R f ->   Acc (one_step R) (Term f l). Proof. intros R HR f l Acc_l Cf'; inversion Cf' as [f' Cf]; clear Cf'; subst f'; rewrite acc_one_step_list in Acc_l. pattern l; refine (@Acc_ind _ (one_step_list R) _ _ l Acc_l). clear l Acc_l; intros l Acc_l IH. apply Acc_intro. intros t H; inversion H as [t1 t2 H' | f' l1 l2 H']; subst. inversion H' as [t1 t2 sigma H'' H3 H''']; subst; destruct t2 as [x2 | f2 l2]. absurd (R t1 (Var x2)); trivial; apply HR. simpl in H'''; injection H'''; clear H'''; intros; subst; absurd (R t1 (Term f l2)); trivial; apply Cf. apply IH. generalize l1 l H'. intro k; induction k as [ | s k]; intros k' K; inversion K; subst. apply head_step; trivial. apply tail_step; trivial. Qed. Lemma acc_subterms_1 :    forall R t s, Acc (one_step R) t -> direct_subterm s t -> Acc (one_step R) s. Proof. intros R t s Acc_t; generalize s; clear s; pattern t; refine (@Acc_ind _ (one_step R) _ _ t Acc_t). clear t Acc_t; intros t Acc_t IH s H; destruct t as [ x | f l]; simpl in H. contradiction. apply Acc_intro; intros u H'; destruct (In_split _ _ H) as [l1 [l2 H'']]; subst l; apply (IH (Term f (l1 ++ u :: l2))). apply one_step_context_in; trivial. simpl; apply in_or_app; right; left; trivial. Qed. Lemma acc_subterms_3 :    forall R p t s, Acc (one_step R) t -> subterm_at_pos t p = Some s ->    Acc (one_step R) s. Proof. intros R p; induction p as [ | i p]; intros t s Acc_t H; simpl in H. injection H; intro; subst; trivial. destruct t as [ x | f l]. discriminate. assert (H' := nth_error_ok_in i l); destruct (nth_error l i) as [ s' | ]. generalize (H' _ (refl_equal _)); clear H'; intro s'_in_l. apply (IHp s'); trivial; apply (acc_subterms_1 R (Term f l)); trivial. destruct s'_in_l as [l1 [l2 [_ H']]]; subst l; simpl; apply in_or_app; right; left; trivial. discriminate. Qed. Lemma acc_with_subterm_subterms :   forall R t, Acc (union _ (one_step R) direct_subterm) t ->                  forall s, direct_subterm s t ->                    Acc (union _ (one_step R) direct_subterm) s. Proof. intros R t Acc_t; induction Acc_t as [t Acc_t IH]. intros s H; apply Acc_t; right; trivial. Qed. Lemma acc_with_subterm :   forall R t, Acc (one_step R) t <-> Acc (union _ (one_step R) direct_subterm) t. Proof. intros R t; split. intro Acc_t; induction Acc_t as [t Acc_t IH]. generalize Acc_t IH; clear Acc_t IH; pattern t; apply term_rec2; clear t. intro n; induction n as [ | n]; intros t size_t Acc_t IH. absurd (1 <= 0); auto with arith; apply le_trans with (size t); trivial; apply size_ge_one. apply Acc_intro. intros u H; destruct H as [H | H]. apply IH; trivial. apply IHn. apply le_S_n; apply le_trans with (size t); trivial. apply size_direct_subterm; trivial. assert (H' : Acc (one_step R) u). apply acc_subterms_1 with t; trivial. apply Acc_intro; apply Acc_t. inversion H'; trivial. intros v v_R_u. destruct t as [ x | f l]. contradiction. destruct (In_split _ _ H) as [l' [l'' H'']]; clear H; subst l. apply (acc_with_subterm_subterms R (Term f (l' ++ v :: l''))). apply IH; apply one_step_context_in; trivial. simpl; apply in_or_app; right; left; trivial. apply Acc_incl; intros t1 t2 H; left; trivial. Qed. Lemma var_acc :    forall R l x sigma, In x (var_list_list l) ->    (forall t, In t (map (apply_subst sigma) l) -> Acc (one_step R) t) ->    Acc (one_step R) (apply_subst sigma (Var x)). Proof. intros R l; pattern l; apply (list_rec3 size); clear l; intro n; induction n as [ | n]; intros [ | t l] Sl x sigma H Acc_l. simpl in H; contradiction. simpl in Sl; absurd (1 <= 0); auto with arith. apply le_trans with (size t). apply size_ge_one. refine (le_trans _ _ _ _ Sl); auto with arith. simpl in H; contradiction. assert (Sl' : list_size size l <= n). apply le_S_n; refine (le_trans _ _ _ _ Sl); simpl; apply (plus_le_compat_r 1 (size t) (list_size size l)); apply size_ge_one. destruct t as [y | g k]. simpl in H; destruct H as [y_eq_x | x_in_l]. subst y; apply Acc_l; simpl map; left; trivial. apply (IHn l); trivial; intros; apply Acc_l; simpl map; right; trivial. assert (Sk : list_size size k <= n). apply le_S_n; refine (le_trans _ _ _ _ Sl); simpl; rewrite (list_size_fold size k); apply le_n_S; apply le_plus_l. assert (Acc_k : forall t, In t (map (apply_subst sigma) k) -> Acc (one_step R) t). intros t H'; apply acc_subterms_1 with (Term g (map (apply_subst sigma) k)). apply Acc_l; simpl map; left; trivial. trivial. replace (var_list_list (Term g k :: l)) with (var_list (Term g k) ++ var_list_list l) in H; trivial. rewrite var_list_unfold in H. generalize (IHn _ Sk x sigma). destruct (in_app_or _ _ _ H) as [x_in_k | x_in_l]. clear H; intro H; generalize (H x_in_k); clear H; intro H; apply H. intros t H'; apply Acc_k; trivial. simpl in H; intros _; apply (IHn l); trivial. intros t H'; apply Acc_l; right; trivial. Qed. Fixpoint compute_head_red s rule_list {struct rule_list} : list term :=   match rule_list with   | nil => nil   | (l,r) :: rule_list =>            match matching ((l,s) :: nil) with            | Some sigma => (apply_subst sigma r) :: compute_head_red s rule_list            | None => compute_head_red s rule_list            end   end. Lemma compute_head_red_is_correct :   forall rule_list, (forall l r, In (l,r) rule_list -> forall v, In v (var_list r) -> In v (var_list l)) ->   forall R, (forall l r, R r l <-> In (l,r) rule_list) ->   forall t s, (In s (compute_head_red t rule_list) <-> axiom R s t). Proof. intros rule_list; induction rule_list as [ | [l r] rule_list]; intros Reg R Equiv t s; split; intro H. contradiction. inversion H; subst. rewrite Equiv in H0; contradiction. simpl in H. case_eq (matching ((l,t) :: nil)). intros sigma mlt_eq_sigma. destruct (matching_correct mlt_eq_sigma) as [C1 [C2 C3]]. assert (H' := C3 _ _ (or_introl _ (refl_equal _))). rewrite mlt_eq_sigma in H. destruct H as [H | H]. subst; apply instance. rewrite Equiv; left; trivial. set (R' := fun r l => In (l,r) rule_list). apply R1_included_in_R2_axiom with R'; trivial. intros l1 r1; unfold R'; rewrite Equiv; intro; right; trivial. rewrite <- IHrule_list; trivial. intros l1 r1 l1r1_in_rule_list; apply Reg; right; trivial. intros l1 r1; unfold R'; intuition. intro mlt_eq_none; rewrite mlt_eq_none in H. set (R' := fun r l => In (l,r) rule_list). apply R1_included_in_R2_axiom with R'; trivial. intros l1 r1; unfold R'; rewrite Equiv; intro; right; trivial. rewrite <- IHrule_list; trivial. intros l1 r1 l1r1_in_rule_list; apply Reg; right; trivial. intros l1 r1; unfold R'; intuition. inversion H; subst. rewrite Equiv in H0. destruct H0 as [H0 | H0]. injection H0; clear H0; intros; subst t1 t2. simpl. assert (C := @matching_correct ((l, apply_subst sigma l) :: nil)). assert (C' := matching_complete ((l, apply_subst sigma l) :: nil) sigma). destruct (matching ((l, apply_subst sigma l) :: nil)) as [tau | ]. generalize (C _ (refl_equal _)); clear C; intros [C1 [C2 C3]]. left. assert (H' : forall v, In v (var_list r) -> apply_subst tau (Var v) = apply_subst sigma (Var v)). intros v v_in_r; assert (v_in_l : In v (var_list l)). apply Reg with r; trivial; left; trivial. apply C' with l (apply_subst sigma l); trivial. intros p s [ps_eq_llsigma | ps_in_nil]; [idtac | contradiction]. injection ps_eq_llsigma; intros; subst; trivial. left; trivial. generalize r H'; clear H'; intro t; pattern t; apply term_rec3; clear t. intros v IH; apply IH; left; trivial. intros f k IHl IH. simpl; apply (f_equal (fun ll => Term f ll)). apply map_eq; intros a a_in_k; apply IHl; trivial. destruct (In_split _ _ a_in_k) as [k1 [k2 K]]; subst. intros v v_in_a; apply IH. apply (@var_in_subterm v a (Term f (k1 ++ a :: k2)) (length k1 :: nil)); trivial. simpl; rewrite nth_error_at_pos; trivial. assert False. apply C'. intros p s [ps_eq_llsigma | ps_in_nil]; [idtac | contradiction]. injection ps_eq_llsigma; intros; subst; trivial. contradiction. simpl. assert (H' : forall l r : term,                In (l, r) rule_list ->                forall v : variable, In v (var_list r) -> In v (var_list l)). intros l1 r1 lr_in_rule_list; apply Reg; right; trivial. destruct (matching ((l, apply_subst sigma t2) :: nil)) as [tau | ]; [right | idtac]. set (R' := fun r l => In (l,r) rule_list). rewrite (IHrule_list H' R'); trivial. intros l1 r1; unfold R'; split; trivial. apply instance; unfold R'; trivial. set (R' := fun r l => In (l,r) rule_list). rewrite (IHrule_list H' R'); trivial. intros l1 r1; unfold R'; split; trivial. apply instance; unfold R'; trivial. Qed. Definition o_size t1 t2 := size t1 < size t2. Lemma wf_size : well_founded o_size. Proof. unfold well_founded, o_size. intros t; apply Acc_intro. generalize (size t); clear t. intro n; induction n as [ | n]. intros y Abs; absurd (size y < 0); auto with arith. intros y Sy; inversion Sy; subst. apply Acc_intro; intros x Sx; apply IHn; trivial. apply IHn; trivial. Defined. Lemma term_acc_subst :   forall R t sigma, Acc (one_step R) (apply_subst sigma t) -> Acc (one_step R) t. Proof. assert (H : forall R s, Acc (one_step R) s ->                  forall t sigma, s = (apply_subst sigma t) -> Acc (one_step R) t). intros R s Acc_s; induction Acc_s as [s Acc_s IH']; intros t sigma H. subst s. assert (IH : forall u tau, one_step R (apply_subst tau u) (apply_subst sigma t) ->                 Acc (one_step R) u). intros u tau H; apply (IH' _ H u tau); trivial. clear IH'. apply Acc_intro. intros u u_R_t; apply IH with sigma. apply one_step_apply_subst; trivial. intros R t sigma H'; apply H with (apply_subst sigma t) sigma; trivial. Qed. Lemma nf_one_step_subterm:   forall R t, nf (one_step R) t -> forall s, direct_subterm s t -> nf (one_step R) s. Proof. intros R t; pattern t; apply term_rec3; clear t. intros v _ s H; contradiction. simpl; intros f l IH Hnf s s_in_l u H. destruct (In_split _ _ s_in_l) as [l' [l'' H']]; subst. apply (Hnf (Term f (l' ++ u :: l''))). apply in_context; clear IH Hnf s_in_l; induction l' as [ | s' l']; simpl. apply head_step; trivial. apply tail_step; apply IHl'. Qed. Lemma nf_rwr_subterm :   forall R t, nf (one_step R) t -> forall p s, subterm_at_pos t p = Some s -> nf (one_step R) s. Proof. intros R t nf_t p; generalize t nf_t; clear t nf_t; induction p as [ | i p]; intros t nf_t s Sub. injection Sub; clear Sub; intros; subst; trivial. simpl in Sub; destruct t as [v | f l]. discriminate. generalize (nth_error_ok_in i l); destruct (nth_error l i) as [ti | ]. intro H; destruct (H _ (refl_equal _)) as [l1 [l2 [L H']]]; clear H; subst. apply (IHp ti); trivial. apply nf_one_step_subterm with (Term f (l1 ++ ti :: l2)); trivial. simpl; apply in_or_app; right; left; trivial. discriminate. Qed. Section Compute_Red. Variable rule_list : list (term * term). ```

### Definition of a step of compute_red.

``` Definition F_compute_red:    forall t (crec : forall s, o_size s t -> list term), list term. Proof. intros t crec; destruct t as [v | f l]. exact (compute_head_red (Var v) rule_list). assert (crec_l : forall t (t_in_l : In t l), list term). intros t t_in_l; exact (crec t (size_direct_subterm t (Term f l) t_in_l)). exact ((compute_head_red (Term f l) rule_list) ++            (map (fun k => Term f k) (mapii_dep (Dep_fun l crec_l)))). Defined. ```

### Definition of compute_red.

``` Definition compute_red : term -> list term := Fix wf_size (fun t => list term) F_compute_red. ```

### A more practical equivalent definition of compute_red.

``` Lemma compute_red_unfold :   forall t : term, compute_red t = @F_compute_red t (fun y _ => compute_red y). Proof. intros t; unfold compute_red. refine (Fix_eq _ _ _ _ t). clear t; intros t F G H. unfold F_compute_red; destruct t as [ v | f l ]; simpl; auto. apply (f_equal (fun kk => compute_head_red (Term f l) rule_list ++                                           (map (fun k => Term f k) kk))). apply mapii_dep_eq. intros t t_in_l; apply H. Qed. Lemma compute_red_is_correct :   (forall l r, In (l,r) rule_list -> forall v, In v (var_list r) -> In v (var_list l)) ->   forall R, (forall l r, R r l <-> In (l,r) rule_list) ->   forall t s, (In s (compute_red t) <-> one_step R s t). Proof. intros Reg R Equiv t; pattern t; apply term_rec3; clear t. intros v s; split; intro H. rewrite compute_red_unfold in H; simpl in H. apply at_top; rewrite <- (compute_head_red_is_correct rule_list Reg R Equiv); trivial. inversion H; subst. rewrite compute_red_unfold; simpl. rewrite (compute_head_red_is_correct rule_list Reg R Equiv); trivial. intros f l IHl; split; intro H. rewrite compute_red_unfold in H; simpl in H. destruct (in_app_or _ _ _ H) as [H1 | H2]; clear H. apply at_top; rewrite <- (compute_head_red_is_correct rule_list Reg R Equiv); trivial. rewrite in_map_iff in H2. destruct H2 as [k [H2 H3]]. subst s; apply in_context. generalize IHl k H3; clear IHl k H3; induction l as [ | a l]; intros IHll k H3; rewrite mapii_dep_unfold in H3; simpl in H3; trivial. contradiction. destruct (in_app_or _ _ _ H3) as [H4 | H5]; clear H3. rewrite in_map_iff in H4. destruct H4 as [b [H4 H5]]; subst. apply head_step. rewrite <- (IHll a); trivial. left; trivial. rewrite in_map_iff in H5. destruct H5 as [l' [H5 H6]]; subst. apply tail_step. apply IHl; trivial. intros t t_in_l; apply IHll; right; trivial. inversion H; clear H; subst. rewrite compute_red_unfold; simpl. apply in_or_app; left; rewrite (compute_head_red_is_correct rule_list Reg R Equiv); trivial. rewrite compute_red_unfold; simpl. apply in_or_app; right. rewrite in_map_iff; exists l1; split; trivial. generalize IHl; clear IHl; induction H2; intros IHl. rewrite mapii_dep_unfold; simpl. apply in_or_app; left. rewrite in_map_iff; exists t1; split; trivial. rewrite (IHl _ (or_introl _ (refl_equal _)) t1); trivial. rewrite mapii_dep_unfold; simpl. apply in_or_app; right. rewrite in_map_iff. exists l1; split; trivial. apply IHone_step_list; trivial. intros u u_in_l2; apply IHl; right; trivial. Qed. End Compute_Red. Lemma FB_nf_dec :   forall R FB, (forall t s, one_step R s t <-> In s (FB t)) ->   forall t, {nf (one_step R) t}+{~ nf (one_step R) t}. Proof. intros R FB red_dec t. case_eq (FB t). intro FBt ; left; unfold nf; intros s; rewrite (red_dec t s); rewrite FBt; contradiction. intros s l FBt; right; unfold nf; intro nf_t. apply (nf_t s); rewrite (red_dec t s); rewrite FBt; left; trivial. Defined. Module VT : decidable_set.S with Definition A := (variable * term)%type. Definition A := (variable * term)%type. Definition eq_A := (@eq A). Lemma eq_dec : forall a1 a2 : A, {eq_A a1 a2} + {~eq_A a1 a2}. Proof. unfold eq_A; intros [v1 t1] [v2 t2]. destruct (eq_variable_dec v1 v2) as [v1_eq_v2 | v1_diff_v2]. destruct (eq_term_dec t1 t2) as [t1_eq_t2 | t1_diff_t2]. left; subst; apply refl_equal. right; intro H; apply t1_diff_t2; injection H; intros; subst; trivial. right; intro H; apply v1_diff_v2; injection H; intros; subst; trivial. Defined. Lemma eq_proof : equivalence A eq_A. Proof. unfold eq_A; constructor. constructor. intros t1 t2 t3 H1 H2; subst; trivial. intros t1 t2 H1; subst; trivial. Qed. End VT. Module D := dickson.Make (VT). Definition rwr_subst R sigma' sigma :=    trans_clos (D.multiset_extension_step (fun yval' xval => rwr R (snd yval') (snd xval))) sigma' sigma. Lemma acc_rwr_subst :   forall R sigma, (forall x val, In (x,val) sigma -> Acc (one_step R) val) <-> Acc (rwr_subst R) sigma. Proof. intros R sigma; split. intro Acc_sigma; unfold rwr_subst. apply Acc_incl with (trans_clos (D.multiset_extension_step (fun yval' xval => rwr R (snd yval') (snd xval)))). intros t1 t2; trivial. apply acc_trans; apply D.dickson_strong. intros [x val] H. apply Acc_incl with (trans_clos (fun (yval' : variable * term) xval => one_step R (snd yval') (snd xval))). intros [x1 t1] [x2 t2]; unfold rwr; simpl; intro H'; induction H'. apply t_step; trivial. apply t_trans with (x1,y); trivial. apply acc_trans. assert (Acc_val := Acc_sigma _ _ H). generalize x; clear x Acc_sigma H; induction Acc_val as [val Acc_val IH]. intro x; apply Acc_intro; intros [y val'] H'; apply IH; trivial. intros Acc_sigma; induction Acc_sigma as [sigma Acc_sigma IH]. intros y val yval_in_sigma; apply Acc_intro; intros val' H. destruct (In_split _ _ yval_in_sigma) as [sigma1 [sigma2 H']]; subst. apply (IH (sigma1 ++ (y,val') :: sigma2)) with y. unfold rwr_subst; apply t_step. refine (@D.rmv_case _ (sigma1 ++ (y, val') :: sigma2) (sigma1 ++ (y, val) :: sigma2)                       (sigma1 ++ sigma2) ((y,val') :: nil) (y,val) _ _ _). unfold D.LP.mem, D.LP.EDS.eq_A, rwr. intros b [H' | H']; [subst; simpl; apply t_step; trivial | contradiction]. simpl; apply D.LP.permut_sym; rewrite <- D.LP.permut_cons_inside; auto. unfold D.LP.EDS.eq_A; trivial. simpl; apply D.LP.permut_sym; rewrite <- D.LP.permut_cons_inside; auto. unfold D.LP.EDS.eq_A, D.LP.EDS.eq_A; trivial. apply in_or_app; right; left; trivial. Qed. Lemma acc_nf_subst :    forall R FB, (forall t s, In s (FB t) <-> one_step R s t) ->    forall sigma, (forall x val, find eq_variable_dec x sigma = Some val -> Acc (one_step R) val) ->    {sigma' : substitution | (forall x val', In (x,val') sigma' <-> find eq_variable_dec x sigma' = Some val') /\                                        (forall x val, find eq_variable_dec x sigma = Some val ->                                                exists val', (In (x,val') sigma' /\ nf (one_step R) val' /\                                                 (val' = val \/ trans_clos (one_step R) val' val))) /\                                          (forall x val', In (x,val') sigma' -> nf (one_step R) val') /\                                          (forall x val', In (x,val') sigma' -> find eq_variable_dec x sigma <> None)}. Proof. intros R FB red_dec sigma Acc_sigma. destruct (remove_garbage_subst sigma) as [tau [H1 [H H']]]. assert (H'' : {sigma' : substitution |                                        (forall x val', In (x,val') sigma' <-> find eq_variable_dec x sigma' = Some val') /\                                        (forall x val, find eq_variable_dec x tau = Some val ->                                                exists val', (In (x,val') sigma' /\ nf (one_step R) val' /\                                                 (val' = val \/ trans_clos (one_step R) val' val))) /\                                          (forall x val', In (x,val') sigma' -> nf (one_step R) val') /\                                          (forall x val', In (x,val') sigma' -> find eq_variable_dec x tau <> None)}). assert (Acc_tau : forall (x : variable) (val : term), In (x,val) tau -> Acc (one_step R) val). intros x val H''; apply (Acc_sigma x val); rewrite H1; apply H; trivial. clear sigma Acc_sigma H1; induction tau as [ | [x val] tau]. exists (nil : substitution); repeat split; simpl. contradiction. discriminate. intros; discriminate. contradiction. contradiction. destruct IHtau as [sigma' [H1 [H2 [H3 K3]]]]. intros y valy H4; destruct (In_split _ _ H4) as [tau1 [tau2 H5]]; subst tau. rewrite <- (H y valy). simpl; destruct (eq_variable_dec y x) as [y_eq_x | y_diff_x]; [absurd (y = x) | idtac]; trivial. subst y; apply (H' x x val valy nil tau1 tau2); trivial. right; apply in_or_app; right; left; trivial. intros y z valy valz tau1 tau2 tau3 H1; apply (H' y z valy valz ((x,val) :: tau1) tau2 tau3); subst; trivial. intros y valy H''; apply Acc_tau with y; right; trivial. destruct (acc_nf FB red_dec (Acc_tau x val (or_introl _ (refl_equal _)))) as [val' [H4 H5]]. exists ((x,val') :: sigma'); split. intros y valy; split; intro H6. simpl in H6; destruct H6 as [H6 | H6]. injection H6; clear H6; intros; subst; simpl. destruct (eq_variable_dec y y) as [_ | y_diff_y]; [idtac | absurd (y = y)]; trivial. assert (H7 := K3 _ _ H6). assert (H8 := find_mem eq_variable_dec y tau). destruct (find eq_variable_dec y tau) as [valy' | ]; [idtac | absurd (@None term = None); trivial]. destruct (H8 _ (refl_equal _)) as [tau1 [tau2 H9]]; subst; clear H7 H8. simpl; destruct (eq_variable_dec y x) as [y_eq_x | _]. subst y; absurd (x = x); trivial; apply (H' x x val valy' nil tau1 tau2); trivial. rewrite <- H1; trivial. destruct (find_mem eq_variable_dec _ _ H6) as [l1 [l2 H7]]; rewrite H7. apply in_or_app; right; left; trivial. repeat split. intros y valy; simpl. destruct (eq_variable_dec y x) as [y_eq_x | y_diff_x]; intro H6. injection H6; clear H6; intros; subst y valy; exists val'; repeat split; trivial; left; trivial. destruct (H2 _ _ H6) as [valy' [K1 [K2 K4]]]. exists valy'; repeat split; trivial; right; trivial. simpl; intros y valy [H6 | H6]. injection H6; clear H6; intros; subst y valy; trivial. apply H3 with y; trivial. intros y valy; simpl. destruct (eq_variable_dec y x) as [y_eq_x | y_diff_x]; intro H6. discriminate. apply K3 with valy; trivial. destruct H6 as [H6 | H6]; trivial. injection H6; intros; subst y; absurd (x = x); trivial. destruct H'' as [sigma' [H2 [H3 [H4 H5]]]]. exists sigma'; split; [idtac | repeat split]; trivial. intros x val H''; rewrite H1 in H''; apply H3; trivial. intros x val H''; rewrite H1; apply H5 with val; trivial. Defined. Definition non_overlapping (R : relation term) :=   forall l1 r1 l2 r2 sigma tau, R r1 l1 -> R r2 l2 ->   forall f l p, subterm_at_pos l1 p = Some (Term f l) ->   apply_subst sigma (Term f l) = apply_subst tau l2 -> p = nil /\ l1 = l2 /\ r1 = r2. Definition overlay (R : relation term) :=   forall l1 r1 l2 r2 sigma tau, R r1 l1 -> R r2 l2 ->   forall f l p, subterm_at_pos l1 p = Some (Term f l) ->   apply_subst sigma (Term f l) = apply_subst tau l2 -> p = nil. Definition sym_refl R (t1 t2 : term) := R t1 t2 \/ R t2 t1 \/ t1 = t2. Definition th_eq R := rwr (sym_refl R). Notation " T '<-[' R '*]->' U " := (th_eq R T U) (at level 80) : term_scope . Lemma th_refl : forall R t, th_eq R t t. Proof. unfold th_eq, sym_refl, rwr. intros R t; apply t_step; apply at_top; rewrite <- (empty_subst_is_id t); apply instance; right; right; trivial. Qed. Lemma th_sym : forall R t1 t2, th_eq R t1 t2 -> th_eq R t2 t1. Proof. intro R. intros t1 t2 H; refine (rwr_inv term (sym_refl R) (fun u1 u2 => th_eq R u2 u1) (fun t => t) _ _ _ _ _); trivial. unfold th_eq, rwr; intros; apply trans_clos_is_trans with a2; trivial. unfold th_eq, rwr; clear t1 t2 H; intros t1 t2 H; apply t_step. assert (axiom_sym : forall t1 t2, axiom (sym_refl R) t1 t2 -> axiom (sym_refl R) t2 t1). clear t1 t2 H; intros t1 t2 H; inversion_clear H as [u1 u2 sigma H']. destruct H' as [H' | [H' | H']]. apply instance; right; left; trivial. apply instance; left; trivial. apply instance; right; right; subst; trivial. generalize t2 H; clear t2 H; pattern t1; apply term_rec3; clear t1. intros v1 t2 H; inversion_clear H as [ H1 H2 H' | f l1 l2 H' ]. apply at_top; apply axiom_sym; trivial. intros f l1 IH t2 H; inversion_clear H as [H1 H2 H' | H1 H2 l2 H']. apply at_top; apply axiom_sym; trivial. apply in_context; generalize l2 H'; clear f t2 l2 H'; induction l1 as [ | t1 l1]. intros l2 H'; inversion H'. intros [ | t2 l2] H'; inversion_clear H' as [ H1 H2 H'' | f l1' l2' H'' ]. apply head_step; apply IH; trivial; left; trivial. apply tail_step; apply IHl1; trivial; intros; apply IH; trivial; right; trivial. Qed. End Make. ```