Tactic to do case-analysis on function return values

destruct_fun.v

Ltac destruct_fun_explicit T t f :=
  match goal with
  | |- ?G => let Fn := fresh in
            let Hn := fresh in
            let En := fresh in
            enough (forall x : T, G) as Hn;
            [ apply Hn; exact t
            | intros Fn; pose (ap := f Fn);
              destruct Fn; destruct ap eqn: En; subst ap
            ]
  | _ => idtac
  end.


Ltac destruct_fun f :=
  match type of f with
  | forall _ : ?T, _ =>
    let Xn := fresh in
    assert (Xn : T);
    [ econstructor
    | destruct_fun_explicit T Xn f]
  | _ => idtac
  end.



Goal forall f, f true = 1.
Proof.
  intros f.
  destruct_fun f.
Admitted.