who can help me formalize this solution

Stream: new members

[klh]

import mathlib

open Nat

/-Let x,y and a0,a1,a2,⋯be integers satisfying a n+2=xa n+1 + ya n + 1for all integers n≥0 . Let p be any prime number. Show that

gcd(a p,a p+1) is either equal to 1 or greater than p-/

variable(x y :ℕ+ ){n:ℕ+}

def a  : ℕ → ℕ

| 0 => 0

| 1 => 0

| n+2 => x * a (n + 1) + y * a n + 1

def a_n:=a n

def a_n₁:=a (n+1)



theorem  theory_1  (p q : ℕ+)(hp:Nat.Prime p) (hq : Nat.Prime q) (hy: q∣y) :Nat.Coprime q (Nat.gcd a_p a_p₁) := by

         sorry

theorem  theory_2(p q : ℕ) (hp : Nat.Prime p) (hq : Nat.Prime q) (hy: Nat.Coprime q y)(ha:q∣a_p∧ q∣a_p₁):q>√p:= by

          sorry

6c11c7cbe5f82f89ca2e0ea16ec7e33.jpg
here is my solution.

[Shreyas Srinivas]

Please first show us your proof attempts

[Shreyas Srinivas]

Where are you getting stuck?

[Derek Rhodes]

(for the sake of convenience, here is the solution, rotated :upside_down: right side up )

image.png

[Shreyas Srinivas]

No I mean the lean attempt

[Ruben Van de Velde]

(That wasn't the OP)

[Notification Bot]

This topic was moved here from #lean4 > who can help me formalize this solution by Kyle Miller.

[klh]

import Mathlib

open Nat

/-Let x,y and a0,a1,a2,⋯be integers satisfying a n+2=xa n+1 + ya n + 1for all integers n≥0 . Let p be any prime number. Show that

gcd(a p,a p+1) is either equal to 1 or greater than sqrt p-/

variable(x y :ℕ+ ){n:ℕ+}

def a  : ℕ → ℕ

| 0 => 0

| 1 => 0

| n+2 => x * a (n + 1) + y * a n + 1

def a_n:=a n

def a_n₁:=a (n+1)


theorem  theory_1  (p q : ℕ+)(hp:Nat.Prime p) (hq : Nat.Prime q) (hy: q∣y) :Nat.Coprime q (Nat.gcd a_p a_p₁) := by

    have h₀:¬ q ∣ Nat.gcd a_p a_p₁ :=by

     intro h₀

     have  h₁:a_p₁ - x*a_p - y*a (p-1)=1:= by norm_num

     have  h₂: q∣a_p ∧ q∣ a_p₁:=by

     apply dvd_trans h₀

     apply  gcd_dvd a_p a_p₁

     have  h3: q∣ a_p₁ - x*a_p - y*a (p-1):=by

     apply  mul_dvd_mul

     apply  dvd_sub

     have  h₄: q∣ 1 := by

     rw[h₁]

     /-then we get a contradiction,so prvoed h₀-/

    apply  Nat.coprime_of_not_dvd h₀

This is my lean attmpt with too many mistakes.Could you help me solve them?

[Ruben Van de Velde]

First issue: import mathlib should be import Mathlib. If it works with a lower case m, that's purely an accident

[klh]

Ruben Van de Velde 发言道：

First issue: import mathlib should be import Mathlib. If it works with a lower case m, that's purely an accident

Thank you

[Derek Rhodes]

Hi, I had to move things around in order for this to check. Watch out in the definition of the sequence a when matching with a pattern like (m + 2), that the pattern variable m is not the same name as the match variable in match m with, (please notice I used p + 2). Also, I had to append .val to some of the variables because ℕ+ are mixed with ℕ, and the auto coercion mechanism was not able to see through differences. In any event, there are fewer red squiggles now :)

import Mathlib

set_option autoImplicit false
open Nat

/-
Let x,y and a0,a1,a2,⋯be integers satisfying a n+2=xa n+1 + ya n + 1for all
integers n≥0 . Let p be any prime number. Show that:

gcd(a p,a p+1) is either equal to 1 or greater than sqrt p
-/

variable (n : ℕ+)

def a (x y : ℕ+) (m: ℕ) : ℕ :=
  match m with
  | 0 => 0
  | 1 => 0
  | p + 2 => x * a x y (p + 1) + y * a x y p + 1

def a_n := a n
def a_n₁ := a (n + 1)

theorem theory_1 (x y p q : ℕ+) (a_p a_p₁ : ℕ) (hp: Nat.Prime p) (hq : Nat.Prime q)
  (hy : q ∣ y) : Nat.Coprime q (Nat.gcd a_p a_p₁) := by
  --

  have h₀ : ¬ q.val ∣ (Nat.gcd a_p a_p₁) := by
    intro h₀
    sorry

  have h₁ : a_p₁ - (x * a_p) - y * (a x y (p - 1)) = 1 := by
    norm_num
    sorry

  have h₂ : (q.val ∣ a_p) ∧ (q.val ∣ a_p₁) := by
    -- apply dvd_trans h₀
    -- apply gcd_dvd a_p a_p₁
    sorry

  have h₃ : q.val ∣ a_p₁ - x * a_p - y.val * (a x y (p - 1)) := by
    -- apply mul_dvd_mul
    -- apply dvd_sub
    sorry

  have h₄: q ∣ 1 := by
    sorry

  rw [h₁] --

  /- then we get a contradiction, so prvoed h₀ -/

  apply Nat.coprime_of_not_dvd h₀

[klh]

Derek Rhodes 发言道：

Hi, I had to move things around in order for this to check. Watch out in the definition of the sequence a when matching with a pattern like (m + 2), that the pattern variable m is not the same name as the match variable in match m with, (please notice I used p + 2). Also, I had to append .val to some of the variables because ℕ+ are mixed with ℕ, and the auto coercion mechanism was not able to see through differences. In any event, there are fewer red squiggles now :)

import Mathlib

set_option autoImplicit false
open Nat

/-
Let x,y and a0,a1,a2,⋯be integers satisfying a n+2=xa n+1 + ya n + 1for all
integers n≥0 . Let p be any prime number. Show that:

gcd(a p,a p+1) is either equal to 1 or greater than sqrt p
-/

variable (n : ℕ+)

def a (x y : ℕ+) (m: ℕ) : ℕ :=
  match m with
  | 0 => 0
  | 1 => 0
  | p + 2 => x * a x y (p + 1) + y * a x y p + 1

def a_n := a n
def a_n₁ := a (n + 1)

theorem theory_1 (x y p q : ℕ+) (a_p a_p₁ : ℕ) (hp: Nat.Prime p) (hq : Nat.Prime q)
  (hy : q ∣ y) : Nat.Coprime q (Nat.gcd a_p a_p₁) := by
  --

  have h₀ : ¬ q.val ∣ (Nat.gcd a_p a_p₁) := by
    intro h₀
    sorry

  have h₁ : a_p₁ - (x * a_p) - y * (a x y (p - 1)) = 1 := by
    norm_num
    sorry

  have h₂ : (q.val ∣ a_p) ∧ (q.val ∣ a_p₁) := by
    -- apply dvd_trans h₀
    -- apply gcd_dvd a_p a_p₁
    sorry

  have h₃ : q.val ∣ a_p₁ - x * a_p - y.val * (a x y (p - 1)) := by
    -- apply mul_dvd_mul
    -- apply dvd_sub
    sorry

  have h₄: q ∣ 1 := by
    sorry

  rw [h₁] --

  /- then we get a contradiction, so prvoed h₀ -/

  apply Nat.coprime_of_not_dvd h₀

I want to use h1,h2,h3,h4 to prove h0,and use h0 to prove my theorem.But h1,h2,h3,h4 can only be right with the condition of h0,I don not konw how to do.You put all h in the same status.In any event, there are fewer red squiggles now.Thank you for helping me solve the type ℕ and ℕ+and some other mistakes

[Derek Rhodes]

I want to use h1,h2,h3,h4 to prove h0 ... You put all h in the same status.

Oh! I see, I wasn't sure about that because there are some odd tab characters that my computer does recognize.

[klh]

Derek Rhodes 发言道：

I want to use h1,h2,h3,h4 to prove h0 ... You put all h in the same status.

Oh! I see, I wasn't sure about that because there are some odd tab characters that my computer does recognize.

import Mathlib

set_option autoImplicit false
open Nat

/-
Let x,y and a0,a1,a2,⋯be integers satisfying a n+2=xa n+1 + ya n + 1for all
integers n≥0 . Let p be any prime number. Show that:

gcd(a p,a p+1) is either equal to 1 or greater than sqrt p
-/

variable (n : ℕ+)

def a (x y : ℕ+) (m: ℕ) : ℕ :=
  match m with
  | 0 => 0
  | 1 => 0
  | p + 2 => x * a x y (p + 1) + y * a x y p + 1


theorem theory_1 (x y p q : ℕ+)  (hp: Nat.Prime p) (hq : Nat.Prime q)
  (hy : q ∣ y) : Nat.Coprime q (Nat.gcd (a x y p) (a x y (p+1))) := by
 have h₀ : ¬ q.val ∣ (Nat.gcd (a x y p) (a x y (p+1))) := by
    intro h₀

    have h₁ : (a x y (p+1)) - (x * a x y p) - y * (a x y (p - 1)) = 1 := by
    --norm_num
    sorry
    have h₂ : q.val ∣ a x y p ∧ (q.val ∣ a x y (p+1)) := by
    -- apply dvd_trans h₀
    -- apply gcd_dvd (a x y p) (a x y (p+1))
    sorry

    have h₃ : q.val ∣(a x y (p+1) - x.val * a x y p - y.val * (a x y (p - 1))) := by
    -- apply mul_dvd_mul
    -- apply dvd_sub
    sorry
    have h₄: q ∣ 1 := by
       rw [h₁] --

  /- then we get a contradiction, so prvoed h₀ -/

 apply Nat.coprime_of_not_dvd h₀

I modificant my lean code, the above is my attmpt.But it seems that 'have' statements cannot be nested.So I want to konw how to solve this.

[Johan Commelin]

Why do you think have cannot be nested? It should work

[klh]

Johan Commelin 发言道：

Why do you think have cannot be nested? It should work

Oh,move'sorry'one space then it can work,thank you.But I still have problem in proving these h,I will try my best :face_with_spiral_eyes: