The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Unsafe is in fact unsafe, and constr does more checks, not to mention more type inference.  I still think it's worth reporting as a bug that transcribing Ltac to Ltac2 incurs a 3x performance overhead in this case; this seems worth understanding and fixing, or else there's not much hope of getting people to switch from Ltac to Ltac2.

On Sat, Aug 1, 2020, 13:17 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.

On Sat, Aug 1, 2020 at 10:09 AM Jason Gross <jasongross9 AT gmail.com> wrote:

I'm not sure how to get Ltac2 that is similar to Ltac and comparably fast (though this example looks like a bug worth reporting), if you use the low-level features in Constr.Unsafe to build your term, I expect you'll get something somewhat faster than uconstr.  Note that if you do this, you'll have to build the types at the same time as the terms, so that you can avoid evars.

On Fri, Jul 31, 2020, 23:04 Gregory Malecha <gregory AT bedrocksystems.com> wrote:

Hello --

I'm trying to evaluate whether Ltac2 is viable for some automation that I'm writing and I'm having a lot of difficulty understanding how to write things efficiently. I cooked up the following as a stupidly simple problem to get myself started:

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

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

Goal foo 10.
  simpl.
  Time Control.enter (fun () =>
    let g := Control.goal () in
    let r := build g in
    exact ($r)).

But it runs about 3x slower than `repeat constructor` suggesting that I'm doing something inefficient. The following Ltac1 program also seems significantly faster, suggesting that it isn't simply the fact that I'm doing an extra match.

Ltac prove_it :=
  lazymatch goal with
  | |- True => exact I
  | |- _ /\ _ => refine (conj _ _); [ prove_it | prove_it ]
  end.

(though replacing [refine] with [apply] is comparable). Even constructing the term in Ltac using cps is significantly faster despite all of the continuations that are constructed. Similarly, the following program is also much faster:

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 uconstr:(conj P Q)))
  end.

Even replacing [uconstr] with [constr] is faster. How do you prove things efficiently in Ltac2? Is there a pattern that I'm missing? Is the interpreter much slower?

Any suggestions or pointers would be greatly appreciated. Thank you!

--

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