The Coq mailing list

[Robert Rand <rrand AT seas.upenn.edu>]

Hi all,

I'm trying to use Ltac to apply a tactic called type_check_once to all goals until no further progress can be made. Often this requires a cascade: type_check_once might instantiate a existential variable in goal #6 which then allows us to solve goal #3. No new goals are generated in this process.

The problem is that the tactics seem to focus on a single goal, and does not cascade properly. 

In Coq 8.5 the following code worked but it fails in 8.6 (that is, we now have to call "all: type_check" multiple times in a row to solve all goals).

Ltac type_check := let n := numgoals in do n type_check_once.

(I've also tried using [> type_check_once..] in place of type_check, but this doesn't seem to buy us anything.)

The following two approaches seemed to show promise, but both fail in some cases, for reasons unclear to me:

Ltac type_check_num := 

  let pre := numgoals in 

  type_check_once;

  let post := numgoals in 

  tryif (guard post < pre) then type_check_num else idtac.

Ltac type_check_circ :=

  intros; compute;

  try (progress [> type_check_once ..]; type_check_circ)

Any suggestions?

Bonus question: These goals are generated using refine. Ideally, I'd like to use Program here, but that forces me to solve the generated obligations in order (since each is deemed to depend on the previous one). Is there any way around this (that is, to replace earlier obligations with evars and proceed to subsequent ones)?

Thanks,

Robert Rand