File size: 1,455 Bytes
0110dee | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 | -- Lean 4 Formal Certificate for candidate_2
-- Generated by Relational Lisp Synthesis Engine
-- Date: 2026-07-31T16:43:01.862Z
-- AST Hash: a4b7e616bf28ed0f1317285c4103978086f7725cdc13f2924f785b10dd0c9f46
theorem append_correct : ∀ (x y z : List ℕ),
append x y z ↔ z = x ++ y := by
intro x y z
constructor
· intro h
induction h with
| nil => rfl
| cons h ih =>
simp [List.cons_append]
exact ih
· intro h
rw [h]
induction x with
| nil => constructor
| cons h t ih =>
constructor
· simp [List.cons_append]
exact ih
-- Synthesis Trace
-- Candidate: candidate_2
-- Z3 Result: SAT
-- Validation: VALID
-- Z3 Model (if SAT)
-- Model: Z = [1,2,3]
-- Generated AST
-- {
-- "type": "if",
-- "test": [
-- "null",
-- "_x"
-- ],
-- "then": [
-- "eq",
-- "_y",
-- "_z"
-- ],
-- "else": [
-- "and",
-- [
-- "cons",
-- [
-- "car",
-- "_x"
-- ],
-- [
-- "cdr",
-- "_x"
-- ],
-- [
-- "car",
-- "_z"
-- ],
-- [
-- "cdr",
-- "_z"
-- ]
-- ],
-- [
-- "append",
-- [
-- "cdr",
-- "_x"
-- ],
-- "_y",
-- [
-- "cdr",
-- "_z"
-- ]
-- ]
-- ]
-- }
-- Verified signature below
|