# 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. ```