Help with debugging

Stream: new members

[Max Bobbin]

Hello,

I have a goal and a hypothesis that appears to be exactly the same as the goal, yet when I use the exact tactic, I end up with a "deterministic (timeout)" error, and if I use rw it gives an error where it doesn't find an instance of the hypothesis, even though they appear to be the same. Is there a way to better examine the hypothesis and goal to see where they exactly differ? I was also wondering if there was a way to see exactly how long Lean is taking with each line. I've noticed that the proof I'm working on now takes a lot longer to compile and is sluggish to work in compared to other stuff I've worked on. I've even commented out all of my "have" proofs with sorry but that doesn't fix the sluggishness. I've had a problem before where Lean had a timeout error because it didn't properly compile a comment and I wanted to see how long Lean was taking with each line to see if I could pinpoint the problem.

[Alex J. Best]

You can click around on the term in the info-view to zoom in and try and see differences in the implicit arguments. Setting set_option pp.all true will show you everything, which is sometimes overwhelming, but the ultimate way to see what lean sees.
You might also want to try tactic#convert, to get goals for the differences between the hypothesis and original goal.
If you post a #mwe here people can try and help more.

[Max Bobbin]

Thank you! I will look at that setting. How do I turn that on? Is it something I type in my proof?

[Alex J. Best]

Just before the lemma statement

[Alex J. Best]

E.g.

set_option pp.all true

lemma hi : 1 = 2 := rfl

[Kevin Buzzard]

Before getting your hands dirty with pp.all I would try convert h if the type of h looks identical to the goal. This will give you new goals indicating where the types diverged.

[Max Bobbin]

So i tried convert h and I still get a (deterministic) timeout error. Do I need to allocate more resources to Lean?

[Max Bobbin]

If I create a minimum working example by copying over the hypothesis and goal, convert h works perfectly. So, my guess is theres another underlying problem in my code that is messing things up and causing the timeout error

[Kevin Buzzard]

If you put pp.all on then you'll see that what you see as an end user is sometimes only a very small percentage of what the term actually is; there are all sorts of things which are suppressed by default. I don't know what you mean by "copying the goal" but unless you're copying it with pp.all on, you have no guarantee that what you're copying is what the goal really is. I wouldn't bother allocating more resources to Lean -- why not post a #mwe ?

[Reid Barton]

What happens if after the exact h you put another tactic, like sorry?

[Max Bobbin]

I worked on creating a mwe. I took out the hypothesises needed for my have statements and sorryed them out and no longer go a timeout error. So, I think I know where Lean is having a problem. With convert, I now see how the two differ. Here is the mwe

import data.real.basic
import analysis.calculus.fderiv
import analysis.calculus.deriv
import measure_theory.integral.interval_integral
import analysis.calculus.parametric_integral
import measure_theory.function.strongly_measurable
import measure_theory.integral.divergence_theorem

open topological_space measure_theory filter metric
open_locale big_operators topological_space filter interval

local notation `ℝ³` := fin 3 → ℝ
local notation `ℝ² ` := fin 2 → ℝ
--set_option pp.all true
theorem some_name
(μ : measure_theory.measure ℝ³)
{V1 V2 V : (ℝ³)}{t0 ε: ℝ} [linear_order ℝ³]
{ρ ρ': ℝ → ℝ³ → ℝ}{M : ℝ → ℝ}(hV : V1 ≤ V2) {F : ℝ³ → ℝ³}{F' : (ℝ³) → (ℝ³) →L[ℝ] ℝ³}
(hM :M = λ (t : ℝ),∫ (V : ℝ³) in V1..V2,(ρ t V) ∂μ)
--differential form of the continuity equation
(DiffCont : ∀ (t : ℝ), deriv M t = - ∑ (i : fin (3)), ((∫ (x : fin 2 → ℝ) in set.Icc (V1 ∘ (i.succ_above)) (V2 ∘ (i.succ_above)), F (i.insert_nth (V2 i) x) i)  - ∫ (x : fin 2 → ℝ) in set.Icc (V1 ∘ (i.succ_above)) (V2 ∘ (i.succ_above)), F (i.insert_nth (V1 i) x) i))
:
∫ (V : ℝ³) in set.Icc V1 V2, ρ' t0 V ∂μ + ∫ (V : ℝ³) in set.Icc V1 V2, ∑(i : fin 3), (F' V) (pi.single i 1) i = 0
:=
begin
  have hM' :  deriv M t0 = ∫ (V : ℝ³) in V1..V2,(ρ' t0 V) ∂μ,
  {
    have h1 : interval_integrable (ρ' t0) μ V1 V2 ∧ has_deriv_at (λ (t : ℝ), ∫ (V : fin 3 → ℝ) in V1..V2, ρ t V ∂μ) (∫ (V : fin 3 → ℝ) in V1..V2, ρ' t0 V ∂μ) t0,
      {
        sorry,
      },
    rw hM,
    cases h1 with h2 h3,
    rw has_deriv_at.deriv,
    apply h3,
  },
  specialize DiffCont t0,
  rw hM' at DiffCont,
  have DiffCont' : ∫ (V : fin 3 → ℝ) in V1..V2, ρ' t0 V ∂μ = -∫ (V : ℝ³) in set.Icc V1 V2, finset.univ.sum (λ (i : fin 3), (F' V) (pi.single i 1) i),
  {
    sorry,
  },
  rw interval_integral.integral_of_le at DiffCont',
  rw integral_Icc_eq_integral_Ioc at DiffCont',
  rw integral_Icc_eq_integral_Ioc',
  rw integral_Icc_eq_integral_Ioc',
  rw add_eq_zero_iff_eq_neg,
  convert DiffCont',
end

[Max Bobbin]

Reid Barton said:

What happens if after the exact h you put another tactic, like sorry?

I still get the timeout error, but from my post above, I think theres something funny happening in my have statements

[Max Bobbin]

this is the full proof

--The continuity equation for mass over a control volume
import data.real.basic
import analysis.calculus.fderiv
import analysis.calculus.deriv
import measure_theory.integral.interval_integral
import analysis.calculus.parametric_integral
import measure_theory.function.strongly_measurable
import measure_theory.integral.divergence_theorem
open topological_space measure_theory filter metric
open_locale big_operators topological_space filter interval
local notation `ℝ³` := fin 3 → ℝ
local notation `ℝ² ` := fin 2 → ℝ
--set_option pp.all true
theorem some_name
(μ : measure_theory.measure ℝ³)
{V1 V2 V : (ℝ³)}{t0 ε: ℝ} [linear_order ℝ³] (ε_pos : 0 < ε) {bound : ℝ³ → ℝ}
(ρ ρ': ℝ → ℝ³ → ℝ )(M : ℝ → ℝ) (hV : V1 ≤ V2)
--differential form of the continuity equation
(DiffCont : ∀ (t : ℝ), deriv M t = - ∑ (i : fin (3)), ((∫ (x : fin 2 → ℝ) in set.Icc (V1 ∘ (i.succ_above)) (V2 ∘ (i.succ_above)), F (i.insert_nth (V2 i) x) i)  - ∫ (x : fin 2 → ℝ) in set.Icc (V1 ∘ (i.succ_above)) (V2 ∘ (i.succ_above)), F (i.insert_nth (V1 i) x) i))

--stuff for hM'
(hρ_meas : ∀ᶠ (t : ℝ) in nhds t0, ae_measurable (ρ t) (μ.restrict (set.interval_oc V1 V2)))
(hρ_int : interval_integrable (ρ t0) μ V1 V2)
(hρ'_meas : ae_measurable (ρ' t0) (μ.restrict (set.interval_oc V1 V2)))
(h_bound : ∀ᵐ (V : ℝ³) ∂μ, V ∈ set.interval_oc V1 V2 → ∀ (t : ℝ), t ∈ metric.ball t0 ε → ∥ρ' t V∥ ≤ bound V)
(bound_integrable : interval_integrable bound μ V1 V2)
(h_diff : ∀ᵐ (V : ℝ³) ∂μ, V ∈ set.interval_oc V1 V2 → ∀ (t : ℝ), t ∈ ball t0 ε → has_deriv_at (λ (t : ℝ), (ρ t V)) (ρ' t V) t)

(F : ℝ³ → ℝ³) -- flux of our fluid
(F' : (ℝ³) → (ℝ³) →L[ℝ] ℝ³) -- a partial derivatvie of our vector
--define how our flux term F relates to density and velocity

--define how mass relates to density
(hM :M = λ (t : ℝ),∫ (V : ℝ³) in V1..V2,(ρ t V) ∂μ) --Mass of control volume at time t is equal to triple integral
-- of density at time t over the control volume
--(hM' : ∀ (t:ℝ), fderiv ℝ M t = ∫(V : ℝ³) in set.Icc V1 V2, (fderiv ℝ ρ t) V) --the time derivative version of hM

--stuff for divergence theorem
(s : set (ℝ³)) -- set of ℝ³ whcih are the variables of our function (like our dimensions mass can flow)
(hs : s.countable) -- the set is finite (we don't have infinite dimensions)
(Hc : continuous_on F (set.Icc V1 V2)) --Our function is continous inside the control volume
-- Hd says that f is differentiable on the interior
(Hd : ∀ (x : fin (3) → ℝ), x ∈ set.pi set.univ (λ (i : fin (3)), set.Ioo (V1 i) (V2 i)) \ s → has_fderiv_at F (F' x) x)
-- Hi defines the divergence and says it is integrable on our control volume
(Hi :measure_theory.integrable_on (λ (x : ℝ³), ∑ (i : fin (3)), (F' x) (pi.single i 1) i) (set.Icc V1 V2) volume)

--differential form of the continuity equation
(DiffCont : ∀ (t : ℝ), deriv M t = - ∑ (i : fin (3)), ((∫ (x : fin 2 → ℝ) in set.Icc (V1 ∘ (i.succ_above)) (V2 ∘ (i.succ_above)), F (i.insert_nth (V2 i) x) i)  - ∫ (x : fin 2 → ℝ) in set.Icc (V1 ∘ (i.succ_above)) (V2 ∘ (i.succ_above)), F (i.insert_nth (V1 i) x) i))
:
∫ (V : ℝ³) in set.Icc V1 V2, ρ' t0 V ∂μ + ∫ (V : ℝ³) in set.Icc V1 V2, ∑(i : fin 3), (F' V) (pi.single i 1) i = 0
:=
begin
  have hM' :  deriv M t0 = ∫ (V : ℝ³) in V1..V2,(ρ' t0 V) ∂μ,
  {
    have h1 : interval_integrable (ρ' t0) μ V1 V2 ∧ has_deriv_at (λ (t : ℝ), ∫ (V : fin 3 → ℝ) in V1..V2, ρ t V ∂μ) (∫ (V : fin 3 → ℝ) in V1..V2, ρ' t0 V ∂μ) t0,
      {
        rw ← ae_restrict_iff at *,
        simp only [interval_integrable_iff, interval_integral.interval_integral_eq_integral_interval_oc, ← ae_restrict_iff measurable_set_interval_oc] at *,
        have := has_deriv_at_integral_of_dominated_loc_of_deriv_le ε_pos hρ_meas hρ_int hρ'_meas h_bound bound_integrable h_diff,
        exact ⟨this.1, this.2.const_smul _⟩,
        sorry,
        sorry,
      },
    rw hM,
    cases h1 with h2 h3,
    rw has_deriv_at.deriv,
    apply h3,
  },
  specialize DiffCont t0,
  rw hM' at DiffCont,
  have DiffCont' : ∫ (V : fin 3 → ℝ) in V1..V2, ρ' t0 V ∂μ = -∫ (V : ℝ³) in set.Icc V1 V2, finset.univ.sum (λ (i : fin 3), (F' V) (pi.single i 1) i),
  {
    rw integral_divergence_of_has_fderiv_within_at_off_countable,
    rw DiffCont,
    exact hV,
    finish,
    exact Hc,
    exact Hd,
    exact Hi,
  },
  rw interval_integral.integral_of_le at DiffCont',
  rw integral_Icc_eq_integral_Ioc at DiffCont',
  rw integral_Icc_eq_integral_Ioc',
  rw integral_Icc_eq_integral_Ioc',
  rw add_eq_zero_iff_eq_neg,


end

[Max Bobbin]

Ok, to update, it is the have DiffCont' statement that is causing the timeout error

[Stuart Presnell]

Just to note that neither of your #mwe s work for me: when I copy and paste them into a fresh file I get a type mismatch error at line 19 in the first one, and a unknown identifier 'F' error at line 19 of the second.

[Stuart Presnell]

Max Bobbin said:

I have a goal and a hypothesis that appears to be exactly the same as the goal, yet when I use the exact tactic, I end up with a "deterministic (timeout)" error

If your hypothesis and goal were really exactly the same (as they appear) then exact ought to be able to close the goal (unless there's some extra complication with exact that I'm not aware of, which is quite possible!) So perhaps there are details behind the scenes in the hypothesis and goal that differ.

Without setting pp.all true, you could try clicking on the goal and on the hypothesis in the Info View. In each case you should get a pop-up showing in more verbose detail what Lean thinks these terms are.

[Max Bobbin]

Interesting, I'm rewriting the proof now because I'm unhappy with its current state anyway. Hopefully, as I rewrite it I can fix the problems that I came across. In its current state, its too all across the place