proposition: Lemma oc_applies : forall c src sigma, VSet.without_red (src :: c) -> is_a_cycle sigma src src c = true -> forall tau, is_a_solution (mk_pb sigma nil) tau -> False.
proof: Proof. intro c; induction c as [ | next c]. intros src sigma W Hcycle tau [_ Hsol]; simpl in Hcycle; simpl in Hsol. generalize (Hsol src); revert Hcycle. case (find X.eq_bool src sigma); [intros [x | f l] | intro src_sol]; [idtac | idtac | discriminate]. intro; discriminate. rewrite var_in_term_is_sound; intro src_in_l. case (var_in_subterm2 _ _ (in_impl_mem (@eq _) (fun a => eq_refl a) _ _ src_in_l)); intros [ | i p] Hsubterm. inversion Hsubterm. assert (Hsubterm' := subterm_at_pos_apply_subst_apply_subst_subterm_at_pos (Term f l) (i :: p) tau). rewrite Hsubterm in Hsubterm'. assert (Hsize := size_subterm_at_pos (apply_subst tau (Term f l)) i p). rewrite Hsubterm' in Hsize. intros src_sol; simpl apply_subst at 1 in Hsize; rewrite src_sol in Hsize. apply (Nat.lt_irrefl _ Hsize). intros src sigma W Hcycle tau. rewrite (rep_var_is_complete src sigma tau). apply (IHc next). apply (VSet.without_red_remove src nil (next :: c) W). rewrite <- is_a_cycle_discard. clear IHc tau; revert src next W Hcycle. assert (H : forall x y src next : DecVar.A, VSet.without_red (x :: next :: c) -> var_in_term y (apply_subst sigma (Var x)) = true -> match find X.eq_bool x sigma with | Some (Var _) => False | Some (Term _ _) => True | None => False end -> is_a_cycle sigma x src (next :: c) = true -> is_a_cycle (map (fun xt : variable * term => (fst xt, apply_subst ((x, apply_subst sigma (Var x)) :: nil) (snd xt))) sigma) y next c = true). induction c as [ | next' c]; intros x y src next W y_in_x_sigma Hx Hcycle. simpl in Hcycle. case_eq (find X.eq_bool src sigma); [intros [v | f l] | idtac]; intro src_sigma; rewrite src_sigma in Hcycle; [discriminate | idtac | discriminate]. case_eq (var_in_term next (Term f l)); [intro next_in_l | intro next_not_in_l]. rewrite next_in_l in Hcycle. simpl. assert (F := find_map X.eq_bool (apply_subst ((x, apply_subst sigma (Var x)) :: nil)) next sigma). case_eq (find X.eq_bool next sigma); [intros [v | g k] | idtac]; intro next_sigma; rewrite next_sigma in Hcycle; [discriminate | idtac | discriminate]. rewrite next_sigma in F. unfold DecVar.A in *; simpl apply_subst at 1 in F; rewrite F; clear F. simpl apply_subst at 1; cbv iota beta. rewrite var_in_term_is_sound in Hcycle. case (var_in_subterm2 _ _ (in_impl_mem (@eq _) (fun a => eq_refl a) _ _ Hcycle)); intros [ | i p] Hsubterm. inversion Hsubterm. assert (Hsubterm' := subterm_at_pos_apply_subst_apply_subst_subterm_at_pos (Term g k) (i :: p) ((x, apply_subst sigma (Var x)) :: nil)). rewrite Hsubterm in Hsubterm'. rewrite var_in_term_is_sound. refine (var_in_subterm y _ (i :: p) Hsubterm' _). simpl; generalize (X.eq_bool_ok x x); case (X.eq_bool x x); [intros _ | intro x_diff_x; apply False_rect; apply x_diff_x; reflexivity]. rewrite <- var_in_term_is_sound; trivial. rewrite next_not_in_l in Hcycle; discriminate. assert (Hsrc := is_a_cycle_all_var_inst _ _ _ _ Hcycle src). case_eq (find X.eq_bool src sigma); [intros [v | f l] | idtac]; intro src_sigma; rewrite src_sigma in Hsrc. apply False_rect; apply Hsrc; left; reflexivity. clear Hsrc. assert (Hnext := is_a_cycle_all_var_inst _ _ _ _ Hcycle next). case_eq (find X.eq_bool next sigma); [intros [v | g k] | idtac]; intro next_sigma; rewrite next_sigma in Hnext. apply False_rect; apply Hnext; right; left; reflexivity. clear Hnext. revert Hcycle; pattern (next' :: c); simpl; intro Hcycle. rewrite src_sigma in Hcycle. rewrite next_sigma in Hcycle. case_eq (var_in_term next (Term f l)); [intro next_in_l | intro next_not_in_l]. rewrite next_in_l in Hcycle. case_eq (var_in_term next' (Term g k)); [intro next'_in_k | intro next'_not_in_k]. rewrite next'_in_k in Hcycle. assert (F := find_map X.eq_bool (apply_subst ((x, apply_subst sigma (Var x)) :: nil)) next sigma). rewrite next_sigma in F. simpl apply_subst at 1 in F; rewrite F; clear F. simpl apply_subst at 1; cbv iota beta. assert (H : var_in_term next' (apply_subst ((x, apply_subst sigma (Var x)) :: nil) (Term g k)) = true). rewrite var_in_term_is_sound in next'_in_k. case (var_in_subterm2 _ _ (in_impl_mem (@eq _) (fun a => eq_refl _) _ _ next'_in_k)); intros [ | i p] Hsubterm. inversion Hsubterm. assert (Hsubterm' := subterm_at_pos_apply_subst_apply_subst_subterm_at_pos (Term g k) (i :: p) ((x, apply_subst sigma (Var x)) :: nil)). rewrite Hsubterm in Hsubterm'. rewrite var_in_term_is_sound. refine (var_in_subterm next' _ (i :: p) Hsubterm' _). simpl; generalize (X.eq_bool_ok next' x); case (X.eq_bool next' x); [intro next'_eq_x; subst next' | intros _; left; trivial]. assert (W' : VSet.without_red (x :: x :: c)). apply (VSet.without_red_remove next (x :: nil) (x :: c) W). simpl in W'; apply False_rect. unfold VSet.without_red in W'; simpl in W'; revert W'; unfold DecVar.eq_bool. generalize (X.eq_bool_ok x x); case (X.eq_bool x x); [intros _; discriminate | intro x_diff_x; apply False_rect; apply x_diff_x; reflexivity]. rewrite H. refine (IHc x y next _ _ y_in_x_sigma Hx _). apply (VSet.without_red_remove next (x :: nil) (next' :: c) W). simpl; rewrite next_sigma. rewrite next'_in_k; trivial. rewrite next'_not_in_k in Hcycle; discriminate. rewrite next_not_in_l in Hcycle; discriminate. apply False_rect; apply Hnext; right; left; reflexivity. apply False_rect; apply Hsrc; left; reflexivity. intros src next W Hcycle; apply H with src; trivial. simpl in Hcycle; simpl. destruct (find X.eq_bool src sigma) as [[v | f l] | ]. discriminate. destruct (var_in_term next (Term f l)); trivial; discriminate. discriminate. apply (is_a_cycle_all_var_inst _ _ _ _ Hcycle); left; reflexivity. unfold VSet.without_red in W; simpl in W; revert W; unfold DecVar.eq_bool. generalize (X.eq_bool_ok src next); case (X.eq_bool src next); [intro src_eq_next | intro src_diff_next]. intros; discriminate. simpl; unfold DecVar.A. generalize (mem_bool_ok _ _ X.eq_bool_ok src c); case (mem_bool X.eq_bool src c); [intro src_in_c | intro src_not_in_c]. intros; discriminate. generalize (mem_bool_ok _ _ X.eq_bool_ok next c); case (mem_bool X.eq_bool next c); [intro next_in_c | intro next_not_in_c]. intros; discriminate. intros _ [src_eq_next | src_in_c]. apply src_diff_next; subst; reflexivity. apply src_not_in_c; apply in_impl_mem; 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)