UR: design decisions for the first prototype.

[yutakang]

• bottom-up conjecturing or goal-oriented conjecturing?
  Both: bidirectional conjecturing.
• structural proofs or backwards proofs?
  - Both: structural proofs for bottom-up conjecturing and backwards proofs for goal-oriented conjecturing.
  - Note that it would involve too many engineering efforts to produce structural proofs for goal-oriented conjecturing.
  - Not really structural proofs. We only want to provide "lemma ... apply ... by ...".
  - [ ] define a new command "prove" that would replace "lemma" and "theorem". This would save me from purely engineering efforts that are not scientifically important.
• best first search?
• what to conjecture in bottom-up conjecturing?
  • for binary functions (wikipedia)
    • associativity
    • left and right identity
    • invertibility using identity element
    • commutativity
    • idempotent element and idenpotency
  • if we have multiple functions
    • left and right distributivity
    • anti-distributivity
  • for relations
    • symmetry
    • reflexibility
    • transitivity
    • connexity
• We do not handle functions with n-arity where n is greater than 2 for now.
• Maybe one bottom-up conjecture helps us prove another bottom-up conjecture. So, we need to iterate. (Prod/TIP_prop_09.thy drop_succ uses drop_nil.)
• Maybe one bottom-up conjecture needs a top-down conjecture to be proved. But they sometimes do not sit well with the abductive reasoning framework. (Prod/TIP_prop_09.thy drop_comm uses drop_succ. But this is not an ab)
• what to conjecture in top-down approach
  • compound-term generalisation (abductive)
  • extension (abductive)
  • specialisation (abductive)
  • function application to variables of the same type on both sides of the equation. (top-down, not abductive, only for unary functions)
• Should I apply goal-oriented conjecturing only to the original goal? Should I apply it to sub-goals as well?
  • Only to the original goals for now.

[yutakang]

Producing this structural proof script is too much work for little gain.

lemma "itrev xs [] = rev xs"
(*
  apply (subgoal_tac "⋀Nil. itrev xs Nil = rev xs @ Nil")
  apply fastforce
  apply (induct xs)
  apply auto
  done 
*)
proof -
  {
  fix ys
  have "itrev xs ys = rev xs @ ys"
    apply(induct xs arbitrary: ys)
     apply auto
    done
  }
  from this
  show "itrev xs [] = rev xs"
    apply fastforce
    done
qed

[yutakang]

specialisation: goal-oriented conjecturing (top-down).

datatype nat = zero ("0") | Suc nat

primrec plus:: "nat ⇒ nat ⇒ nat" where
  "plus  zero   y = y"
| "plus (Suc x) y = Suc (plus x y)"

lemma 4: "plus x (plus x x) = plus (plus x x) x"
  (*try_hard fails*)
  apply(subgoal_tac "⋀x y. plus x (plus y y) = plus (plus x y) y")
   apply fastforce
  apply(induct_tac x)
   apply auto
  done

[yutakang]

How do we mutate proof goals to produce conjectures?

• term generalisation.
• extension (done in our CICM2018 paper)
• one-step unfolding

[yutakang]

How do we mutate proof goals to produce conjectures?

• term generalisation.
• extension (done in our CICM2018 paper)
• one-step unfolding

So far, these are done by ML functions.
We should improve SeLFiE to make these.