0
$\begingroup$

I'm learning Lean4.

I'm trying to prove in lean4 these basic properties of subsets:

  1. $ X \subseteq X $

  2. $ X \subseteq Y , Y \subseteq Z \Rightarrow X \subseteq Z$

  3. $ X \subseteq Y , Y \subseteq X \Rightarrow X = Y $

I'm wondering whether these translations in lean4 are correct:

import Mathlib.Data.Set.Lattice
variable {α : Type*}
open Set

variable {x y z: Set α}

example (h: x ⊆ x) : x ⊆ x := by
  sorry

example (h: x ⊆ z) : x ⊆ y ∧ y ⊆ z := by
  sorry

example (h: s = t) : x ⊆ y ∧ y ⊆ x := by
  sorry
$\endgroup$
2
  • 1
    $\begingroup$ All three examples are stated incorrectly. The first is trivially true. You are assuming what you are proving. The second you have the assumptions and the concluding reversed. The third is the same plus you have s and t. $\endgroup$
    – Jason Rute
    Commented Apr 13 at 12:22
  • $\begingroup$ I rewrote my answer below to tell you the correct way to write these. $\endgroup$
    – Jason Rute
    Commented Apr 14 at 14:22

1 Answer 1

1
$\begingroup$

Edit: Rewrote answer.

The correct way to write this is:

import Mathlib.Init.Set
variable {α : Type _}
variable {x y z: Set α}

example : x ⊆ x := by
  intro a
  sorry

example (h1 : x ⊆ y) (h2 : y ⊆ z) : x ⊆ z := by
  intro a
  sorry

example (h1 : x ⊆ y) (h2 : y ⊆ x) : x = y := by
  funext a
  apply propext
  sorry

These are all in Mathlib already. You should be able to find them with the apply? tactic or http://moogle.ai .

But they are also good exercises. The main idea is that a set x : Set α is just a predicate α -> Prop and a ∈ x is just x a. So with this translation, x ⊆ y is just ∀ a : α, a ∈ x -> a ∈ y which is just ∀ a : α, x a -> y a. So to prove these, just pretend they are already translated into logic. I gave you some tactics to get you started.

$\endgroup$
2
  • $\begingroup$ But perhaps stating the theorems properly will help the OP? $\endgroup$ Commented Apr 13 at 14:30
  • $\begingroup$ Thank you for your reply @jason-rute, I have realised my mistakes. $\endgroup$
    – teoobo
    Commented Apr 14 at 17:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.