wlog performance/segfault

Stream: general

[Bolton Bailey]

Another post about a tactic that seems to take a long time. Some very strange stuff seems to be going on here with deterministic timeouts. Just after restarting lean, I run this file and the wlog tactic works for the first two theorems, but the third gives deterministic timeout. Then I comment out noncomputable theory and now the first and third wlog tactics work, but the second one fails with deterministic timeout. Then, I uncomment noncomputable theory and the server has stopped due to signal SIGSEGV.

/-
Author: Bolton Bailey
-/
import data.mv_polynomial.basic
import tactic.wlog

section

open mv_polynomial

noncomputable theory


universes u


/-- The finite field parameter of our SNARK -/
parameter {F : Type u}
parameter [field F]


/-- The coefficients of the CRS elements in the algebraic adversary's representation -/
parameters {A_α A_β B_α B_β : F}

/-- An inductive type from which to index the variables of the 3-variable polynomials the proof manages -/
@[derive decidable_eq]
inductive vars : Type
| α : vars
| β : vars

parameters {C_α C_β : F}


theorem case_1 :
  (A_α • X vars.α + A_β • X vars.β) * (B_α • X vars.α + B_β • X vars.β : mv_polynomial vars F) = 0
  -> 1 = 0
:=
begin
  intros eqn,

  wlog h : B_α = 0 using [A_α A_β B_α B_β,
                          B_α B_β A_α A_β],


end

theorem case_2 :
  (A_α • (X vars.α) + A_β • (X vars.β)) * (B_α • (X vars.α) + B_β • X vars.β : mv_polynomial vars F) = 0
  -> 1 = 0
:=
begin
  intros eqn,

  wlog h : B_α = 0 using [A_α A_β B_α B_β,
                          B_α B_β A_α A_β],


end

theorem case_3 :
  (A_α • (X vars.α) + A_β • (X vars.β)) * (B_α • X vars.α + B_β • (X vars.β : mv_polynomial vars F)) = 0
  -> 1 = 0
:=
begin
  intros eqn,

  wlog h : B_α = 0 using [A_α A_β B_α B_β,
                          B_α B_β A_α A_β],


end


end

The first two theorems correctly apply the tactic, though they do take a while.

[Bolton Bailey]

Restarting the server with noncomputable theory uncommented, now the last two cases timeout, different from before, despite the fact that it's supposed to be deterministic.

[Yaël Dillies]

Personally I prefer writing down auxiliary lemmas (stated with a have if it's not worth having on its own) because wlog never does what I want it to.