proposition: Lemma decomposition_step_is_complete : forall l sigma theta, is_a_solution (mk_pb sigma l) theta -> match decomposition_step (mk_pb sigma l) with | Normal _ pb' => is_a_solution pb' theta | No_solution _ => False | Not_appliable _ pb' => is_a_solution pb' theta end.
proof: Proof. intros [ | [s t] l] sigma theta; unfold decomposition_step; simpl unsolved_part; cbv iota beta; trivial. generalize (T.eq_bool_ok s t); case (T.eq_bool s t); [intro s_eq_t | intro s_diff_t]. unfold is_a_solution; simpl solved_part; simpl unsolved_part; intros [Hl Hsigma]; split; [intros; apply Hl; right | intros; apply Hsigma]; trivial. destruct s as [ x | f l1 ]; destruct t as [ y | g l2 ]. assert (Hx := find_map_subst x x (Var y) sigma). case_eq (find X.eq_bool x sigma); [intros x_val x_sigma | intro x_sigma]; rewrite x_sigma in Hx. unfold is_a_solution; simpl solved_part; simpl unsolved_part; intros [Hl Hsigma]; assert (Htheta : forall t, apply_subst theta t = apply_subst theta (apply_subst ((x, Var y) :: nil) t)). intro t; pattern t; apply term_rec3; clear t; [intros v | intros f l']. simpl; generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intro v_eq_x; subst v | intro v_diff_x]. apply (Hl (Var x) (Var y) (or_introl _ (eq_refl _))). trivial. intros IH; simpl; apply (f_equal (fun l => Term f l)); induction l' as [ | s' l']; trivial. simpl; rewrite (IH s' (or_introl _ (eq_refl _))); rewrite IHl'; trivial; intros; apply IH; right; trivial. rewrite Hx; split. intros s t H; destruct (in_inv H) as [s_t_eq_y_x_val' | s_t_in_l']; clear H. assert (H':=Hsigma x); rewrite x_sigma in H'; injection s_t_eq_y_x_val'; clear s_t_eq_y_x_val'; intros; subst s t; rewrite <- (Hl _ _ (or_introl _ (eq_refl _))); rewrite H'; apply Htheta. rewrite in_map_iff in s_t_in_l'; destruct s_t_in_l' as [[s' t'] [H s'_t'_in_l]]; injection H; intros; subst; clear H; do 2 rewrite <- Htheta; apply Hl; right; trivial. intro z; simpl. generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intro z_eq_x; subst z | intro z_diff_x]. apply (Hl (Var x) (Var y) (or_introl _ (eq_refl _))). assert (Hz := find_map_subst z x (Var y) sigma). case_eq (find X.eq_bool z sigma); [ intros z_val z_sigma | intro z_sigma ]; rewrite z_sigma in Hz; rewrite Hz. rewrite <- Htheta; generalize (Hsigma z); rewrite z_sigma; trivial. exact I. unfold is_a_solution; simpl solved_part; simpl unsolved_part; intros [Hl Hsigma]; assert (Htheta : forall t, apply_subst theta t = apply_subst theta (apply_subst ((x, Var y) :: nil) t)). intro t; pattern t; apply term_rec3; clear t; [intros v | intros f l']. simpl; generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intro v_eq_x; subst v | intro v_diff_x]. apply (Hl (Var x) (Var y) (or_introl _ (eq_refl _))). trivial. intros IH; simpl; apply (f_equal (fun l => Term f l)); induction l' as [ | s' l']; trivial. simpl; rewrite (IH s' (or_introl _ (eq_refl _))); rewrite IHl'; trivial; intros; apply IH; right; trivial. rewrite Hx; simpl; split. intros s t s_t_in_l'; rewrite in_map_iff in s_t_in_l'; destruct s_t_in_l' as [[s' t'] [H s'_t'_in_l]]; injection H; intros; subst; clear H; do 2 rewrite <- Htheta; apply Hl; right; trivial. intro z; simpl. generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intro z_eq_x; subst z | intro z_diff_x]. apply (Hl (Var x) (Var y) (or_introl _ (eq_refl _))). assert (Hz := find_map_subst z x (Var y) sigma). case_eq (find X.eq_bool z sigma); [ intros z_val z_sigma | intro z_sigma ]; rewrite z_sigma in Hz; rewrite Hz. rewrite <- Htheta; generalize (Hsigma z); rewrite z_sigma; trivial. exact I. unfold is_a_solution; simpl solved_part; simpl unsolved_part; case_eq (find X.eq_bool x sigma); [intros x_val x_sigma| intro x_sigma]. intros [Hl Hsigma]. destruct (lt_ge_dec (T.size (Term g l2)) (T.size x_val)) as [L | L]. simpl; split. intros s t [s_t_eq_x_val_g_l2 | s_t_in_l]. injection s_t_eq_x_val_g_l2; intros; subst s t; apply trans_eq with (apply_subst theta (Var x)). generalize (Hsigma x); rewrite x_sigma; intro; apply sym_eq; trivial. apply Hl; left; trivial. apply Hl; right; trivial. intro z; simpl. generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intro z_eq_x; subst z | intro z_diff_x]. apply (Hl _ _ (or_introl _ (eq_refl _))). apply (Hsigma z). simpl; split. intros s t [s_t_eq_x_val_g_l2 | s_t_in_l]. injection s_t_eq_x_val_g_l2; intros; subst s t; apply trans_eq with (apply_subst theta (Var x)). generalize (Hsigma x); rewrite x_sigma; intro; apply sym_eq; trivial. apply Hl; left; trivial. apply Hl; right; trivial. intro z; apply (Hsigma z). simpl; split. intros s t s_t_in_l. apply H; right; trivial. intro z; simpl. generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intro z_eq_x; subst z | intro z_diff_x]. apply ((proj1 H) _ _ (or_introl _ (eq_refl _))). apply ((proj2 H) z). unfold is_a_solution; simpl solved_part; simpl unsolved_part; case_eq (find X.eq_bool y sigma); [intros y_val y_sigma | intro y_sigma]. intros [Hl Hsigma]. destruct (lt_ge_dec (T.size (Term f l1)) (T.size y_val)) as [L | L]. simpl; split. intros s t [s_t_eq_y_val_f_l1 | s_t_in_l]. injection s_t_eq_y_val_f_l1; intros; subst s t; apply trans_eq with (apply_subst theta (Var y)). generalize (Hsigma y); rewrite y_sigma; intro; apply sym_eq; trivial. apply sym_eq; apply Hl; left; trivial. apply Hl; right; trivial. intro z; simpl. generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intro z_eq_y; subst z | intro z_diff_y]. apply sym_eq; apply (Hl _ _ (or_introl _ (eq_refl _))). apply (Hsigma z). simpl; split. intros s t [s_t_eq_y_val_f_l1 | s_t_in_l]. injection s_t_eq_y_val_f_l1; intros; subst s t; apply trans_eq with (apply_subst theta (Var y)). generalize (Hsigma y); rewrite y_sigma; intro; apply sym_eq; trivial. apply sym_eq; apply Hl; left; trivial. apply Hl; right; trivial. intro z; apply (Hsigma z). simpl; split. intros s t s_t_in_l. apply (proj1 H); right; trivial. intro z; simpl. generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intro z_eq_y; subst z | intro z_diff_y]. apply sym_eq; apply ((proj1 H) _ _ (or_introl _ (eq_refl _))). apply ((proj2 H) z). generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intro f_eq_g | intro f_diff_g]. generalize (beq_nat_ok (length l1) (length l2)); case (Nat.eqb (length l1) (length l2)); intro L. unfold is_a_solution; simpl solved_part; simpl unsolved_part; intros [Hl Hsigma]. split; trivial. assert (Hl' : forall s t, In (s,t) l -> apply_subst theta s = apply_subst theta t). intros; apply Hl; right; trivial. assert (Hl12 : map (apply_subst theta) l1 = map (apply_subst theta) l2). generalize (Hl _ _ (or_introl _ (eq_refl _))); simpl; intro H; injection H; intros; trivial. clear Hsigma; generalize l2 l L Hl' Hl12; clear s_diff_t l2 l L Hl Hl' Hl12; induction l1 as [ | s1 l1]; intros [ | s2 l2] l L Hl Hl12. intros s t; simpl; intros s_t_in_l; apply Hl; trivial. discriminate. discriminate. simpl. intros s t s_t_in_l'; refine (IHl1 l2 _ _ _ _ _ _ s_t_in_l'); clear s t s_t_in_l'. injection L; intro; assumption. intros s t [s_t_eq_s1_s2 | s_t_in_l]. injection s_t_eq_s1_s2; simpl in Hl12; injection Hl12; intros; subst s t; trivial. apply Hl; trivial. simpl in Hl12; injection Hl12; intros; trivial. unfold is_a_solution; simpl solved_part; simpl unsolved_part. intros [Hl _]; generalize (Hl _ _ (or_introl _ (eq_refl _))); simpl; intro H; injection H; intros H' _. apply L; rewrite <- (length_map (apply_subst theta)); rewrite H'; apply length_map. intros [Hl _]; generalize (Hl _ _ (or_introl _ (eq_refl _))); simpl; intro H; injection H; intros _ H'. apply f_diff_g; assumption. Qed.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)