The Coq mailing list

[Gregory Malecha <gregory AT bedrocksystems.com>]

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