Skip to content

Instantly share code, notes, and snippets.

@mukeshtiwari

mukeshtiwari/Finite.v

Created August 18, 2016 07:03
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mukeshtiwari/ff8311aca9c7407abde8fdab86e72d57 to your computer and use it in GitHub Desktop.
Save mukeshtiwari/ff8311aca9c7407abde8fdab86e72d57 to your computer and use it in GitHub Desktop.
Download ZIP
Finite type no duplicate element
Raw
Finite.v
Theorem noduplicate : forall (l1 l2 : list bool), NoDup l1 -> NoDup l2 ->
(forall a : bool, In a l1) -> length l2 <= length l1.
@mukeshtiwari
Copy link
Author

Proof.
intros l1 l2 H1 H2 H3.
apply NoDup_incl_length. assumption.

l1, l2 : list bool

H1 : NoDup l1
H2 : NoDup l2
H3 : forall a : bool, In a l1

incl l2 l1

@mukeshtiwari
Copy link
Author

Finally proved :)

                                       (forall a : bool, In a l1) -> length l2 <= length l1.

Proof.
intros l1 l2 H1 H2 H3.
apply NoDup_incl_length. assumption.
unfold incl. intros. specialize (H3 a).
assumption.
Qed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment