calc block error: Trying to understand invalidity

Stream: lean4

[Oscar Matemb ⚛️]

import Mathlib

example {height weight parachute_resist net_resist acceleration time Svelocity : ℝ}
  (h1 : height = 300)
  (h2 : weight = 90)
  (h3 : parachute_resist = 875)
  (h4 : net_resist = (weight * 9.8) - parachute_resist)
  (h5 : acceleration = net_resist / weight)
  (h6 : time = (2 * height / acceleration)^(1/2))
  (h7 : Svelocity = acceleration * time) : Svelocity ≤ 7 ∧ time ≤ 100 :=
by
  -- Step-by-step calculations for time
  have ht : time = (2 * height / acceleration)^(1/2) := by rw [h6]
  have ha : acceleration = net_resist / weight := by rw [h5]
  have hn : net_resist = (weight * 9.8) - parachute_resist := by rw [h4]


  calc -- error at this block
    time = (2 * 300 / (net_resist / weight))^(1/2) := by rw [ht, h1, ha]
    _  = (2 * 300 / (((weight * 9.8) - parachute_resist) / weight))^(1/2) := by rw [hn]
    _  = (2 * 300 / (((90 * 9.8) - 875) / 90))^(1/2) := by rw [h2, h3]
    _  = (2 * 300 / ((882 - 875) / 90))^(1/2) := by norm_num
    _  = (2 * 300 / (7 / 90))^(1/2) := by norm_num
    _  = (2 * 300 * 90 / 7)^(1/2) := by rw [div_eq_mul_inv, mul_div_assoc]
    _  = (54000 / 7)^(1/2) := by norm_num
    _  = (7714.2857)^(1/2) := by norm_num
    _  = 87.83 := by norm_num
    _ ≤ 100 := by norm_num

  have hb : 87.83 ≤ 100 := by norm_num


  calc
    Svelocity = acceleration * time := by rw [h7]
   _  = (net_resist / weight) * (2 * height / acceleration)^(1/2) := by rw [ht, ha]
   _  = (net_resist / weight) * (2 * 300 / (net_resist / weight))^(1/2) := by rw [h1]
   _  = ((weight * 9.8) - parachute_resist) / 90 * (2 * 300 / (((weight * 9.8) - parachute_resist) / 90))^(1/2) := by rw [hn]
   _  = ((90 * 9.8) - 875) / 90 * (2 * 300 / (((90 * 9.8) - 875) / 90))^(1/2) := by rw [h2, h3]
   _  = 7 / 90 * (2 * 300 * 90 / 7)^(1/2) := by norm_num
   _  = 7 / 90 * (54000 / 7)^(1/2) := by rw [div_eq_mul_inv, mul_div_assoc]
   _  = 7 / 90 * 87.83 := by norm_num
   _  = 7 : by norm_num
   _  ≤ 7 : by norm_num

  have hs : _ ≤ 7 := by norm_num

  exact ⟨hs, hb⟩



```

[Oscar Matemb ⚛️]

Oscar Matemb ⚛️ said:
``````-- error thrown at second calc block : invalid 'calc' step, failed to synthesize Trans instance Trans Eq And ?m.2269 use set_option diagnostics true` to get diagnostic information

import Mathlib

example {height weight parachute_resist net_resist acceleration time Svelocity : ℝ}
  (h1 : height = 300)
  (h2 : weight = 90)
  (h3 : parachute_resist = 875)
  (h4 : net_resist = (weight * 9.8) - parachute_resist)
  (h5 : acceleration = net_resist / weight)
  (h6 : time = (2 * height / acceleration)^(1/2))
  (h7 : Svelocity = acceleration * time) : Svelocity ≤ 7 ∧ time ≤ 100 :=
by
  -- Step-by-step calculations for time
  have ht : time = (2 * height / acceleration)^(1/2) := by rw [h6]
  have ha : acceleration = net_resist / weight := by rw [h5]
  have hn : net_resist = (weight * 9.8) - parachute_resist := by rw [h4]


  calc -- error at this block
    time = (2 * 300 / (net_resist / weight))^(1/2) := by rw [ht, h1, ha]
    ... = (2 * 300 / (((weight * 9.8) - parachute_resist) / weight))^(1/2) := by rw [hn]
    ... = (2 * 300 / (((90 * 9.8) - 875) / 90))^(1/2) := by rw [h2, h3]
    ... = (2 * 300 / ((882 - 875) / 90))^(1/2) := by norm_num
    ... = (2 * 300 / (7 / 90))^(1/2) := by norm_num
    ... = (2 * 300 * 90 / 7)^(1/2) := by rw [div_eq_mul_inv, mul_div_assoc]
    ... = (54000 / 7)^(1/2) := by norm_num
    ... = (7714.2857)^(1/2) := by norm_num
    ... = 87.83 := by norm_num
    ... ≤ 100 := by norm_num

  have hb : 87.83 ≤ 100 := by norm_num


  calc
    Svelocity = acceleration * time := by rw [h7]
   _  = (net_resist / weight) * (2 * height / acceleration)^(1/2) := by rw [ht, ha]
   _  = (net_resist / weight) * (2 * 300 / (net_resist / weight))^(1/2) := by rw [h1]
   _  = ((weight * 9.8) - parachute_resist) / 90 * (2 * 300 / (((weight * 9.8) - parachute_resist) / 90))^(1/2) := by rw [hn]
   _  = ((90 * 9.8) - 875) / 90 * (2 * 300 / (((90 * 9.8) - 875) / 90))^(1/2) := by rw [h2, h3]
   _  = 7 / 90 * (2 * 300 * 90 / 7)^(1/2) := by norm_num
   _  = 7 / 90 * (54000 / 7)^(1/2) := by rw [div_eq_mul_inv, mul_div_assoc]
   _  = 7 / 90 * 87.83 := by norm_num
   _  = 7 : by norm_num
   _  ≤ 7 : by norm_num

  have hs : _ ≤ 7 := by norm_num

  exact ⟨hs, hb⟩



```
```````

[Kim Morrison]

Replace all the ... with _. Perhaps you were copying syntax from something in Lean 3/?

[Oscar Matemb ⚛️]

Kim Morrison said:

Replace all the ... with _. Perhaps you were copying syntax from something in Lean 3/?

oh yes, I sure did. It still threw the same error

[Kevin Buzzard]

If you add import Mathlib.Tactic then the only errors it throws to me are the ones which are obvious syntax errors (e.g. you write : instead of := in a couple of places, and the error message says exactly this). Edit: sorry, my mistake, I missed the error which you're talking about. Looking into it...

[Kevin Buzzard]

Right, the error makes sense: your goal is velocity ≤ 7 ∧ time ≤ 100 and the head symbol here is ∧ which doesn't make sense when using calc. You'll have to change the goal to an inequality before you can hope that calc works.

[Oscar Matemb ⚛️]

Okay I understand.

[Oscar Matemb ⚛️]

Thanks

[Oscar Matemb ⚛️]

I was thinking ‘’’calc’’’ could be used to prove goals with ‘’’and’’’ as well

[Oscar Matemb ⚛️]

Do you think ‘obtain’ could work

[Oscar Matemb ⚛️]

?

[Oscar Matemb ⚛️]

Do you think ‘obtain’ could work

[Damiano Testa]

constructor should work.

[Oscar Matemb ⚛️]

Could you please write it out? I’m not sure where’d it may be placed

[Ruben Van de Velde]

After the first by, perhaps

[Damiano Testa]

I'm not at a computer, but if your goal is ... ∧ ..., then constructor will create two goals.

[Oscar Matemb ⚛️]

Oh yes, I figured. Thank you!