proposition: Lemma decomposition_step_is_sound : forall l sigma theta, match decomposition_step (mk_pb sigma l) with | Normal _ pb' => is_a_solution pb' theta -> is_a_solution (mk_pb sigma l) theta | No_solution _ => is_a_solution (mk_pb sigma l) theta -> False | Not_appliable _ pb' => is_a_solution pb' theta -> is_a_solution (mk_pb sigma l) 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; [idtac | intros; apply Hsigma; trivial]. intros s' t' [s'_t'_eq_s_t | s'_t'_in_l]; [idtac | apply Hl; trivial]. injection s'_t'_eq_s_t; intros; subst s s' t'; 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. simpl solved_part; rewrite Hx. unfold is_a_solution; simpl solved_part; simpl unsolved_part; intros [Hl Hsigma]. assert (x_theta_eq_y_theta : apply_subst theta (Var x) = apply_subst theta (Var y)). generalize (Hsigma x); simpl. generalize (X.eq_bool_ok x x); case (X.eq_bool x x); [intros _; trivial | intro x_diff_x; apply False_rect; apply x_diff_x; reflexivity]. 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]; 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. split. intros s t [s_t_eq_x_y | s_t_in_l]. injection s_t_eq_x_y; intros; subst; trivial. do 2 (apply sym_eq; rewrite Htheta). apply Hl; right. apply (in_map (B:= term*term) (fun (uv : term * term) => let (u,v) := uv in (apply_subst ((x,Var y) :: nil) u, apply_subst ((x,Var y) :: nil) v)) _ _ s_t_in_l). intro z; generalize (Hsigma 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]. rewrite x_sigma; intro H; rewrite H; apply sym_eq; rewrite Htheta; apply sym_eq; apply Hl; left; trivial. 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; trivial. intro H; rewrite H; rewrite <- Htheta; trivial. simpl; rewrite Hx. unfold is_a_solution; simpl solved_part; simpl unsolved_part; intros [Hl Hsigma]. assert (x_theta_eq_y_theta : apply_subst theta (Var x) = apply_subst theta (Var y)). generalize (Hsigma x); simpl; generalize (X.eq_bool_ok x x); case (X.eq_bool x x); [intros _; trivial | intro x_diff_x; apply False_rect; apply x_diff_x; reflexivity]. 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]; 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. split. intros s t [s_t_eq_x_y | s_t_in_l]. injection s_t_eq_x_y; intros; subst; trivial. do 2 (apply sym_eq; rewrite Htheta). apply Hl; apply (in_map (B:= term*term) (fun (uv : term * term) => let (u,v) := uv in (apply_subst ((x,Var y) :: nil) u, apply_subst ((x,Var y) :: nil) v)) _ _ s_t_in_l). intro z; generalize (Hsigma 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]. rewrite x_sigma; trivial. 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. intro H; rewrite H; rewrite <- Htheta; trivial. trivial. 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]. destruct (lt_ge_dec (T.size (Term g l2)) (T.size x_val)) as [L | L]; intros [Hl Hsigma]. simpl; split. intros s t [s_t_eq_x_g_l2 | s_t_in_l]. injection s_t_eq_x_g_l2; intros; subst s t; apply trans_eq with (apply_subst theta x_val). generalize (Hsigma x); simpl; rewrite x_sigma; generalize (X.eq_bool_ok x x); case (X.eq_bool x x); [intros _; trivial | intro x_diff_x; apply False_rect; apply x_diff_x; reflexivity]. intro H; rewrite H; apply sym_eq; apply Hl; left; trivial. apply Hl; left; trivial. apply Hl; right; trivial. intro z; generalize (Hsigma 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]. intro H; rewrite H; rewrite x_sigma. apply sym_eq; apply Hl; left; trivial. trivial. simpl; split. intros s t [s_t_eq_x_g_l2 | s_t_in_l]. injection s_t_eq_x_g_l2; intros; subst s t; apply trans_eq with (apply_subst theta x_val). generalize (Hsigma x); simpl; rewrite x_sigma; intro; trivial. apply Hl; left; trivial. apply Hl; right; trivial. intro z; apply (Hsigma z). simpl; intros [Hl Hsigma]; split. intros s t [s_t_eq_x_g_l2 | s_t_in_l]. injection s_t_eq_x_g_l2; intros; subst s t; generalize (Hsigma x); simpl; generalize (X.eq_bool_ok x x); case (X.eq_bool x x); [intros _; trivial | intro x_diff_x; apply False_rect; apply x_diff_x; reflexivity]. apply Hl; trivial. intro z; generalize (Hsigma 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]. intro H; rewrite H; rewrite x_sigma; trivial. trivial. 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]. destruct (lt_ge_dec (T.size (Term f l1)) (T.size y_val)) as [L | L]; intros [Hl Hsigma]. simpl; split. intros s t [s_t_eq_f_l1_y | s_t_in_l]. injection s_t_eq_f_l1_y; intros; subst s t; apply trans_eq with (apply_subst theta y_val). apply sym_eq; apply Hl; left; trivial. generalize (Hsigma y); simpl; rewrite y_sigma; generalize (X.eq_bool_ok y y); case (X.eq_bool y y); [intros _; trivial | intro y_diff_y; apply False_rect; apply y_diff_y; reflexivity]. intro H; rewrite H; apply Hl; left; trivial. apply Hl; right; trivial. intro z; generalize (Hsigma 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]. intro H; rewrite H; rewrite y_sigma. apply sym_eq; apply Hl; left; trivial. trivial. simpl; split. intros s t [s_t_eq_f_l1_y | s_t_in_l]. injection s_t_eq_f_l1_y; intros; subst s t; apply trans_eq with (apply_subst theta y_val). apply sym_eq; apply Hl; left; trivial. generalize (Hsigma y); simpl; rewrite y_sigma; simpl; intro; apply sym_eq; trivial. apply Hl; right; trivial. intro z; apply (Hsigma z). simpl; intros [Hl Hsigma]; split. intros s t [s_t_eq_f_l1_y | s_t_in_l]. injection s_t_eq_f_l1_y; intros; subst s t; generalize (Hsigma y); simpl; generalize (X.eq_bool_ok y y); case (X.eq_bool y y); [intros _; trivial | intro y_diff_y; apply False_rect; apply y_diff_y; reflexivity]. simpl; intro; apply sym_eq; trivial. apply Hl; trivial. intro z; generalize (Hsigma 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]. intro H; rewrite H; rewrite y_sigma; trivial. trivial. 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 ((forall s t, In (s,t) l -> apply_subst theta s = apply_subst theta t) /\ map (apply_subst theta) l1 = map (apply_subst theta) l2). generalize l2 l L Hl; clear l2 L l Hl s_diff_t; induction l1 as [ | s1 l1]; intros [ | s2 l2] l L Hl. split; trivial; apply Hl; trivial. discriminate. discriminate. assert (H : forall s t : term, In (s, t) ((s1,s2) :: l) -> apply_subst theta s = apply_subst theta t). intros s t H; refine (proj1 (IHl1 l2 _ _ _) s t H); clear s t H. injection L; intros; assumption. intros s t H; apply Hl; trivial. split. intros s t s_t_in_l; apply H; right; trivial. simpl; rewrite (H s1 s2); [apply f_equal | left; trivial]. refine (proj2 (IHl1 l2 _ _ Hl)). injection L; intro; assumption. intros s t [s_t_eq_f_l1_g_l2 | s_t_in_l]. injection s_t_eq_f_l1_g_l2; intros; subst; simpl; destruct H as [ _ H ]; rewrite H; subst; trivial. destruct H as [ H _ ]; apply H; trivial. unfold is_a_solution; simpl solved_part; simpl unsolved_part; intros [Hl Hsigma]. apply L; do 2 (apply sym_eq; rewrite <- (length_map (apply_subst theta))); assert (Abs := Hl _ _ (or_introl _ (eq_refl _))); simpl in Abs; injection Abs; intros H _; rewrite H; trivial. unfold is_a_solution; simpl solved_part; simpl unsolved_part; intros [Hl Hsigma]. apply f_diff_g; assert (Abs := Hl _ _ (or_introl _ (eq_refl _))); simpl in Abs; injection Abs; intros _ H; rewrite H; trivial. 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)