The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

1. I think this is effectively the difference between running check at every leaf vs running once for all leaves.

2. Ultimately, lazy_match does use the OCaml equivalent of Constr.Unsafe, but there's extra layers of interpretation overhead.  Note that the difference between using Constr.Unsafe and the like to build terms in Ltac2 vs writing exactly the same algorithm as an OCaml plugin is about 300x, last I checked, so there's reason to believe that the overhead of interpretation is significant.  Presumably someday this compilation process can become automatic, but that feature isn't implemented yet.

On Sun, Aug 2, 2020 at 10:44 AM Gregory Malecha <gregory AT bedrocksystems.com> wrote:

Thanks Jason and Jonathan!

I'm still on 8.11.2, it looks like I need to upgrade to 8.12 to get more array functions.

Regarding the two suggestions,

1. In the AST, references to globals are leaf nodes (modulo universe instances), so I had expected this to happen anyways without any manual intervention on my part. I do have other cases with universe polymorphism and in those cases I definitely can not pull that trick without building a sub-optimal proof at the universe level. I could do the comparisons manually, but it seems that there are no equality tests on types like [inductive] and [constructor]. I opened an issue for that: https://github.com/coq/coq/issues/12786

That said, this is great because it actually gives me a way to bind the universe [instance], unfortunately, there seem to be no accessors on [instance]..so it might not help as much as I would like.

2. I want to check that the head constant is [and], otherwise I'd be returning an incorrect proof term. Again, I am probably mistaken, but I thought that lazy_match was implemented using Constr.Unsafe. This should definitely be possible when the pattern is linear, and might also be true when the pattern is non-linear, though there would be some side-conditions to check.

On Sun, Aug 2, 2020 at 12:14 AM Jason Gross <jasongross9 AT gmail.com> wrote:

> constructing the array is quite annoying, maybe there is notation that I missed?

I generally use `Array.of_list` with the notation `[x; y; z]` (or maybe it's `[|x; y; z|]`?, I can't quite recall),which is a tiny bit more expensive, but much more compact.

> (* Ltac2 (Unsafe) implementation *)

I would suggest two changes:

1. pass in `constr:(I)` and `'conj` at the top level (and pass them down recursively) so you only construct them once rather than at every node

2. Use `match Constr.Unsafe.kind p with` rather than `lazy_match!`.  It's significantly more opaque and less robust to mis-matches (generally, e.g., I'll skip the check that the head constr is and, skip the array length checks, etc), but I think it's significantly faster.

On Sat, Aug 1, 2020 at 11:57 PM Gregory Malecha <gregory AT bedrocksystems.com> wrote:

The unsafe version of the tactic is included below, constructing the array is quite annoying, maybe there is notation that I missed? Certainly adding the [check] here is pretty expensive.

I filed an issue here which contains the full text (also included below): https://github.com/coq/coq/issues/12785

Returning to the earlier question, I get back a decent amount of performance in my original tactic by using [@conj p q l r] rather than [conj l r] in both the Ltac and the Ltac2 case.

My latest figures show less performance loss than I originally measured (2x instead of 3x), there might have been too much jitter in my tests. The numbers below are averages of 10 fresh runs.

(* Ltac2 implementation *)
Ltac2 rec build2 p :=
  lazy_match! p with
  | True => constr:(I)
  | ?p /\ ?q =>
    let l := build2 p in
    let r := build2 q in
    constr:(@conj $p $q $l $r)
  end.

(* Ltac2 (Unsafe) implementation *)
Ltac2 rec build2_unsafe p :=
  lazy_match! p with
  | True => constr:(I)
  | ?p /\ ?q =>
    let l := build2_unsafe p in
    let r := build2_unsafe q in
    let ary := Array.make 4 p in
    let _ := Array.set ary 1 q in
    let _ := Array.set ary 2 l in
    let _ := Array.set ary 3 r in
    Unsafe.make (Unsafe.App 'conj ary)
  end.

(* Ltac2 (Unsafe-Check) implementation *)
Ltac2 rec build2_unsafe_check p :=
  lazy_match! p with
  | True => constr:(I)
  | ?p /\ ?q =>
    let l := build2_unsafe_check p in
    let r := build2_unsafe_check q in
    let ary := Array.make 4 p in
    let _ := Array.set ary 1 q in
    let _ := Array.set ary 2 l in
    let _ := Array.set ary 3 r in
    match Unsafe.check (Unsafe.make (Unsafe.App 'conj ary)) with
    | Val v => v
    | Err e => Control.throw e
    end
  end.

(* Ltac implementation *)
Ltac build_it p k :=
  lazymatch p with
  | True => k constr:(I)
  | ?p /\ ?q => build_it p ltac:(fun P => build_it q ltac:(fun Q => k constr:(@conj p q P Q)))
  end.

Fixpoint build_goal (n : nat) : Prop :=
  match n with
  | 0 => True
  | S n => build_goal n /\ build_goal n
  end.

Goal build_goal 10.
  simpl.
  Time Control.enter (fun () =>
    let g := Control.goal () in
    let pf := build2 g in
    exact $pf).

  (** ~0.2241s *)
  Undo.
  Time Control.enter (fun () =>
    let g := Control.goal () in
    let pf := build2_unsafe g in
    exact $pf).

  (** ~0.1444s *)

Time Control.enter (fun () =>
    let g := Control.goal () in
    let pf := build2_unsafe_check g in
    exact $pf).

  (** ~0.2307s *)

  Undo.
  Time repeat constructor.

  (** ~0.1658s *)
  Undo.
  Time ltac1:(match goal with
              | |- ?G => build_it G ltac:(fun p => exact p)
              end).

  (** ~0.0939s *)
Qed.

On Sat, Aug 1, 2020 at 2:02 PM jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

On Sat, 1 Aug 2020 13:16:32 -0400
Gregory Malecha <gregory AT bedrocksystems.com> wrote:

> Thanks for pointing that out. It inspired me to look at the resulting
> code. I get the following:
>
> build : constr -> constr
> build :=
>   fun x =>
>   let rec build :=
>     fun p =>
>     let m :=
>       [Pattern.MatchPattern, pattern:(True), (fun _ => fun _ =>
> constr:(I)); Pattern.MatchPattern, pattern:(and ?p ?q),
>         (fun _ =>
>          fun p => let q := Array.get p 1 with p := Array.get p 0 in
> let l := build p in let r := build q in constr:(@conj _ _ _ _))] with
>       t := p in
>     Pattern.lazy_match0 t m in
>   build x
>
> I assume that the `_`s in the constr: are printing artifacts.
>
> You are right, building the term with Unsafe gets me performance on
> par with Ltac. It seems like this would be a natural implementation
> of constr, and for some reason I thought that I had read that it was
> in the manual, but I must be mistaken.

Grregory,

What does the Unsafe-using version of your example look like?

--

Gregory Malecha

Mail: gregory AT bedrocksystems.com

BedRock

Systems Inc
UNBREAKABLE FOUNDATION FOR

FORMALLY SECURED COMPUTING

--

Gregory Malecha

Mail: gregory AT bedrocksystems.com

BedRock

Systems Inc
UNBREAKABLE FOUNDATION FOR

FORMALLY SECURED COMPUTING