the next generation of the in-browser educational proof assistant
Merge pull request #14 from joshcbrown/push-votzpspyrtyv
Elimination fixes
authored by
Liam O'Connor
and committed by
GitHub
153e6a5b
500fae8d
+52
-14
+21
index.html
+21
index.html
···
345
345
(= (A a) (B a))
346
346
</hol-comp>
347
347
<hol-config id="index.html/myconfig">Gentzen</hol-config>
348
+
<!-- <hol-proof id="index.html/prooftest" deps="index.html/myconfig index.html/baz index.html/nat"> -->
349
+
<!-- n. -->
350
+
<!-- (Even (S (S n))) -->
351
+
<!-- --------------- -->
352
+
<!-- (Even n) -->
353
+
<!---->
354
+
<!-- n. asm |- ? -->
355
+
<!-- </hol-proof> -->
356
+
<hol-proof id="index.html/prooftest2" deps="index.html/myconfig index.html/baz index.html/nat">
357
+
x.y.
358
+
(/\ x y)
359
+
--------
360
+
(/\ y x)
361
+
362
+
x.y. asm |- by (AI ((x. x. \1) y x) ((x. x. x) y x)) {
363
+
|- ?
364
+
|- ?}
365
+
366
+
</hol-proof>
367
+
348
368
<hol-proof id="index.html/prooftest" deps="index.html/myconfig index.html/baz index.html/nat">
349
369
a.
350
370
(Nat a)
···
352
372
(Nat (S (S a)))
353
373
354
374
a. asm |- ?
375
+
355
376
</hol-proof>
356
377
357
378
<hol-proof id="index.html/prooftest2" deps="index.html/myconfig index.html/baz index.html/nat">
+21
-9
src/Method.res
+21
-9
src/Method.res
···
34
34
) => string
35
35
}
36
36
37
+
let seqSizeLimit = 100
38
+
37
39
module Derivation = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
38
40
module Rule = Rule.Make(Term, Judgment)
39
41
module Context = Context(Term, Judgment)
···
138
140
let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => {
139
141
let ret = Dict.make()
140
142
ctx.facts->Dict.forEachWithKey((rule, key) => {
141
-
let insts = rule->Rule.schematise(gen, ~scope=ctx.fixes)
143
+
let insts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
142
144
let res = rule->Rule.instantiate(insts)
143
145
let substs = Judgment.unify(res.conclusion, j, ~gen)
144
-
substs->Seq.forEach(subst => {
146
+
substs
147
+
->Seq.take(seqSizeLimit)
148
+
->Seq.forEach(subst => {
145
149
let new = {
146
150
ruleName: key,
147
151
instantiation: insts,
···
348
352
ctx.facts
349
353
->Dict.toArray
350
354
->Array.filter(((_, r)) =>
351
-
r.premises->Array.length > 0 && (r.premises[0]->Option.getExn).premises->Array.length == 0
355
+
r.premises->Array.length > 0 && {
356
+
let fst = r.premises[0]->Option.getExn
357
+
fst.premises->Array.length == 0 && fst.vars->Array.length == 0
358
+
}
352
359
)
353
360
let possibleElims =
354
-
ctx.facts->Dict.toArray->Array.filter(((_, r)) => r.premises->Array.length == 0)
361
+
ctx.facts
362
+
->Dict.toArray
363
+
->Array.filter(((_, r)) => r.premises->Array.length == 0 && r.vars->Array.length == 0)
355
364
possibleRules->Array.forEach(((ruleName, rule)) => {
356
365
possibleElims->Array.forEach(((elimName, elim)) => {
357
-
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))
360
-
Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion)->Seq.forEach(
366
+
let ruleInsts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes)
367
+
let rule' = rule->Rule.instantiate(ruleInsts)
368
+
Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion)
369
+
->Seq.take(seqSizeLimit)
370
+
->Seq.forEach(
361
371
elimSub => {
362
372
let rule'' = rule'->Rule.substituteBare(elimSub)
363
-
Judgment.unify(rule''.conclusion, j, ~gen)->Seq.forEach(
373
+
Judgment.unify(rule''.conclusion, j, ~gen)
374
+
->Seq.take(seqSizeLimit)
375
+
->Seq.forEach(
364
376
ruleSub => {
365
377
let new = {
366
378
ruleName,
+3
-3
src/Rule.res
+3
-3
src/Rule.res
···
11
11
{
12
12
vars: rule.vars,
13
13
premises: rule.premises->Array.map(premise => premise->substitute(subst')),
14
-
conclusion: rule.conclusion->Judgment.substitute(subst'),
14
+
conclusion: rule.conclusion->Judgment.substitute(subst')->Judgment.reduce,
15
15
}
16
16
}
17
17
let rec substDeBruijn = (rule: t, substs: array<Judgment.substCodom>, ~from: int=0) => {
···
39
39
let substituteBare = (rule: bare, subst: Judgment.subst) => {
40
40
{
41
41
premises: rule.premises->Array.map(premise => premise->substitute(subst)),
42
-
conclusion: rule.conclusion->Judgment.substitute(subst),
42
+
conclusion: rule.conclusion->Judgment.substitute(subst)->Judgment.reduce,
43
43
}
44
44
}
45
45
let instantiate = (rule: t, terms: array<Judgment.substCodom>) => {
···
51
51
conclusion: rule.conclusion->Judgment.substDeBruijn(terms')->Judgment.reduce,
52
52
}
53
53
}
54
-
let schematise = (rule: t, gen: Term.gen, ~scope: array<Judgment.meta>) => {
54
+
let genSchemaInsts = (rule: t, gen: Term.gen, ~scope: array<Judgment.meta>) => {
55
55
rule.vars->Array.map(m => Judgment.placeSubstCodom(gen->Term.fresh(~replacing=m), ~scope))
56
56
}
57
57
let parseRuleName = str => {
+7
-2
src/Scratch.res
+7
-2
src/Scratch.res
···
12
12
module DerivationsOrLemmasView = MethodView.CombineMethodView(
13
13
HOTerm,
14
14
HOTermJ,
15
-
MethodView.DerivationView(HOTerm, HOTermJ),
16
-
MethodView.LemmaView(HOTerm, HOTermJ, HOTermJView),
15
+
MethodView.CombineMethodView(
16
+
HOTerm,
17
+
HOTermJ,
18
+
MethodView.DerivationView(HOTerm, HOTermJ),
19
+
MethodView.LemmaView(HOTerm, HOTermJ, HOTermJView),
20
+
),
21
+
MethodView.EliminationView(HOTerm, HOTermJ),
17
22
)
18
23
module DLRView = MethodView.CombineMethodView(
19
24
HOTerm,