「ソフトウェアの基礎」Rel_J 練習問題 rtc_rsc_coincide の証明

rtc_rsc_coincide.v

(** **** 練習問題:★★★, optional (rtc_rsc_coincide) *)
Theorem rtc_rsc_coincide :
         forall (X:Type) (R: relation X) (x y : X),
  clos_refl_trans R x y <-> refl_step_closure R x y.
Proof.
 intros. split; intro H.
  induction H.
   apply rsc_R.

   apply H.

   apply rsc_refl.

   apply rsc_trans with y.
    apply IHclos_refl_trans1.

    apply IHclos_refl_trans2.

  induction H.
   apply rt_refl.

   apply rt_trans with y.
    apply rt_step. apply H.

    apply IHrefl_step_closure.
Qed.