the next generation of the in-browser educational proof assistant
fix elimination with first+higher order terms
+57
-34
+17
-7
index.html
+17
-7
index.html
···
331
331
--------------------------- E-ind
332
332
(P n) </hol-comp>
333
333
<hol-config id="index.html/myconfig">Gentzen</hol-config>
334
-
<hol-proof id="index.html/prooftest" deps="index.html/myconfig index.html/baz index.html/nat">
335
-
a.
336
-
(Nat a)
337
-
-------
338
-
(Nat (S (S a)))
339
-
340
-
a. asm |- ?
334
+
<!-- <hol-proof id="index.html/prooftest" deps="index.html/myconfig index.html/baz index.html/nat"> -->
335
+
<!-- n. -->
336
+
<!-- (Even (S (S n))) -->
337
+
<!-- --------------- -->
338
+
<!-- (Even n) -->
339
+
<!---->
340
+
<!-- n. asm |- ? -->
341
+
<!-- </hol-proof> -->
342
+
<hol-proof id="index.html/prooftest2" deps="index.html/myconfig index.html/baz index.html/nat">
343
+
x.y.
344
+
(/\ x y)
345
+
--------
346
+
(/\ y x)
347
+
348
+
x.y. asm |- by (AI ((x. x. \1) y x) ((x. x. x) y x)) {
349
+
|- ?
350
+
|- ?}
341
351
</hol-proof>
342
352
<h1>String</h1>
343
353
<h2>Basic</h2>
+24
-20
src/HOTerm.res
+24
-20
src/HOTerm.res
···
168
168
assert(subst->Belt.Map.Int.has(schematic) == false)
169
169
subst->Belt.Map.Int.set(schematic, term)
170
170
}
171
-
let rec substitute = (term: t, subst: subst) =>
172
-
switch term {
173
-
| Schematic({schematic, _}) =>
174
-
switch Belt.Map.Int.get(subst, schematic) {
175
-
| None => term
176
-
| Some(found) => found
177
-
}
178
-
| Lam({name, body}) =>
179
-
Lam({
180
-
name,
181
-
// upshift is not needed for pattern unification, but it is safer to have upshift here
182
-
body: substitute(body, subst->Belt.Map.Int.map(t => upshift(t, 1))),
183
-
})
184
-
| App({func, arg}) =>
185
-
App({
186
-
func: substitute(func, subst),
187
-
arg: substitute(arg, subst),
188
-
})
189
-
| Var(_) | Unallowed | Symbol(_) => term
190
-
}
191
171
192
172
// TODO: check how will this interact with meta variables (schematics) and check if it is needed to have a subst parameter - it should not be needed for subst produced by pattern unification
193
173
let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) =>
···
236
216
237
217
| Unallowed => Unallowed
238
218
}
219
+
}
220
+
let substitute = (term: t, subst: subst) => {
221
+
let rec inner = (term, subst) =>
222
+
switch term {
223
+
| Schematic({schematic, _}) =>
224
+
switch Belt.Map.Int.get(subst, schematic) {
225
+
| None => term
226
+
| Some(found) => found
227
+
}
228
+
| Lam({name, body}) =>
229
+
Lam({
230
+
name,
231
+
// upshift is not needed for pattern unification, but it is safer to have upshift here
232
+
body: inner(body, subst->Belt.Map.Int.map(t => upshift(t, 1))),
233
+
})
234
+
| App({func, arg}) =>
235
+
App({
236
+
func: inner(func, subst),
237
+
arg: inner(arg, subst),
238
+
})
239
+
| Var(_) | Unallowed | Symbol(_) => term
240
+
}
241
+
242
+
inner(term, subst)->reduce
239
243
}
240
244
let reduceSubst = (subst: subst): subst => {
241
245
subst->Belt.Map.Int.map(x => reduce(substitute(x, subst)))
+9
-5
src/Method.res
+9
-5
src/Method.res
···
184
184
}
185
185
let updateAtKey = (it: t<'a>, key: int, f: 'a => 'a) => {
186
186
let newsgs = it.subgoals->Array.copy
187
-
newsgs->Array.set(key, f(newsgs[key]->Option.getExn))
187
+
newsgs->Array.set(key, f(newsgs[key]->Option.getExn))
188
188
{...it, subgoals: newsgs}
189
189
}
190
190
}
···
348
348
ctx.facts
349
349
->Dict.toArray
350
350
->Array.filter(((_, r)) =>
351
-
r.premises->Array.length > 0 && (r.premises[0]->Option.getExn).premises->Array.length == 0
351
+
r.premises->Array.length > 0 && {
352
+
let fst = r.premises[0]->Option.getExn
353
+
fst.premises->Array.length == 0 && fst.vars->Array.length == 0
354
+
}
352
355
)
353
356
let possibleElims =
354
-
ctx.facts->Dict.toArray->Array.filter(((_, r)) => r.premises->Array.length == 0)
357
+
ctx.facts
358
+
->Dict.toArray
359
+
->Array.filter(((_, r)) => r.premises->Array.length == 0 && r.vars->Array.length == 0)
355
360
possibleRules->Array.forEach(((ruleName, rule)) => {
356
361
possibleElims->Array.forEach(((elimName, elim)) => {
357
362
let ruleInsts = rule->Rule.schematise(gen, ~scope=ctx.fixes)
358
-
let elimInsts = elim->Rule.schematise(gen, ~scope=ctx.fixes)
359
-
let (rule', elim) = (rule->Rule.instantiate(ruleInsts), elim->Rule.instantiate(elimInsts))
363
+
let rule' = rule->Rule.instantiate(ruleInsts)
360
364
Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion)->Seq.forEach(
361
365
elimSub => {
362
366
let rule'' = rule'->Rule.substituteBare(elimSub)
+7
-2
src/Scratch.res
+7
-2
src/Scratch.res
···
5
5
module DerivationsOrLemmasView = MethodView.CombineMethodView(
6
6
HOTerm,
7
7
HOTermJ,
8
-
MethodView.DerivationView(HOTerm, HOTermJ),
9
-
MethodView.LemmaView(HOTerm, HOTermJ, HOTermJView),
8
+
MethodView.CombineMethodView(
9
+
HOTerm,
10
+
HOTermJ,
11
+
MethodView.DerivationView(HOTerm, HOTermJ),
12
+
MethodView.LemmaView(HOTerm, HOTermJ, HOTermJView),
13
+
),
14
+
MethodView.EliminationView(HOTerm, HOTermJ),
10
15
)
11
16
module TheoremS = Editable.TextArea(
12
17
Theorem.Make(HOTerm, HOTermJ, HOTermJView, DerivationsOrLemmasView),