The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi Jonathan

Nice!

P

Le jeu. 2 avr. 2020 à 19:14, jonikelee AT gmail.com <jonikelee AT gmail.com> a écrit :

On Thu, 2 Apr 2020 11:55:51 -0400
"jonikelee AT gmail.com" <jonikelee AT gmail.com> wrote:

> On Thu, 2 Apr 2020 11:23:31 -0400
> "jonikelee AT gmail.com" <jonikelee AT gmail.com> wrote:
>
> > On Thu, 2 Apr 2020 10:45:49 +0200
> > Pierre Courtieu <Pierre.Courtieu AT cnam.fr> wrote:
> >   
> > > Nice ltac!
> > > I have something similar in LibHyps without touching the proof
> > > term (thanks to ltac hack from J.Leivant).   
> >
> > Here's the source for that hypothesis harvesting and iteration hack:
> > https://github.com/jonleivent/mindless-coding-phase2/blob/master/hypiter.v
> > 
>
> Somewhere, I had a version of this hack that grouped like-typed
> hypotheses together to take full advantage of ProofGeneral's ability
> to list adjacent like-typed hypotheses on the same line.  I'll look
> for it...

This 'minlines' tactic is it, from:
https://github.com/jonleivent/mindless-coding-phase2/blob/master/utils.v

Ltac revert_all :=
  repeat lazymatch goal with H:_ |- _ => revert H end.

Ltac get_value H := eval cbv delta [H] in H.

Ltac has_value H := let X:=get_value H in idtac.

Ltac minlines :=
  idtac; (*prevent early eval*)
  let stop:=fresh "stop" in
  generalize I as stop;
  revert_all;
  let rec f :=
    try (intro;
         lazymatch goal with H:?T |- _ =>
          first[constr_eq H stop; clear stop
               |let v := get_value H in
                try match goal with H' := v : T |- _ =>
                 first[constr_eq H H'; fail 1
                      |move H before H'] end; f
               |try match goal with H':T |- _ =>
                 first[constr_eq H H'; fail 1
                      |has_value H'; fail 1
                      |move H before H'] end; f
               |f]
          end)
  in f.



What this does to the goal in Pierre's example in ProofGeneral:  After
the 'onAllHyps move_up_types' tactic, the goal is:

1 subgoal (ID 63)

  y : nat
  bs2 : list bool
  x : nat
  bs1 : list bool
  l2, l1 : list nat
  H0 : l1 = l2 ++ l2
  H1 : true :: bs1 = bs2 ++ bs1
  H2 : x :: l1 = y :: y :: l2
  ============================
  l1 ++ l2 ++ l1 = (l1 ++ l2) ++ l1

If you then execute 'minlines', the goal becomes:

1 subgoal (ID 96)

  y, x : nat
  bs2, bs1 : list bool
  l2, l1 : list nat
  H0 : l1 = l2 ++ l2
  H1 : true :: bs1 = bs2 ++ bs1
  H2 : x :: l1 = y :: y :: l2
  ============================
  l1 ++ l2 ++ l1 = (l1 ++ l2) ++ l1


They are usable separately or together.  I think minlines is idempotent.

I have found minlines particularly useful in goals which have many
hypotheses of simple types (consider a goal with 20 nats scattered
about) and only a few with complex types important to furthering the
proof.

-- Jonathan