Zulip Chat Archive

Stream: new members

Topic: Help with proof on list membership

yokatta (Jul 03 2023 at 03:27):

I'm trying to complete the following proof:

import Mathlib.Data.List.Basic

theorem foo {α : Type} {as : List α} {ms : List { a // a  as }} (nodup : List.Nodup ms) : ms.length  as.length := by
  cases nodup with
  | nil => simp only [List.length_nil, zero_le]
  | cons p nodup =>
      rename_i m ms
      rw [List.length_cons]
      have h := foo nodup

      show ms.length < as.length

but am not sure how to proceed. Intuitively, I can convince myself by imagining a mapping between the two lists where the map from ms to as has to be injective, but it seems like there should be an easier way of proving it?

Martin Dvořák (Jul 03 2023 at 09:01):

I don't know how to finish your proof, but if I were working on it, I would start as follows:

lemma qux {α : Type} {ms : List α} (nodup : List.Nodup ms) {as : List α} (subt :  x  ms, x  as) :
  ms.length  as.length :=
  revert as
  induction ms with
  | nil => simp
  | cons m ms ih =>
      intros as hyp
      -- apply `ih` to the list `as` without the element `m`

Martin Dvořák (Jul 03 2023 at 09:07):

What I want to say is that I'd perform induction on ms but I cannot have as fixed. I want to work with ∀ as in the induction step.

Last updated: Dec 20 2023 at 11:08 UTC