the next generation of the in-browser educational proof assistant
generated cases rules
+49
-4
+49
-4
src/InductiveSet.res
+49
-4
src/InductiveSet.res
···
177
177
allGroups->Array.filter(g => Belt.Set.has(reachableKeys, makeKey(g.name, g.arity)))
178
178
}
179
179
180
+
let generateCasesRule = (group: constructorGroup): Rule.t => {
181
+
let {name: str, arity: _i} = group
182
+
183
+
let caseSubgoal = ((_constructorName: string, constructorRule: Rule.t)): Rule.t => {
184
+
let offset = Array.length(constructorRule.vars)
185
+
186
+
let equalityPremise = {
187
+
Rule.vars: [],
188
+
premises: [],
189
+
conclusion: HOTerm.app(
190
+
HOTerm.Symbol({name: "="}),
191
+
[HOTerm.Var({idx: offset}), constructorRule.conclusion],
192
+
),
193
+
}
194
+
195
+
{
196
+
Rule.vars: constructorRule.vars,
197
+
premises: Array.concat([equalityPremise], constructorRule.premises),
198
+
conclusion: HOTerm.Var({idx: offset + 1}),
199
+
}
200
+
}
201
+
202
+
let subgoals = Array.map(group.rules, ((name, rule)) => caseSubgoal((name, rule)))
203
+
204
+
{
205
+
Rule.vars: Array.concat(["§0"], ["§P"]),
206
+
premises: [
207
+
{
208
+
Rule.vars: [],
209
+
premises: [],
210
+
conclusion: HOTerm.app(HOTerm.Symbol({name: str}), [HOTerm.Var({idx: 0})]),
211
+
},
212
+
...subgoals,
213
+
],
214
+
conclusion: HOTerm.Var({idx: 1}),
215
+
}
216
+
}
217
+
180
218
let derived = (state: state): state =>
181
219
state
182
220
->groupByConstructor
183
-
->Array.map(group => {
221
+
->Array.flatMap(group => {
184
222
let mutualComponent = findMutuallyInductiveComponent(group, groupByConstructor(state))
185
-
let rule = generateInductionRule(group, mutualComponent)
186
-
("§induction-" ++ makeKey(group.name, group.arity), rule)
223
+
let inductionRule = generateInductionRule(group, mutualComponent)
224
+
let casesRule = generateCasesRule(group)
225
+
[
226
+
("§induction-" ++ makeKey(group.name, group.arity), inductionRule),
227
+
("§cases-" ++ makeKey(group.name, group.arity), casesRule),
228
+
]
187
229
})
188
230
->Dict.fromArray
189
231
let serialise = (state: state) =>
···
217
259
}
218
260
}
219
261
}
220
-
ret.contents->Result.map(state => (state, {Ports.facts: state->Dict.copy->Dict.assign(derived(state)), ruleStyle: None}))
262
+
ret.contents->Result.map(state => (
263
+
state,
264
+
{Ports.facts: state->Dict.copy->Dict.assign(derived(state)), ruleStyle: None},
265
+
))
221
266
}
222
267
223
268
let make = props => {