proposition: Lemma usable_dec : forall R Rlist, (forall l r, R r l <-> In (l,r) Rlist) -> forall t, {URlist | forall r l, Usable R t r l <-> In (l,r) URlist}.
proof: Proof. intros R Rlist Rlist_ok t. destruct (symb_sup_list _ _ Rlist_ok) as [Slist Slist_ok]. assert (SR_dec := refl_trans_clos_dec _ F.Symb.eq_bool_ok _ _ Slist_ok). unfold Usable; set (SR := refl_trans_clos (symb_sup R)) in *; clearbody SR; clear Slist Slist_ok. revert R Rlist_ok; induction Rlist as [ | [l r] Rlist]; intros R Rlist_ok. exists nil; intros r l; split; intro H. destruct H as [H _]; rewrite Rlist_ok in H; assumption. contradiction. set (R' := fun b a => R b a /\ In (a,b) Rlist). assert (Rlist_ok' : forall a b, R' b a <-> In (a,b) Rlist). intros a b; split; intro H. destruct H as [_ H]; assumption. split; [rewrite Rlist_ok; right | ]; assumption. destruct (IHRlist _ Rlist_ok') as [URlist URlist_ok]. destruct l as [x | f l]. exists URlist; intros u v; split; intro H. destruct H as [H1 H2]; rewrite Rlist_ok in H1; simpl in H1; destruct H1 as [H1 | H1]. injection H1; clear H1; intros; subst. contradiction. rewrite <- URlist_ok; split; [rewrite Rlist_ok' | ]; assumption. rewrite <- URlist_ok in H; destruct H as [H1 H2]; split; [ rewrite Rlist_ok; right; rewrite <- Rlist_ok' | ]; assumption. assert (split_case : {f0 : symbol | symb_in_term f0 t = true /\ SR f0 f}+{forall f0, ~(symb_in_term f0 t = true /\ SR f0 f)}). case_eq (filter (fun g => if SR_dec g f then true else false) (symb_list t)). intro H; right; intros g [g_in_t Sgf]. assert (g_in_nil : In g nil). rewrite <- H; rewrite filter_In; split. rewrite symb_list_ok; assumption. destruct (SR_dec g f); [apply eq_refl | absurd (SR g f); assumption]. contradiction g_in_nil. intros g k H; left; exists g. assert (g_in_gk : In g (g :: k)). left; apply eq_refl. rewrite <- H in g_in_gk; rewrite filter_In in g_in_gk; destruct g_in_gk as [g_in_t Sgf]; split. rewrite <- symb_list_ok; assumption. destruct (SR_dec g f); [assumption | discriminate]. destruct split_case as [[g [g_in_t Sgf]] | Ko]. exists ((Term f l,r) :: URlist); intros u v; split; intro H. destruct H as [H1 H2]. rewrite Rlist_ok in H1; simpl in H1; destruct H1 as [H1 | H1]. left; assumption. right; rewrite <- URlist_ok; split; [rewrite Rlist_ok' | ]; assumption. simpl in H; destruct H as [H | H]. injection H; clear H; intros; subst; split. rewrite Rlist_ok; left; apply eq_refl. exists g; split; assumption. rewrite <- URlist_ok in H; destruct H as [H1 H2]; split; [ rewrite Rlist_ok; right; rewrite <- Rlist_ok' | ]; assumption. exists URlist; intros u v; split; intro H. destruct H as [H1 H2]; rewrite Rlist_ok in H1; simpl in H1; destruct H1 as [H1 | H1]. injection H1; clear H1; intros; subst. destruct H2 as [g H2]; apply False_rect; apply (Ko g); assumption. rewrite <- URlist_ok; split; [rewrite Rlist_ok' | ]; assumption. rewrite <- URlist_ok in H; destruct H as [H1 H2]; split; [ rewrite Rlist_ok; right; rewrite <- Rlist_ok' | ]; assumption. Defined.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)