Hugging Face's logo

Spaces:
ProCreations
/
repro-formal-problem-solving-framework-benchmark
Running

App Files Community
repro-formal-problem-solving-framework-benchmark
File size: 3,864 Bytes
6c3fe2a
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
import Lean
import Mathlib

open Lean Elab Command Term Meta Tactic

set_option autoImplicit false
set_option relaxedAutoImplicit false

structure ProblemSol {Ξ± : Type} (P : Ξ± β†’ Prop) where
  Answer : Ξ±
  Proof : P Answer

def ProblemTarget (p : Prop) : Prop := p

def getRawBody (e : Expr) (i : Nat := 2) : MetaM Expr := do
  lambdaTelescope e fun args body => do
    let body ← whnf body
    if body.isAppOf ``ProblemSol.mk then
      let val := body.getAppArgs[i]!
      mkLambdaFVars args val
    else
      throwError "Extraction failed: Body is not a ProblemSol constructor. Body: {body}"

elab "extract_ans_type " id:ident : term => do
  let name ← resolveGlobalConstNoOverload id
  let info ← getConstInfoDefn name
  getRawBody info.value 0

elab "extract_predicate " id:ident : term => do
  let name ← resolveGlobalConstNoOverload id
  let info ← getConstInfoDefn name
  getRawBody info.value 1

elab "extract_answer " id:ident : term => do
  let name ← resolveGlobalConstNoOverload id
  let info ← getConstInfoDefn name
  getRawBody info.value 2

elab "extract_proof " id:ident : term => do
  let name ← resolveGlobalConstNoOverload id
  let info ← getConstInfoDefn name
  getRawBody info.value 3


namespace FPS
scoped syntax (name := problemSyntax)
  "problem" ident bracketedBinder* "find" "(" ident ":" term ")"
  "s.t." bracketedBinder* ":" term ":=" term : command

scoped macro_rules
| `(problem $name:ident $vars* find ($ansId:ident : $ansType:term) s.t. $hyps* : $concl:term := $body:term) => do
  let proofSpec ← `(fun $ansId:ident : $ansType => βˆ€ $hyps*, ProblemTarget $concl)
  `(@[reducible] noncomputable def $name $vars* : ProblemSol $proofSpec := $body)

scoped syntax (name := solveSyntax) "solve" (ppSpace tacticSeq)? : term

@[term_elab solveSyntax]
def elabSolve : TermElab := fun stx expectedType? => do
  let some expectedType := expectedType?
    | throwError "`solve` must be used in a position of known type"

  let mvar ← mkFreshExprMVar expectedType
  let mvarId := mvar.mvarId!
  let setupTx ← `(tactic|
    apply ProblemSol.mk;
    intros;
    unfold ProblemTarget
  )

  let _ ← Lean.Elab.Tactic.run mvarId do
    withOptions (fun o => o.setBool `tactic.hygienic false) do
      evalTactic setupTx
    withTacticInfoContext stx[0] (pure ())
    if let some seq := stx[1].getOptional? then
      evalTactic seq

  return mvar

end FPS


namespace DFPS

scoped syntax (name := problemSyntax)
  "problem" ident bracketedBinder* "find_all" "(" ident ":" term ")"
  "iff" bracketedBinder* ":" term ":=" term : command

scoped macro_rules
| `(problem $name:ident $vars* find_all ($ansId:ident : $ansType:term) iff $hyps* : $concl:term := $body:term) => do
  let proofSpec ← `(fun answer_predicate :  Prop => βˆ€ $hyps*, (ProblemTarget $concl) ↔ (answer_predicate))
  `(@[reducible] noncomputable def $name $vars* ($ansId : $ansType) : ProblemSol $proofSpec := $body)

scoped syntax (name := solveSyntax) "solve" (ppSpace tacticSeq)? : term
@[term_elab solveSyntax]
def elabSolve : TermElab := fun stx expectedType? => do
  let some expectedType := expectedType?
    | throwError "`solve` must be used in a position of known type"

  let hAnswerName := mkIdent `_h_answer
  let hConclusionName := mkIdent `_h_conclusion
  let mvar ← mkFreshExprMVar expectedType
  let mvarId := mvar.mvarId!

  let setupTx ← `(tactic|
    apply ProblemSol.mk;
    intros;
    unfold ProblemTarget;
    refine @Iff.intro ?_ _ ?Forward ?Backward;
    rotate_left;
    intros $hAnswerName;
    rotate_right;
    intros $hConclusionName;
  )

  let _ ← Lean.Elab.Tactic.run mvarId do
    withOptions (fun o => o.setBool `tactic.hygienic false) do
      evalTactic setupTx
    withTacticInfoContext stx[0] (pure ())
    if let some seq := stx[1].getOptional? then
      evalTactic seq

  return mvar

end DFPS