Submission Details

Back to Submissions List

Challenge: solveAdd

Submitted by: James Payor

Submitted at: 2024-11-26 04:09:38

Code:

import Init.Data.Int

def solveAdd (a b:Int): Int

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 

import Init.Data.Int

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

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

Status: Incorrect

Feedback:

Compilation error for /root/CodeProofTheArena/temp/tmp_mi8p12j/proof.lean:
/root/CodeProofTheArena/temp/tmp_mi8p12j/proof.lean:8:27: error: unexpected token 'def'; expected ':=', 'where' or '|'
/root/CodeProofTheArena/temp/tmp_mi8p12j/proof.lean:10:4: error: 'solveAdd' has already been declared
/root/CodeProofTheArena/temp/tmp_mi8p12j/proof.lean:14:58: error: unexpected token 'theorem'; expected ':=', 'where' or '|'
/root/CodeProofTheArena/temp/tmp_mi8p12j/proof.lean:18:2: error: tactic 'apply' failed, failed to unify
  ?a - ?b = ?a + -?b
with
  solveAdd a b = ?b
case h₁
a b : Int
⊢ solveAdd a b = ?b
/root/CodeProofTheArena/temp/tmp_mi8p12j/proof.lean:25:8: error: 'solveAdd_correct' has already been declared