the next generation of the in-browser educational proof assistant
Merge pull request #16 from joshcbrown/push-lnxxwrzxonvz
Add mutual induction for string terms
authored by
Liam O'Connor
and committed by
GitHub
0a6acbae
44791561
+72
-21
+10
index.html
+10
index.html
···
587
587
"$s" L
588
588
s. sM |- ?
589
589
</hol-string-proof>
590
+
<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">
591
+
s. "$s" L
592
+
----------- mexp-lexp
593
+
"$s" M
594
+
s. sL |- elim (L_mutualInduct sL "" "$s" "" "M" "M") {
595
+
|- by (M-Empty) {}
596
+
s1.s2. 0 1 2 3 |- elim (M-Juxtapose 2 "$s1" "$s2") {
597
+
|- by (3) {}}
598
+
s. 0 1 |- elim (M-Surround 1 "$s") {}}
599
+
</hol-string-proof>
590
600
<script type="module" src="./src/testcomponent.tsx"></script>
591
601
</body>
592
602
</html>
+62
-21
src/StringAxiomSet.res
+62
-21
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->Pair.second->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->Pair.second == Symbol({name: name}))
53
-
->Array.map(r => replaceJudgeRHS(r, aIdx, bIdx, pIdx))
86
+
->Array.filter(r => lookupGroup(r.conclusion->Pair.second)->Option.isSome)
87
+
->Array.map(r => replaceJudgeRHS(r, baseIdx))
88
+
let pIdx = lookupGroup(rule.conclusion->Pair.second)->Option.getExn
54
89
{
55
90
vars: rule.vars,
56
91
premises: rule.premises->Array.concat(inductionHyps),
57
-
conclusion: (surround(rule.conclusion->Pair.first, aIdx, bIdx), Var({idx: pIdx})),
92
+
conclusion: (
93
+
surround(rule.conclusion->Pair.first, 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
})
···
135
178
<div
136
179
className={"axiom-set axiom-set-"->String.concat(
137
180
String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
138
-
)}
139
-
>
181
+
)}>
140
182
{content
141
183
->Dict.toArray
142
184
->Array.mapWithIndex(((n, r), i) =>
···
144
186
rule={r}
145
187
scope={[]}
146
188
key={String.make(i)}
147
-
style={props.imports.ruleStyle->Option.getOr(Hybrid)}
148
-
>
189
+
style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
149
190
{React.string(n)}
150
191
</RuleView>
151
192
)