proposition: Lemma usablerules_dec : forall R Rlist, (forall l r, R r l <-> In (l,r) Rlist) -> forall P Plist, (forall u v, P v u <-> In (u,v) Plist) -> {URlist | forall l r, UsableRules R P r l <-> In (l,r) URlist}.
proof: Proof. intros R Rlist Rlist_ok P Plist; revert P; induction Plist as [ | [u v] Plist]; intros P Plist_ok. exists nil; intros l r; split; intro H. destruct H as [u [v [H _]]]; rewrite Plist_ok in H; assumption. contradiction. set (P' := fun b a => P b a /\ In (a,b) Plist). assert (Plist_ok' : forall a b, P' b a <-> In (a,b) Plist). intros a b; split; intro H. destruct H as [_ H]; assumption. split; [rewrite Plist_ok; right | ]; assumption. destruct (IHPlist _ Plist_ok') as [URlist URlist_ok]. destruct (usable_dec _ _ Rlist_ok v) as [Uv Uv_ok]. exists (Uv ++ URlist); intros l r; split; intro H. destruct H as [s [t [H1 H2]]]. rewrite Plist_ok in H1; simpl in H1; destruct H1 as [H1 | H1]. injection H1; clear H1; intros; subst. apply in_or_app; left; rewrite <- Uv_ok; assumption. apply in_or_app; right; rewrite <- URlist_ok; exists s; exists t; split; [ rewrite Plist_ok' | ]; assumption. destruct (in_app_or _ _ _ H) as [H1 | H1]; clear H. rewrite <- Uv_ok in H1. exists v; exists u; split; [rewrite Plist_ok; left; apply eq_refl | assumption]. rewrite <- URlist_ok in H1; destruct H1 as [s [t [H1 H2]]]. exists s; exists t; split; [ rewrite Plist_ok; right; rewrite <- Plist_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)