The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Here is a description of lazymatch in Coq 8.4:
Recall that there are two phases of tactic evaluation: there is tactic _expression_ evaluation, and tactic running.  During tactic running, sequencing, refine, rewrite, etc, are executed. During tactic _expression_ evaluation, the following constructs are evaluated, of found in the head position:
- tactic calls are resolved/followed
- [let ... in ...] binds the evaluation of it's argument to the name, and does substitution
- constr:(...) is evaluated and type checked
- lazymaytch ... with ... end is evaluated (with back tracking), and returns the first matching branch which successfully _expression_-evaluates
- match ... with ... end is evaluated (with backtracking) *and the branch is eagerly executed*.  Note that in this picture, match is strange, because it forces the execution of a tactic to come early.  If you've ever seen "immediate tactic-producing match statements are not allowed in lets", or similar, I'm guessing it's because this confusing behavior is a wart that the original devs implementing Ltac wanted to hide.  So the only place you can notice it in 8.4 is if you stick match inside of lazymatch and play with failure levels.

In 8.5, you can do strange things like:
  let dummy := match goal with _ => rewrite H end in
  constr:(true)
and have constr-producing tactics with side effects.  However, you can no longer do:
  let tac := lazymatch b with
                  | true => tac1
                  | false => tac2
                  end in
  tac long args.
This is because in 8.5, lazymatch also eagerly evaluates it's branches, without backtracking.

On Wed, Oct 12, 2016, 5:10 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 10/12/2016 05:03 PM, Clément Pit--Claudel wrote:
> Hi coq-club,
>
> The CHANGES file says:
>
>      - Matching using "lazymatch" was fundamentally modified. It now behaves
>        like "match" (immediate execution of the matching branch) but without
>        the backtracking mechanism in case of failure.
>
> The description of the new behaviour sounds close to what my understanding of lazymatch was in 8.4 (as long as the result of the lazy match isn't bound to a variable).  Beyond the 8.4 issue that caused lazymatch to backtrack when a branch contained a type error, what are examples of differences between the old and the new lazymatch?
>
> Thanks!
> Clément.
>

Unfortunately, I don't have an 8.4 around to test this on - but AFAIR
lazymatch prior to 8.5 didn't have the greedy evaluation of branches
behavior as does (and did) match.  Hence, something like:

Goal True.
let x := lazymatch goal with _ => idtac "hello" end in
idtac "there".

in 8.4 would just print "there" and not "hello" "there".

-- Jonathan