proposition: Lemma idp_criterion_aux : forall R, (forall x t, ~ (R t (Var x))) -> (forall s t, R s t -> forall x, In x (var_list s) -> In x (var_list t)) -> (forall f, {constructor R f} + {defined R f}) -> forall t, Acc (idp_step R) t -> (forall s, direct_subterm s t -> Acc (P_step R (inner R)) s) -> Acc (P_step R (inner R)) t.
proof: Proof. intros R HR RR CD. assert (Acc_var : forall x, Acc (P_step R (inner R)) (Var x)). intro x; apply Acc_intro; intros s H; inversion H; subst. inversion H1; subst. destruct t2 as [v2 | ]. absurd (R t1 (Var v2)); trivial; apply HR. discriminate. intros t Acc_t; induction Acc_t as [t Acc_t IH]. intros Acc_l; destruct t as [x | f l]. apply Acc_var. simpl in Acc_l; rewrite acc_one_step_list in Acc_l; revert IH. induction Acc_l as [l Acc_l IHl]; intros IH'. assert (Acc_l' : forall t, In t l -> Acc (P_step R (inner R)) t). rewrite acc_one_step_list; apply Acc_intro; exact Acc_l. apply Acc_intro; intros s H; destruct s as [x1 | f1 l1]. apply Acc_var. inversion H as [t s Hnf H' | f' lt ls H']; clear H; subst. inversion H' as [t1 t2 sigma t1_R_t2 H1 H2]; clear H'. destruct t2 as [x | g k]. absurd (R t1 (Var x)); trivial; apply HR. simpl in H2; injection H2; clear H2; intros; subst g l. assert (H'' : forall n t, size (apply_subst sigma t) <= n -> (exists p, subterm_at_pos t1 p = Some t) -> Acc (P_step R (inner R)) (apply_subst sigma t)). intro n; induction n as [ | n]. intros t St; absurd (1 <= 0); auto with arith; apply Nat.le_trans with (size (apply_subst sigma t)); trivial; apply size_ge_one. intros [x | g h] St [p H'']. apply var_P_acc with k; trivial. assert (H : In x (var_list (Term f k))). apply RR with t1; trivial. apply var_in_subterm with (Var x) p; trivial. simpl; left; trivial. rewrite var_list_unfold in H; trivial. assert (Acc_h : forall t, In t h -> Acc (P_step R (inner R)) (apply_subst sigma t)). intros t t_in_h; destruct (In_split _ _ t_in_h) as [h' [h'' K]]; subst h. apply IHn. apply le_S_n; refine (Nat.le_trans _ _ _ _ St); apply size_direct_subterm; trivial. simpl; rewrite map_app; apply in_or_app; right; left; trivial. exists (p ++ (length h' :: nil)). generalize t1 H''; clear t1 H'' H1 t1_R_t2 IHn; induction p as [ | i p]. intros t1 H''; simpl in H''; injection H''; intros; subst; simpl. rewrite nth_error_at_pos; trivial. intros t1 H''; simpl; simpl in H''; destruct t1 as [ | g1 k1]. discriminate. destruct (nth_error k1 i) as [ti | ]. apply IHp; trivial. discriminate. destruct (CD g) as [Cg | Dg]. simpl; apply P_acc_subterms; trivial. intros t t_in_map_h; rewrite in_map_iff in t_in_map_h. destruct t_in_map_h as [t' [H''' t'_in_h]]; subst; apply Acc_h; trivial. destruct (subterm_at_pos_dec_alt (Term f k) (Term g h)) as [[q Sub] | not_Sub]. destruct q as [ | i q]. apply IH'. apply IDp_step with (map (apply_subst sigma) k). left. replace (Term f (map (apply_subst sigma) k)) with (apply_subst sigma (Term f k)); trivial. apply Idp; trivial. apply instance; apply Dp with t1 p; trivial. simpl; intros t t_in_map_h; rewrite in_map_iff in t_in_map_h. destruct t_in_map_h as [t' [H''' t'_in_h]]; subst; apply Acc_h; trivial. simpl in Sub. generalize (nth_error_ok_in i k); destruct (nth_error k i) as [ti | ]. intro H; destruct (H _ (eq_refl _)) as [k1 [k2 [L H']]]. apply P_acc_subterms_3 with q (apply_subst sigma ti). apply Acc_l'. rewrite in_map_iff; exists ti; split; trivial. subst; apply in_or_app; right; left; trivial. generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos ti q sigma). rewrite Sub; trivial. discriminate. apply IH'. apply IDp_step with (map (apply_subst sigma) k). left. replace (Term f (map (apply_subst sigma) k)) with (apply_subst sigma (Term f k)); trivial. apply Idp; trivial. apply instance; apply Dp with t1 p; trivial. intros s s_in_h; simpl in s_in_h. rewrite in_map_iff in s_in_h. destruct s_in_h as [u [H2 u_in_h]]; subst. apply Acc_h; trivial. apply (H'' (size (Term f1 l1))). rewrite H1; apply le_n. exists (@nil nat); simpl; trivial. apply IHl; trivial. intros t H; apply Acc_t. inversion H; subst. apply IDp_step with l2; trivial. apply refl_trans_clos_is_trans with l1; trivial. right; left; assumption. intros s H'' H'''; apply IH'; trivial. inversion H''; subst. apply (IDp_step R f l l2 s); trivial. apply refl_trans_clos_is_trans with l1; trivial; right; left; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)