Skip to Content.
Sympa Menu

coq-club - [Coq-Club] a trick for iterating over hypotheses

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] a trick for iterating over hypotheses


Chronological Thread 
  • From: Jonathan <jonikelee AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] a trick for iterating over hypotheses
  • Date: Mon, 08 Dec 2014 11:59:34 -0500

If you have tried to compose tacticals that iterate over hypotheses, this trick might interest you:

First, a preliminary tactic:

Ltac revert_clearbody_all :=
repeat lazymatch goal with H:_ |- _ => try clearbody H; revert H end.


Now, the real trick:

Ltac hyp_stack :=
constr:($(revert_clearbody_all;constructor)$ : True).

This tactic returns a function application term where the arguments are all of the current hypotheses (ignore the function itself). This can be used to drive iteration of various kinds over the hypotheses by popping them off of that term at the right one by one with a recursive tactic. I have found this to be very fast even when there are a very large number of hypotheses, as it avoids the non-linear performance one would get with nesting match statements to find the next hypothesis by matching the first one that doesn't match one that has been seen so far.

One might prefer a more directly supported way to do this - see enhancement request 3835 - although that would be somewhat fragile as it wouldn't compensate for changes to the order of hypotheses that might occur during iteration.

One can use the above hyp_stack trick to compose the following iterator tacticals:

Ltac next_hyp hs step last :=
lazymatch hs with (?hs' ?H) => step H hs' | _ => last end.

Tactic Notation "dohyps" tactic3(tac) :=
let hs := hyp_stack in
let rec step H hs := tac H; next_hyp hs step idtac in
next_hyp hs step idtac.

Tactic Notation "dohyps" "reverse" tactic3(tac) :=
let hs := hyp_stack in
let rec step H hs := next_hyp hs step idtac; tac H in
next_hyp hs step idtac.

Tactic Notation "do1hyp" tactic3(tac) :=
let hs := hyp_stack in
let rec step H hs := tac H + next_hyp hs step fail in
next_hyp hs step fail.

Tactic Notation "do1hyp" "reverse" tactic3(tac) :=
let hs := hyp_stack in
let rec step H hs := next_hyp hs step fail + tac H in
next_hyp hs step fail.

These iterator tacticals also support full backtracking from outside back in - which isn't currently possible if one uses match to step the iteration, as match behaves somewhat as if it is wrapped in a once tactical. There's a discussion on coqdev about maybe adding a new match tactical that would support full backtracking.

Here's a demo of the usage of the above tacticals:

Goal True.
(*create some hyps of various kinds*)
do 5 pose proof 0 as ?n0.
set (v:=n0).
do 3 pose proof true as ?b0.
dohyps (fun H => idtac H).
do1hyp (fun H => match type of H with nat => idtac H end).
try (do1hyp reverse (fun H => idtac H); fail). (*backtracking works*)
Abort.

The support of full backtracking is the motivation behind the do1hyp variants. For example, a fully backtracking version of eassumption would be:

Ltac bassumption := do1hyp (fun H => exact H).

-- Jonathan



  • [Coq-Club] a trick for iterating over hypotheses, Jonathan, 12/08/2014

Archive powered by MHonArc 2.6.18.

Top of Page