Yutaka Ng
Yutaka Ng
UR: use the state monad to update the estimate of the importance of proof node. The importance of a proof node should be updated after discharging a sub-goal.
Currently, each `point` has only three fields: `cname`, `utyp`, and `level`. Therefore, it is possible that a syntax tree has multiple `point`s of the same value. We should avoid such...
Look at, for example, `Prod/TIP_prop_04.thy`. One can `apply (induct y y rule: x.induct)`. Such combination is not currently supported. But it should be.
Use the standard library and the AFP entries as target data.
See, for example, proof (induct s rule:reachable.induct) in Abortable_Linearizable_Modules/IOA.thy.
Currently, PaMpeR's database construction component ignores the proof component. A reviewer from ITP2018 suggested we should not omit these.
When PaMpeR looks up relevant derived lemmas in proof contexts, often it only uses constants and types that appear in the first subgoal. But probably PaMpeR should also use constants...
induct, induction, and induct_tac take up each others' share. We can generate these proof methods automatically using PSL and see in which cases they behave as the same proof method...
In the evaluation results for ITP2018, it was clear that PaMpeR's recommendations for **coinduct** and **coinduction** was suffering form over-fitting. We can fix this by pruning based on cross-validation.
Two possible approaches: 1. create a database for each assertion. - pros: we can find out which assertion causes problems. - pros: Isabelle is less likely to run out of...