The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/11/2016 11:28 AM, Jonathan Leivent wrote:
> On 01/11/2016 05:35 AM, Pierre Courtieu wrote:
> > Nice, thanks Jonathan!
> >
> > One small glitch yet: the name of the re-asbtracted hypothesis are 
> > not kept
> > the same. I guess it is hard to keep them around.
> >
> > P.
> Unfortunately, I don't think there's a way to keep the names and also 
> get the generality and fairly nice syntax, because of limitations of 
> Ltac.

I lied.

Here is a version with a very slightly less nice syntax (a prefix 
operator), but that keeps the names.  It also no longer needs to use 
number_goals.  Examples are at the end of the attached file.

-- Jonathan

Definition argindex(t : Type)(Admit : forall T, T) : t.
Proof.
  intros.
  apply Admit.
Qed.

Ltac remove_argindexes n f :=
  match f with
  | context[?C] =>
    lazymatch C with
      (argindex (let a := n in ?T) _) =>
      lazymatch (eval pattern C in f) with
        ?F _ =>
        constr:(ltac:(
                  (*Try renaming any hyp a so that there is no clash.  The
                  rename will not be visible outside this constr.*)
                  tryif is_var a then (let a' := fresh in rename a into a') else idtac;
                  let r := constr:(
                            fun (a : T) =>
                              ltac:(let b := (eval cbn beta in (F a)) in
                                    let r := remove_argindexes (S n) b in
                                    exact r)) in exact r))
      end
    end
  | context[?C] =>
    (*If the above case failed, it was probably because of a clash between a
    and something in T.  One would not expect this to happen, considering how
    a encloses T without binding anything in it, but it does for some
    reason.  Probably a Coq bug?  So, in this case, we just use a fresh name.*)
    lazymatch C with
      (argindex (let a := n in ?T) _) =>
      lazymatch (eval pattern C in f) with
        ?F _ =>
        let v := fresh a in
        constr:(fun (v : T) =>
                  ltac:(let b := (eval cbn beta in (F v)) in
                        let r := remove_argindexes (S n) b in
                        exact r))
      end
    end
  | context[argindex (let _ := n in _)] =>
    fail 1 "Something unexpectedly went wrong:" n f
  | context[argindex (let _ := _:nat in _)] =>
    (*in case of missing argindex numbers, due to specializing*)
    remove_argindexes (S n) f
  | context[argindex] =>
    fail 1 "Did you remember to use the abstractable prefix operator '#'?"
  | _ => f
  end.

Ltac label_args n T :=
  lazymatch T with
  | (forall (a : ?T), @?b a) => 
    constr:(forall (a : (let a:=n in T)), 
               ltac:(let b' := eval cbn beta in (b a) in 
                     let c:= label_args (S n) b' in exact c))
  | _ => T
  end.

Tactic Notation "abstracted" "as" ident(result) tactic3(tac) :=
  refine (let result := _ in _);
  let dummy :=
      constr:(
        ltac:(
          let Admit := fresh in
          intro Admit;
          let f := constr:(
                      ltac:(unshelve tac;
                            [apply (@argindex _ Admit)..])) in
          let r := remove_argindexes 1 f in
          let r' := eval cbn beta zeta in r in
          instantiate (1 := r') in (Value of result);
          exact I
        ): (forall T, T) -> True) in idtac.

(*Unfortunately, we have to clutter up the syntax even more with a first pass
over the function to be abstracted in order to label its args*)
Ltac abstractable f :=
  constr:(ltac:(let ft := type of f in
                let laft := label_args 1 ft in
                let F := fresh in
                pose (f : laft) as F;
                (*this appears fragile - various other combos collapse to ft
                in the result*)
                exact F)).

(*but we can minimize that clutter to a single prefix operator:*)
Notation "# f" := (ltac:(let f' := abstractable f in exact f')) (at level 0, only parsing).

(**********************************************************************)

Variable P : nat -> nat -> Type.
Variable Q : nat -> nat -> nat -> Type.
Variable R : Type.

Goal forall a b c, Q a b c -> (forall (x t y z : nat)(p : P x t)(q : Q x y z), R) -> True.
Proof.
  intros a b c H0 H.
  abstracted as H' eapply #H with (2 := H0).
  exact I.
Qed.

Goal forall a b, P a b -> (forall (x t y z : nat), P x t -> P y z -> Q x y z -> R) -> True.
Proof.
  intros a b H0 H.
  abstracted as H1 eapply #H with (1 := H0).
  abstracted as H2 eapply #H with (2 := H0).
  Fail abstracted as H3 eapply H with (1 := H0) (2 := H0).
  abstracted as H3 eapply #H with (1 := H0) (2 := H0).
  exact I.
Qed.