proposition: Lemma interp_subst : forall l sigma, Interp_dom (apply_subst sigma l) -> {sigma' | forall x, In x (var_list l) -> Interp (apply_subst sigma (Var x)) (apply_subst sigma' (Var x)) }.
proof: Proof. intros l sigma Acc_ls. assert (Acc_sigma : forall x, In x (var_list l) -> Interp_dom (apply_subst sigma (Var x))). intros x x_in_l; assert (x_mem_l : mem (@eq _) x (var_list l)). apply in_impl_mem; trivial. destruct (var_in_subterm2 x l x_mem_l) as [p Sub]. apply interp_dom_subterm with (apply_subst sigma l) p; trivial. generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos l p sigma). rewrite Sub; exact (fun p => p). set (varl := var_list l) in *; clearbody varl. destruct (remove_garbage_subst sigma) as [tau [H1 [H2 H3]]]. assert (H4 : { tau' : list (variable * (term * term)) | tau = map (fun xtt' => match xtt' with (x,(t,t')) => (x,t) end) tau' /\ (forall x t t', In x varl -> In (x,(t,t')) tau' -> Interp t t') }). assert (Acc_tau : forall x : variable, In x varl -> Interp_dom (apply_subst tau (Var x))). intros; simpl; rewrite <- H1; apply Acc_sigma; assumption. revert H2 H3 Acc_tau; clear -R_reg Rlist_ok P Plist Plist_ok Gdef'; induction tau as [ | [v vval] tau]; intros H2 H3 Acc_tau. exists nil; split; [apply eq_refl | intros; contradiction]. destruct IHtau as [tau' [K1 K2]]. intros x xval xval_in_tau; generalize (H2 _ _ (or_intror _ xval_in_tau)); simpl. generalize (eq_var_bool_ok x v); case (eq_var_bool x v); [intro x_eq_v | intros _; trivial]. apply False_rect. destruct (In_split _ _ xval_in_tau) as [tau' [tau'' H4]]. apply (H3 v x vval xval nil tau' tau''); subst; trivial. intros x y xval yval tau1 tau2 tau3 H4; apply (H3 x y xval yval ((v,vval) :: tau1) tau2 tau3); subst; trivial. intros x x_in_l; generalize (Acc_tau x x_in_l); simpl. assert (Acc_x : Interp_dom (Var x)). intros [ | i p] f l Sub; discriminate. generalize (eq_var_bool_ok x v); case (eq_var_bool x v); [intro x_eq_v | intros _; trivial]. intros _; subst x; generalize (find_mem _ _ eq_var_bool_ok v tau). case (find eq_var_bool v tau). intros t K; destruct (K _ (eq_refl _)) as [v' [tau1 [tau2 [K' K'']]]]. apply False_rect. apply (H3 v v' vval t nil tau1 tau2); subst; trivial. intros; assumption. generalize (mem_bool_ok _ _ eq_var_bool_ok v varl); case (mem_bool eq_var_bool v varl). intro v_mem_varl; assert (v_in_varl : In v varl). apply mem_impl_in with (@eq _); trivial. assert (Acc_vval : Interp_dom vval). generalize (Acc_tau _ v_in_varl); simpl; rewrite eq_var_bool_refl; exact (fun p => p). destruct (interp_defined _ (interp_well_defined _ Acc_vval)) as [vval' K]. exists ((v,(vval,vval')) :: tau'); split. simpl; rewrite K1; apply eq_refl. intros x t t' x_in_varl [x_eq_v | xtt'_in_tau']; [injection x_eq_v; intros; subst; assumption | apply (K2 x); assumption]. intro v_not_in_varl; exists ((v,(vval,vval)) :: tau'); split. simpl; rewrite K1; apply eq_refl. intros x t t' x_in_varl [x_eq_v | xtt'_in_tau']; [ injection x_eq_v; intros; subst; apply False_rect; apply v_not_in_varl; apply in_impl_mem; trivial | apply (K2 x); assumption]. destruct H4 as [tau' [H4 H5]]. exists (map (fun xtt' => match xtt' with (x,(t,t')) => (x,t') end) tau'). intros x x_in_varl; simpl; rewrite (H1 x). rewrite H4. generalize (find_map eq_var_bool (fun y : (term * term) => fst y) x tau') (find_map eq_var_bool (fun y : (term * term) => snd y) x tau') (find_mem _ _ eq_var_bool_ok x tau'). rewrite (map_eq (fun xval0 : variable * (term * term) => (fst xval0, fst (snd xval0))) (fun xtt' : variable * (term * term) => let (x0, y) := xtt' in let (t, _) := y in (x0, t)) tau' (fun xtt' _ => match xtt' with (x,(t,_)) => eq_refl (x,t) end)). rewrite (map_eq (fun xval0 : variable * (term * term) => (fst xval0, snd (snd xval0))) (fun xtt' : variable * (term * term) => let (x0, y) := xtt' in let (_, t'0) := y in (x0, t'0)) tau' (fun xtt' _ => match xtt' with (x,(_,t')) => eq_refl (x,t') end)). case (find eq_var_bool x tau'). intros [xval xval']; simpl. intros K1 K2 K3; rewrite K1, K2. destruct (K3 _ (eq_refl _)) as [x' [tau1 [tau2 [K4 K5]]]]. subst x'; apply (H5 x); trivial. subst tau'; apply in_or_app; right; left; apply eq_refl. intros K1 K2 _; rewrite K1, K2; apply Vcase. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)