Library examples.cime_trace.rpo_extension
Require rpo.
Require equational_theory.
Require term.
Require Import List.
Require Import list_permut.
Require Import terminaison.
Require Import Relations.
Module Make_EQTH_facts (Eqt:equational_theory.EqTh).
Lemma rwr_as_star : forall R t t', Eqt.rwr R t t' -> star _ (Eqt.one_step R) t t'.
Proof.
induction 1.
apply star_R. assumption.
apply star_trans with y;auto.
apply star_R; trivial.
Qed.
Lemma one_step_list_star_decompose_cons : forall R x l l'', star _ (Eqt.one_step_list R) (x::l) l'' ->
exists x', exists l', l'' = x'::l' /\ star _ (Eqt.one_step R) x x'/\star _ (Eqt.one_step_list R) l l'.
Proof.
intros R x l l''.
set (l1 := x::l) in *.
generalize (refl_equal l1);
unfold l1 at 1;clearbody l1.
intros H H0 .
revert x l H.
induction H0; intros x l He;subst.
exists x;exists l;repeat split;constructor.
destruct (IHstar _ _ (refl_equal (x::l))) as [x' [l' [h1 [h2 h3]]]];clear IHstar;subst.
inversion H;clear H;subst.
exists t2;exists l';repeat split;auto.
constructor 2 with x';auto.
exists x';exists l2;repeat split;auto.
constructor 2 with l';auto.
Qed.
Lemma one_step_list_star_decompose_nil : forall R l'', star _ (Eqt.one_step_list R) nil l'' -> l'' = nil.
Proof.
intros R l'' H.
set (l:= @nil Eqt.T.term) in *.
generalize (refl_equal l).
unfold l at 1;clearbody l.
induction H;intro;subst;auto.
rewrite (IHstar (refl_equal (@nil Eqt.T.term))) in H0.
inversion H0.
Qed.
Lemma one_step_list_star_l : forall R l x y,
star _ (Eqt.one_step R) x y ->
star _ (Eqt.one_step_list R) (x::l) (y::l).
Proof.
induction 1.
constructor.
constructor 2 with (y::l).
assumption.
constructor;assumption.
Qed.
Lemma one_step_list_star_r : forall R l l' x,
star _ (Eqt.one_step_list R) l l' ->
star _ (Eqt.one_step_list R) (x::l) (x::l').
Proof.
induction 1.
constructor.
constructor 2 with (x::y).
assumption.
constructor;assumption.
Qed.
End Make_EQTH_facts.
Module rpo_facts (M:term.Term)
(Prec:rpo.Precedence with Definition A := M.symbol)
(Eqt : equational_theory.EqTh with Module T := M)
(Rpo : rpo.RPO with Module T := M with Module P := Prec)
.
Lemma rpo_in_list :
forall f (f_stat:Rpo.P.status f=rpo.Lex) l1 l2, length l1 = length l2 ->
(exists t1', exists t2', Rpo.rpo t1' t2' /\ In (t1',t2') (combine l1 l2) /\
forall t1 t2 : Eqt.T.term,
In (t1, t2) (combine l1 l2) -> Rpo.rpo_eq t1 t2) ->
Rpo.rpo (M.Term f l1) (M.Term f l2).
Proof.
intro f.
intros f_stat l1 l2 H H0.
constructor 3.
exact f_stat.
revert l2 H H0;induction l1.
destruct l2;simpl length;[intros _|intros;discriminate].
intro abs;destruct abs as [t1' [t2' [_ [abs' _]]]];simpl in abs';tauto.
destruct l2;simpl;[intros;discriminate|intros Hlength;injection Hlength;clear Hlength;intro Hlength].
intros H.
destruct (H) as [t1' [t2' [Hrpo [Hin1 Hin2]]]].
inversion Hin1.
injection H;clear H;intros;subst.
apply Rpo.List_gt. exact Hrpo. exact Hlength.
assert (Hin3:forall t1 t2 : Eqt.T.term,
In (t1, t2) (combine l1 l2) -> Rpo.rpo_eq t1 t2).
intros;auto.
assert (Rpo.rpo_eq a t). auto.
destruct H0.
apply Rpo.List_eq. assumption.
apply IHl1. assumption.
exists t1';exists t2';repeat split;auto.
apply Rpo.List_gt. exact H0. exact Hlength.
destruct (H0) as [t1' [t2' [Hrpo [Hin1 Hin2]]]].
intros.
assert (exists s'',exists t',(Rpo.equiv s' s'' /\In (s'',t') (combine l1 l2)) /\ In t' l2).
clear - H H0.
revert l2 H.
induction l1;simpl in *.
tauto.
destruct l2;simpl in *.
intros;discriminate.
intros Hlength;injection Hlength;clear Hlength;intros Hlength.
destruct H0.
exists a;exists t;auto.
destruct (IHl1 H l2 Hlength) as [s'' [t' [[H' H''] H''']]].
exists s''; exists t';auto.
destruct H1 as [s'' [t' [[H' H''] H''']]].
apply Rpo.Subterm with t'; auto.
clear -H''';induction l2.
simpl in H''';tauto.
simpl in H''';inversion H'''.
subst;simpl;left;constructor.
simpl;right;auto.
destruct (Rpo.equiv_rpo_equiv_4 _ _ H' t').
apply H2.
apply Hin2;auto.
Qed.
Lemma equiv_in_list :
forall f (f_stat:Rpo.P.status f=rpo.Lex) l1 l2,
length l1 = length l2 ->
(
forall t1 t2 : Eqt.T.term,
In (t1, t2) (combine l1 l2) -> Rpo.equiv t1 t2) ->
Rpo.equiv (M.Term f l1) (M.Term f l2).
Proof.
intros.
constructor 2.
exact f_stat.
revert l2 H H0.
induction l1;destruct l2;simpl;try (intros;discriminate).
constructor.
intros Heq.
injection Heq;clear Heq;intro Heq.
intro Hcomb.
constructor.
apply Hcomb;auto.
apply IHl1;auto.
Qed.
Lemma rpo_eq_in_list : forall f (f_stat:Rpo.P.status f=rpo.Lex) l1 l2,
length l1 = length l2 ->
(
forall t1 t2 : Eqt.T.term,
In (t1, t2) (combine l1 l2) -> Rpo.rpo_eq t1 t2) ->
Rpo.rpo_eq (M.Term f l1) (M.Term f l2).
Proof.
intros f f_stat l1 l2 Hlength H.
assert ((exists t1',exists t2', Rpo.rpo t1' t2' /\ In (t1',t2') (combine l1 l2) /\
forall t1 t2 : Eqt.T.term,
In (t1, t2) (combine l1 l2) -> Rpo.rpo_eq t1 t2) \/ (forall t1 t2 : Eqt.T.term,
In (t1, t2) (combine l1 l2) -> Rpo.equiv t1 t2)).
revert l2 Hlength H;induction l1.
destruct l2;simpl;[idtac|intros;discriminate].
right;tauto.
destruct l2;simpl;[intros;discriminate|idtac].
injection 1. clear Hlength;intros Hlength.
intros.
case (H a t). auto.
intros.
assert ((forall t1 t2 : Eqt.T.term,
In (t1, t2) (combine l1 l2) -> Rpo.rpo_eq t1 t2) ) by auto.
destruct (IHl1 _ Hlength H1).
left.
destruct H2 as [t1' [t2' [h1 [h2 h3]]]].
exists t1';exists t2';repeat split;auto.
inversion 1;auto.
injection H3;intros;subst. constructor;assumption.
right.
inversion 1;auto.
injection H4;intros;subst. auto.
intros;left;exists s;exists t0;repeat split;auto.
inversion 1;auto.
injection H2;intros;subst. constructor 2;auto.
destruct H0.
constructor 2;apply rpo_in_list;auto.
constructor;apply equiv_in_list;auto.
Qed.
Ltac prove_prec := constructor;fail 0.
Ltac is_In x l :=
match l with
| List.nil => constr:false
| x::_ => constr:true
| _::?tl => let e := is_In x tl in constr:e
end.
Ltac remove acc x l :=
match l with
| List.nil => let e := eval simpl in (List.rev acc) in constr:e
| x::?tl => remove acc x tl
| ?y::?tl => remove (y::acc) x tl
end.
Ltac prove_in t :=
match t with
| Rpo.LP.EDS.eq_A ?t ?t => exact (@Rpo.Eq t)
| Rpo.LP.EDS.eq_A ?t ?t \/ _ => left;exact (@Rpo.Eq t)
| _ \/ ?t' => right; prove_in t'
end.
Ltac split_lists rev_ls rev_lc l' l :=
match l' with
| List.nil =>
let ls := eval simpl in (List.rev rev_ls) in
let lc := eval simpl in (List.rev rev_lc) in
constr:(l,ls,lc)
| ?h::?tl =>
let e := is_In h l in
match constr:e with
| true =>
let l0 := remove (List.nil:list Rpo.T.term) h l in
(let l'0 := remove (List.nil:list Rpo.T.term) h tl in
split_lists rev_ls (h::rev_lc) l'0 l0)
| false =>
let l'0 := remove (List.nil:list Rpo.T.term) h tl in
split_lists (h::rev_ls) rev_lc l'0 l
end
end.
Ltac combine_tac l1 l2 :=
match constr:(l1,l2) with
| (nil,nil) => constr:nil
| (?x::?l1,?y::?l2) =>
let l := combine_tac l1 l2 in
constr:((x,y)::l)
end.
Ltac prove_permut tac :=
match goal with
| |- permut ?R nil nil => exact (Pnil R)
| |- @permut ?A ?R (?a::?l) ?l2 =>
prove_permut_aux tac R a l (@nil A) l2
end
with prove_permut_aux tac R a l rev_l1 l2 :=
match l2 with
| nil => fail 1
| ?b::?l2 =>
(
let l1 := eval vm_compute in (List.rev rev_l1) in
refine (@Pcons _ R a b l l1 l2 _ _);[tac | simpl app;prove_permut tac ]
)||
(prove_permut_aux tac R a l (b::rev_l1) l2)
end
.
Ltac prove_equiv := match goal with
| H: Rpo.equiv ?t1 ?t2 |- Rpo.equiv ?t1 ?t2 => exact H
| |- Rpo.equiv ?t ?t => exact (@Rpo.Eq t)
| |- Rpo.equiv (?Term ?f ?l1) (?Term ?f ?l2) =>
let f_status := eval compute in (Rpo.P.status f) in
match f_status with
| rpo.Lex => prove_equiv_lex || fail 1
| rpo.Mul => prove_equiv_mul || fail 1
| _ => prove_equiv_lex || prove_equiv_mul || fail 1
end
end
with prove_equiv_lex :=
match goal with
| |- Rpo.equiv (?Term ?f ?lhs) (?Term' ?f ?rhs) =>
refine (@Rpo.Eq_lex f lhs rhs _ _ );
[ reflexivity (* preuve que status f = Lex *) |
prove_equiv_list_lex (* preuve que args' =equiv_list_lex args *)
]
end
with prove_equiv_mul :=
match goal with
| |- Rpo.equiv (?Term ?f ?lhs) (?Term' ?f ?rhs) =>
refine (@Rpo.Eq_mul f lhs rhs _ _);
[ reflexivity (* preuve que status f = Mul *) |
prove_permut prove_equiv (* preuve que args' <_lex args *) |
]
end
with prove_equiv_list_lex :=
match goal with
| |- Rpo.equiv_list_lex nil nil => exact (Rpo.Eq_list_nil)
| |- Rpo.equiv_list_lex (?s::?l1) (?t::?l2) =>
refine (@Rpo.Eq_list_cons s t l1 l2 _ _);[prove_equiv | prove_equiv_list_lex]
end
.
Ltac prove_rpo := match goal with
| H: Rpo.rpo ?t ?u |- Rpo.rpo ?t ?u => exact H
| |- Rpo.rpo _ (?Var _) => fail 1
| |- Rpo.rpo (?Var _) (?Term ?f ?args) => (prove_rpo_subterm args) || fail 1 | |- Rpo.rpo _ (?Term ?f ?args) => prove_rpo_subterm args
| |- Rpo.rpo (?Term ?f ?lhs) (?Term' ?f ?rhs) =>
let f_status := eval compute in (Rpo.P.status f) in
match f_status with
| rpo.Lex => prove_rpo_eq_lex || fail 1
| rpo.Mul => prove_rpo_eq_mul || fail 1
| _ =>prove_rpo_eq_lex || prove_rpo_eq_mul || fail 1
end
| H: Rpo.equiv _ ?t |- Rpo.rpo _ ?t => rewrite <- H;prove_rpo
| H: Rpo.rpo ?t ?u |- Rpo.rpo ?v ?u => let Htrans := fresh "H" in
(
let H2 := fresh "H" in
(destruct (Rpo.rpo_closure u t v) as [Htrans H2];
apply (Htrans H);clear Htrans H2;prove_rpo
)
)
| |- Rpo.rpo (?Term ?g ?lhs) (?Term' ?f ?rhs) =>
(refine (@Rpo.Top_gt f g rhs lhs _ _);
[ prove_prec (* preuve que prec g f *) |
prove_all_rpo (* preuve de (forall s', In s' args' -> rpo s' (Term f args)) *)
])
||
prove_rpo_eq_lex || prove_rpo_eq_mul
| H: Rpo.rpo ?t ?s |- Rpo.rpo ?u ?s => refine (Rpo.rpo_trans s t u H _);prove_rpo
end
with prove_rpo_eq_lex :=
match goal with
| |- Rpo.rpo (?Term ?f ?lhs) (?Term' ?f ?rhs) =>
refine (@Rpo.Top_eq_lex f rhs lhs _ _ _);
[ reflexivity (* preuve que status f = Lex *) |
prove_rpo_lex (* preuve que args' <_lex args *) |
prove_all_rpo (* preuve de (forall s', In s' args' -> rpo s' (Term f args)) *)
]
end
with prove_rpo_eq_mul :=
match goal with
| |- Rpo.rpo (?Term ?f ?lhs) (?Term' ?f ?rhs) =>
refine (@Rpo.Top_eq_mul f rhs lhs _ _);
[ reflexivity (* preuve que status f = Lex *) |
prove_rpo_mul (* preuve que args' <_mul args *)
]
end
with prove_rpo_eq :=
match goal with
| H: Rpo.rpo_eq ?t ?u |- Rpo.rpo_eq ?t ?u => assumption
| |- Rpo.rpo_eq ?lhs ?rhs =>
(refine (@Rpo.Equiv lhs rhs _); prove_equiv)||
(refine (@Rpo.Lt lhs rhs _);prove_rpo)
end
with prove_rpo_subterm args := match args with
| List.nil => fail 0
| ?arg::?largs =>
match goal with
| |- Rpo.rpo ?lhs (?Term ?f ?rhs) =>
((refine (@Rpo.Subterm f rhs lhs arg _ _); [ (solve [simpl;match goal with |- ?t => prove_in t end]) | prove_rpo_eq ]
) ||
( prove_rpo_subterm largs
))
end
end
with prove_rpo_lex :=
match goal with
| H: Rpo.rpo_lex ?t ?u |- Rpo.rpo_lex ?t ?u => exact H
| |- Rpo.rpo_lex (?lhs::?lhss) (?rhs::?rhss) =>
(refine (@Rpo.List_gt lhs rhs lhss rhss _ _);
[ prove_rpo (* preuve de lhs < rhs *) |
vm_compute;reflexivity
]
)
||
(refine (@Rpo.List_eq lhs rhs lhss rhss _ _); [prove_equiv | prove_rpo_lex])
end
with prove_all_rpo := let s := fresh "s'" in
(let Hin := fresh "Hin" in
(intros s Hin; simpl Rpo.LP.mem in Hin;prove_all_rpo_aux s Hin))
with prove_all_rpo_aux s Hin :=
match type of Hin with
| False => inversion Hin
| _ \/ _ =>
let Hin' := fresh "Hin" in
(case ( Hin);clear Hin;intro Hin';
[ match type of Hin' with
Rpo.LP.EDS.eq_A ?t ?x =>
match goal with
| |- Rpo.rpo t ?rhs =>
let h1 := fresh "h1" in
destruct (Rpo.equiv_rpo_equiv_2 _ _ Hin' rhs) as [_ h1];
apply h1;prove_rpo
end
end
| prove_all_rpo_aux s Hin' ])
end
with prove_rpo_mul :=
match goal with
| |- Rpo.rpo_mul ?l' ?l =>
let l := eval simpl in l in
let l' := eval simpl in l' in
let res := split_lists (List.nil:list Rpo.T.term) (List.nil:list Rpo.T.term) l' l in
match constr:res with
| (List.nil,?ls,?lc) => fail 0
| (?a::?lg,?ls,?lc) =>
refine (@Rpo.List_mul a lg ls lc l l' _ _ _);[prove_permut|prove_permut|prove_all_rpo_mul]
end
end
with prove_all_rpo_mul :=
let b := fresh "b" in
let Hin := fresh "Hin" in
(intros b Hin;simpl in Hin; prove_all_rpo_mul_aux Hin)
with prove_all_rpo_mul_aux Hin :=
match type of Hin with
| False => tauto
| (?t1 = ?t2)\/?t =>
let Hin' := fresh "Hin" in
(case Hin;intro Hin';[
subst t2;prove_all_rpo_mul_exists|
prove_all_rpo_mul_aux Hin'
])
end
with prove_all_rpo_mul_exists :=
match goal with
| |- exists b' , In b' ?l /\ ?rpo ?b b' => let l := eval simpl in l in prove_all_rpo_mul_exists_aux l
end
with prove_all_rpo_mul_exists_aux l :=
match l with
| List.nil => fail 0
| ?h::?tl =>
(exists h;constructor;[intuition|prove_rpo]) || prove_all_rpo_mul_exists_aux tl
end.
Scheme one_step_ind2 := Induction for Eqt.one_step Sort Prop
with one_step_list_ind2 := Induction for Eqt.one_step_list Sort Prop.
Lemma apply_subst_in :
forall sigma t1 t2 l , In (t1,t2) (map
(fun st : Rpo.T.term * Rpo.T.term =>
(Rpo.T.apply_subst sigma (fst st),
Rpo.T.apply_subst sigma (snd st))) l) ->
exists t1', exists t2', In (t1',t2') l /\ t1 = Rpo.T.apply_subst sigma t1'
/\ t2 = Rpo.T.apply_subst sigma t2'.
Proof.
intros sigma t1 t2 l; induction l as [ | a l IH];intro H;simpl in H.
tauto.
simpl in H;destruct H as [Heq | H'].
destruct a as [t1' t2'];inversion Heq;subst t1 t2;exists t1'; exists t2';simpl in *;repeat split;auto.
destruct (IH H') as [t1' [t2' [h1 [ h2 h3]]]];subst t1 t2;exists t1';exists t2';simpl in *;auto.
Qed.
Lemma In_map_l :
forall (A B:Type) (t1:A) (t2:B) l, In (t1,t2) l ->
In t1 (map (fun st : A*B => fst st) l)/\
In t2 (map (fun st : A*B => snd st) l).
Proof.
induction l as [ | x l IH];intros H;simpl in H.
tauto.
destruct H.
subst x;simpl;auto.
simpl;destruct (IH H);auto.
Qed.
Lemma map_map_fst : forall (A B:Type) (f : A -> B) (l:list (A*A)),
map (@fst B B) (map (fun st => (f (fst st), f (snd st))) l) =
map f (map (@fst A A) l).
Proof.
induction l as [ | x l IH];simpl.
reflexivity.
rewrite IH;reflexivity.
Qed.
Lemma map_map_snd : forall (A B:Type) (f : A -> B) (l:list (A*A)),
map (@snd B B) (map (fun st => (f (fst st), f (snd st))) l) =
map f (map (@snd A A) l).
Proof.
induction l as [ | x l IH];simpl.
reflexivity.
rewrite IH;reflexivity.
Qed.
Lemma one_R_in_rpo :
forall (R:Relation_Definitions.relation Rpo.T.term)
(R_in_rpo:forall x y, R x y -> Rpo.rpo x y),
forall x y, Eqt.one_step R x y -> Rpo.rpo x y.
Proof.
intros R R_in_rpo.
induction 1 using one_step_ind2 with
(P0:= fun l1 l2 (H: Eqt.one_step_list R l1 l2) =>
exists l, exists l', exists x, exists y,
l1 = l++x::l' /\ l2 = l++y::l' /\ Rpo.rpo x y
).
destruct a.
apply Rpo.rpo_subst.
apply R_in_rpo;auto.
destruct IHone_step as [l [l' [x [y h]]]];intuition;subst.
replace Eqt.T.Term with M.Term.
replace (M.Term f (l ++ x :: l')) with (M.replace_at_pos (M.Term f (l ++ x :: l')) x (length l::nil)).
replace (M.Term f (l ++ y :: l')) with (M.replace_at_pos (M.Term f (l ++ x :: l')) y (length l::nil)).
apply Rpo.rpo_add_context;auto.
clear;induction l;simpl in *;auto.
clear;induction l;simpl in *;auto.
injection IHl;intro h;rewrite h;auto.
clear;induction l;simpl in *;auto.
clear;induction l;simpl in *;auto.
injection IHl;intro h;rewrite h;auto.
reflexivity.
exists (nil:list M.term);exists l;exists t1;exists t2;intuition.
destruct IHone_step as [l [l' [x [y h]]]];intuition;subst.
exists (t::l);exists l';exists x;exists y;intuition.
Qed.
Lemma equiv_subst :
forall sigma t s, Rpo.equiv s t ->
Rpo.equiv (M.apply_subst sigma s) (M.apply_subst sigma t).
Proof.
induction t as [ n | f l IH ] using Rpo.T.term_rec3;intros s H.
inversion H;clear H;subst.
constructor.
inversion H; clear H;subst.
constructor 1.
simpl.
constructor.
assumption.
revert IH.
induction H4.
intros IH; simpl;constructor.
intros IH;simpl.
constructor.
apply IH.
simpl;auto.
assumption.
apply IHequiv_list_lex.
intros t H0 s H1.
apply IH;auto.
simpl;auto.
simpl.
constructor 3.
assumption.
revert IH.
induction H4.
intros IH; simpl;constructor.
intros IH;simpl.
rewrite map_app;simpl map.
constructor 2.
apply IH.
apply in_or_app;simpl;auto.
assumption.
rewrite <- map_app;
apply IHpermut.
intros t H0 s H1.
apply IH.
destruct (in_app_or l1 l2 t H0);apply in_or_app;simpl;auto.
auto.
Qed.
Lemma rpo_eq_subst :
forall sigma t s, Rpo.rpo_eq s t ->
Rpo.rpo_eq (M.apply_subst sigma s) (M.apply_subst sigma t).
Proof.
inversion 1;subst.
constructor 1.
apply equiv_subst;auto.
constructor 2.
apply Rpo.rpo_subst;assumption.
Qed.
RPO is compatible with adding context.
Lemma equiv_add_context :
forall p ctx s t, Rpo.equiv s t -> M.is_a_pos ctx p = true ->
Rpo.equiv (M.replace_at_pos ctx s p) (M.replace_at_pos ctx t p).
Proof.
induction p.
simpl;auto.
destruct ctx as [v | f l];[simpl;intros;discriminate|idtac].
intros s t s_equiv_t is_a_pos.
do 2 rewrite M.replace_at_pos_unfold.
case_eq (Rpo.P.status f);intro f_stat.
constructor 2.
exact f_stat.
generalize dependent p.
generalize dependent t.
generalize dependent a.
induction l.
intros a t s_equiv_t p IHp is_a_pos.
simpl;constructor.
intros a0 t s_equiv_t p IHp is_a_pos.
simpl.
destruct a0.
constructor.
apply IHp.
exact s_equiv_t.
exact is_a_pos.
clear;induction l.
constructor.
constructor;auto.
constructor.
constructor.
constructor.
apply IHl.
exact s_equiv_t.
exact IHp.
exact is_a_pos.
constructor 3.
exact f_stat.
generalize dependent p.
generalize dependent t.
generalize dependent a.
induction l.
intros a t s_equiv_t p IHp is_a_pos.
simpl;constructor.
intros a0 t s_equiv_t p IHp is_a_pos.
simpl.
destruct a0.
refine (@Pcons _ _ Rpo.equiv _ _ l (@nil M.term) l _ _).
apply IHp.
exact s_equiv_t.
exact is_a_pos.
simpl.
clear;induction l.
constructor.
change (a::l) with (nil++a::l).
unfold app at 1.
constructor.
constructor.
auto.
change (a :: M.replace_at_pos_list l t a0 p) with (nil++(a :: M.replace_at_pos_list l t a0 p)).
constructor.
constructor.
simpl. apply IHl.
exact s_equiv_t.
exact IHp.
exact is_a_pos.
Qed.
Lemma rpo_eq_add_context :
forall p ctx s t, Rpo.rpo_eq s t -> M.is_a_pos ctx p = true ->
Rpo.rpo_eq (M.replace_at_pos ctx s p) (M.replace_at_pos ctx t p).
Proof.
intros p ctx s t H H0.
destruct H.
constructor 1;apply equiv_add_context;auto.
apply Rpo.Lt.
apply Rpo.rpo_add_context; assumption.
Qed.
Lemma one_R_in_rpo_eq :
forall (R:Relation_Definitions.relation M.term)
(R_in_rpo:forall x y, R x y -> Rpo.rpo_eq x y),
forall x y, Eqt.one_step R x y -> Rpo.rpo_eq x y.
Proof.
intros R R_in_rpo.
induction 1 using one_step_ind2 with
(P0:= fun l1 l2 (H:Eqt.one_step_list R l1 l2) =>
exists l, exists l', exists x, exists y,
l1 = l++x::l' /\ l2 = l++y::l' /\ Rpo.rpo_eq x y
).
destruct a.
apply rpo_eq_subst.
apply R_in_rpo;auto.
destruct IHone_step as [l [l' [x [y h]]]];intuition;subst.
replace Eqt.T.Term with M.Term by reflexivity.
replace (M.Term f (l ++ x :: l')) with (M.replace_at_pos (M.Term f (l ++ x :: l')) x (length l::nil)).
replace (M.Term f (l ++ y :: l')) with (M.replace_at_pos (M.Term f (l ++ x :: l')) y (length l::nil)).
apply rpo_eq_add_context;auto.
clear;induction l;simpl in *;auto.
clear;induction l;simpl in *;auto.
injection IHl;intro h;rewrite h;auto.
clear;induction l;simpl in *;auto.
clear;induction l;simpl in *;auto.
injection IHl;intro h;rewrite h;auto.
exists (nil:list M.term);exists l;exists t1;exists t2;intuition.
destruct IHone_step as [l [l' [x [y h]]]];intuition;subst.
exists (t::l);exists l';exists x;exists y;intuition.
Qed.
Lemma rpo_eq_trans :
forall x y z, Rpo.rpo_eq x y -> Rpo.rpo_eq y z -> Rpo.rpo_eq x z.
Proof.
do 2 inversion 1;subst.
constructor;destruct Rpo.equiv_equiv;eapply equiv_trans;eauto.
constructor 2;rewrite (Rpo.equiv_rpo_equiv_2 x y);auto.
constructor 2;destruct Rpo.equiv_equiv;rewrite (Rpo.equiv_rpo_equiv_1 z y);auto.
constructor 2;apply Rpo.rpo_trans with y;auto.
Qed.
Lemma equiv_refl : forall t, Rpo.equiv t t.
Proof.
destruct Rpo.equiv_equiv;auto.
Qed.
Lemma equiv_sym : forall t t', Rpo.equiv t t' -> Rpo.equiv t' t.
Proof.
destruct Rpo.equiv_equiv;intros t t';auto.
Qed.
Lemma equiv_trans : forall t t' t'', Rpo.equiv t t' -> Rpo.equiv t' t'' -> Rpo.equiv t t''.
Proof.
destruct Rpo.equiv_equiv;intros t t';red in equiv_trans;eauto.
Qed.
Add Relation Rpo.T.term Rpo.equiv
reflexivity proved by equiv_refl
symmetry proved by equiv_sym
transitivity proved by equiv_trans
as equiv_rel.
Add Morphism Rpo.rpo : rpo_morph .
Proof.
intros x1 x2 H x0 x3 H0.
split;intro H1.
rewrite <- (Rpo.equiv_rpo_equiv_1 _ _ H0);
rewrite <- (Rpo.equiv_rpo_equiv_2 _ _ H);exact H1.
rewrite (Rpo.equiv_rpo_equiv_1 _ _ H0);
rewrite (Rpo.equiv_rpo_equiv_2 _ _ H);exact H1.
Qed.
Add Morphism Rpo.rpo_eq : rpo_eq_morph .
Proof.
intros x1 x2 H x0 x3 H0.
split;intro H1.
rewrite <- (Rpo.equiv_rpo_equiv_3 _ _ H0);
rewrite <- (Rpo.equiv_rpo_equiv_4 _ _ H);exact H1.
rewrite (Rpo.equiv_rpo_equiv_3 _ _ H0);
rewrite (Rpo.equiv_rpo_equiv_4 _ _ H);exact H1.
Qed.
Import Relations.
Require Import terminaison.
Lemma wf_prec_implies_wf_R : forall (R:relation M.term)
(R_in_rpo: forall x y, R x y -> Rpo.rpo x y), well_founded Rpo.P.prec ->
well_founded (Eqt.one_step R).
Proof.
intros R R_in_rpo H.
intro x.
apply Inclusion.wf_incl with Rpo.rpo.
unfold inclusion.
intros.
eapply one_R_in_rpo;eauto.
apply Rpo.wf_rpo;assumption.
Qed.
Ltac prove_prec_wf :=
let a := fresh "a" in
(intro a;destruct a;
repeat (constructor;inversion 1;subst)).
End rpo_facts.