CODEWITHSUNDEEP
isabelle
Paul Breen
Paul Breen

Reputation: 95

Transformation of goals by "rule"

I'm trying to use rule dec_induct to do an induction proof with a base case that is not 0, but I don't understand how the rule is being applied by Isabelle. If I state the following lemma:

lemma test:
shows "P a"
proof (rule dec_induct)

Isabelle transforms it into three subgoals, which I assume are supposed to be the premises of dec_induct unified with my goal. dec_induct is

⟦?i ≤ ?j; ?P ?i; ⋀n. ⟦?i ≤ n; n < ?j; ?P n⟧ ⟹ ?P (Suc n)⟧ ⟹ ?P ?j

, so I would think that the ?j in its conclusion would unify with the "a" of my goal. That is, I would expect the following three subgoals:

  1. ?i ≤ a
  2. ?P ?i
  3. ⋀n. ⟦?i ≤ n; n < a; ?P n⟧ ⟹ ?P (Suc n)

But the subgoals Isabelle actually transforms it to are

  1. ?i ≤ ?j
  2. P a
  3. ⋀n. ⟦?i ≤ n; n < ?j; P a⟧ ⟹ P a

How is Isabelle getting that, and how can I get it to perform the induction as I expect? I realize I should be using the induct method, but I'm just trying to understand how rule works.

Upvotes: 1

Views: 87

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8258

Higher order unification can produce very unintuitive results, especially when you have patterns like ?f ?x, i.e. a schematic variable of function type, applied to another schematic variable. I don't know much about higher order unification, but it seems that if you unify ?f ?x with something like f x, you tend to get the unifier [?f ↦ λy. f x] instead of [?f ↦ f, ?x ↦ x], which is probably what you wanted.

You can experiment with it like this to see precisely what the possible inferred unifiers are:

context
  fixes P :: "int ⇒ bool" and j :: int
begin

ML ‹
  local
    val ctxt = Context.Proof @{context}
    val env = Envir.init
    val ctxt' = @{context} |> Proof_Context.set_mode Proof_Context.mode_schematic
    val s1 = "?P ?j"
    val s2 = "P j"
    val (t1, t2) = apply2 (Syntax.read_term ctxt') (s1, s2)
    val prt = Syntax.pretty_term @{context}
    fun pretty_schem s = prt (Var ((s, 0), \<^typ>‹unit›))
    fun pretty_unifier (Envir.Envir {tenv, ...}, _) =
      tenv
      |> Vartab.dest
      |> map (fn ((s,_),(_,t)) => Pretty.block
             (Pretty.breaks [pretty_schem s, Pretty.str "↦", prt t]))
      |> (fn x => Pretty.block (Pretty.str "[" :: Pretty.commas x @ [Pretty.str "]"]))
  in
    val _ =
      Pretty.breaks [Pretty.str "Unifiers for", prt t1, Pretty.str "and", prt t2, Pretty.str ":"]
      |> Pretty.block
      |> Pretty.writeln
    val _ = 
      Unify.unifiers (ctxt, env, [(t1, t2)])
      |> Seq.list_of
      |> map pretty_unifier
      |> map (fn x => Pretty.block [Pretty.str "∙ ", x])
      |> map (Pretty.indent 2)
      |> Pretty.fbreaks
      |> Pretty.block
      |> Pretty.writeln
  end
›

Output:

Unifiers for ?P ?j and P j : 
  ∙ [?P ↦ λa. P j]

(Disclaimer: This is only experimental code to illustrate what is going on, this is not clean Isabelle/ML coding style.)

To summarise: don't rely on higher-order unification to figure out instantiations of function variables, especially when you have patterns like ?f ?x.

Upvotes: 2

Related Questions