proposition: Lemma ddp_list_is_sound : forall R rule_list, (forall l r, R r l <-> In (l,r) rule_list) -> forall is_def, (forall f, is_def f = true <-> defined R f) -> forall x y, In (y,x) (ddp_list is_def rule_list) -> ddp R x y.
proof: Proof. assert (H' : forall Rlist is_def x y, In (y, x) (ddp_list is_def Rlist) -> (exists t2, exists f2, exists l2, exists p, x = Term f2 l2 /\ In (y,t2) Rlist /\ subterm_at_pos t2 p = Some (Term f2 l2) /\ is_def f2 = true ) /\ (forall i p, subterm_at_pos y (i :: p) <> Some x)). intros Rlist is_def x y H. induction Rlist as [ | [l1 r1] Rlist]. contradiction. unfold ddp_list in H; simpl in H. rewrite <- app_nil_end in H. replace (ddp_rule is_def l1 r1) with (nil ++ ddp_rule is_def l1 r1) in H; [ | apply eq_refl]. rewrite fold_left_in_acc_split in H; destruct H as [H | H]. destruct (IHRlist H) as [[t2 [f2 [ l2 [p [H1 [H2 H3]]]]]] H4]. split; [ | assumption]. exists t2; exists f2; exists l2; exists p; split. assumption. split; [right | ]; assumption. clear IHRlist. unfold ddp_rule in H. rewrite in_map_iff in H. destruct H as [x' [H1 H2]]. injection H1; clear H1; intros; subst. destruct x as [x | g k]. apply False_rect. induction r1 using term_rec3. contradiction. simpl in H2; rewrite fold_left_defined_subterms_unfold in H2. destruct H2 as [H2 | H2]. induction l as [ | t l]. contradiction. simpl in H2; rewrite fold_left_defined_subterms_unfold in H2. destruct H2 as [H2 | H2]. apply IHl; [ | assumption]. intros u u_in_l; apply (H u); right; assumption. apply (H _ (or_introl _ (eq_refl _))); assumption. revert H2; case (is_def f). case (eq_bool y (Term f l)). intros [H1 | H2]; [discriminate | contradiction]. case (is_subterm (Term f l) y). contradiction. intros [H1 | H2]; [discriminate | contradiction]. contradiction. destruct (defined_subterms_is_sound _ _ _ _ _ H2) as [Dg [[p Sub] K2]]. split; [ | assumption]. exists r1; exists g; exists k; exists p. split. apply eq_refl. split. left; apply eq_refl. split; assumption. intros R Rlist Rlist_ok is_def is_def_ok x y H. destruct (H' _ _ _ _ H) as [[t2 [f2 [l2 [p [H1 [H2 [H3 H4]]]]]]] H5]. split; [ | assumption]. subst x; constructor 1 with t2 p. rewrite Rlist_ok; assumption. assumption. rewrite <- is_def_ok; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)