Library examples.cime_trace.equational_extension
Require Import List.
Require Import Bool.
Require term.
Module Make(M:term.Term).
Import M.
Definition term_eq (x y:term) : bool :=
if eq_term_dec x y then true else false
.
Lemma term_eq_ok : forall x y, term_eq x y = true -> x = y.
Proof.
unfold term_eq.
intros x y.
case (eq_term_dec x y).
tauto.
intros;discriminate.
Qed.
Lemma term_eq_refl : forall x, term_eq x x = true.
Proof.
unfold term_eq.
intros x.
case (eq_term_dec x x).
tauto.
intro abs;elim abs;reflexivity.
Qed.
Definition ST (x y:term) : Prop :=
match y with
| (Term f l) => existsb (term_eq x) l = true
| _ => False
end.
Lemma existsb_term_eq_In : forall x l, existsb (term_eq x) l = true -> In x l.
induction l.
simpl;intro abs;discriminate.
intro H0; simpl in H0;case (orb_prop _ _ H0);clear H0;intro H0.
rewrite (term_eq_ok _ _ H0);simpl;auto 100.
simpl;auto.
Qed.
Lemma In_existsb_term_eq :
forall (x : term) (l : list term), In x l -> existsb (term_eq x) l = true .
Proof.
induction l;simpl.
tauto.
inversion_clear 1;subst.
apply orb_true_intro;left;apply term_eq_refl.
apply orb_true_intro;right;auto.
Qed.
Lemma Well_Founded_ST : well_founded ST.
Proof.
intro x;induction x using term_rec3; split; simpl;intros.
exact (False_ind _ H).
induction l.
simpl in H0;discriminate.
simpl in H0.
case (orb_prop _ _ H0);clear H0;intro H0.
rewrite (term_eq_ok _ _ H0);auto 100.
apply H;simpl;auto 100.
apply H.
simpl;right;apply existsb_term_eq_In;auto.
Qed.
Section Monotony.
Variable R : term->term->Prop.
Fixpoint R_list (l l':list term) {struct l} : Prop :=
match (l,l') with
| (t::l,t'::l') =>
(R t t'/\ l = l')\/ (t = t' /\ R_list l l')
| _ => False
end.
Lemma Acc_R_list : forall l, (forall x, In x l -> Acc R x) -> Acc R_list l.
Proof.
induction l.
intros _;split. destruct y; simpl; tauto.
intro H.
assert (Acc R_list l).
apply IHl;intros;apply H;simpl;auto.
assert (Acc R a).
apply H;simpl;auto.
clear - H0 H1.
pattern a;apply Acc_ind with (2:=H0).
clear l H0.
pattern a;apply Acc_ind with (2:=H1).
clear.
intros a H H0 l H1 H2.
split;simpl.
destruct y. simpl;tauto.
simpl.
inversion 1;clear H3.
destruct H4;subst.
apply H0;auto.
intros l' H4.
apply Acc_inv with (a::l');auto.
simpl;auto.
destruct H4;subst.
apply H2;auto.
Qed.
Lemma R_list_Acc : forall l, Acc R_list l -> (forall x, In x l -> Acc R x) .
Proof.
intros l H.
pattern l;apply Acc_ind with (2:=H);clear.
intros l H H0 t H1.
clear H.
induction l;simpl in *.
tauto.
inversion_clear H1;subst.
split.
intros.
apply H0 with (y::l);
simpl;auto.
apply IHl;auto.
intros l' H1.
intros t' H2.
apply H0 with (a::l');
simpl;auto.
Qed.
Lemma existsb_app : forall x ls le, existsb (term_eq x) le = true -> existsb (term_eq x) (ls++le) = true.
Proof.
induction ls.
simpl;tauto.
simpl.
intros le H.
apply orb_true_intro;auto.
Qed.
Inductive Monotone : Prop :=
Monotone_c : (forall f l l', R_list l l' -> R (Term f l) (Term f l')) ->
Monotone.
Lemma STSN : Monotone -> forall x : term , Acc R x -> forall t : term , ST t x -> Acc R t.
Proof.
intros Hmon x HSNx.
induction HSNx;auto.
intros.
split; intros y.
destruct Hmon;destruct x;simpl in H1.
exact (False_ind _ H1).
intros H3.
assert (exists ls,exists le,l=ls++t::le).
clear - H1;induction l.
simpl in H1;discriminate.
simpl in H1. case (orb_prop _ _ H1);clear H1;intro H1.
exists (@nil term);exists l;simpl;rewrite (term_eq_ok _ _ H1);reflexivity.
destruct (IHl H1) as [ls [le H]].
exists (a::ls);exists le;simpl;rewrite H;reflexivity.
destruct H4 as [ls [le Hls_le]];subst l.
apply H0 with (Term a (ls ++ y :: le)).
apply H2; clear - H3;induction ls;simpl;auto.
simpl; apply existsb_app;simpl; apply orb_true_intro;left;apply term_eq_refl.
Qed.
Require terminaison.
Require Relation_Operators.
Lemma STPSN : Monotone -> forall x, (forall y : term, ST y x -> Acc R y) ->
forall t, (Relation_Operators.clos_trans _ ST t x) -> Acc R t.
Proof.
intros Hmon x Acc_x t t_st_x.
induction t_st_x;auto.
apply IHt_st_x1.
intros y0 H.
eapply STSN with y;auto.
Qed.
Ltac find_path sub t :=
match t with
| sub => constr:(@nil term)
| Var _ => constr:(@None term)
| Term _ ?l =>
find_path_list sub l
end
with find_path_list sub l :=
match l with
| nil => constr:(@None term)
| ?t::?l =>
match find_path sub t with
| None => find_path_list sub l
| ?e => constr:(t::e)
end
end
.
Ltac prove_STP_aux l :=
match l with
| nil => constructor 1;simpl;auto 100 using term_eq_refl with bool
| ?t'::?l =>
constructor 2 with t';[prove_STP_aux l | constructor 1;simpl;auto 100 using term_eq_refl with bool]
end.
Ltac prove_STP :=
match goal with
|- Relation_Operators.clos_trans _ _ ?t ?t' =>
let l := find_path t t' in
prove_STP_aux l
end.
Definition STb (x y:term) : bool :=
match y with
| (Term f l) => existsb (term_eq x) l
| _ => false
end.
Fixpoint STPb (x y:term) {struct y} : bool :=
match y with
| (Term f l) => STb x y || existsb (STPb x) l
| _ => false
end.
Lemma STb_equiv : forall x y, ST x y <-> STb x y = true.
Proof.
clear R.
split.
unfold ST;
destruct y;simpl;tauto.
destruct y;simpl;try tauto.
discriminate.
Qed.
Lemma STP_equiv : forall x y, STPb x y = true -> Relation_Operators.clos_trans _ ST x y.
Proof.
clear R.
intros x y.
induction y using term_rec3.
simpl.
intro;discriminate.
simpl. intro H';case (orb_prop _ _ H');clear H'.
intro;constructor;simpl;assumption.
intros.
assert (exists y, exists ls, exists le, l = ls ++ y :: le /\ STPb x y = true).
clear H.
induction l.
simpl in H0;discriminate.
simpl in H0.
case (orb_prop _ _ H0);clear H0.
intros H.
exists a;exists (@nil term);exists l.
split;auto with *.
intros H.
destruct (IHl H) as [y [ls [le [h1 h2]]]].
subst.
exists y;exists (a::ls); exists le;split;auto with *.
destruct H1 as [y [ls [le [h1 h2]]]].
subst.
constructor 2 with y.
apply H. auto with *. assumption.
constructor.
unfold ST;apply In_existsb_term_eq;auto with *.
Qed.
Inductive RST : term -> term -> Prop :=
| RST_c :
forall f l l',
R_list l l' -> RST (Term f l) (Term f l').
Lemma RSTSN_symb : forall f l, (forall x, In x l -> Acc R x) -> Acc RST (Term f l).
Proof.
intros f l H.
generalize (Acc_R_list _ H).
clear H;intro H.
pattern l;apply Acc_ind with (2:=H).
clear.
intros l H H0.
split.
inversion 1;subst.
apply H0.
assumption.
Qed.
Lemma RSTSN : forall x : term , ( forall y : term , ST y x -> Acc R y )-> Acc RST x.
Proof.
intros;match goal with x:term,H:_|- _ => destruct x end.
split;inversion 1.
split; inversion 1; subst.
apply RSTSN_symb.
clear -H3 H. intros x H0.
generalize dependent l.
induction l0;simpl in *;try tauto.
destruct l;try tauto.
intros H H3.
inversion_clear H0;subst.
inversion_clear H3;subst.
destruct H0;subst.
apply Acc_inv with (2:=H0).
apply H;simpl;apply orb_true_intro;left;apply term_eq_refl.
destruct H0;subst.
apply H;simpl;apply orb_true_intro;left;apply term_eq_refl.
inversion_clear H3;destruct H0;subst.
apply H;apply In_existsb_term_eq;simpl;auto with *.
apply IHl0 with l.
assumption.
intros y H0;apply H;simpl;apply orb_true_intro;right;assumption.
assumption.
Qed.
End Monotony.
End Make.