Library term_algebra.rwr_strategies


Add LoadPath "basis".

Add LoadPath "list_extensions".

Add LoadPath "term_algebra".

strategies for rewriting in a term algebra





Require Import List.

Require Import Relations.

Require Import Wellfounded.

Require Import Arith.

Require Import closure.

Require Import more_list.

Require Import term.

Require Import equational_theory.

Require Import dp.

Require Import rpo.




Module Make (E : EqTh).




  Import E.

  Import T.




Inductive P_step (R : relation term) (P : term -> Prop) : term -> term -> Prop :=

  | P_at_top : forall t s, P t -> axiom R s t -> P_step R P s t

  | P_in_context : 

     forall f lt ls, P_list R P ls lt -> P_step R P (Term f ls) (Term f lt)



   with P_list (R : relation term) (P : term -> Prop) : list term -> list term -> Prop :=

    | P_head_step : forall t1 t2 l, P_step R P t1 t2 -> P_list R P (t1 :: l) (t2 :: l)

    | P_tail_step : forall t l1 l2, P_list R P l1 l2 -> P_list R P (t :: l1) (t :: l2).




Lemma P_step_one_step :

  forall R P s t, P_step R P s t -> one_step R s t.

Proof.

intros R P s t; generalize s; clear s; pattern t; apply term_rec3; clear t.

intros v s H; inversion H; subst; apply at_top; trivial.

intros f l Hl s H; 

inversion H as [t' s' Hnf H' | f' lt ls H']; 

clear H; subst.

apply at_top; trivial.

apply in_context.

generalize ls H'; clear ls H';

induction l as [ | t l]; intros ls H';

inversion H' as [t1 t2 l' H'' | t' l1 l2 H'']; clear H'; subst.

apply head_step; apply Hl; trivial; left; trivial.

apply tail_step; apply IHl; trivial; intros; apply Hl; trivial; right; trivial.

Qed.




Lemma trans_clos_P_step_P_list :

  forall R P t1 t2 l, trans_clos (P_step R P) t1 t2 -> trans_clos (P_list R P) (t1 :: l) (t2 :: l).

Proof.

intros R P t1 t2 l H; induction H.

apply t_step; apply P_head_step; trivial.

apply t_trans with (y :: l); trivial.

apply P_head_step; trivial.

Qed.




Lemma trans_clos_P_list_P_list :

  forall R P t l1 l2, trans_clos (P_list R P) l1 l2 -> trans_clos (P_list R P) (t :: l1) (t :: l2).

Proof.

intros R P t l1 l2 H; induction H.

apply t_step; apply P_tail_step; trivial.

apply t_trans with (t :: y); trivial.

apply P_tail_step; trivial.

Qed.




Lemma P_context_cons :

  forall R P f t1 t2 l, trans_clos (P_step R P) t1 t2 -> 

      trans_clos (P_step R P) (Term f (t1 :: l)) (Term f (t2 :: l)).

Proof.

intros R P f t1 t2 l H;

induction H as [ | t1 t2 t3 Trans1 Trans2].

apply t_step; apply P_in_context; apply P_head_step; trivial.

apply t_trans with (Term f (t2 :: l)); trivial.

apply P_in_context; apply P_head_step; trivial.

Qed.




Lemma P_step_context_in :

  forall R P t1 t2 f l l', P_step R P t1 t2 -> 

   P_step R P (Term f (l ++ t1 :: l')) (Term f (l ++ t2 :: l')).

Proof.

intros R P t1 t2 f l l' H; apply P_in_context; 

induction l as [ | t l ]; simpl; [ apply P_head_step | apply P_tail_step ]; 

trivial.

Qed.




Lemma P_context_in :

  forall R P t1 t2, trans_clos (P_step R P) t1 t2 -> 

  forall f l l', trans_clos (P_step R P) (Term f (l ++ t1 :: l')) (Term f (l ++ t2 :: l')).

Proof.

intros R P t1 t2 H; 

induction H as [ t1 t2 Step 
                          | t1 t2 t3 Trans1 Trans2].

intros f l l'; apply t_step; apply P_step_context_in; trivial.

intros f l l'; apply trans_clos_is_trans with (Term f (l ++ t2 :: l')); trivial.

apply t_step; apply P_step_context_in; trivial.

Qed.




Lemma P_list_length_eq :

    forall R P l1 l2, trans_clos (P_list R P) l1 l2 -> length l1 = length l2.

Proof.

intros R P l1 l2 H.

refine (@inv_trans (list term) (P_list R P) (fun l2 => length l1 = length l2) _ _ _ _ H); trivial.

clear l2 H; intros l2 l L H.

rewrite L; clear l1 L; induction H; simpl; trivial.

rewrite IHP_list; trivial.

Qed.




Lemma P_list_expand : 

  forall R P l1 l2, P_list R P l1 l2 -> 

  exists t1, exists l', exists l'', exists t2, l1 = l' ++ t1 :: l'' /\ l2 = l' ++ t2 :: l'' /\ P_step R P t1 t2.

Proof.

intros R P l1 l2 H; induction H.

exists t1; exists (@nil term); exists l; exists t2; repeat split; trivial.

destruct IHP_list as [t1 [l' [l'' [t2 [H1 [H2 H3]]]]]]; subst.

exists t1; exists (t :: l'); exists l''; exists t2; repeat split; trivial.

Qed.




Lemma trans_clos_P_list_split :

  forall R P a1 a2 l1 l2, trans_clos (P_list R P) (a1 :: l1) (a2 :: l2) ->

  (a1 = a2 /\ trans_clos (P_list R P) l1 l2) \/

  (trans_clos (P_step R P) a1 a2 /\ l1 = l2) \/

  (trans_clos (P_step R P) a1 a2 /\ trans_clos (P_list R P) l1 l2).

Proof.

intros R P;

assert (H :   forall k1 k2, trans_clos (P_list R P) k1 k2 -> 

                   forall a1 a2 l1 l2, k1 = a1 :: l1 -> k2 = a2 :: l2 ->

  (a1 = a2 /\ trans_clos (P_list R P) l1 l2) \/

  (trans_clos (P_step R P) a1 a2 /\ l1 = l2) \/

  (trans_clos (P_step R P) a1 a2 /\ trans_clos (P_list R P) l1 l2)).

intros k1 k2 H; induction H; intros a1 a2 l1 l2 H1 H2; subst.

inversion H; clear H; subst.

right; left; split; trivial; apply t_step; trivial.

left; split; trivial; apply t_step; trivial.

inversion H; clear H; subst.

destruct (IHtrans_clos _ _ _ _ (refl_equal _) (refl_equal _)) as [H | [H | H]].

destruct H as [H1 H2]; subst.

right; right; split; trivial; apply t_step; trivial.

destruct H as [H1 H2]; subst.

right; left; split; trivial; apply t_trans with t2; trivial.

destruct H as [H1 H2]; subst.

right; right; split; trivial; apply t_trans with t2; trivial.

destruct (IHtrans_clos _ _ _ _ (refl_equal _) (refl_equal _)) as [H | [H | H]].

destruct H as [H1 H2]; subst.

left; split; trivial; apply t_trans with l3; trivial.

destruct H as [H1 H2]; subst.

right; right; split; trivial; apply t_step; trivial.

destruct H as [H1 H2]; subst.

right; right; split; trivial; apply t_trans with l3; trivial.

intros a1 a2 l1 l2 H'; apply (H (a1 :: l1) (a2 :: l2)); trivial.

Qed.




Lemma trans_clos_P_list_expand : 

  forall R P l1 l2, trans_clos (P_list R P) l1 l2 <-> 

  exists t1, exists l1', exists l1'', exists t2, exists l2', exists l2'',

  l1 = l1' ++ t1 :: l1'' /\ l2 = l2' ++ t2 :: l2'' /\

  (l1' = l2' \/ trans_clos (P_list R P) l1' l2') /\

  trans_clos (P_step R P) t1 t2 /\

  (l1'' = l2'' \/ trans_clos (P_list R P) l1'' l2'').

Proof.

intros R P l1 l2; split; intro H.

induction H.

destruct (P_list_expand _ _ _ _ H) as [t1 [l' [l'' [t2 [H1 [H2 H3]]]]]]; subst.

exists t1; exists l'; exists l''; exists t2; exists l'; exists l''; repeat split; trivial.

left; trivial.

apply t_step; trivial.

left; trivial.

destruct IHtrans_clos as [t1 [l1' [l1'' [t2 [l2' [l2'' [H1 [H2 [H3 [H4 H5]]]]]]]]]]; subst.

destruct (P_list_expand _ _ _ _ H) as [u1 [k [k'' [u2 [K1 [K2 K3]]]]]]; subst.

destruct (in_in_split_set _ _ _ _ _ _ K2) as [[K | K] | K]; clear K2.

destruct K as [l [K K']]; subst.

exists t1; exists (k ++ u1 :: l); exists l1''; exists t2; exists l2'; exists l2''; repeat split; trivial.

rewrite <- ass_app; simpl; trivial.

right; destruct H3 as [H3 | H3].

subst; clear H H0; apply t_step; induction k as [ | a k]; simpl.

apply P_head_step; trivial.

apply P_tail_step; trivial.

apply trans_clos_is_trans with (k ++ u2 :: l); trivial.

clear H H0 H3; apply t_step; induction k as [ | a k]; simpl.

apply P_head_step; trivial.

apply P_tail_step; trivial.




destruct K as [l [K K']]; subst.

exists t1; exists l1'; exists (l ++ u1 :: k''); exists t2; exists l2'; exists l2''; repeat split; trivial.

rewrite <- ass_app; simpl; trivial.

right; destruct H5 as [H5 | H5].

subst; clear H H0; apply t_step; induction l as [ | a l]; simpl.

apply P_head_step; trivial.

apply P_tail_step; trivial.

apply trans_clos_is_trans with (l ++ u2 :: k''); trivial.

clear H H5 H0; apply t_step; induction l as [ | a l]; simpl.

apply P_head_step; trivial.

apply P_tail_step; trivial.




destruct K as [K [K' K'']]; subst.

exists u1; exists k; exists k''; exists t2; exists l2'; exists l2''; repeat split; trivial.

apply trans_clos_is_trans with u2; trivial.

apply t_step; trivial.




generalize l2 H; clear l2 H; induction l1 as [ | a1 l1];

intros l2 H; destruct H as [t1 [l1' [l1'' [t2 [l2' [l2'' [H1 [H2 [H3 [H4 H5]]]]]]]]]]; subst.

destruct l1' as [ | a1' l1']; discriminate.

destruct l1' as [ | a1' l1'].

simpl in H1; injection H1; clear H1; intros; subst.

destruct H3 as [H3 | H3]; subst.

destruct H5 as [H5 | H5]; subst.

simpl; apply trans_clos_P_step_P_list; trivial.

simpl; apply trans_clos_is_trans with (t1 :: l2'').

apply trans_clos_P_list_P_list; trivial.

apply trans_clos_P_step_P_list; trivial.

assert (L' := P_list_length_eq _ _ _ _ H3).

destruct l2' as [ | a2' l2'].

destruct H5 as [H5 | H5]; subst.

simpl; apply trans_clos_P_step_P_list; trivial.

simpl; apply trans_clos_is_trans with (t1 :: l2'').

apply trans_clos_P_list_P_list; trivial.

apply trans_clos_P_step_P_list; trivial.

simpl in L'; discriminate.

simpl in H1; injection H1; clear H1; intros; subst.

destruct H3 as [H3 | H3]; subst; simpl.

apply trans_clos_P_list_P_list; apply IHl1; trivial.

exists t1; exists l1'; exists l1''; exists t2; exists l1'; exists l2''; split; trivial.

do 2 (split; trivial).

left; trivial.

split; trivial.

assert (L' := P_list_length_eq _ _ _ _ H3).

destruct l2' as [ | a2' l2'].

simpl in L'; discriminate.

destruct (trans_clos_P_list_split _ _ _ _ _ _ H3) as [H6 | [H6 | H6]].

destruct H6 as [H6 H7]; subst.

simpl; apply trans_clos_P_list_P_list; apply IHl1.

exists t1; exists l1'; exists l1''; exists t2; exists l2'; exists l2''; split; trivial.

do 2 (split; trivial).

right; trivial.

split; trivial.

destruct H6 as [H6 H7]; subst.

apply trans_clos_is_trans with (a2' :: l2' ++ t1 :: l1'').

apply trans_clos_P_step_P_list; trivial.

simpl; apply trans_clos_P_list_P_list; apply IHl1.

exists t1; exists l2'; exists l1''; exists t2; exists l2'; exists l2''; split; trivial.

do 2 (split; trivial).

left; trivial.

split; trivial.

destruct H6 as [H6 H7]; subst.

apply trans_clos_is_trans with (a2' :: l1' ++ t1 :: l1'').

apply trans_clos_P_step_P_list; trivial.

simpl; apply trans_clos_P_list_P_list; apply IHl1.

exists t1; exists l1'; exists l1''; exists t2; exists l2'; exists l2''; split; trivial.

do 2 (split; trivial).

right; trivial.

split; trivial.

Qed.




Lemma P_general_context_aux :

  forall R P f l1 l2 l' l'', trans_clos (P_list R P) l1 l2 -> 

  trans_clos (P_step R P) (Term f (l' ++ l1 ++ l'')) (Term f (l' ++ l2 ++ l'')).

Proof.

intros R P f l1 l2 l' l'' H; generalize l' l''; clear l' l''; induction H; intros l' l''.

apply t_step; apply P_in_context; generalize l'; clear l'; induction H; intros l'.

induction l' as [ | a' l']; simpl.

apply P_head_step; trivial.

apply P_tail_step; trivial.

replace (l' ++ (t :: l1) ++ l'') with ((l' ++ t :: nil) ++ l1 ++ l'').

replace (l' ++ (t :: l2) ++ l'') with ((l' ++ t :: nil) ++ l2 ++ l'').

apply IHP_list.

rewrite <- ass_app; simpl; trivial.

rewrite <- ass_app; simpl; trivial.

apply trans_clos_is_trans with (Term f (l' ++ y ++ l'')); trivial.

apply t_step; apply P_in_context; generalize l'; clear l' H0 IHtrans_clos; induction H; intros l'.

induction l' as [ | a' l']; simpl.

apply P_head_step; trivial.

apply P_tail_step; trivial.

replace (l' ++ (t :: l1) ++ l'') with ((l' ++ t :: nil) ++ l1 ++ l'').

replace (l' ++ (t :: l2) ++ l'') with ((l' ++ t :: nil) ++ l2 ++ l'').

apply IHP_list.

rewrite <- ass_app; simpl; trivial.

rewrite <- ass_app; simpl; trivial.

Qed.




Lemma P_general_context :

  forall R P f l1 l2, trans_clos (P_list R P) l1 l2 -> trans_clos (P_step R P) (Term f l1) (Term f l2).

Proof.

intros R P f l1 l2 l1_R_l2; 

assert (H:= P_general_context_aux R P f l1 l2 nil nil l1_R_l2); 

simpl in H; do 2 rewrite <- app_nil_end in H; exact H.

Qed.




Lemma nf_P_step_subterm:

  forall R P t, nf (P_step R P) t -> forall s, direct_subterm s t -> nf (P_step R P) s.

Proof.

intros R P 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 P_in_context; clear IH Hnf s_in_l; induction l' as [ | s' l']; simpl.

apply P_head_step; trivial.

apply P_tail_step; apply IHl'.

Qed.




Lemma acc_P_list :

 forall R P l, (forall t, In t l -> Acc (P_step R P) t) <-> Acc (P_list R P) l.

Proof.

assert (H : forall R P t, Acc (P_step R P) t -> 

                      (forall l, Acc (P_list R P) l -> Acc (P_list R P) (t :: l))).

intros R P t Acc_t; pattern t; refine (@Acc_ind _ (P_step R P) _ _ t Acc_t).

clear t Acc_t; intros t Acc_t IHt l Acc_l.

pattern l; refine (@Acc_ind _ (P_list R P) _ _ 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 P 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 P_head_step; trivial.

simpl; apply P_tail_step; trivial.

apply in_or_app; right; left; trivial.

Qed.




Lemma P_acc_subterms :

  forall R P, (forall x t, ~ (R t (Var x))) -> 

  forall f l, (forall t, In t l -> Acc (P_step R P) t) -> constructor R f ->

                   Acc (P_step R P) (Term f l).

Proof.

intros R P HR f l Acc_l Cf'; inversion Cf' as [f' Cf]; clear Cf'; subst f';

rewrite acc_P_list in Acc_l.

pattern l; refine (@Acc_ind _ (P_list R P) _ _ l Acc_l).

clear l Acc_l; intros l Acc_l IH.

apply Acc_intro.

intros t H; inversion H as [t' s Hnf 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 l2 l H'.

intro k; induction k as [ | s k]; intros k' K; inversion K; subst.

apply P_head_step; trivial.

apply P_tail_step; trivial.

Qed.




Lemma P_acc_subterms_1 :

   forall R P t s, Acc (P_step R P) t -> direct_subterm s t -> Acc (P_step R P) s.

Proof.

intros R P t s Acc_t; generalize s; clear s; pattern t;

refine (@Acc_ind _ (P_step R P) _ _ 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 P_step_context_in; trivial.

simpl; apply in_or_app; right; left; trivial.

Qed.




Lemma P_acc_subterms_3 : 

   forall R P p t s, Acc (P_step R P) t -> subterm_at_pos t p = Some s ->  Acc (P_step R P) s.

Proof.

intros R P 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 (P_acc_subterms_1 R P (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 var_P_acc : 

   forall R P l x sigma, In x (var_list_list l) -> 

   (forall t, In t (map (apply_subst sigma) l) -> Acc (P_step R P) t) ->

   Acc (P_step R P) (apply_subst sigma (Var x)).

Proof.

intros R P 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 (P_step R P) t).

intros t H'; apply P_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.




Lemma P_acc_with_subterm_subterms :

  forall R P t, Acc (union _ (P_step R P) direct_subterm) t ->

                 forall s, direct_subterm s t -> Acc (union _ (P_step R P) direct_subterm) s.

Proof.

intros R P t Acc_t; induction Acc_t as [t Acc_t IH].

intros s H; apply Acc_t; right; trivial.

Qed.




Lemma P_acc_with_subterm :

  forall R P t, Acc (P_step R P) t <->  Acc (union _ (P_step R P) direct_subterm) t.

Proof.

intros R P 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 (P_step R P) u).

apply P_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 (P_acc_with_subterm_subterms R P (Term f (l' ++ v :: l''))).

apply IH; apply P_step_context_in; trivial.

simpl; apply in_or_app; right; left; trivial.

apply Acc_incl; intros t1 t2 H; left; trivial.

Qed.




Lemma P_step_in_list :

  forall R P l l', P_list R P l' l ->

  exists t, exists t', exists l1, exists l2, P_step R P t' t /\  l = l1 ++ t :: l2 /\ l' = l1 ++ t' :: l2.

Proof.

intros R P 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.




Definition inner (R : relation term) (t : term) :=

  forall s, direct_subterm s t -> nf (one_step R) s.




Lemma one_step_nf_inner_step_nf :

  forall (R : relation term), (forall t v, R t (Var v) -> False) ->

  forall t, nf (one_step R) t <-> nf (P_step R (inner R)) t.

Proof.

intros R Rvar t; split.

intros H s H'; apply (H s); apply (P_step_one_step R (inner R)); trivial.

pattern t; apply term_rec3; clear t.

intros v _ s H'; inversion H' as [t1 t2 H'' | f' l1 l2 H'']; clear H'; subst.

inversion H''; clear H''; subst.

destruct t2 as [v2 | f2 l2].

apply (Rvar t1 v2); trivial.

discriminate.

intros f l IH H s H'.

apply (H s); apply P_at_top.

intros t t_in_l; apply IH; trivial.

apply nf_P_step_subterm with (Term f l); trivial.

inversion H' as [t1 t2 H'' | f' l1 l2 H'']; clear H'; subst; trivial.

assert (H' : forall t, In t l -> nf (one_step R) t).

intros t t_in_l; apply IH; trivial.

apply nf_P_step_subterm with (Term f l); trivial.

assert False.

generalize l1 H'' H'; clear IH H l1 H'' H'; 

induction l as [ | t l]; intros l1 H'' H';

inversion H'' as [t1 t2' l' H3 | t' l1' l2' H3]; clear H''; subst.

apply (H' t (or_introl _ (refl_equal _)) t1); trivial.

apply (IHl l1'); trivial.

intros s s_in_l; apply H'; right; trivial.

contradiction.

Qed.




Lemma nf_dec_inner_dec : 

  forall R, (forall t, {nf (one_step R) t}+{~ nf (one_step R) t}) -> 

  forall t, {inner R t}+{~inner R t}.

Proof.

intros R nf_dec [v | f l].

left; intro s; simpl; contradiction.

unfold inner; simpl; induction l as [ | t l].

left; intro s; simpl; contradiction.

destruct (nf_dec t) as [nf_t | red_t].

destruct IHl as [nf_l | red_l].

left; intros s [s_eq_t | s_in_l]; [subst | apply nf_l]; trivial.

right; intro nf_tl; apply red_l; intros s s_in_l; apply nf_tl; right; trivial.

right; intro nf_tl; apply red_t; apply nf_tl; left; trivial.

Defined.




Lemma rwr_inner_or_eq : 

  forall R ll, (forall s t, In (s,t) ll -> s = t \/ trans_clos (P_step R (inner R)) s t) -> 

            map (@fst term term) ll = map (@snd term term) ll \/

            trans_clos (P_list R (inner 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.

right; apply trans_clos_P_list_P_list; trivial.

destruct IHll as [H2 | H2].

intros; apply H; right; trivial.

right; simpl; rewrite H2; apply trans_clos_P_step_P_list; trivial.

right; apply trans_clos_is_trans with (t :: map (@fst term term) ll).

simpl; apply trans_clos_P_step_P_list; trivial.

simpl; apply trans_clos_P_list_P_list; trivial.

Qed.




Lemma rwr_inner_or_eq_bis : 

  forall R l (f g : term -> term), 

    (forall s, In s l -> g s = f s \/ trans_clos (P_step R (inner R)) (g s) (f s)) -> 

            map g l = map f l \/

            trans_clos (P_list R (inner R)) (map g l) (map f l).

Proof.

intros R l f g; induction l as [ | s l]; intro H.

left; trivial.

destruct (H s (or_introl _ (refl_equal _))) as [H1 | H1].

simpl; rewrite H1; destruct IHl as [H2 | H2].

intros; apply H; right; trivial.

left; rewrite H2; trivial.

right; apply trans_clos_P_list_P_list; trivial.

destruct IHl as [H2 | H2].

intros; apply H; right; trivial.

right; simpl; rewrite H2; apply trans_clos_P_step_P_list; trivial.

right; apply trans_clos_is_trans with (f s :: map g l).

simpl; apply trans_clos_P_step_P_list; trivial.

simpl; apply trans_clos_P_list_P_list; trivial.

Qed.




Lemma rwr_inner_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) \/

                               trans_clos (P_step R (inner R)) (apply_subst sigma (Var x)) (apply_subst tau (Var x))) ->

            apply_subst sigma t = apply_subst tau t \/

            trans_clos (P_step R (inner 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 \/

            trans_clos (P_list R (inner 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.

right; rewrite H1; apply trans_clos_P_list_P_list; 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; rewrite H2; apply trans_clos_P_step_P_list; trivial.

right; apply trans_clos_is_trans with (apply_subst tau t :: map (apply_subst sigma) l).

apply trans_clos_P_step_P_list; trivial.

apply trans_clos_P_list_P_list; trivial.

destruct H' as [H' | H'].

left; rewrite H'; trivial.

right; apply P_general_context; trivial.

Qed.




End Make.