Zulip Chat Archive

Stream: lean4

Topic: What is the best souce of documentation?


kvanvels (Aug 08 2022 at 00:43):

I am a newbie trying to implement a bunch of statements about the natural numbers (basically the natural numbers game in lean4) I am trying to prove very simple things like for all natural numbers a, a < a + 1, which is easy enough. I want to state and prove a trivial corollary that for all natural number a, a+ 1 > a. Where can I look to start figuring out these questions for myself? Is it best to look at the source code? Maybe in the Ord collection?

For completeness, this is what I need to figure out,

namespace myNamespace
inductive  where
  | zero : 
  | succ :   
  deriving Repr

def add (m n : ) :  :=
  match n with
  | ℕ.zero => m
  | ℕ.succ l => ℕ.succ (add m l)

instance : Add  where
  add := add

open 

def lt (m n : )  : Prop :=   l : ,  (m + l = n   l  zero)
def le (n m : ) : Prop :=  l : , n + l = m

instance : LT  where
   lt := lt

instance : LE  where
  le := le

theorem add_succ {m n :  } : m + n.succ = (m + n).succ := rfl
theorem add_zero {m : } : m + zero = m := rfl

theorem lt_succ (n : ) : n < succ n := by sorry  --(I have a decent proof here that I want to reuse)

theorem succ_gt (n : ) : succ n > n := by
  suffices h₁ : n < succ n from sorry
    --how can I find out what to put here, I want something like ((a < b) implies (b > a) )
  exact lt_succ n



end myNamespace

I appreciate any ideas and direction.

Yakov Pechersky (Aug 08 2022 at 00:50):

theorem succ_gt (n : ℕ) : succ n > n := lt_succ n

Yakov Pechersky (Aug 08 2022 at 00:51):

theorem {X : Type _} [LT X] {a b : X} : a < b  b > a := iff.rfl

kvanvels (Aug 08 2022 at 01:00):

This is surprising to me. Is it correct to say that this means that lean switches greater-thans to less-thans automatically, and that there is no reason to even have my theorem and proof?

kvanvels (Aug 08 2022 at 01:01):

thanks for the response. I appreciate it.

Yakov Pechersky (Aug 08 2022 at 01:07):

afaiu, lean4 is able to interpret the gt-syntax as the lt, and vice versa. They (a < b, b > a) both stand for LT.lt a b.

kvanvels (Aug 08 2022 at 01:14):

Ok. That is nice. In C++ you have define all the different relations. This way seems to make more sense. Do you dig through the source code to learn something like that?

Arthur Paulino (Aug 08 2022 at 01:26):

I'm not on my PC, but what does #check 1 > 0 say?

Ugh, nvm, I guess it's going to say Prop

Kevin Buzzard (Aug 08 2022 at 13:22):

@kvanvels b > a is _definitionally equal_ to a < b, and tactics like refl and exact work up to definitional equality. It's the same reason as why m + zero = m is proved by rfl (but of course zero + m = m is not rfl; definitional equality is "not mathematical" in some sense.)


Last updated: Dec 20 2023 at 11:08 UTC