## Stream: new members

### Topic: How to understand this "=" in "h = h₂"?

#### chenjulang (Dec 04 2023 at 06:16):

lemma foo1 (s : Set ι) (i : ι) (h h₂ : i ∈ s) : h = h₂ := by
rfl
#print foo1

theorem foo2 : ∀ {ι : Type u_1} (s : Set ι) (i : ι) (h h₂ : i ∈ s), h = h₂ :=
fun {ι} s i h h₂ ↦ Eq.refl h


Waiting......

#### Yongyi Chen (Dec 04 2023 at 06:18):

It's proof irrelevance! i ∈ s is a Prop and any two terms of the same Prop are definitionally equal.

Oh

#### chenjulang (Dec 04 2023 at 06:32):

@Yongyi Chen Can I change it into the following theorem?

theorem foo3 : ∀ {ι : Type u_1} (s : Set ι) (i : ι) (h h₂ :Prop := i ∈ s), h = h₂ := by
intros h1 h2 h3 h4 h5
refine (Iff.to_eq ?h).symm
constructor
intro  h6


#### chenjulang (Dec 04 2023 at 06:33):

But I cannot prove it......

#### Yongyi Chen (Dec 04 2023 at 06:58):

After some digging, I have found that the syntax (h h₂ : Prop := i ∈ s) means that h and h₂ are optional parameters of type Prop with default values i ∈ s. Of course this means the user of the theorem can set h and h₂ to whatever Props they like, and so h = h₂ cannot be proved.

#### chenjulang (Dec 04 2023 at 07:11):

like this , Right?

variable (h1 : 0<1) (h2 : 0<1)
#check h1 -- h1 : 0 < 1
#check h2 -- h2 : 0 < 1
theorem foo2:  h1 = h2 := by
exact rfl


#### Yongyi Chen (Dec 04 2023 at 07:12):

I don't know what you mean by "like this."

#### chenjulang (Dec 04 2023 at 07:12):

If h1 and h2 has the same "type" , they are equal

#### chenjulang (Dec 04 2023 at 07:21):

But these h1 and h2 is not equal.
Seems like self-defined type such as "0 < 1" would work,
But System-defined type such as "N" cannot work.

variable (h1 : ℕ ) (h2 : ℕ )
#check h1 -- h1 : ℕ
#check h2 -- h2 : ℕ
theorem foo3:  h1 = h2 := by


#### Ruben Van de Velde (Dec 04 2023 at 07:52):

You may benefit from reading this chapter of #tpil: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html

#### chenjulang (Dec 04 2023 at 08:04):

Alright

Last updated: Dec 20 2023 at 11:08 UTC