Submission Details

Back to Submissions List

Challenge: solveAdd

Submitted by: James Payor

Submitted at: 2024-11-26 04:10:47

Code:

import Init.Data.Int

def solveAdd (a b:Int): Int

:= b - a

First Theorem Proof:

theorem solveAdd_correct (a b: Int): a + (solveAdd a b) =b 

:= by
  have p := ap_eq_add a (solveAdd_eq_neg_a_plus_b a b)
  have q := Int.add_neg_cancel_left a b
  exact Eq.trans p q

theorem solveAdd_eq_neg_a_plus_b (a b: Int): solveAdd a b = -a + b := by
  apply Eq.trans
  apply Int.sub_eq_add_neg
  apply Int.add_comm

theorem ap_eq_add (a: Int) {b c: Int} (p: b = c): a + b = a + c := by
  rewrite [<- p]
  rfl

Status: Incorrect

Feedback:

Compilation error for /root/CodeProofTheArena/temp/tmp2awkeymy/proof.lean:
/root/CodeProofTheArena/temp/tmp2awkeymy/proof.lean:12:12: error: unknown identifier 'ap_eq_add'
/root/CodeProofTheArena/temp/tmp2awkeymy/proof.lean:11:3: error: unsolved goals
a b : Int
⊢ a + solveAdd a b = b