proposition: Lemma acyclic_minimize1 X (r : relation X) : acyclic r <-> ~ exists f n, << ENDS: f 0 = f (S n) >> /\ << STEP: forall i (LT: i <= n), r (f i) (f (S i)) >> /\ << MIN: forall i (LTi: i <= n) j (LTj: j <= S n), r (f i) (f j) -> j = S i \/ i = n /\ j = 0 >>.
proof: Proof. split; repeat red; ins; desf. { destruct (H (f 0)). rewrite ENDS at 2; clear - STEP. induction n; vauto. by apply t_step, STEP. by eapply t_trans, t_step; eauto. } apply path_minimize in H0; desf. destruct H; unnw. destruct (get_first_nat (fun x => x <= n /\ exists mm, mm <= x /\ r (f x) (f mm))) as [(m & M & M'')|M]; desc. assert (M' : forall k k', k' <= k -> k <= n -> r (f k) (f k') -> m <= k). by ins; apply M''; eauto. clear M''. { forward eapply get_max_bounded_nat with (P := fun x => r (f m) (f x)) (x := mm) (n := m) as [kk K]; ins; desc. clear mm M0 M1; rename kk into mm. exists (fun x => if eq_op x (S (m - mm)) then (f mm) else (f (x + mm))), (m - mm); repeat split; ins; desf; desf; try lia. by rewrite Nat.sub_add. eapply STEP; lia. left; apply M' in H; lia. destruct (eqP j 0); desf; ins. right; apply M' in H; lia. left; apply MIN in H; try split; try lia. apply NNPP; intro K'. assert (Z:=H); apply M' in Z; try lia. assert (i = m - mm) by lia; subst. rewrite Nat.sub_add in *; ins; apply K1 in H; lia. } { exists f, n; repeat split; ins; desf; try lia. destruct (le_lt_dec j i); [edestruct M|]; eauto. } Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnRewrite