Beginner question

Stream: new members

[Guilherme Espada]

The following code:

inductive term
|t_true : term
|t_false : term
|t_zero : term


def size : term -> ℕ
| t_true := 1
| t_false := 1
| t_zero := 1

does not work. What am I missing?

[Kevin Buzzard]

I'm missing the error message

[Kevin Buzzard]

And you're probably missing open term

[Guilherme Espada]

This fixes it!
(the error message is invalid application, function expected)
Another question, when I list only a single option on the size function, it doesn't error. Why?

def size : term -> ℕ
| t_true := 1

[Reid Barton]

Same reason that

def size : term -> ℕ
| anything := 1

doesn't error

[Guilherme Espada]

Thanks!

[Omar Shehab]

 let M := factorial N + 1;
  let p := minFac M;
  have pp : Prime p | {
    refine minFac_prime _:
    have : factorial N > 0,
    from factorial_pos N;
    linarith,
  },

I have an error in this part can anybody help with that

[Yaël Dillies]

You can add #backticks to make your message readable

[Arthur Paulino]

Note: #backticks is a clickable like that will tell you what people mean by "backticks"

[Alex J. Best]

It looks like you are trying to use lean 3 syntax (which is the old deprecated version). Are you trying to use lean 3 or lean 4 (recommended)

[Alex J. Best]

If you are trying to use lean 4 you should try to follow some materials from https://leanprover-community.github.io/learn.html

[Riccardo Brasca]

I think one error is that docs#Nat.minFac_prime proves that Nat.Prime p, while you said you wanted to prove Prime p

[Omar Shehab]

import Mathlib.Data.Nat.Prime
import Mathlib.Tactic

theorem infinitude_of_primes (N : ℕ) : ∃ p, p ≥ N ∧ Nat.Prime p :=
let M := Nat.factorial N + 1;
let p := Nat.minFac M;
have h0 : 0 < N := Nat.zero_lt_succ _;
have h1 : M ≠ 1 := Nat.ne_of_gt (Nat.succ_lt_succ (Nat.factorial_pos N));
have primeP : Nat.Prime p := Nat.minFac_prime h1;
have h2 : p ∣ M := Nat.minFac_dvd M;
have h3 : N < p :=
  Nat.lt_of_not_ge (λ hge,
    have h4 : p ∣ Nat.factorial N := primeP.dvd_factorial (Nat.le_of_succ_le hge);
    have h5 : p ∣ 1 := Nat.dvd_sub' h2 h4;
    Nat.prime.not_dvd_one primeP h5);
⟨p, Nat.le_of_lt h3, primeP⟩

I have edited the code so that it follows the lean4 syntax but I still get an error

[Riccardo Brasca]

The first error I see is the fact that you write a function using λ x, x + 3: this is Lean3 style, in Lean 4 we write

fun x ↦ x + 3

[Riccardo Brasca]

Also, we don't use ; to finish a line

[Riccardo Brasca]

Is there a reason why you are not in tactic mode?