proposition: Lemma rough_unif_is_ok : forall (R dpR : relation term) mark is_def, (forall x t, ~R t (Var x)) -> (forall f, defined R f -> is_def f = true) -> (forall u v, dpR v u -> dp R v u) -> forall u v u' v', are_connected (mrel mark dpR) R (u',v') (u,v) -> connect_approx is_def v u' = true.
proof: Proof. intros R dpR mark is_def R_var is_def_ok dpR_in_dpR _u _v _u' _v' H. destruct H as [sigma [sigma' [_H1 [_H2 H3]]]]. inversion _H1 as [v u H1]; clear _H1; subst. inversion _H2 as [v' u' H2]; clear _H2; subst. assert (K1 := dpR_in_dpR _ _ H1); clear H1. assert (K2 := dpR_in_dpR _ _ H2); clear H2. inversion K1 as [t1 t2 p f2 l2 H Sub Df2]. inversion K2 as [t1' t2' p' f2' l2' H' Sub' Df2']. subst; destruct u' as [x | g k]. apply False_rect; apply (R_var _ _ H'). simpl in H3; destruct H3 as [H3 H4]. simpl; rewrite <- H3. simpl; rewrite eq_symb_bool_refl. assert (K0 : forall k' l' sigma sigma', refl_trans_clos (one_step_list (one_step R)) (map (apply_subst sigma') k') (map (apply_subst sigma) l') -> rough_unif_list is_def l' k' = true). clear -R_var is_def_ok. intro k; pattern k; apply (list_rec3 size); clear k. intro n; induction n as [ | n]; intros k Sk l sigma sigma' H; destruct k as [ | s k]. destruct l as [ | t l]. apply eq_refl. assert (L:= refl_trans_clos_one_step_list_length_eq H). discriminate. absurd (1 <= 0). intro Abs; inversion Abs. apply Nat.le_trans with (list_size size (s :: k)); trivial. apply Nat.le_trans with (size s). apply size_ge_one. simpl; apply Nat.le_add_r. destruct l as [ | t l]. apply eq_refl. assert (L:= refl_trans_clos_one_step_list_length_eq H). discriminate. destruct l as [ | t l]. assert (L:= refl_trans_clos_one_step_list_length_eq H). discriminate. simpl in H; rewrite refl_trans_clos_one_step_list_head_tail in H. destruct H as [H' H]. assert (Sk' : list_size size k <= n). apply le_S_n. apply Nat.le_trans with (list_size size (s :: k)); trivial. simpl; refine (proj1 (Nat.add_le_mono_r 1 (size s) _) _). apply size_ge_one. assert (Ss : size s <= S n). apply Nat.le_trans with (list_size size (s :: k)); trivial. simpl; apply Nat.le_add_r. simpl; rewrite IHn with k l sigma sigma'; trivial. clear l k Sk Sk' H. rewrite rough_unif_unfold. destruct t as [x | f l]. apply eq_refl. destruct s as [x | g k]. apply eq_refl. simpl; simpl in H'. inversion H'; clear H'; subst. destruct (is_def f). apply eq_refl. rewrite eq_symb_bool_refl. simpl. rewrite size_unfold in Ss; generalize (le_S_n _ _ Ss); clear Ss; intro Ss. rewrite IHn with k l sigma sigma'; trivial. rewrite H2; left. assert (Df : defined R f \/ (f = g /\ refl_trans_clos (one_step_list (one_step R)) (map (apply_subst sigma') k) (map (apply_subst sigma) l))). set (l' := map (apply_subst sigma) l) in *; clearbody l'. set (k' := map (apply_subst sigma') k) in *; clearbody k'. set (fl := Term f l') in *. assert (Hf := eq_refl fl). unfold fl at 2 in Hf; clearbody fl; revert Hf. set (gk := Term g k') in *. assert (Hg := eq_refl gk). unfold gk at 2 in Hg; clearbody gk; revert Hg. clear Ss; revert f g l' k'; induction H; intros f g l' k'. inversion H; clear H; subst. inversion H0; clear H0; subst. destruct t2 as [v | f2 l2]. apply False_rect; apply (R_var _ _ H). intros _ H1; simpl in H1; injection H1; clear H1; intros; subst. left; constructor 1 with l2 t1; assumption. intros H1 H2; injection H1; injection H2; intros; subst; subst; right; split. apply eq_refl. right; left; assumption. intros H1 H2. inversion H; clear H; subst. inversion H3; clear H3; subst. destruct t2 as [v | f2 l2]. apply False_rect; apply (R_var _ _ H1). destruct (IHtrans_clos f f2 l' (map (apply_subst sigma0) l2) (eq_refl _) (eq_refl _)) as [Df | [f_eq_f2 K]]. left; assumption. subst f2; left; constructor 1 with l2 t1; assumption. destruct (IHtrans_clos f f0 l' l2 (eq_refl _) (eq_refl _)) as [Df | [f_eq_f0 K]]. left; assumption. subst f0; injection H4; intros; right; split. assumption. subst; apply refl_trans_clos_is_trans with l2; trivial. right; left; assumption. destruct Df as [Df | [f_eq_g K]]. rewrite (is_def_ok f Df). apply eq_refl. subst g; destruct (is_def f). apply eq_refl. simpl; rewrite eq_symb_bool_refl. rewrite size_unfold in Ss; generalize (le_S_n _ _ Ss); clear Ss; intro Ss. rewrite IHn with k l sigma sigma'; trivial. apply K0 with sigma sigma'; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)