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.