Lean segfaults on `unfold`, and is slower than Coq at reduction

[JasonGross]

Consider this Lean file:

def some_lets : ℕ → ℕ → ℕ
| 0            v := v
| (nat.succ n) v := let k := some_lets n v + some_lets n v in some_lets n k

def some_unfolded_lets (n : ℕ) : Σ' v : ℕ , v = some_lets 6 n :=
begin
  constructor; unfold some_lets; constructor
end

universe variables u v
inductive let_inM : Sort u → Sort (u+1)
| ret : Π {A : Sort u} , A → let_inM A
| bind : Π {A : Sort u} {B : Sort u} , let_inM A → (A → let_inM B) → let_inM B
| app2 : Π {A B C : Sort u} , (A → B → C) → let_inM A → let_inM B → let_inM C

def denote_let_inM : Π {A : Sort (u+1)} , let_inM A → A
| A (@let_inM.ret ._ v) := v
| B (@let_inM.bind A ._ v f) := let v' := @denote_let_inM A v in @denote_let_inM B (f v')
| C (@let_inM.app2 A B ._ f x y) := f (denote_let_inM x) (denote_let_inM y)
attribute [simp] denote_let_inM

def under_lets : Π {A B : Sort (u+1)} , let_inM A → (A → let_inM B) → let_inM B
| A B (@let_inM.ret ._ v) f := let_inM.bind (let_inM.ret v) f
| A B (@let_inM.bind A2 ._ v g) f := under_lets v (λ v' , under_lets (g v') f)
| A B (@let_inM.app2 A2 B2 ._ g x y) f := under_lets x (λ x' , under_lets y (λ y' , f (g x' y')))
attribute [simp] under_lets

def lift_lets : Π {A : Sort (u+1)} , let_inM A → let_inM A :=
  λ A v , @under_lets A A v (@let_inM.ret _)

lemma denote_under_lets_correct {A : Sort (u+1)} {B : Sort (u+1)} (v : let_inM A)
 : ∀ (f : A → let_inM B), @denote_let_inM B (@under_lets A B v f)
                            = @denote_let_inM B (f (@denote_let_inM A v)) :=
begin
  induction v; intro f; try { reflexivity }; simp; rewrite ih_1; rewrite ih_2
end
lemma lift_lets_correct {A : Sort (u+1)} (v : let_inM A)
 : denote_let_inM v = denote_let_inM (lift_lets v)
:= by symmetry; apply denote_under_lets_correct

meta def reify_to_let_in_pexpr : expr → pexpr
| (expr.elet n ty val body) :=
    let val' := reify_to_let_in_pexpr val in
    let body' := reify_to_let_in_pexpr body in
    let body' := expr.lam n binder_info.default (pexpr.of_expr ty) body' in
    ``(@let_inM.bind %%ty _ %%val' %%body')
| `(%%a + %%b) := let a' := reify_to_let_in_pexpr a in
                  let b' := reify_to_let_in_pexpr b in
                  ``(@let_inM.app2 _ _ _ (λ a' b' , a' + b') %%a' %%b')
| e := ``(@let_inM.ret _ %%e)

meta def is_eq : expr → option (expr × expr × expr)
| `(@eq %%α %%a %%b) := some (α, a, b)
| _                  := none

open tactic
meta def unify_reify_rhs_to_let_in : tactic unit :=
  do [g] <- tactic.get_goals,
     gl_ty <- tactic.infer_type g,
     match is_eq gl_ty with
     | some (ty, ev, v)
        := let v' := reify_to_let_in_pexpr v in
           let v' := ``(denote_let_inM %%v') in
           do _ <- tactic.refine ``(@eq.trans _ _ %%v' _ _ (eq.refl _)),
              (g0 :: g :: []) <- tactic.get_goals,
              tactic.set_goals [g]
     | none := tactic.fail "not an equality"
     end

-- set_option debugger true
set_option profiler true
open tactic
def some_lifted_lets (n : ℕ) : Σ' (v : ℕ), v = psigma.fst (some_unfolded_lets n) :=
begin
  constructor; unfold some_unfolded_lets psigma.fst; symmetry; transitivity; symmetry,
  {
    unify_reify_rhs_to_let_in; symmetry; to_expr ``(lift_lets_correct) >>= apply
  },
  {
     symmetry; transitivity; symmetry,
     {
       unfold lift_lets under_lets; constructor
      },
     { unfold denote_let_inM; constructor }
  }

end

I get:

-*- mode: compilation; default-directory: "~/Documents/repos/lean-playgorund/" -*-
Compilation started at Sun Jun  4 18:17:20

/home/jgross/Documents/repos/lean/bin/lean  /home/jgross/Documents/repos/lean-playgorund/test.lean
tactic execution took 0ms
tactic execution took 0ms
tactic execution took 0ms
tactic execution took 0ms
tactic execution took 0ms
tactic execution took 0ms
tactic execution took 2.46s
 2460ms   100.0%   tactic.istep._lambda_1
 2460ms   100.0%   scope_trace
 2460ms   100.0%   _interaction._lambda_2
 2460ms   100.0%   tactic.istep
 2459ms   100.0%   tactic.seq
 2454ms    99.8%   tactic.solve1
 2162ms    87.9%   tactic.interactive.dunfold
 2162ms    87.9%   tactic.dunfold
 1212ms    49.3%   tactic.dunfold_core._lambda_4
 1212ms    49.3%   tactic.dsimplify_core
  950ms    38.6%   tactic.change
  632ms    25.7%   tactic.dunfold_core._lambda_2
  376ms    15.3%   tactic.dunfold_expr_core
  295ms    12.0%   unify_reify_rhs_to_let_in
  289ms    11.7%   unify_reify_rhs_to_let_in._lambda_2
  289ms    11.7%   tactic.refine
  216ms     8.8%   tactic.to_expr
  154ms     6.3%   interaction_monad.failed
  138ms     5.6%   list.any
  132ms     5.4%   list.foldr
  111ms     4.5%   list.any._lambda_1
   93ms     3.8%   expr.is_app_of
   83ms     3.4%   tactic.dunfold_core._lambda_3
   73ms     3.0%   tactic.exact
   69ms     2.8%   char.of_nat
   63ms     2.6%   expr.get_app_fn
   27ms     1.1%   string.str
   23ms     0.9%   expr.is_constant_of
   19ms     0.8%   interaction_monad.fail
   16ms     0.7%   nat.decidable_lt
   13ms     0.5%   interaction_monad.mk_exception
   10ms     0.4%   coe_decidable_eq
    7ms     0.3%   bool.decidable_eq
    7ms     0.3%   all_goals_core
    7ms     0.3%   tactic.all_goals
    7ms     0.3%   bor
    6ms     0.2%   expr.lam
    6ms     0.2%   reify_to_let_in_pexpr
    4ms     0.2%   expr.const
    4ms     0.2%   expr.subst
    3ms     0.1%   return
    3ms     0.1%   expr.local_const
    2ms     0.1%   interaction_monad.monad
    2ms     0.1%   tactic.apply_core
    2ms     0.1%   decidable.to_bool
    2ms     0.1%   relation_tactic
    2ms     0.1%   _private.2546847332.relation_tactic._lambda_2
    1ms     0.0%   name.has_decidable_eq
    1ms     0.0%   tactic.set_goals
    1ms     0.0%   expr.elet
    1ms     0.0%   interaction_monad.monad._lambda_4
elaboration of some_lifted_lets took 2.68s
type checking time of some_lifted_lets took 5.01ms

Compilation finished at Sun Jun  4 18:17:25

If I change the 6 to `7, then I get:

-*- mode: compilation; default-directory: "~/Documents/repos/lean-playgorund/" -*-
Compilation started at Sun Jun  4 18:18:26

/home/jgross/Documents/repos/lean/bin/lean  /home/jgross/Documents/repos/lean-playgorund/test.lean
tactic execution took 0ms
tactic execution took 0ms
tactic execution took 0ms
tactic execution took 0ms
tactic execution took 0ms
tactic execution took 0ms

Compilation segmentation fault at Sun Jun  4 18:18:31

To remove the segfault, I need to comment out unfold denote_let_inM; constructor and also replace unfold lift_lets under_lets; constructor with unfold lift_lets.

For reference, here is a similar-length Coq file which performs better than Lean:

Definition Let_In {A B} (v : A) (f : A -> B) := let v' := v in f v'.
Reserved Notation "'dlet' x .. y := v 'in' f"
         (at level 200, x binder, y binder, f at level 200,
          format "'dlet'  x .. y  :=  v  'in' '//' f").
Notation "'dlet' x .. y := v 'in' f" := (Let_In v (fun x => .. (fun y => f) .. )).
Fixpoint some_lets (n : nat) (v : nat) : nat :=
  match n with
  | 0 => v
  | S n' => dlet k := some_lets n' v + some_lets n' v in some_lets n' k
  end.

Definition some_unfolded_lets (n : nat) : { v : nat | v = some_lets 6 n }.
Proof.
  econstructor; cbv beta iota delta [some_lets]; constructor.
Defined.

Inductive let_inM : Type -> Type :=
| ret {A : Type} : A -> let_inM A
| bind {A : Type} {B : Type} : let_inM A -> (A -> let_inM B) -> let_inM B
| app2 {A B C : Type} : (A -> B -> C) -> let_inM A -> let_inM B -> let_inM C.

Fixpoint denote_let_inM {A : Type} (v : let_inM A) : A
  := match v with
     | ret v => v
     | bind v f => (dlet v' := denote_let_inM v in denote_let_inM (f v'))
     | app2 f x y => f (denote_let_inM x) (denote_let_inM y)
     end.

Fixpoint under_lets {A B : Type} (v : let_inM A) : (A -> let_inM B) -> let_inM B
  := match v with
     | ret v => fun f => bind (ret v) f
     | bind v g => fun f => under_lets v (fun v' => under_lets (g v') f)
     | app2 g x y => fun f => under_lets x (fun x' => under_lets y (fun y' => f (g x' y')))
     end.

Definition lift_lets : forall {A : Type} , let_inM A -> let_inM A :=
  fun A v => @under_lets A A v (@ret _).

Lemma denote_under_lets_correct {A : Type} {B : Type} (v : let_inM A)
  : forall (f : A -> let_inM B), @denote_let_inM B (@under_lets A B v f)
                                           = @denote_let_inM B (f (@denote_let_inM A v)).
Proof.
  induction v; intro f; try reflexivity; simpl; unfold Let_In; simpl;
    rewrite ?IHv, ?IHv1, ?IHv2, ?H; try reflexivity.
Qed.
Definition lift_lets_correct {A : Type} (v : let_inM A)
  : denote_let_inM v = denote_let_inM (lift_lets v).
Proof. symmetry; apply @denote_under_lets_correct. Qed.

Ltac reify_to_let_in_pexpr e :=
  lazymatch e with
  | (dlet n : ?T := ?val in ?body)
    => let val' := reify_to_let_in_pexpr val in
       let n' := fresh n in
       let n' := fresh n' in
       let n' := fresh n' in
       let n' := fresh n' in
       let body' := constr:(fun n : T => match body with
                                         | n' => ltac:(let n'' := (eval cbv delta [n'] in n') in
                                                       let ret := reify_to_let_in_pexpr n'' in
                                                       exact ret)
                                         end) in
       constr:(bind val' body')
  | (?a + ?b)%nat
    => let a' := reify_to_let_in_pexpr a in
       let b' := reify_to_let_in_pexpr b in
       constr:(app2 Nat.add a' b')
  | ?v => constr:(ret v)
  end.

Ltac unify_reify_rhs_to_let_in :=
  lazymatch goal with
  | [ |- ?ev = ?v :> ?ty ]
    => let v' := reify_to_let_in_pexpr v in
       let v' := constr:(denote_let_inM v') in
       refine (@eq_trans _ _ v' _ _ _); [ | abstract (cbv [denote_let_inM]; reflexivity) ]
  end.

Ltac vm_compute_rhs :=
  lazymatch goal with
  | [ |- ?ev = ?rhs ]
    => let rhs := match (eval pattern Nat.add in rhs) with ?rhs _ => rhs end in
       let rhs' := (eval vm_compute in rhs) in
       unify ev (rhs' Nat.add);
       abstract (exact_no_check (f_equal (fun f => f Nat.add) (eq_refl rhs' <: rhs' = rhs)))
  end.

Definition some_lifted_lets (n : nat) : { v : nat | v = proj1_sig (some_unfolded_lets n) }.
Proof.
  Time
    econstructor; unfold some_unfolded_lets, proj1_sig; symmetry; etransitivity; symmetry;
    [ unify_reify_rhs_to_let_in; symmetry; apply lift_lets_correct
    | symmetry; etransitivity; symmetry;
        [ apply f_equal; vm_compute_rhs
        | cbv [denote_let_inM]; reflexivity ] ].
Defined.

It has some Coq-specific-optimization around the equivalent of unfold. With this optimization, Coq is much slower than Lean on the reification step, but much faster on the reduction; is there a way to improve the performance of Lean's unfolding and reduction machinery?

[leodemoura]

The commit above fixes the segfault. Now, we get the following error:

let.lean:87:0: error: deep recursion was detected at 'replace' (potential solution: increase stack space in your system)

I can process the example by increasing the thread stack size (command line option -s).

lean -s 50000 let.lean 

I didn't investigate the performance problem yet.