help with two proofs

Stream: lean4

[Arthur Paulino]

I'm stuck with these two proofs, which I believe shouldn't bee too hard :sad:
Can someone help me?

abbrev IntervalsSeq := List Int

namespace IntervalsSeq

@[simp] def allPositive : IntervalsSeq → Prop
  | h :: t => 0 < h ∧ allPositive t
  | _      => True

@[simp] def delta : IntervalsSeq → Int
  | h :: t => h + delta t
  | _      => 0

theorem appendPosOfPos (s s' : IntervalsSeq)
    (hps : s.allPositive) (hps' : s'.allPositive) :
      (s ++ s').allPositive := by
  cases s' with
    | nil => simp only [List.append_nil]; exact hps
    | cons h' t' => sorry

theorem deltaAppendEqSumDeltas (s s' : IntervalsSeq) :
    delta (s ++ s') = delta s + delta s' := sorry

end IntervalsSeq

Any hint is appreciated :pray:

[Henrik Böving]

The first is:

theorem appendPosOfPos (s s' : IntervalsSeq) (hps : s.allPositive) (hps' : s'.allPositive) : (s ++ s').allPositive := by
  induction s with
  | nil =>
    rw [List.nil_append]
    exact hps'
  | cons x xs ih =>
    simp only [allPositive]
    simp only [allPositive] at hps
    apply And.intro
    case left => exact hps.left
    case right => exact ih hps.right

[Kevin Buzzard]

Yeah, easier to do induction on s rather than s'

[Arthur Paulino]

Thanks!!! Indeed, so much simpler!

theorem appendPosOfPos (s s' : Intervals)
    (hps : s.allPositive) (hps' : s'.allPositive) :
      (s ++ s').allPositive := by
  induction s with
    | nil         => rw [List.nil_append]; exact hps'
    | cons _ _ hi => exact ⟨hps.1, hi hps.2⟩

[Henrik Böving]

My stab at the second would be:

theorem deltaAppendEqSumDeltas (s s' : IntervalsSeq) : delta (s ++ s') = delta s + delta s' := by
  induction s with
  | nil =>
    rw [List.nil_append]
    simp only [delta]
    rw [Int.zero_add] -- Mathlib4 proof
  | cons x xs ih =>
    simp only [delta]
    simp only [HAppend.hAppend, Append.append] at ih -- a bit ugly
    rw [ih]
    rw [add_assoc]

although as noted the happend stuff is a bit ugly and can most likely be done better.

[Kevin Buzzard]

I remember being stuck for a while on reverse(reverse L))=L when I was learning Lean. I mean, I'm a professor of mathematics and this is a triviality -- how hard can it be!

[Arthur Paulino]

Thank you very much!

[Kevin Buzzard]

Somehow the issue is that as humans we have an intuitive understanding of things and sometimes don't think recursively at all. It's like a+b=b+a is obvious for naturals because we have a geometric understanding of addition as well as a recursive one, and we just use the geometric one here.

[Yakov Pechersky]

In cases like this, I would always suggest to describe how your function operates on the different inductive constructors. That's part of building the API

[Yakov Pechersky]

append is a "derived" function that has different branches depending on the constructors of at least one of the arguments. So of course it is easier to prove things about it if you have proofs about what happens to the inductive constructors.

[Arthur Paulino]

Yakov Pechersky said:

In cases like this, I would always suggest to describe how your function operates on the different inductive constructors. That's part of building the API

Do you know an example of that?