tracking: induction

[c-cube]

• custom induction schema, with a toplevel command

  • structural induction on datatypes:
    inductive (n:nat) := { (zero, {}), (succ(n'), {n'}) }

  • induction on sets
    inductive (S:set a) := { (S=empty, {}), (∃x S'. (S = S' ∪ {x} ∧ x∉S'), {S'}) }
    corresponding to axioms:
    forall S. S = empty xor ∃x S'. (S = S' ∪ {x} ∧ x∉S')
[ P empty && (forall x S S'. x ∈ S ∧ S = S' ∪ {x} ∧ x∉S' ∧ P(S') => P(S)) ] => ∀S. P S.
    NOTE: need to restrict its application, not needed for most use cases
    and will only slow things down
    → only when goal involves recursive function on sets?

  • inductive relations? if R transitive:
    inductive (R(x,y)) := { (x=y, {}), (x ≠ y, {∃z. R(x,y) ∧ R(y,z)}) }

• discussion

  • it all becomes sound (assuming hidden induction principle): each cut is really the introduction of an instance of the induction principle
  • no nested induction anymore
  • allows to use smallcheck before trying a lemma
  • allows to refine a lemma by generalizing (Aubin 77) some specific
    subterms and some specific occurrences of variables, based on
    their position below defined symbols (in particular, for accumulator terms)
  • similar subgoals that would be distinct before (same goal, different
    skolems) are now the same lemma, thanks to the α-equiv checking

• from a clause C with inductive skolems {a,b,c} we can generalize
  on these skolems without worrying,
  and try to prove ∀xyz. ¬C[x/a,y/b,z/c] (but only do induction
  on variables that occur in active positions)

• remove trail literals for induction (and remove clause context,
  might have the higher-order induction principle for proof
  production though)

• generate fresh coverset every time; new inductive skolem constants
  really become branch dependent
  (no need to prevent branches from interfering every again!)

• call small_check on candidate inductive formulas;
  try simple generalizations backed by small_check before starting.
  → will be useful after purification (approximation leads to too
  many inferences, some of which yield non-inductively true constraints,
  so we need to check constraints before solving them by induction)

• only do induction on active positions
  → check that it fixes previous regression on list10_easy.zf, nat2.zf…)

• might be a bug in candidate lemmas regarding α-equiv checking
  (see on nat2.zf, should have only one lemma?)

• do induction on simplified formula (e.g. for HO functions)

• notion of active position should also work for
  defined propositions (look into clause rules)
  + [x] factor the computation of positions out of rewrite_term
  and abstract it so it takes a list of LHS
  + [x] move this into Statement? propositions defined by clause rules
  with atom t as LHS should be as "defined" as term RW rules
  + [x] small check truly needs to use clause rules, too

• check if two variables are interchangeable (i.e. {X→Y,Y→X}
  gives same form). In this case don't do induction on the second one.

• do induction on multiple variables, iff they occur in active
  positions in the same subterm.
  + just combine the coversets for each variable
  + same as splitting, do union-find of x,y if there is an active subterm
  f …x…y… where both x and y are active
  + should subsume/replace the individual inductions (which are bound
  to fail since the subterms will not reduce because of one of
  their arg)
  + goes with generalization? If a non-var occurs in active position,
  it must be generalized? Maybe in 2 successive steps…
  + [ ] example: should prove transitivity of ≤
  ./zipperposition.native --print-lemmas --stats -o none -t 30 --dot /tmp/truc.dot examples/ind/nat21.zf
  → might be sufficient for many cases where we used to use nested ind.

• generalize a bit notion of ind_cst (to ground terms made of skolems)

• functional induction:

  • based on assumption that recursive functions terminate
    → ask for [wf] attribute?
    → maybe prove termination myself?
    → require that such functions are total! (not just warning)
  • build functional induction scheme(s) based on recursive def, might
    prove very useful for some problems.
  • applies for goals of the form P[f(x…)] with only variables in
    active/accumulator positions of f. In inductive hypothesis,
    use P[f(skolems…)]? or is it automatic with multi-var-induction?

• use subsumption on candidate lemmas:

  • if a proved lemma subsumes the current candidate, then skip candidate
  • if an unknown lemma subsumes the current candidate, delay it; wait until the subsuming one is proved/disproved
  • OR,
    when a candidate lemma is subsumed by some active lemma,
    lock it and store it somewhere, waiting for one of the following
    conditions to happen:
    1. when a lemma is proved, delete candidate lemmas it subsumes
    2. when a lemma is disproved, unlock candidate lemmas that it
       subsumes and activate them (unless they are locked by other lemmas)
       → might even be in Avatar itself, as a generic mechanism!
  • when a lemma is proved, find other lemmas that are subsumed by it?
    or this might be automatic, but asserting [L2] if L1 proved and L1⇒L2
    might still help with the many clauses derived from L2
  • might need a signal on_{dis_,}proved_lemma for noticing
    that a lemma is now (dis,)proved by the SAT solver.
    → Hook into it to unlock/remove candidates subsumed by the lemma.

• some clause constraints (e.g. a+s b ≠ s (a+b)) might deserve
  their own induction, because no other rule (not even E-unification)
  will be able to solve these.
  → Again, need very good and fast small_check…

• when generalizing f X a != f a X, which currently yields
  the lemma f X Y = f Y X, instead we could "skolemize" X
  with a HO variable, obtaining f (H Y) Y = f Y (H Y).
  see examples/ind/nat6.zf for a case where it can help
  (we need H because there already is a skolem out there).

• strong induction?

  • use explicit <| subterm relation for the hypothesis
  • use special transitive rel saturation rules for <|
    (and nonstrict version ≤|)
  • also use custom rules for subterm (using constructors)
    including simplification of t <| cstor^N(t)
    and corresponding unification inference rule
    → acyclicity just becomes the axiom ¬ (x <| x) combined with above rules
  • no need for coverset anymore, just introduce skolems, but need
    (depth-limited) case-split on arbitrary constants/ground terms.
    → decouples case split and induction
  • when generalizing ¬P[a,b] into ∀xy. P[x,y], when doing induction
    on x, might instead prove: ∀xy. y ≤| b ⇒ P[x,y]? this way we
    can re-use hypothesis on y (and maybe x)?
  • multi-variable induction requires <| to work on tuples or multisets
    on both sides…
  • ./zipperposition.native --print-lemmas --stats -o none -t 30 --dot /tmp/truc.dot examples/ind/nat21.zf

• lemma guessing in induction:

  • simple generalization of a variable with ≥ 2 occurrences in active pos,
    and ≥ 1 passive occurrences
  • generalization of subterms that are not variables nor constructors,
    occurring at least twice in active positions.
  • track variable dependencies for generalized subterms, to avoid
    losing the (often crucial) relation between them
    and other terms containing the same variables.
    → need to also prove t = t' for every generalized term t
    and other term t' that shared ≥1 var with t
  • purification of composite terms occurring in passive position
  • anti-unification in sub-goal solving
    (e.g. append a t1 != append a t2, where a is a skolem
    → try to prove t1!=t2 instead,
    if append is found to be left-injective by testing or lemma)
  • paramodulation of sub-goal with inductive hypothesis (try on list7.zf)?

• make real inductive benchmarks
  (ok using tip-benchmarks)

  • add lemma statement to tip-parser
  • parse this in Zipperposition
  • use quickspec to generate lemmas on Isaplanner problems
  • run benchmarks (without induction, with induction, with quickspec lemmas)

• lemma by generalization (if t occurs on both sides of ineq?)

  • see what isaplanner does
  • use "Aubin" paper (generalize exactly the subterms at reductive position),
    but this requires to have tighter control over rules/definitions first

• generate all lemmas up to given depth

  • need powerful simplifications from the beginning (for smallchecking)