proposition: Lemma trans_clos_dec : forall (A : Type) eq_bool, (forall a b : A, match eq_bool a b with true => a = b | false => a <> b end) -> forall (R : relation A) Rlist, (forall a b, R a b <-> In (a,b) Rlist) -> forall a b, {trans_clos R a b}+{~trans_clos R a b}.
proof: Proof. intros A eq_bool eq_bool_ok R Rlist; revert R; induction Rlist as [ | [u v] Rlist]; intros R Rlist_ok a b. right; intro H; inversion H as [x y K | x y z K1 K2]; subst. rewrite Rlist_ok in K; contradiction. rewrite Rlist_ok in K1; contradiction. revert a b; set (R' := fun a b => R a b /\ In (a,b) Rlist). assert (Rlist_ok' : forall a b, R' a b <-> In (a,b) Rlist). intros a b; split; intro H. destruct H as [_ H]; assumption. split; [rewrite Rlist_ok; right | ]; assumption. assert (H := IHRlist _ Rlist_ok'). assert (split_case : forall a b, trans_clos R a b <-> (trans_clos R' a b \/ (refl_trans_clos R' a u /\ refl_trans_clos R' v b))). assert (R'_in_R : inclusion _ R' R). intros x y [K _]; assumption. assert (Ruv : R u v). rewrite Rlist_ok; left; apply eq_refl. intros a b; split; [intro H1 | intros [H1 | [H1 H2]]]. induction H1 as [a b H1 | a b c H1 H2]; rewrite Rlist_ok in H1; simpl in H1; destruct H1 as [H1 | H1]. injection H1; intros; subst; right; split; left. do 2 left; rewrite Rlist_ok'; assumption. injection H1; clear H1; intros; subst. destruct IHH2 as [H3 | H3]. right; split; [left | right; assumption]. destruct H3 as [_ H3]; right; split; [left | assumption]. rewrite <- Rlist_ok' in H1. destruct IHH2 as [H3 | [H3 H3']]. left; right with b; assumption. right; split; [ apply refl_trans_clos_is_trans with b; [right; left | ] | ]; assumption. apply trans_incl with R'; [apply R'_in_R | ]; assumption. inversion H1 as [x | x y K1]; clear H1; subst. inversion H2 as [x' | x' y' K2]; clear H2; subst. left; apply Ruv. right with v; [rewrite Rlist_ok; left; apply eq_refl | apply trans_incl with R'; [apply R'_in_R | ]; assumption]. apply trans_clos_is_trans with u; [apply trans_incl with R'; [apply R'_in_R | assumption] | ]. inversion H2 as [x' | x' y' K2]; clear H2; subst. left; assumption. right with v; [rewrite Rlist_ok; left; apply eq_refl | apply trans_incl with R'; [apply R'_in_R | ]; assumption]. assert (Hrefl : forall a b, {refl_trans_clos R' a b}+{~refl_trans_clos R' a b}). intros a b; generalize (eq_bool_ok a b); destruct (eq_bool a b); [intro a_eq_b; subst; do 2 left | intro a_diff_b]. destruct (H a b) as [Hab | Hab]. left; right; assumption. right; intro K; inversion K; subst; [apply a_diff_b; apply eq_refl | apply Hab; assumption]. intros a b; destruct (H a b) as [Hab | Hab]. left; apply trans_incl with R'; [intros x y [K _] | ]; assumption. destruct (Hrefl a u) as [Hau | Hau]. destruct (Hrefl v b) as [Hvb | Hvb]. left; rewrite split_case; right; split; assumption. right; intro K; rewrite split_case in K; destruct K as [K | [H1 H2]]. apply Hab; assumption. apply Hvb; assumption. right; intro K; rewrite split_case in K; destruct K as [K | [H1 H2]]. apply Hab; assumption. apply Hau; assumption. Defined.
imports: Coq(Setoid Relations List Utf8)