Induction by hand in Coq

induction_by_hand.v

Require Import List.
Import ListNotations.

Definition map_length {A B} (f : A -> B) :
  forall l, length (map f l) = length l.
refine (fix loop l := _).
refine (match l with
        | [] => _
        | x :: xs => _
        end).
refine eq_refl.
change (S (length (map f xs)) = S (length xs)).  (* optional: cleaner simplifying by hand *)
refine (f_equal S _).
refine (loop xs).
Defined.
Print map_length.