The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Attached.  Example usage at the end of abstractedas.v.  I haven't tested 
any other cases - so caveats apply.  Let me know if it needs fixing.

The one undocumented v8.5 feature it uses is named evars in 
numbergoals.v (?[__Number_Goals]) - but this can be removed in the case 
of the abstracted as tactic if necessary (by using an evar created in 
abstracted as prior to the "unshelve tac" call).

-- Jonathan

On 01/08/2016 07:14 PM, Pierre Courtieu wrote:
> That would be very nice. Thanks Jonathan!
>
> Pierre
>
> Le vendredi 8 janvier 2016, Jonathan Leivent 
> <jonikelee AT gmail.com>
>  a écrit :
>
> > On 01/08/2016 01:03 PM, Pierre Courtieu wrote:
> >
> > > Thanks for the answers. This is also the solution I came up with, more
> > > or less. But what one really want is to use the unification stuff
> > > during the process, so that instantiating one argument also
> > > instantiates some other (prvious) arguments.
> > >
> > > Suppose you have
> > >
> > > H0: Q a b c
> > > H: forall x t y z, P x t -> Q x y z -> R.
> > > ======
> > > ...
> > >
> > > Then "specialize with (2:=H0)" should actually instantiate x y and z:
> > > H0: Q a b c
> > > H: forall t, P a t -> R.
> > > ======
> > > ...
> > >
> > > P.
> > I think I can do this entirely in Ltac in v8.5 (but not v8.4). Briefly, it
> > would start off with something like this:
> >
> > Goal forall a b c, Q a b c ->
> >                (forall x t y z, P x t -> Q x y z -> R) -> False.
> > Proof.
> >    intros a b c H0 H.
> >
> >    evar (T:Type).
> >    let p := constr:(ltac:(
> >                      intro Admit;
> >                      subst T;
> >                      unshelve eapply H with (2:=H0);
> >                      apply Admit): (forall T, T) -> T) in
> >    idtac p.
> >
> > but would also use a goal numbering tactic I wrote to first number each of
> > the subgoals generated by the eapply, then incorporate that number into the
> > Admit so that the resulting subterm generated for each subgoal has
> > something like a De Bruijn index in it.  Then parse that result with
> > match/context replacement to change each of those Admit subterms into a
> > variable bound in an outer fun.
> >
> > I'll give it a try if you don't mind the fact that the result will contain
> > a lot of Ltac hacking.  Also, unfortunately, because there is no Tactic
> > Notation arg type for passing a "constr_with_bindings_arg_list" down to
> > that eapply, you'd have to pass the eapply in as a tactic - so the
> > top-level invocation would have to look at least something like:
> >
> >    foo eapply H with (2:=H0)
> >
> > But, it would be a general solution in as much as eapply is itself a
> > general solution: any number of correct bindings would be allowed.
> >
> > -- Jonathan

(***********************************************************************

Tag each goal in focus with its number and the number of focused goals.

***********************************************************************)

(*Type for the tag hypothesis*)
Inductive goalNumber(n ofN : nat) : Prop := GoalNumber.

Ltac number_goals :=
  [>
   tryif is_evar ?__Number_Goals
   then fail "number_goals: The evar name ?__Number_Goals is being used"
   else idtac | ..];
  (*Clear any previous goal number tags*)
  [> repeat match goal with H : goalNumber _ _ |- _ => clear H end..];
  [>
   assert True as _;
   [ clear; refine (let _ := ?[__Number_Goals] : nat in _) |]
  | ..];
  [> | pose (?__Number_Goals) ..];
  [>
  | lazymatch goal with
    NG := ?V : nat |- _ =>
    let rec f x n :=
        lazymatch x with
        | S ?X => f X (S n)
        | ?E =>
          is_evar E;
          let Gn := fresh "Gn" in
          assert (goalNumber n V) as Gn by exact (GoalNumber n V);
          move Gn at top;
          let H := fresh in
          set (H := E) in NG;
          instantiate (1 := (S ltac:(clear))) in (Value of H);
          subst H;
          clear NG
        end in
      f V 1
   end ..];
  [>
   lazymatch goal with
     NG := ?V : nat |- _ =>
     instantiate (1 := 0) in (Value of NG)
   end;
   exact I
  | ..].

Definition argindex(n : nat)(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 n ?T _) =>
      lazymatch (eval pattern C in f) with
        ?F _ =>
        let a := fresh "a" in
        eval cbn beta zeta in
            (fun (a : T) =>
               ltac:(let b := (eval cbn beta in (F a)) in
                     let r := remove_argindexes (S n) b in exact r))
      end
    end
  | _ => f
  end.

Load "numbergoals.v".

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

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

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 x t -> Q x y z -> R) -> True.
Proof.
  intros a b c H0 H.
  abstracted as H' eapply H with (2 := H0).
  exact I.
Qed.