lean3
lean3 copied to clipboard
Published
20 hours ago •
leanprover
leanprover
Lean segfaults on `unfold`, and is slower than Coq at reduction
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?
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.
