proposition: Lemma remove_garbage_subst : forall sigma : substitution, {sigma' : substitution | (forall x, find eq_var_bool x sigma = find eq_var_bool x sigma') /\ (forall x val, In (x,val) sigma' -> find eq_var_bool x sigma' = Some val) /\ (forall x y val val' (tau tau' tau'' : substitution), sigma' = tau ++ (x,val) :: tau' ++ (y,val') :: tau'' -> x <> y)}.
proof: Proof. fix remove_garbage_subst 1. intro sigma; case sigma; clear sigma. exists nil; repeat split. intros x val Abs; elim Abs. intros x y val val' tau tau' tau''; case tau; clear tau. intro Abs; discriminate. intros p tau Abs; discriminate. intros p sigma; case p; clear p; intros x val. destruct (remove_garbage_subst sigma) as [sigma' [H1 [H2 H3]]]. case_eq (find eq_var_bool x sigma'). intros val' H; destruct (find_mem _ _ X.eq_bool_ok _ _ H) as [x' [sigma1 [sigma2 [H' H'']]]]. exists ((x,val) :: sigma1 ++ sigma2); subst x'; repeat split. intros y; simpl; case_eq (eq_var_bool y x); [intro y_eq_x | intro x_diff_y]; [trivial | idtac]. rewrite (H1 y); rewrite H''; clear sigma' H1 H2 H3 H H''; induction sigma1 as [ | [x1 val1] sigma1]; simpl. rewrite x_diff_y; reflexivity. case_eq (eq_var_bool y x1); [intro y_eq_x1 | intro y_diff_x1]; [idtac | apply IHsigma1]; trivial. simpl; intros y val'' [H4 | H4]. injection H4; clear H4; intros; subst. rewrite eq_var_bool_refl; reflexivity. case_eq (eq_var_bool y x); [intro y_eq_x | intro y_diff_x]. destruct (in_app_or _ _ _ H4) as [H5 | H5]; destruct (In_split _ _ H5) as [tau1 [tau2 H6]]; subst. absurd (y = x). apply (H3 y x val'' val' tau1 tau2 sigma2); rewrite <- ass_app; trivial. generalize (X.eq_bool_ok y x); rewrite y_eq_x; intro y_eq_x'; exact y_eq_x'. absurd (x = y). apply (H3 x y val' val'' sigma1 tau1 tau2); trivial. generalize (X.eq_bool_ok y x); rewrite y_eq_x; intro y_eq_x'; rewrite y_eq_x'; reflexivity. rewrite <- (H2 y val''); subst sigma'. rewrite (find_diff (@eq variable)). reflexivity. exact X.eq_bool_ok. exact y_diff_x. apply in_insert; trivial. clear sigma H1 H2. intros x1 y val1 valy [ | [z zval] tau] tau' tau''; simpl; intro H'''; simpl in H'''; injection H'''; clear H'''; intros; subst. assert (yvaly_in_sigma12 : In (y,valy) (sigma1 ++ sigma2)). rewrite H0; apply in_or_app; right; left; trivial. destruct (in_app_or _ _ _ yvaly_in_sigma12) as [yvaly_in_sigma1 | yvaly_in_sigma2]. destruct (In_split _ _ yvaly_in_sigma1) as [tau1 [tau2 H']]. intro x1_eq_y; apply (H3 y x1 valy val' tau1 tau2 sigma2); subst; trivial. rewrite <- ass_app; trivial. destruct (In_split _ _ yvaly_in_sigma2) as [tau1 [tau2 H']]. apply (H3 x1 y val' valy sigma1 tau1 tau2); subst; trivial. destruct (insert_2 _ _ _ _ _ (z,val') _ _ H0) as [tau1 [tau2 [tau3 H4]]]. apply (H3 _ _ _ _ _ _ _ H4). intro H4; exists ((x,val) :: sigma'); repeat split. intros y; simpl; case_eq (eq_var_bool y x); [intro y_eq_x | intro y_diff_x]; [idtac | apply H1]; trivial. simpl; intros y valy [H | H]. injection H; clear H; intros; subst. rewrite eq_var_bool_refl; reflexivity. case_eq (eq_var_bool y x); [intro y_eq_x | intro y_diff_x]. absurd (In (y,valy) sigma'). apply find_not_found with eq_var_bool x. assumption. generalize (X.eq_bool_ok x y) (X.eq_bool_ok y x); rewrite y_eq_x. case (eq_var_bool x y). intros _ _; reflexivity. intros x_diff_y y_eq_x'; apply False_rect; apply x_diff_y; rewrite y_eq_x'; reflexivity. assumption. apply H2; trivial. intros y z valy valz [ | [u valu] tau] tau' tau'' H; simpl in H; injection H; clear H; intros; subst. intro y_eq_z; subst y; apply (find_not_found eq_var_bool _ z valz _ H4). apply eq_var_bool_refl. apply in_or_app; right; left; trivial. apply (H3 _ _ _ _ _ _ _ (eq_refl _)). Defined.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)