hide things

Stream: new members

[lorã]

How to hide things propely in Lean4?

in some days ago i was working on this:

namespace MyList

--import List as L

inductive Nat : Type
  | O : Nat
  | S : Nat → Nat

open Nat

inductive List (α : Type) : Type
  | Nil  : List α
  | Cons : α → List α → List α
  deriving Repr, BEq

open List

def take {α : Type} : Nat → List α → List α
  | _, Nil              => Nil
  | O, _                => Nil
  | S n, Cons x xs => Cons x (take n xs)

def drop {α : Type} : Nat → List α → List α
  | _, Nil           => Nil
  | O, xs            => xs
  | S n, Cons _ xs => drop n xs

#check id

def concat : List α → List α → List α
  | Nil, ys       => ys
  | Cons x xs, ys => Cons x (concat xs ys)

#eval concat (Cons 3 Nil) (Cons 1 (Cons 2 Nil))


def comp : (β → γ) → (α → β) → (α → γ)
  | g, f, x => g (f x)

infixl: 55 " ∘ "   => comp


theorem concat_take_drop {α : Type} : ∀(xs : List α), ∀(n : Nat),
  concat (take n xs) (drop n xs) = xs :=
by
 intro xs
  induction xs with
  | Nil =>
    intro n
    rw [take]
    rw [drop]
    rw [concat]

  | Cons k ks HI =>
      intro n
      match n with
      | O =>
        rw [take]
        rw [drop]
        rw [concat]
        exact List.noConfusion
        exact List.noConfusion

      |S k =>
        rw [take]
        rw [drop]
        rw [concat]
        rw [HI k]

theorem take_drop_drop_take {α : Type} : ∀(xs: List α), ∀(n m : Nat),
  (comp (take m) (drop n)) xs = (comp (drop m) (take n)) xs :=
by

but beeing unable to use fresh simbols because all of they are already pick make the things so much verbous and if i try to use some of the built-in ones, the inductions and rw's would not act like i would like to (or like i would expect to).

[lorã]

So, theres a good way to just hide things and use my own definicions with the simbols that i want to? Ive been looking for some solutions but they didnt really work. Even with hiding, for examble, im not able to hide the \circ, cause its a notation and etc etc.

[Kyle Miller]

It's not possible to hide notations unfortunately. The choices are (1) define your notation and hope Lean can disambiguate it or (2) use a different symbol like " ∘' ".

[Kyle Miller]

You don't need to define your own comp however, since that's already the definition.

[Kyle Miller]

def comp : (β → γ) → (α → β) → (α → γ)
  | g, f, x => g (f x)

example (g : β → γ) (f : α → β) : comp g f = g ∘ f := rfl

[Kyle Miller]

draell said:

but beeing unable to use fresh simbols because all of they are already pick make the things so much verbous and if i try to use some of the built-in ones, the inductions and rw's would not act like i would like to (or like i would expect to).

Can you expand on this? Which notations and symbols?

[lorã]

The [] by example