x ∈ list + maximal wrt string inclusion implies x ∈ list

Stream: general

[nrs]

def NonemptyList (α : Type)  := @PSigma (List α) (fun list => list ≠ [])

def nextUncontainedString : NonemptyList String -> String
  | ⟨x :: y :: ys, _⟩ => if List.isPrefixOf x.toList y.toList
                              then nextUncontainedString ⟨y :: ys, by simp⟩
                              else nextUncontainedString ⟨x :: ys, by simp⟩
  | ⟨([x]), _⟩ => x
termination_by nel => match nel with | ⟨l, _⟩ => l.length

def MemberOfList (α : Type) (l : List α) := @PSigma α (fun a => a ∈ l)

The above isn't in theorem format because I'm trying to use these to write a dependently-typed application. Now, I'm trying to write the function

def memFromNextUncontainedString : (nel : NonemptyList String) -> MemberOfList String nel.fst
  | nel => PSigma.mk (nextUncontainedString nel) proof
  where proof := sorry

Is the only approach to proof here to use by rw [nextUncontainedString.eq_def] then repeatedly split until all cases are covered?

context: this is a lemma for a function def filterOutNonMaximalWrtStringInclusion : Nonemptylist String -> Nonemptylist String that filters out all members of the list that are not maximal wrt string prefix inclusion (so ["/my/path", "/another/path", "/my/path/with/more"] is transformed to ["/another/path", "/my/path/with/more"])

[nrs]

hm, I think working with something similar to

inductive NonemptyList' (A : Type)
| first: A -> NonemptyList' A
| cons: A -> NonemptyList' A -> NonemptyList' A

would make the workflow more natural here, but this probably throws away much of the work on Lists in the ecosystem

[Daniel Weber]

Is there a reason you're using PSigma instead of docs#Subtype ?

[nrs]

Daniel Weber said:

Is there a reason you're using PSigma instead of docs#Subtype ?

None at all, just to remind myself that Subtype is a special kind of sigma type. Will adopt it if it it makes easier it to prove properties

[nrs]

edit: thought I had an answer, but it is wrong

[Kim Morrison]

Generally for something like this it is much easy to write your definitions just in terms of List, then prove after the fact that if the input is nonempty the output is nonempty.

[Kim Morrison]

Moreover generality is your friend, you could write a filterMaximal for any type with LT, then specialize that to string prefix order.

[nrs]

Kim Morrison said:

Generally for something like this it is much easy to write your definitions just in terms of List, then prove after the fact that if the input is nonempty the output is nonempty.

These are great suggestions! tyvm for the help