Submission Details

Back to Submissions List

Challenge: modInv

Submitted by: GasStationManager

Submitted at: 2024-11-24 22:29:54

Code:

import Mathlib.Data.Prime.Defs

def modInv(a: Nat) (p:Nat)(hp:p.Prime): Option Nat

:=sorry

import Mathlib.Data.Prime.Defs 

First Theorem Proof:

theorem modInv_correct(a:Nat) (p:Nat)(hp:p.Prime):
  (∃ x:Nat, (a*x)%p=1)->(a*(modInv a p hp).get!)%p=1

:=sorry

Status: Incorrect

Feedback:

Compilation error for /root/CodeProofTheArena/temp/tmputc1f8y5/target.lean:
/root/CodeProofTheArena/temp/tmputc1f8y5/target.lean:2:30: error: invalid field 'Prime', the environment does not contain 'Nat.Prime'
  p
has type
  Nat
/root/CodeProofTheArena/temp/tmputc1f8y5/target.lean:6:41: error: invalid field 'Prime', the environment does not contain 'Nat.Prime'
  p
has type
  Nat

Second Theorem Proof:

theorem modInv_none(a:Nat) (p:Nat)(hp:p.Prime): (Not (∃ x, (a*x)%p=1))-> modInv a p hp=none

:=sorry

Status: Incorrect

Feedback:

Compilation error for /root/CodeProofTheArena/temp/tmputc1f8y5/target2.lean:
/root/CodeProofTheArena/temp/tmputc1f8y5/target2.lean:2:30: error: invalid field 'Prime', the environment does not contain 'Nat.Prime'
  p
has type
  Nat
/root/CodeProofTheArena/temp/tmputc1f8y5/target2.lean:5:38: error: invalid field 'Prime', the environment does not contain 'Nat.Prime'
  p
has type
  Nat