Set Implicit Arguments.
Unset Strict Implicit.

Notation "R <<= S" := (forall x y, R x y -> S x y) (at level 70).
Notation "R === S" := (R <<= S /\ S <<= R) (at level 70).

Section Sec1.
  Variables (X: Type) (R: X -> X -> Prop).
  Implicit Types x y z : X.

  Inductive star : X -> X -> Prop :=
  | starRefl x     : star x x
  | starStep x x' y : R x x' -> star x' y -> star x y.

  (* We offer two proofs for the following claims, 
     one detailled, and one with eauto *)
  
  Fact star_exp :
    R <<= star.
  Proof.
    intros x y H.
    eapply starStep. exact H. constructor.
  Qed.

  Fact star_exp' :
    R <<= star.
  Proof.
    eauto using star.
  Qed.
  
  Fact star_trans x y z :
    star x y -> star y z -> star x z.
  Proof.
    intros H1 H2.
    induction H1 as [x|x x' y H _ IH].
    + exact H2.
    + eapply starStep. exact H. apply IH, H2.
  Qed.

  Fact star_trans' x y z :
    star x y -> star y z -> star x z.
  Proof.
    induction 1; eauto using star.
  Qed.

  (* Coq generates a too complex induction lemma (star_ind).
     We prove the minimal induction lemma (star induction)
     and use it to reprove transtivity *)      
  
  Fact star_Ind y (p: X -> Prop) :
    p y ->
    (forall x x', R x x' -> p x' -> p x) ->
    forall x, star x y -> p x.
  Proof.
    intros H1 H2. induction 1; eauto.
  Qed.

  Fact star_trans'' x y z :
    star x y -> star y z -> star x z.
  Proof.
    intros H H1. revert x H.
    refine (star_Ind _ _).
    - exact H1.
    - intros x x' H IH. exact (starStep H IH).
    (* We cannot use the induction tactic since our induction lemma 
       doesn't observe the parameters registered with Coq *)
  Qed.

  Fact star_Ind' x (p: X -> Prop) :
    p x ->
    (forall y y', R y' y -> p y' -> p y) ->
    forall y, star x y -> p y.
  Proof.
    intros HB HI y H. revert x H HB.
    refine (star_Ind _ _).
    - intros HB. exact HB.
    - intros x x' H IH HB.
      apply IH, (HI x' x H), HB.
  Qed.
End Sec1.

Definition reflexive X (R: X -> X -> Prop) :=
  forall x, R x x.
Definition transitive X (R: X -> X -> Prop) :=
  forall x y z, R x y -> R y z -> R x z.

Section Sec2.
  Variable X: Type.
  Implicit Types (x y z : X) (R S : X -> X -> Prop).

  Fact star_closure R S :
    reflexive S -> transitive S -> R <<= S -> star R <<= S.
  Proof.
    intros H1 H2 H3 x y.
    induction 1 as [x|x x' y H4 _ IH].
    - apply H1.
    - eapply H2. 2:exact IH. apply H3, H4.
  Qed.

  Fact star_idem R :
    star (star R) === star R.
  Proof.
    split.
    - apply star_closure.
      + intros x. constructor.
      + intros x y z. apply star_trans.
      + auto.
    - apply star_exp.
  Qed.

  Fact star_mono R S :
    R <<= S -> star R <<= star S.
  Proof.
    intros H x y.
    induction 1; eauto using star.
  Qed.
End Sec2.