proposition: Lemma min_cycle X (r r' : relation X) (dom : X -> Prop) (TOT: is_total dom r') (T : transitive r') (INCL: r' ⊆ r⁺) (INV: irreflexive (r ⨾ r')) : acyclic r <-> acyclic (restr_rel (fun x => ~ dom x) r) /\ (forall x (CYC: r x x) (D: dom x), False) /\ (forall c1 b1 (R: r c1 b1) b2 (S : r'^? b1 b2) c2 (R': r b2 c2) (S': clos_refl_trans (restr_rel (fun x => ~ dom x) r) c2 c1) (D1 : dom b1) (D2: dom b2) (ND1: ~ dom c1) (ND2: ~ dom c2), False).
proof: Proof. split; intros A; repeat split; ins; desc; eauto. by intros x P; eapply A, clos_trans_mon; eauto; unfold restr_rel; ins; desf. by eauto using t_step. eapply (A c1), t_trans, rt_t_trans, t_rt_trans; eauto using t_step; try (by eapply clos_refl_trans_mon; eauto; unfold restr_rel; ins; desf). by red in S; desf; eauto using clos_refl_trans, clos_trans_in_rt. assert (INCL': forall a b (R: r a b) (D: dom a) (D': dom b), r' a b). by unfold seq in *; ins; destruct (classic (a = b)) as [|N]; [|eapply TOT in N]; desf; exfalso; eauto. intros x P. assert (J: clos_refl_trans (restr_rel (fun x : X => ~ dom x) r) x x \/ r' x x /\ dom x /\ dom x \/ dom x /\ (exists m n k, r'^? x m /\ r m n /\ clos_refl_trans (restr_rel (fun x : X => ~ dom x) r) n k /\ r^? k x /\ dom m /\ ~ dom n /\ ~ dom k) \/ (exists k m, clos_refl_trans (restr_rel (fun x : X => ~ dom x) r) x k /\ r k m /\ r'^? m x /\ ~ dom k /\ dom m /\ dom x) \/ (exists k m m' n, clos_refl_trans (restr_rel (fun x : X => ~ dom x) r) x k /\ r k m /\ r'^? m m' /\ r m' n /\ clos_refl_trans (restr_rel (fun x : X => ~ dom x) r) n x /\ ~ dom k /\ dom m /\ dom m' /\ ~ dom n)). by vauto. revert P J; generalize x at 1 4 6 8 11 13 14 16. unfold restr_rel in *; ins; apply clos_trans_tn1 in P; induction P; eauto. { rename x0 into x; desf; eauto. destruct (classic (dom x)); rewrite clos_refl_transE in *; desf; eauto using clos_trans. by destruct (clos_trans_restrD J); desf. by destruct (clos_trans_restrD J); eapply A, t_trans, t_step; vauto. by eapply INV; vauto. unfold clos_refl in J3; desf. by eapply A1 with (c1 := x) (b2 := m); eauto using rt_trans, rt_step. destruct (classic (dom x)). by eapply A1 with (c1 := k) (b2 := m); eauto; unfold clos_refl in *; desf; eauto. by eapply A1 with (c1 := x) (b2 := m); eauto using rt_trans, rt_step. destruct (classic (dom y)). by rewrite clos_refl_transE in J; desf; destruct (clos_trans_restrD J); desf. by eapply A1 with (c1 := k) (b2 := x); eauto 8 using rt_trans, rt_step. destruct (classic (dom x)). by rewrite clos_refl_transE in J3; desf; destruct (clos_trans_restrD J3); desf. destruct (classic (dom y)). by rewrite clos_refl_transE in J; desf; destruct (clos_trans_restrD J); desf. by eapply A1 with (c1 := k) (b2 := m'); eauto 8 using rt_trans, rt_step. } eapply clos_tn1_trans in P; desf. { destruct (classic (dom y)). rewrite clos_refl_transE in J; desf. destruct (classic (dom x0)). by eapply IHP; right; left; eauto using t_step. eapply IHP; do 2 right; left; split; ins. by eexists y,x0,x0; repeat eexists; vauto; eauto using clos_trans_in_rt. destruct (clos_trans_restrD J). apply IHP; right; right; left; split; ins. by eexists y,z,x0; repeat eexists; vauto; eauto using clos_trans_in_rt. rewrite clos_refl_transE in J; desf. destruct (classic (dom x0)). eapply IHP; do 3 right; left. by eexists y,x0; repeat eexists; vauto; eauto using clos_trans_in_rt. by eapply IHP; left; vauto. by destruct (clos_trans_restrD J); eapply IHP; left; eauto 8 using rt_trans, rt_step, clos_trans_in_rt. } { destruct (classic (dom y)). by apply IHP; eauto 8 using clos_trans. apply IHP; do 3 right; left; eexists y, z; repeat eexists; vauto; eauto using clos_trans_in_rt. } { destruct (classic (dom y)). by eapply IHP; do 2 right; left; split; ins; eexists m; repeat eexists; eauto; red in J0; red; desf; eauto. destruct (classic (dom x0)). destruct (classic (m = x0)) as [|NEQ]; subst. by eapply IHP; do 3 right; left; eexists y,z; repeat eexists; vauto. eapply TOT in NEQ; desf. by eapply IHP; do 3 right; left; eexists y,z; repeat eexists; vauto; eauto; red; red in J0; desf; eauto. by red in J3; desf; eapply A1 with (c1 := k) (b2 := m); eauto 8 using rt_trans, rt_step, clos_trans_in_rt. by eapply IHP; do 4 right; eexists y,z; repeat eexists; vauto; unfold clos_refl in *; desf; vauto. } { destruct (classic (dom z)). by rewrite clos_refl_transE in J; desf; destruct (clos_trans_restrD J); desf. destruct (classic (y = m)) as [|NEQ]; desf. by unfold clos_refl in *; desf; eauto. destruct (classic (dom y)). eapply TOT in NEQ; desf. by unfold clos_refl in *; desf; apply IHP; right; left; eauto using t_rt_trans, t_step. by eapply A1 with (c1 := k) (b2 := y); eauto 8 using rt_trans, rt_step, clos_trans_in_rt. by eapply IHP; do 3 right; left; eexists k, m; repeat eexists; vauto. } destruct (classic (dom x0)). by rewrite clos_refl_transE in J3; desf; destruct (clos_trans_restrD J3); desf. destruct (classic (dom z)). by rewrite clos_refl_transE in J; desf; destruct (clos_trans_restrD J); desf. destruct (classic (y = m)) as [|NEQ]; desf. by eapply IHP; do 2 right; left; split; ins; eexists m', n; repeat eexists; vauto. destruct (classic (dom y)). eapply TOT in NEQ; desf. by unfold clos_refl in *; desf; eapply IHP; do 2 right; left; split; ins; eexists m', n; repeat eexists; vauto; eauto using rt_trans, clos_trans_in_rt. by eapply A1 with (c1 := k) (b2 := y); eauto 8 using rt_trans, rt_step, clos_trans_in_rt. by eapply IHP; do 4 right; eexists k,m,m'; repeat eexists; vauto. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnRewrite