the next generation of the in-browser educational proof assistant
add mutual induction principles for string terms
+70
-17
+10
index.html
+10
index.html
···
488
488
"$s" L
489
489
s. sM |- ?
490
490
</hol-string-proof>
491
+
<hol-string-proof id="index.html/lexp-mexp" deps="index.html/myconfig index.html/mexp index.html/mexp-induct index.html/lexp index.html/lexp-n">
492
+
s. "$s" L
493
+
----------- mexp-lexp
494
+
"$s" M
495
+
s. sL |- elim (L_mutualInduct sL "" "$s" "" "M" "M") {
496
+
|- by (M-Empty) {}
497
+
s1.s2. 0 1 2 3 |- elim (M-Juxtapose 2 "$s1" "$s2") {
498
+
|- by (3) {}}
499
+
s. 0 1 |- elim (M-Surround 1 "$s") {}}
500
+
</hol-string-proof>
491
501
<script type="module" src="./src/testcomponent.tsx"></script>
492
502
</body>
493
503
</html>
+60
-17
src/StringAxiomSet.res
+60
-17
src/StringAxiomSet.res
···
18
18
onChange: (state, ~exports: Ports.t=?) => unit,
19
19
}
20
20
21
+
type judgeGroup = {
22
+
name: string,
23
+
rules: array<Rule.t>,
24
+
}
25
+
21
26
module Set = Belt.Set.String
22
27
let varsInRule = (rule: Rule.t) => {
23
28
rule.premises->Array.reduce(Set.fromArray(rule.vars), (s, r) =>
···
25
30
)
26
31
}
27
32
28
-
let derive = (name: string, rules: array<Rule.t>): Rule.t => {
29
-
// TODO: can we remove some of the hardcoding?
30
-
let allVars = rules->Array.reduce(Set.empty, (s, r) => s->Set.union(varsInRule(r)))
33
+
let getSExpName = (t: SExp.t): option<string> =>
34
+
switch t {
35
+
| Symbol({name}) => Some(name)
36
+
| _ => None
37
+
}
38
+
39
+
let findMentionedRuleGroups = (group: judgeGroup, allGroups: array<judgeGroup>): array<
40
+
judgeGroup,
41
+
> => {
42
+
let allGroupNames = allGroups->Array.map(g => g.name)
43
+
let groupNames: array<string> = Array.concat(
44
+
[group.name],
45
+
group.rules
46
+
->Array.flatMap(r =>
47
+
r.premises
48
+
->Array.map(p => p.conclusion->snd->getSExpName)
49
+
->Array.keepSome
50
+
->Array.filter(name => allGroupNames->Array.find(name' => name' == name)->Option.isSome)
51
+
)
52
+
->Set.fromArray
53
+
->Set.remove(group.name)
54
+
->Set.toArray,
55
+
)
56
+
groupNames->Array.map(name => allGroups->Array.find(g => g.name == name))->Array.keepSome
57
+
}
58
+
59
+
let derive = (group: judgeGroup, mentionedGroups: array<judgeGroup>): Rule.t => {
60
+
let allVars =
61
+
mentionedGroups
62
+
->Array.flatMap(g => g.rules)
63
+
->Array.reduce(Set.empty, (s, r) => s->Set.union(varsInRule(r)))
31
64
let rec genVar = (base: string) => {
32
65
if allVars->Set.has(base) {
33
66
genVar(`${base}'`)
···
35
68
base
36
69
}
37
70
}
38
-
let (p, b, x, a) = (genVar("P"), genVar("b"), genVar("x"), genVar("a"))
39
-
let vars = [p, b, x, a]
71
+
let ps = mentionedGroups->Array.map(g => genVar(`P${g.name}`))
72
+
let (b, x, a) = (genVar("b"), genVar("x"), genVar("a"))
73
+
let vars = Array.concat(ps, [b, x, a])
40
74
let xIdx = vars->Array.findIndex(i => i == x)
41
75
let aIdx = vars->Array.findIndex(i => i == a)
42
76
let bIdx = vars->Array.findIndex(i => i == b)
43
-
let pIdx = vars->Array.findIndex(i => i == p)
44
77
let surround = (t: StringTerm.t, aIdx: int, bIdx: int) => {
45
78
Array.concat(Array.concat([StringTerm.Var({idx: aIdx})], t), [StringTerm.Var({idx: bIdx})])
46
79
}
47
-
let rec replaceJudgeRHS = (rule: Rule.t, aIdx: int, bIdx: int, pIdx: int): Rule.t => {
48
-
let n = Array.length(rule.vars)
49
-
let (aIdx, bIdx, pIdx) = (aIdx + n, bIdx + n, pIdx + n)
80
+
let lookupGroup = (t: SExp.t): option<int> =>
81
+
mentionedGroups->Array.findIndexOpt(g => t == SExp.Symbol({name: g.name}))
82
+
let rec replaceJudgeRHS = (rule: Rule.t, baseIdx: int): Rule.t => {
83
+
let baseIdx = baseIdx + Array.length(rule.vars)
50
84
let inductionHyps =
51
85
rule.premises
52
-
->Array.filter(r => r.conclusion->snd == Symbol({name: name}))
53
-
->Array.map(r => replaceJudgeRHS(r, aIdx, bIdx, pIdx))
86
+
->Array.filter(r => lookupGroup(r.conclusion->snd)->Option.isSome)
87
+
->Array.map(r => replaceJudgeRHS(r, baseIdx))
88
+
let pIdx = lookupGroup(rule.conclusion->snd)->Option.getExn
54
89
{
55
90
vars: rule.vars,
56
91
premises: rule.premises->Array.concat(inductionHyps),
57
-
conclusion: (surround(rule.conclusion->fst, aIdx, bIdx), Var({idx: pIdx})),
92
+
conclusion: (
93
+
surround(rule.conclusion->fst, aIdx + baseIdx, bIdx + baseIdx),
94
+
Var({idx: pIdx + baseIdx}),
95
+
),
58
96
}
59
97
}
60
98
{
···
64
102
{
65
103
Rule.vars: [],
66
104
premises: [],
67
-
conclusion: ([StringTerm.Var({idx: xIdx})], Symbol({name: name})),
105
+
conclusion: ([StringTerm.Var({idx: xIdx})], Symbol({name: group.name})),
68
106
},
69
107
],
70
-
rules->Array.map(r => replaceJudgeRHS(r, aIdx, bIdx, pIdx)),
108
+
mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))),
71
109
),
72
-
conclusion: (surround([StringTerm.Var({idx: xIdx})], aIdx, bIdx), Var({idx: pIdx})),
110
+
conclusion: (surround([StringTerm.Var({idx: xIdx})], aIdx, bIdx), Var({idx: 0})), // TODO: clean here
73
111
}
74
112
}
75
113
···
114
152
| _ => ()
115
153
}
116
154
)
155
+
let allGroups = grouped->Dict.toArray->Array.map(((name, rules)) => {name, rules})
117
156
let derived: Dict.t<Rule.t> = Dict.make()
118
-
grouped->Dict.forEachWithKey((rules, name) => {
157
+
allGroups->Array.forEach(group => {
119
158
// NOTE: this can clash with other names. is this an issue?
120
-
derived->Dict.set(`${name}_induct`, derive(name, rules))
159
+
derived->Dict.set(`${group.name}_induct`, derive(group, [group]))
160
+
let mentionedGroups = findMentionedRuleGroups(group, allGroups)
161
+
if mentionedGroups->Array.length > 1 {
162
+
derived->Dict.set(`${group.name}_mutualInduct`, derive(group, mentionedGroups))
163
+
}
121
164
})
122
165
({raw, derived}, {Ports.facts: raw->Dict.copy->Dict.assign(derived), ruleStyle: None})
123
166
})