The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

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

> There is no "ignore line"
> though. And I must say it has a better effect with the "Set Compact
> Context" which is only available for proofgeneral I think.
> 
> 
> Just do "onAllHyps move_up_types." once you have imported the library.
> Here is a minimal header (you don't need it if you import LibHyps) to
> see what the "onAllHyps move_up_types." does at the end.
> 
> Hope this helps
> P.
> PS LibHyps:  https://github.com/Matafou/LibHyps, available as opam
> package, coq-8.11 supported but not yet declared as such in opam
> (should happen quickly).
> --------------------------8X----------------------------
> 
> Require Import List.
> Import ListNotations.
> 
> (* Credit for the harvesting of hypothesis: Jonathan Leivant *)
> Ltac harvest_hyps harvester := constr:(ltac:(harvester; constructor)
> : True).
> 
> Ltac revert_clearbody_all :=
>   repeat lazymatch goal with H:_ |- _ => try clearbody H; revert H
> end.
> 
> Ltac all_hyps := harvest_hyps revert_clearbody_all.
> 
> Ltac next_hyp hs step last :=
>   lazymatch hs with
>   | (?hs' ?H) => step H hs'
>   | _ => last
>   end.
> 
> Ltac map_hyps tac hs :=
>   idtac;
>   let rec step H hs := next_hyp hs step idtac; tac H in
>   next_hyp hs step idtac.
> 
> Ltac map_all_hyps tac := map_hyps tac all_hyps.
> 
> (* For less parenthesis: OnAllHyp tacA;tac2. *)
> Tactic Notation (at level 3) "onAllHyps" tactic(Tac) := (map_all_hyps
> Tac).
> 
> 
> Ltac revertHyp H := revert H. (* revert is a tactic notation *)
> Ltac move_up_types H := match type of H with
>                         | ?T => match type of T with
>                                 | Set => move H at top
>                                 | Type => move H at top
>                                 | _ => idtac
>                                 end
>                         end.
> 
> Goal forall
>     (l1 l2: list nat)
>     (H0: l1 = l2 ++ l2)
>     (bs1: list bool)
>     (x: nat)
>     (bs2: list bool)
>     (H1: true :: bs1 = bs2 ++ bs1)
>     (y: nat)
>     (H2: x :: l1 = y :: y :: l2),
>     l1 ++ l2 ++ l1 = (l1 ++ l2) ++ l1.
> Proof.
>   intros.
>   onAllHyps move_up_types.
>