Zulip Chat Archive

Stream: lean4

Topic: How to port to Lean 4 some Lean-3 expression


YurySerdyuk (Oct 09 2024 at 11:57):

Hi !
How to port to Lean 4 expression like
theorem trans {l₁ l₂ l₃ : List α} : l₁ ≃ l₂ → l₂ ≃ l₃ → l₁ ≃ l₃
| ⟨x, y⟩ ⟨z, w⟩ := ⟨Subset.trans x z, Subset.trans w y⟩

Lean 4 gives the error to := symbol ...

Ruben Van de Velde (Oct 09 2024 at 11:59):

Try => instead of :=

YurySerdyuk (Oct 09 2024 at 12:04):

I have tried this - gives the new error:
"identifier expected" for ⟨x, y⟩ ⟨z, w⟩ - expression

Ruben Van de Velde (Oct 09 2024 at 12:07):

Please post a #mwe

YurySerdyuk (Oct 09 2024 at 12:14):

This is full code --

import Mathlib.Data.Set.Lattice
open Set

example (α : Type) (p q : α  Prop) : ( x, p x  q x)   x, q x  p x := by
  intro
  | w, Or.inl h => exact w, Or.inr h
  | w, Or.inr h => exact w, Or.inl h

namespace List



private def equiv (l₁ l₂ : List α) := l₁  l₂  l₂  l₁
  infix:50 " ≃ " => List.equiv

@[refl, simp] theorem equiv.refl (l : List α) : l  l :=
  by simp, by simp

@[symm] theorem equiv.symm {l₁ l₂ : List α} : l₁  l₂  l₂  l₁ :=
  And.symm

@[trans] theorem equiv.trans {l₁ l₂ l₃ : List α} : l₁  l₂  l₂  l₃  l₁  l₃
  | x, y z, w => Subset.trans x z, Subset.trans w y

Note, that the example after open Set is working ..

Ruben Van de Velde (Oct 09 2024 at 12:14):

With #backticks, please

Marcus Rossel (Oct 09 2024 at 12:21):

Add a comma between ⟨x, y⟩ and ⟨z, w⟩.

YurySerdyuk (Oct 09 2024 at 12:23):

Thanks - all is working !


Last updated: May 02 2025 at 03:31 UTC