The Coq mailing list

[Gregory Malecha <gregory AT bedrocksystems.com>]

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