proposition: Lemma inv_solved_part : forall pb, Inv_solved_part pb -> match decomposition_step pb with | Normal _ pb' => Inv_solved_part pb' | _ => True end.
proof: Proof. unfold Inv_solved_part, decomposition_step; simpl. intros [sigma [ | [s t] l]] Inv_pb; simpl. trivial. generalize (T1.eq_bool_ok s t); case (T1.eq_bool s t); [intros _ | intro s_diff_t]. intros x; generalize (Inv_pb x); clear Inv_pb; simpl solved_part. case_eq (find X.eq_bool x sigma); [idtac | trivial]. intros [y | ]; [idtac | trivial]. intro F; do 2 rewrite solved_var; rewrite F. intros [H1 H2]; split; [idtac | assumption]. intro H; apply H1; apply VSet.union_2; 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; rewrite Hx; simpl. intro z; generalize (Inv_pb z); simpl; clear Inv_pb. generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intro z_eq_x; subst z | intro z_diff_x]. intro Inv_pb_x; rewrite solved_var; simpl. generalize (X.eq_bool_ok x x); case (X.eq_bool x x); [intros _; split | intro x_diff_x; apply False_rect; apply x_diff_x; reflexivity]. intro x_in_y_x_val'_l'; destruct_set x_in_y_x_val'_l' x_in_y_x_val' x_in_l'. destruct_set x_in_y_x_val' x_in_y x_in_x_val'. apply s_diff_t; apply f_equal; destruct x_in_y as [x_eq_y | x_in_nil]; [trivial | contradiction]. refine (solved_var_inc_not_mem _ _ _ _ x_in_x_val'); intro; apply s_diff_t; subst; trivial. refine (solved_var_inc_not_mem_list _ _ _ _ x_in_l'); intro; apply s_diff_t; subst; trivial. intro x_in_y_sigma'; destruct_set x_in_y_sigma' x_in_y x_in_sigma'. apply s_diff_t; apply f_equal; destruct x_in_y as [x_eq_y | x_in_nil]; [trivial | contradiction]. refine (solved_var_inc_not_mem_subst _ _ _ _ x_in_sigma'); intro; apply s_diff_t; subst; 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; [idtac | trivial]. destruct z_val as [v | f l']; simpl; [rewrite solved_var; rewrite z_sigma | trivial]. assert (H : match (if eq_var_bool v x then Some (Var y) else None) with | Some v_sigma => v_sigma | None => Var v end = Var (if eq_var_bool v x then y else v)). case (X.eq_bool v x); reflexivity. rewrite H; clear H; rewrite solved_var; intros [z_not_in_x_y_l z_not_in_sigma]. simpl; generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intro z_eq_x; absurd (z=x); assumption | intros _]. rewrite Hz; split. intro z_in_y_x_val'_l'. destruct_set z_in_y_x_val'_l' z_in_y_x_val' z_in_l'. destruct_set z_in_y_x_val' z_in_y z_in_x_val'. apply z_not_in_x_y_l; apply VSet.union_1; apply VSet.union_2; trivial. generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intro z_eq_y | intro z_diff_y]. apply z_not_in_x_y_l; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity. apply z_not_in_sigma; apply solved_var_inc_subst with x y; trivial; apply (solved_var_inc_occ_in_subst _ _ _ _ Hx z_in_x_val'). generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intro z_eq_y | intro z_diff_y]. apply z_not_in_x_y_l; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity. apply z_not_in_x_y_l; apply VSet.union_2; apply solved_var_inc_list with x y; trivial. intro z_in_y_sigma; destruct_set z_in_y_sigma z_in_y z_in_sigma. apply z_not_in_x_y_l; unfold VSet.mem in *; apply VSet.union_1; apply VSet.union_2; trivial. generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intro z_eq_y | intro z_diff_y]. apply z_not_in_x_y_l; unfold VSet.mem in *; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity. apply z_not_in_sigma; apply solved_var_inc_subst with x y; trivial. intro z; generalize (Inv_pb z); simpl; clear Inv_pb. generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intro z_eq_x; subst z | intro z_diff_x]. intros _; rewrite solved_var; simpl. generalize (X.eq_bool_ok x x); case (X.eq_bool x x); [intros _; split | intro x_diff_x; apply False_rect; apply x_diff_x; reflexivity]. intro x_in_l'; refine (solved_var_inc_not_mem_list _ _ _ _ x_in_l'); intro; apply s_diff_t; subst; trivial. intro x_in_y_sigma'; destruct_set x_in_y_sigma' x_in_y x_in_sigma'. apply s_diff_t; apply f_equal; destruct x_in_y as [x_eq_y | x_in_nil]; [trivial | contradiction]. refine (solved_var_inc_not_mem_subst _ _ _ _ x_in_sigma'); intro; apply s_diff_t; subst; trivial. assert (Hz := find_map_subst z x (Var y) sigma). case_eq (find X.eq_bool z sigma); [ intros z_val z_sigma | intros z_sigma]; rewrite z_sigma in Hz; rewrite Hz; [idtac | trivial]. destruct z_val as [v | f l']; simpl; [idtac | trivial]. assert (H : match (if eq_var_bool v x then Some (Var y) else None) with | Some v_sigma => v_sigma | None => Var v end = Var (if eq_var_bool v x then y else v)). case (X.eq_bool v x); reflexivity. rewrite H; clear H; do 2 rewrite solved_var; rewrite z_sigma. intros [z_not_in_x_y_l z_not_in_sigma]; simpl. generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intro z_eq_x; subst z | intros _; rewrite Hz; split]. apply False_rect; apply z_diff_x; reflexivity. intro z_in_l'. generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intro z_eq_y | intro z_diff_y]. apply z_not_in_x_y_l; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity. apply z_not_in_x_y_l; apply VSet.union_2; apply solved_var_inc_list with x y; trivial. intro z_in_y_sigma; destruct_set z_in_y_sigma z_in_y z_in_sigma. apply z_not_in_x_y_l; unfold VSet.mem in *; apply VSet.union_1; apply VSet.union_2; trivial. generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intro z_eq_y | intro z_diff_y]. apply z_not_in_x_y_l; unfold VSet.mem in *; apply VSet.union_1; apply VSet.union_2; left; subst; reflexivity. apply z_not_in_sigma; apply solved_var_inc_subst with x y; trivial. 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 ]. intro z; generalize (Inv_pb z); simpl; clear Inv_pb. simpl; generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intros _; trivial | intro z_diff_x]. case_eq (find X.eq_bool z sigma); [ intros z_val z_sigma | intros _; trivial]. destruct z_val as [v | f l']; [idtac | trivial]. do 2 rewrite solved_var; simpl find; rewrite z_sigma. generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intros x_eq_z; absurd (z =x); assumption | intros _]. intros [z_not_in_x_t2_l z_not_in_sigma]; split; [intro z_in_x_val_t2_l | intro z_in_t2_sigma]. destruct_set z_in_x_val_t2_l z_in_x_val_t2 z_in_l. destruct_set z_in_x_val_t2 z_in_x_val z_in_t2. apply z_not_in_sigma; apply solved_var_inc_occ_in_subst with x x_val; trivial. apply z_not_in_x_t2_l; simpl; unfold VSet.mem in *; apply VSet.union_1; apply VSet.union_2; trivial. apply z_not_in_x_t2_l; simpl; unfold VSet.mem in *; apply VSet.union_2; trivial. destruct_set z_in_t2_sigma z_in_t2 z_in_sigma. apply z_not_in_x_t2_l; simpl; unfold VSet.mem in *; apply VSet.union_1; apply VSet.union_2; trivial. apply z_not_in_sigma; trivial. intro z; generalize (Inv_pb z); simpl; clear Inv_pb. case_eq (find X.eq_bool z sigma); [ intros z_val z_sigma | intros _; trivial]. destruct z_val as [v | f l']; [idtac | trivial]. do 2 rewrite solved_var; rewrite z_sigma. intros [z_not_in_x_t2_l z_not_in_sigma]; split; [intro z_in_x_val_t2_l | assumption]. destruct_set z_in_x_val_t2_l z_in_x_val_t2 z_in_l. destruct_set z_in_x_val_t2 z_in_x_val z_in_t2. apply z_not_in_sigma; apply solved_var_inc_occ_in_subst with x x_val; trivial. apply z_not_in_x_t2_l; apply VSet.union_1; apply VSet.union_2; trivial. apply z_not_in_x_t2_l; apply VSet.union_2; trivial. intros z; generalize (Inv_pb z); simpl; clear Inv_pb. generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intros z_eq_x; subst z | intro z_diff_x]. rewrite x_sigma; trivial. case_eq (find X.eq_bool z sigma); [ intros z_val z_sigma | intros _; trivial]. destruct z_val as [v | f l']; [idtac | trivial]. do 2 rewrite solved_var; simpl find; rewrite z_sigma. generalize (X.eq_bool_ok z x); case (X.eq_bool z x); [intros z_eq_x; absurd (z =x); trivial | intros _]. intros [z_not_in_x_t2_l z_not_in_sigma]; split; [intro z_in_x_val_t2_l | intro z_in_t2_sigma]. apply z_not_in_x_t2_l; apply VSet.union_2; assumption. destruct_set z_in_t2_sigma z_in_t2 z_in_sigma. apply z_not_in_x_t2_l; apply VSet.union_1; apply VSet.union_2; assumption. apply z_not_in_sigma; assumption. 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 ]. intro z; generalize (Inv_pb z); simpl; clear Inv_pb. simpl; generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intros _; trivial | intro z_diff_y]. case_eq (find X.eq_bool z sigma); [ intros z_val z_sigma | intros _; trivial]. destruct z_val as [v | g l']; [idtac | trivial]. do 2 rewrite solved_var; simpl find; rewrite z_sigma. generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intros z_eq_y; absurd (z =y); assumption | intros _]. intros [z_not_in_y_t1_l z_not_in_sigma]; split; [intro z_in_y_val_t1_l | intro z_in_t1_sigma]. destruct_set z_in_y_val_t1_l z_in_y_val_t1 z_in_l. destruct_set z_in_y_val_t1 z_in_y_val z_in_t1. apply z_not_in_sigma; apply solved_var_inc_occ_in_subst with y y_val; trivial. apply z_not_in_y_t1_l; apply VSet.union_1; apply VSet.union_1; trivial. apply z_not_in_y_t1_l; apply VSet.union_2; trivial. destruct_set z_in_t1_sigma z_in_t1 z_in_sigma. apply z_not_in_y_t1_l; apply VSet.union_1; apply VSet.union_1; trivial. apply z_not_in_sigma; trivial. intro z; generalize (Inv_pb z); simpl; clear Inv_pb. case_eq (find X.eq_bool z sigma); [ intros z_val z_sigma | intros _; trivial]. destruct z_val as [v | g l']; [idtac | trivial]. do 2 rewrite solved_var; rewrite z_sigma. intros [z_not_in_y_t1_l z_not_in_sigma]; split; [intro z_in_y_val_t1_l | assumption]. destruct_set z_in_y_val_t1_l z_in_y_val_t1 z_in_l. destruct_set z_in_y_val_t1 z_in_y_val z_in_t1. apply z_not_in_sigma; apply solved_var_inc_occ_in_subst with y y_val; trivial. apply z_not_in_y_t1_l; apply VSet.union_1; apply VSet.union_1; trivial. apply z_not_in_y_t1_l; apply VSet.union_2; trivial. intros z; generalize (Inv_pb z); simpl; clear Inv_pb. generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intros z_eq_y; subst z | intro z_diff_y]. rewrite y_sigma; trivial. case_eq (find X.eq_bool z sigma); [ intros z_val z_sigma | intros _; trivial]. destruct z_val as [v | g l']; [idtac | trivial]. do 2 rewrite solved_var; simpl find; rewrite z_sigma. generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intros z_eq_y; absurd (z =y); trivial | intros _]. intros [z_not_in_y_t1_l z_not_in_sigma]; split; [intro z_in_y_val_t1_l | intro z_in_t1_sigma]. apply z_not_in_y_t1_l; apply VSet.union_2; assumption. destruct_set z_in_t1_sigma z_in_t1 z_in_sigma. apply z_not_in_y_t1_l; apply VSet.union_1; apply VSet.union_1; assumption. apply z_not_in_sigma; assumption. generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intro f_eq_g; subst g | intros _; trivial]. generalize (beq_nat_ok (length l1) (length l2)); case (Nat.eqb (length l1) (length l2)); intro L; trivial. intros z; generalize (Inv_pb z); clear Inv_pb; simpl. case_eq (find X.eq_bool z sigma); [ intros z_val z_sigma | intros _; trivial]. destruct z_val as [v | h l']; trivial. do 2 rewrite solved_var; rewrite z_sigma. intros [z_not_in_t1_t2_l z_not_in_sigma]; split; [intro z_in_l1_l2_l | trivial]. apply z_not_in_t1_t2_l. clear z_sigma z_not_in_t1_t2_l z_not_in_sigma s_diff_t. clear L. revert l2 l z_in_l1_l2_l; induction l1 as [ | t1 l1]; intros [ | t2 l2] l z_in_l1_l2_l. apply VSet.union_2; trivial. apply VSet.union_2; trivial. apply VSet.union_2; trivial. generalize (IHl1 l2 ((t1,t2) :: l) z_in_l1_l2_l); clear z_in_l1_l2_l; intro z_in_l1_l2_l. destruct_set z_in_l1_l2_l z_in_t1_t2 z_in_l1_l2_l'. destruct_set z_in_t1_t2 z_in_t1 z_in_t2. apply VSet.union_1; apply VSet.union_1; apply VSet.union_2; trivial. apply VSet.union_1; apply VSet.union_2; apply VSet.union_2; trivial. destruct_set z_in_l1_l2_l' z_in_l1_l2 z_in_l. destruct_set z_in_l1_l2 z_in_l1 z_in_l2. do 3 apply VSet.union_1; trivial. apply VSet.union_1; apply VSet.union_2; apply VSet.union_1; trivial. apply VSet.union_2; trivial. Defined.
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)