[SOLVED] Path induction using eq

Path induction using eq_rect

According to Homotopy Type Theory (page 49), this is the full induction principle for equality :

Definition path_induction (A : Type) (C : forall x y : A, (x = y) -> Type)
           (c : forall x : A, C x x eq_refl) (x y : A) (prEq : x = y)
  : C x y prEq :=
  match prEq with
  | eq_refl => c x
  end.

I don't understand much about HoTT, but I do see path induction is stronger than eq_rect :

Lemma path_ind_stronger : forall (A : Type) (x y : A) (P : A -> Type)
                            (prX : P x) (prEq : x = y),
    eq_rect x P prX y prEq =
    path_induction A (fun x y pr => P x -> P y) (fun x pr => pr) x y prEq prX.
Proof.
  intros. destruct prEq. reflexivity.
Qed.

Conversely, I failed to construct path_induction from eq_rect. Is it possible ? If not, what is the correct induction principle for equality ? I thought those principles were mechanically derived from the Inductive type definitions.

EDIT

Thanks to the answer below, the full induction principle on equality can be generated by

Scheme eq_rect_full := Induction for eq Sort Prop.

Then we get the converse,

Lemma eq_rect_full_works : forall (A : Type) (C : forall x y : A, (x = y) -> Prop)
                             (c : forall x : A, C x x eq_refl) (x y : A)
                             (prEq : x = y),
    path_induction A C c x y prEq
    = eq_rect_full A x (fun y => C x y) (c x) y prEq.
Proof.
  intros. destruct prEq. reflexivity.
Qed.

Solution

I think you are referring to the fact that the result type of path_induction mentions the path that is being destructed, whereas the one of eq_rect does not. This omission is the default for inductive propositions (as opposed to what happens with Type), because the extra argument is not usually used in proof-irrelevant developments. Nevertheless, you can instruct Coq to generate more complete induction principles with the Scheme command: https://coq.inria.fr/distrib/current/refman/user-extensions/proof-schemes.html?highlight=minimality. (The Minimality variant is the one used for propositions by default.)