Submission Details

Back to Submissions List

Challenge: minFac

Submitted by: Quang Dao

Submitted at: 2024-11-19 23:16:39

Code:

def minFac(a:Nat) (h: a>1): Nat 

  Nat.find (p := fun x => x > 1 ∧ x ∣ a) ⟨a, And.intro h (Nat.dvd_refl a)⟩

First Theorem Proof:

theorem minFac_isfac(a:Nat)(h: a>1): ( (minFac a h) ∣a) ∧(minFac a h>1)

by
  simp [minFac]
  constructor
  · have := Nat.find_spec (p := fun x => x > 1 ∧ x ∣ a) ⟨a, And.intro h (Nat.dvd_refl a)⟩
    exact this.2
  · intro m hm hm'
    contrapose! hm'
    exact hm

Status: Incorrect

Feedback:

/tmp/tmp3qxk0_ex/code.lean:7:0: error: unexpected end of input; expected ':=', 'where' or '|'
/tmp/tmp3qxk0_ex/code.lean:5:11: error: invalid argument name 'p' for function 'Nat'

Second Theorem Proof:

theorem minFac_ismin(a:Nat)(h:a>1): Not (∃ y>1,( y ∣ a) ∧y<minFac a h)

by
  simp [minFac]
  intro x hGt hDiv
  have := Nat.find_min' (p := fun x => x > 1 ∧ x ∣ a) ⟨a, And.intro h (Nat.dvd_refl a)⟩ (And.intro hGt hDiv)
  refine ⟨minFac a h, ?_⟩
  constructor
  · simp [this, minFac]
  · exact And.comm.mp (minFac_is_fac a h)

Status: Incorrect

Feedback:

/tmp/tmp3qxk0_ex/proof2.lean:5:74: error: unexpected token 'theorem'; expected ':=', 'where' or '|'
/tmp/tmp3qxk0_ex/proof2.lean:5:11: error: invalid argument name 'p' for function 'Nat'
/tmp/tmp3qxk0_ex/proof2.lean:9:58: error: expected token