proposition: Lemma path_minimize : forall X (r : relation X) a b (PATH: r⁺ a b), exists f n, << START: f 0 = a >> /\ << END: f (S n) = b >> /\ << STEP: forall i (LT: i <= n), r (f i) (f (S i)) >> /\ << MIN: forall i (LTi: i <= n) j (LTj: i < j <= S n), r (f i) (f j) -> j = S i >> .
proof: Proof. ins; apply clos_trans_tn1 in PATH; induction PATH; desf; unnw. exists (fun x => match x with 0 => a | S _ => y end), 0; intuition; try lia. by apply Nat.le_0_r in LT; desf. destruct (get_first_nat (fun x => x <= n /\ r (f x) z)) as [(m & M)|M]; desc. { exists (fun x => if Compare_dec.le_dec x m then f x else z), m; repeat split; ins; desf; try lia. by eapply STEP; lia. by assert (i = m) by lia; desf. by eapply MIN; eauto; lia. assert (j = S m) by lia; desf. specialize (M0 i); specialize_full M0; try split; ins; lia. } { exists (fun x => if Compare_dec.le_dec x (S n) then f x else z), (S n); repeat split; ins; desf; try lia. by eapply STEP; lia. assert (i = S n) by lia; desf. eapply MIN; eauto; try lia. destruct (eqP i (S n)); desf; try lia. destruct (M i); split; ins; lia. } Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnRewrite