the next generation of the in-browser educational proof assistant
Proofs?
+360
-79
+24
-5
index.html
+24
-5
index.html
···
263
263
</head>
264
264
<body>
265
265
<hol-comp id="test.html/baz" deps="test.html/myconfig">
266
-
x.y.
267
-
[z. (P z) (R [] z) |- (Q z)] [x. (P x)]
268
-
(And x y \3) [ Foo ]
269
-
---- name
270
-
Baz
266
+
x.y.
267
+
(/\ x y)
268
+
---- AE1
269
+
x
270
+
271
+
x.y.
272
+
(/\ x y)
273
+
---- AE2
274
+
y
275
+
276
+
x.y.
277
+
x y
278
+
---- AI
279
+
(/\ x y)
271
280
</hol-comp>
272
281
<hol-config id="test.html/myconfig">Gentzen</hol-config>
282
+
<hol-proof id="test.html/prooftest" deps="test.html/baz">
283
+
x.y. ayx |- have x
284
+
|- by (AE2 x y) {
285
+
|- by (ayx) {} }
286
+
asm |- by (AI x y) {
287
+
|- by (asm) {}
288
+
|- by (AE1 x y) {
289
+
|- by (ayx) {} }
290
+
}
291
+
</hol-proof>
273
292
<script type="module" src="./src/testcomponent.tsx"></script>
274
293
</body>
275
294
</html>
+279
-69
src/ProofEngine.res
+279
-69
src/ProofEngine.res
···
1
1
2
2
open Signatures
3
3
4
-
module Make = (Term : TERM, Judgment : JUDGMENT with module Term := Term) => {
4
+
module Context = (Term : TERM, Judgment : JUDGMENT with module Term := Term) => {
5
5
module Rule = Rule.Make(Term,Judgment)
6
-
module Step = {
7
-
type t<'a> = {
8
-
fixes: array<Term.meta>,
9
-
facts: Dict.t<Rule.t>,
10
-
proof: 'a
6
+
type rec t = {
7
+
fixes: array<Term.meta>,
8
+
facts: Dict.t<Rule.t>,
9
+
}
10
+
}
11
+
12
+
module type PROOF_METHOD = {
13
+
module Term : TERM
14
+
module Judgment : JUDGMENT with module Term := Term
15
+
module Rule : module type of Rule.Make(Term,Judgment)
16
+
module Context : module type of Context(Term,Judgment)
17
+
type t<'a>
18
+
let keywords : array<string>
19
+
let check : (t<'a>, Context.t, Judgment.t,
20
+
('a, Rule.t) => 'b) => result<t<'b>,string>
21
+
let uncheck : (t<'a>, 'a => 'b) => t<'b>
22
+
let parse : (string, ~keyword: string, ~scope: array<Term.meta>,~gen: Term.gen,
23
+
~subparser: (string, ~scope: array<Term.meta>, ~gen: Term.gen)
24
+
=> result<('a,string),string> )
25
+
=> result<(t<'a>,string),string>
26
+
}
27
+
28
+
29
+
module Derivation = (
30
+
Term : TERM, Judgment : JUDGMENT with module Term := Term
31
+
) => {
32
+
module Rule = Rule.Make(Term,Judgment)
33
+
module Context = Context(Term,Judgment)
34
+
type t<'a> = {
35
+
ruleName: string,
36
+
instantiation: array<Term.t>,
37
+
subgoals: array<'a>
38
+
}
39
+
let uncheck = (it : t<'a>, f) => {
40
+
{ ruleName: it.ruleName,
41
+
instantiation: it.instantiation,
42
+
subgoals: it.subgoals->Array.map(f)
11
43
}
12
-
let bind : (t<'a>, 'a => t<'b>) => t<'b> = (s, f) => {
13
-
let t = f(s.proof);
14
-
{
15
-
fixes: t.fixes->Array.concat(s.fixes),
16
-
facts: Dict.copy(s.facts)->Dict.assign(t.facts),
17
-
proof: t.proof
44
+
}
45
+
exception InternalParseError(string)
46
+
let keywords = ["by"]
47
+
let parse = (input, ~keyword as _, ~scope, ~gen, ~subparser) => {
48
+
let cur = ref(String.trim(input))
49
+
if (cur.contents->String.get(0) == Some("(")) {
50
+
switch Rule.parseRuleName(cur.contents->String.sliceToEnd(~start=1)) {
51
+
| Ok((ruleName,rest)) => {
52
+
cur := rest
53
+
let instantiation = [];
54
+
let it = ref(Error(""))
55
+
while {it := Term.parse(cur.contents,~scope,~gen);
56
+
it.contents->Result.isOk} {
57
+
let (val, rest) = it.contents->Result.getExn
58
+
Array.push(instantiation, val)
59
+
cur := String.trim(rest)
60
+
}
61
+
if (cur.contents->String.get(0) == Some(")")) {
62
+
cur := String.trim(cur.contents->String.sliceToEnd(~start=1))
63
+
let subgoals = []
64
+
if (cur.contents->String.get(0) == Some("{")) {
65
+
cur := String.trim(cur.contents->String.sliceToEnd(~start=1))
66
+
try {
67
+
while (cur.contents->String.get(0) != Some("}")) {
68
+
switch subparser(cur.contents,~scope,~gen) {
69
+
| Ok((sg, rest)) => {
70
+
Array.push(subgoals,sg)
71
+
cur := String.trim(rest)
72
+
}
73
+
| Error(e) => raise(InternalParseError(e))
74
+
}
75
+
}
76
+
if (cur.contents->String.get(0) == Some("}")) {
77
+
cur := String.trim(cur.contents->String.sliceToEnd(~start=1))
78
+
Ok(({ruleName,instantiation,subgoals},cur.contents))
79
+
} else {
80
+
Error("} or subgoal proof expected")
81
+
}
82
+
} catch {
83
+
| InternalParseError(e) => Error(e)
84
+
}
85
+
} else {
86
+
Error("{ expected")
87
+
}
88
+
} else {
89
+
Error(") or term expected")
90
+
}
91
+
}
92
+
| Error(e) => Error(e)
18
93
}
94
+
} else {
95
+
Error("Expected (")
19
96
}
20
97
}
21
-
module Goal = {
22
-
type t = {
23
-
fix: array<Term.meta>,
24
-
assume: array<Rule.t>,
25
-
assumeNames: array<string>,
26
-
show: Judgment.t
27
-
}
28
-
let toRule : t => Rule.t = (goal : t) => {
29
-
vars: goal.fix,
30
-
premises: goal.assume,
31
-
conclusion: goal.show
98
+
let check = (it: t<'a>, ctx : Context.t, j: Judgment.t, f : ('a, Rule.t) => 'b) => {
99
+
switch ctx.facts->Dict.get(it.ruleName) {
100
+
| None =>
101
+
Error("Cannot find rule '"->String.concat(it.ruleName)->String.concat("'") )
102
+
| Some(rule) if Array.length(rule.vars) == Array.length(it.instantiation) => {
103
+
let {premises,conclusion} = Rule.instantiate(rule,it.instantiation)
104
+
if Judgment.equivalent(conclusion,j) {
105
+
if Array.length(it.subgoals) == Array.length(premises) {
106
+
Ok({
107
+
ruleName: it.ruleName,
108
+
instantiation: it.instantiation,
109
+
subgoals: Belt.Array.zipBy(it.subgoals,premises,f)
110
+
})
111
+
} else {
112
+
Error("Incorrect number of subgoals")
113
+
}
114
+
} else {
115
+
Error("Conclusion of rule doesn't match goal")
116
+
}
117
+
}
118
+
| _ => Error("Incorrect number of binders")
32
119
}
33
120
}
34
-
module type PROOFT = {
35
-
type t<'a>
36
-
let subproofs : (Goal.t,t<'a>, 'a=>Goal.t) => Dict.t<Step.t<'a>>
121
+
}
122
+
module Lemma = (
123
+
Term : TERM, Judgment : JUDGMENT with module Term := Term
124
+
) => {
125
+
module Rule = Rule.Make(Term,Judgment)
126
+
module Context = Context(Term,Judgment)
127
+
type t<'a> = {
128
+
rule: Rule.t,
129
+
proof: 'a,
130
+
show: 'a
37
131
}
38
-
module Either = (A : PROOFT, B : PROOFT) => {
39
-
type t<'a> = L(A.t<'a>) | R(B.t<'a>)
40
-
let subproofs = (goal:Goal.t,it : t<'a>, f : 'a => Goal.t) => switch it {
41
-
| L(x) => A.subproofs(goal,x,f)
42
-
| R(x) => B.subproofs(goal,x,f)
132
+
let uncheck = (it: t<'a>, f) => {
133
+
{ rule: it.rule,
134
+
proof: f(it.proof),
135
+
show: f(it.show)
43
136
}
44
137
}
45
-
46
-
module Deduction : PROOFT = {
47
-
type t<'a> = {
48
-
from: array<'a>,
49
-
ruleName: string,
50
-
instantiation: array<Term.t>
138
+
let keywords = ["have"]
139
+
let parse = (input, ~keyword as _, ~scope, ~gen, ~subparser) => {
140
+
//todo add toplevel
141
+
switch Rule.parseInner(input, ~scope, ~gen) {
142
+
| Ok((rule,rest)) => {
143
+
switch (subparser(rest,~scope,~gen)) {
144
+
| Ok((proof,rest')) =>
145
+
switch String.trim(rest')->subparser(~scope,~gen) {
146
+
| Ok((show,rest'')) => Ok({rule,proof,show}, rest'')
147
+
| Error(e) => Error(e)
148
+
}
149
+
| Error(e) => Error(e)
150
+
}
151
+
}
152
+
| Error(e) => Error(e)
51
153
}
52
-
let subproofs = (goal : Goal.t,it : t<'a>, _ : 'a => Goal.t) => {
53
-
let toStep : 'a => Step.t<'a> = (a) => {
54
-
fixes: goal.fix,
55
-
facts: Belt.Array.zip(goal.assumeNames,goal.assume)->Dict.fromArray,
56
-
proof: a
57
-
};
58
-
Belt.Array.range(0,Array.length(it.from))
59
-
->Array.map(x =>Belt.Int.toString(x))
60
-
->Belt.Array.zip(it.from->Array.map(toStep))
61
-
->Dict.fromArray
154
+
}
155
+
let check = (it: t<'a>, ctx : Context.t, j: Judgment.t, f : ('a, Rule.t) => 'b) => {
156
+
let first = f(it.proof,it.rule)
157
+
let second = f(it.show,{vars:[],premises:[it.rule],conclusion:j})
158
+
Ok({rule:it.rule, proof:first, show:second})
159
+
}
160
+
}
161
+
module Combine = (
162
+
Term : TERM, Judgment : JUDGMENT with module Term := Term,
163
+
Method1 : PROOF_METHOD with module Term := Term and module Judgment := Judgment,
164
+
Method2 : PROOF_METHOD with module Term := Term and module Judgment := Judgment
165
+
) => {
166
+
module Rule = Rule.Make(Term,Judgment)
167
+
module Context = Context(Term,Judgment)
168
+
type t<'a> = First(Method1.t<'a>) | Second(Method2.t<'a>)
169
+
let uncheck = (it, f) => switch it {
170
+
| First(m) => First(Method1.uncheck(m,f))
171
+
| Second(m) => Second(Method2.uncheck(m,f))
172
+
}
173
+
let keywords = Array.concat(Method1.keywords,Method2.keywords)
174
+
175
+
let check = (it,ctx, j, f) => switch it {
176
+
| First(m) => m->Method1.check(ctx,j,f)->Result.map(x => First(x))
177
+
| Second(m) => m->Method2.check(ctx,j,f)->Result.map(x => Second(x))
178
+
}
179
+
let parse = (input, ~keyword, ~scope, ~gen, ~subparser) => {
180
+
if Method1.keywords->Array.indexOf(keyword) > -1 {
181
+
Method1.parse(input,~keyword,~scope,~gen,~subparser)->Result.map(((x,r)) => (First(x),r))
182
+
} else {
183
+
Method2.parse(input,~keyword,~scope,~gen,~subparser)->Result.map(((x,r)) => (Second(x),r))
62
184
}
63
185
}
64
-
module Lemma : PROOFT = {
65
-
type t<'a> = {
66
-
name: string,
67
-
have: 'a,
68
-
show: 'a
186
+
}
187
+
module Proof = (
188
+
Term : TERM, Judgment : JUDGMENT with module Term := Term,
189
+
Method : PROOF_METHOD with module Term := Term and module Judgment := Judgment
190
+
) => {
191
+
module Rule = Rule.Make(Term,Judgment)
192
+
module Context = Context(Term,Judgment)
193
+
type rec t = {
194
+
fixes: array<Term.meta>,
195
+
assumptions: array<string>,
196
+
method: option<Method.t<t>>
197
+
}
198
+
type rec checked
199
+
= Checked({
200
+
fixes: array<Term.meta>,
201
+
assumptions: array<string>,
202
+
method: option<Method.t<checked>>,
203
+
rule: Rule.t
204
+
})
205
+
| ProofError({ raw: t, rule: Rule.t, msg: string})
206
+
let parseKeyword = (input) => {
207
+
Method.keywords
208
+
->Array.concat(["?"])
209
+
->Array.find(kw => String.trim(input)->String.startsWith(kw))
210
+
}
211
+
let rec parse = (input, ~scope,~gen) => {
212
+
let it = ref(Error(""))
213
+
let cur = ref(String.trim(input))
214
+
let fixes = []
215
+
while {it := Term.parseMeta(cur.contents); it.contents->Result.isOk} {
216
+
let (n,r) = Result.getExn(it.contents)
217
+
cur := String.trim(r)
218
+
fixes->Array.unshift(n)
69
219
}
70
-
let subproofs = (goal: Goal.t,it : t<'a>, f : 'a => Goal.t) => {
71
-
let haveGoal : Step.t<'a> = {
72
-
fixes: goal.fix,
73
-
facts: Belt.Array.zip(goal.assumeNames,goal.assume)->Dict.fromArray,
74
-
proof: it.have
75
-
};
76
-
let showGoal : Step.t<'a> = {
77
-
fixes: goal.fix,
78
-
facts: Belt.Array.zip(goal.assumeNames,goal.assume)
79
-
->Array.concat([(it.name,f(it.have)->Goal.toRule)])
80
-
->Dict.fromArray,
81
-
proof: it.show
82
-
};
83
-
Dict.fromArray([(it.name,haveGoal), ("@show",showGoal)])
220
+
let it = ref(Error(""))
221
+
let assumptions = []
222
+
while {it := Rule.parseRuleName(cur.contents); it.contents->Result.isOk} {
223
+
let (a,r) = Result.getExn(it.contents)
224
+
cur := String.trim(r)
225
+
assumptions->Array.push(a)
226
+
}
227
+
if cur.contents->String.slice(~start=0,~end=2) != "|-" {
228
+
Console.log((fixes,assumptions))
229
+
Error("expected turnstile or rule name"->String.concat(cur.contents))
230
+
} else {
231
+
cur := cur.contents->String.trim->String.sliceToEnd(~start=2)->String.trim
232
+
let scope' = Array.concat(fixes, scope)
233
+
switch parseKeyword(cur.contents) {
234
+
| Some("?") => {
235
+
Ok(({fixes,assumptions,method:None},
236
+
cur.contents->String.sliceToEnd(~start=1)))
237
+
}
238
+
| Some(keyword) => {
239
+
cur := cur.contents->String.sliceToEnd(~start=String.length(keyword))
240
+
switch Method.parse(
241
+
cur.contents, ~keyword,~scope=scope',~gen,~subparser=parse) {
242
+
| Ok((method,r)) => Ok(({fixes,assumptions,method:Some(method)},r))
243
+
| Error(e) => Error(e)
244
+
}
245
+
}
246
+
| None => Error("Expected keyword")
247
+
}
84
248
}
85
249
}
86
-
module Proof = (A : PROOFT) => {
87
-
type rec t = {goal:Goal.t, step?: A.t<t> }
250
+
let enter = (ctx : Context.t, prf: t, rule: Rule.t) => {
251
+
if Array.length(prf.fixes) == Array.length(rule.vars) {
252
+
if Array.length(prf.assumptions) == Array.length(rule.premises) {
253
+
let newFacts = Dict.fromArray(Belt.Array.zip(prf.assumptions,rule.premises))
254
+
Ok({
255
+
Context.fixes: rule.vars->Array.concat(ctx.fixes),
256
+
facts: Dict.copy(ctx.facts)->Dict.assign(newFacts)
257
+
})
258
+
} else {
259
+
Error("Proof introduces a different number of assumptions than the rule")
260
+
}
261
+
} else {
262
+
Error("Proof introduces a different number of variables than the rule")
263
+
}
264
+
265
+
} //result<Context, string>
266
+
267
+
let rec uncheck = (prf : checked) => switch prf {
268
+
| ProofError({ raw, rule:_, msg:_ }) => raw
269
+
| Checked({fixes,assumptions,method,rule:_}) => {
270
+
fixes, assumptions,
271
+
method: method->Option.map(xs => xs->Method.uncheck(uncheck))
272
+
}
88
273
}
274
+
let rec check = (ctx : Context.t, prf: t, rule: Rule.t) => {
275
+
switch enter(ctx,prf,rule) {
276
+
| Ok(ctx') => switch prf.method {
277
+
| Some(m) =>
278
+
switch m->Method.check(ctx', rule.conclusion, (s, r) => check(ctx',s,r)) {
279
+
| Ok(m') => Checked({
280
+
rule, fixes: prf.fixes,
281
+
assumptions: prf.assumptions,
282
+
method:Some(m')
283
+
})
284
+
| Error(e) => ProofError({raw:prf, rule, msg:e})
285
+
}
286
+
| None => Checked({
287
+
rule, fixes: prf.fixes, assumptions: prf.assumptions, method: None
288
+
})
289
+
}
290
+
| Error(e) => ProofError({raw:prf, rule, msg: e})
291
+
}
292
+
}// result<checked,string>
293
+
89
294
}
90
-
//module TestProofs = Proof(Either(Deduction,Lemma))
295
+
296
+
/*
297
+
298
+
299
+
300
+
*/
+13
-2
src/Rule.res
+13
-2
src/Rule.res
···
1
1
open Signatures
2
2
// the tree sitter plugin hates backslashes in string literals unless they're on the top
3
3
// level..
4
-
let vinculumRES = "^\s*\\n\\s*[-—][-—][\\-—]+([^\\n\\-—][^\\n]*)?"
4
+
let ruleNamePattern = "^[^|()\\s\\-—][^()\\s]*"
5
+
let vinculumRES = "^\s*\\n\\s*[-—][-—][\\-—]+[ \t]*([^()|\\s\\-—][^()\\s]*)?"
5
6
module Make = (Term : TERM, Judgment : JUDGMENT with module Term := Term) => {
6
7
type rec t = {vars: array<Term.meta>, premises: array<t>, conclusion: Judgment.t}
7
8
let rec substitute = (rule: t, subst: Term.subst) => {
···
41
42
conclusion: rule.conclusion->Judgment.substDeBruijn(terms')
42
43
}
43
44
}
44
-
45
+
let parseRuleName = (str) => {
46
+
let re = RegExp.fromStringWithFlags(ruleNamePattern,~flags="y")
47
+
switch re->RegExp.exec(String.trim(str)) {
48
+
| None => Error("expected rule name")
49
+
| Some(res) => { switch res[0] {
50
+
| Some(Some(n)) if String.trim(n) != ""
51
+
=> Ok(n,String.sliceToEnd(String.trim(str),~start=RegExp.lastIndex(re)))
52
+
| _ => Error("expected rule name")
53
+
}}
54
+
}
55
+
}
45
56
let parseVinculum = (str) => {
46
57
let re = RegExp.fromStringWithFlags(vinculumRES,~flags="y")
47
58
switch re->RegExp.exec(str) {
+3
src/SExp.res
+3
src/SExp.res
···
8
8
type meta = string
9
9
type schematic = int
10
10
type subst = Map.t<schematic,t>
11
+
let equivalent = (a : t, b: t) => {
12
+
a == b
13
+
}
11
14
let rec schematicsIn : (t) => Belt.Set.t<int, IntCmp.identity> = (it : t) => switch it {
12
15
| Schematic({schematic,_}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic)
13
16
| Compound({subexps}) => subexps->Array.reduce(
+4
src/Scratch.res
+4
src/Scratch.res
···
1
1
open Editable
2
+
open ProofEngine
2
3
module RuleSExpTE = RuleSetSB(SExp,SExp,SExpJView)
3
4
module RuleSExpView = WithTextArea(RuleSExpTE)
4
5
include RuleSExpView//(RuleSExpView.Hypothetical(RuleSExpView.Inline))
6
+
module PM = Proof(SExp,SExp,Combine(SExp,SExp,Derivation(SExp,SExp),Lemma(SExp,SExp)))
7
+
8
+
5
9
//include SExpBaseView
6
10
+3
src/Signatures.res
+3
src/Signatures.res
···
6
6
type subst = Map.t<schematic,t>
7
7
let substitute : (t, subst) => t
8
8
let unify : (t, t) => array<subst>
9
+
// law: unify(a,b) == [{}] iff equivalent(a,b)
10
+
let equivalent : (t, t) => bool
9
11
let substDeBruijn : (t, array<t>, ~from:int=?) => t
10
12
let upshift : (t, int, ~from:int=?) => t
11
13
type gen
···
23
25
module Term : TERM
24
26
type t
25
27
let substitute : (t, Term.subst) => t
28
+
let equivalent : (t,t) => bool
26
29
let unify : (t, t) => array<Term.subst>
27
30
let substDeBruijn : (t, array<Term.t>, ~from:int=?) => t
28
31
let upshift : (t, int, ~from:int=?) => t
+34
-3
src/testcomponent.tsx
+34
-3
src/testcomponent.tsx
···
1
1
import * as ComponentGraph2 from './componentgraph'
2
-
import { make as SExpBaseView, RuleSExpTE } from './Scratch.mjs'
2
+
import { make as SExpBaseView, RuleSExpTE, PM } from './Scratch.mjs'
3
3
import ReactDOM from 'react-dom/client';
4
4
import React from 'react';
5
5
···
56
56
};
57
57
}
58
58
}
59
-
//window.localStorage.clear()
60
-
ComponentGraph.setup({"hol-comp": TestComponent,"hol-config": ConfigComponent});
59
+
60
+
61
+
export class ProofComponent implements Component {
62
+
data : any;
63
+
dependencies : Record<string,any>;
64
+
dependencyChanged : (id: string, comp: Component) => void;
65
+
root : ReactDOM.Root;
66
+
toString() {
67
+
return ""
68
+
}
69
+
constructor(str : string, deps : Record<string,Component>, signal : (msg: any) => void, view? : HTMLElement) {
70
+
console.log("FOO")
71
+
for (const x in deps) {
72
+
if (deps[x] instanceof TestComponent) {
73
+
this.dependencies = deps[x].data
74
+
}
75
+
}
76
+
var gen = {contents:0};
77
+
this.data = PM.parse(str, [], gen);
78
+
console.log(this.data)
79
+
if (view != null) {
80
+
//this.root = ReactDOM.createRoot(view);
81
+
//this.root.render(<SExpBaseView rules={this.data} style={this.config}
82
+
// onChange={ e => { this.data = e.rules; signal("changed") }} />)
83
+
}
84
+
this.dependencyChanged = (_depName, comp) => {
85
+
};
86
+
}
87
+
}
88
+
89
+
90
+
window.localStorage.clear()
91
+
ComponentGraph.setup({"hol-comp": TestComponent,"hol-config": ConfigComponent, "hol-proof":ProofComponent});