SumT.thy

theory SumT
imports Main
begin

(* http://isabelle.in.tum.de/exercises/lists/sum-tail/sol.pdf *)

fun sumTAux :: "nat list ⇒ nat ⇒ nat" where
  "sumTAux [] s = s" |
  "sumTAux (n#ns) s = sumTAux ns (n+s)"
  
(* From the answers, this works immediately: *)
lemma sumtaux_add: "∀ a b. sumTAux ns (a+b) = a + sumTAux ns b"
by (induct ns) auto

(* Why does this have a more complicated proof? *)
lemma sumtaux_add: "∀ a. sumTAux ns a = a + sumTAux ns 0"
  apply (induct ns)
  apply simp
by (metis add.assoc add.commute sumTAux.simps(2))

(* Sledgehammer can't progress beyond `simp`, and `auto` hangs. *)
(* Why does the ∀ make a difference? *)
lemma sumtaux_add: "sumTAux ns a = a + sumTAux ns 0"
  apply (induct ns)
  apply simp
sorry

(* Same problem *)
lemma sumtaux_add: "sumTAux ns (a+b) = a + sumTAux ns b"
  apply (induct ns)
  apply simp
sorry

end

Initial question: irclog.perlgeek.de/isabelle/2015-12-23

(Note: My comment is longer than your post. I can delete this, and whether useful or not, I may delete it someday.)

A summary would be the following, where my claims are partly speculative, based on some knowledge and some experience:

• A single change can result in simp or auto following a very different line of simp rules. To answer any "why" would require following the simp trace, and there can be hundreds or thousands of rewrites in a simp trace.
• When using "magic proof tools", if you obtain a more complicated proof for lemma_1, than for lemma_2, it does not mean a simpler proof doesn't exist for lemma_1. It only means the magic tools didn't give you a simpler proof. Their magic is only so strong. To understand the "why", well, remember, this is supposed to be the summary.
• The strength of Sledgehammer is as a first-order-logic prover. It's good at matching up hypotheses and conclusions. One of its weakness is proving LHS = RHS, when the LHS and RHS are "hopelessly expanded".
• The \<forall> operator is a first-order-ish logic operator (polymorphic here, but also a standard op for 1st-order logic). I assume it lends itself to first-order provers, because definitions and theorems integrate it with the other first-order connectives, and sledgehammer somehow knows how to work well with all of that.
• The use of \<forall> means there's only one free variable, ns, to apply induction to. This keeps the formula simple enough for Sledgehammer to be successful.
• With two free variables, ns and a, if you don't also induct on a::nat, then Sledgehammer can't work its magic. But if you do induct on a (in a separate apply), you end up with a formula that's hopelessly expanded.
• The difference between \<And>, the meta-logic quantifier, and \<forall>, the object-logic quantifier, is the hardest part to explain, but only because \<And> is hard to explain.
• The \<forall> operator is "easy" in the sense that if you work hard enough, you can see that it and its properties are purely a result of how it is defined in HOL.thy, and how axioms are used to give it its properties.

Here's some source I messed around with.

fun sumTAux :: "nat list ⇒ nat ⇒ nat" where
  "sumTAux [] s = s" |
  "sumTAux (n#ns) s = sumTAux ns (n+s)"

lemma
  "sumTAux ns a = a + sumTAux ns 0"           (*[eq.1a]*)
proof-
  fix ns :: "nat list" and a :: nat
  have "∀a. sumTAux ns a = a + sumTAux ns 0"  (*[eq.1b]*)
    apply(induct ns, simp)
    by(metis add.assoc add.commute sumTAux.simps(2))
  thus "sumTAux ns a = a + sumTAux ns 0"
  by(blast)
qed

lemma
  "∀a. sumTAux ns a = a + sumTAux ns 0"       (*[eq.2]*)
apply(induct ns, simp)                        (*[apply.2a]*)(*
goal (1 subgoal):
 1. ⋀(a::nat) ns::nat list.
       ∀a::nat. sumTAux ns a = a + sumTAux ns (0::nat) 
       ==> ∀aa::nat. sumTAux (a # ns) aa = aa + sumTAux (a # ns) (0::nat)
*)
oops

lemma
  "sumTAux ns a = a + sumTAux ns 0"           (*[eq.3]*)
apply(induct ns, auto)                        (*[apply.3a]*)
apply(induct a, auto)                         (*[apply.3b]*)
(*sledgehammer. No magic like below.*)(*
goal (1 subgoal):
1. ⋀(a::nat) (aa::nat) ns::nat list.
     (⋀(aa::nat) ns::nat list. sumTAux ns a = a + sumTAux ns (0::nat) 
       ==> sumTAux ns (aa + a) = a + sumTAux ns aa) 
       ==> sumTAux ns (Suc a) = Suc (a + sumTAux ns (0::nat)) 
       ==> sumTAux ns (Suc (aa + a)) = Suc (a + sumTAux ns aa)
*)
oops

lemma
  "sumTAux ns a = a + sumTAux ns 0"           (*[eq.4]*)
apply(induct ns arbitrary: a, simp)           (*By suggestion of 3of8.*)
by(metis add.assoc add.commute sumTAux.simps(2))

Accept the gift of workarounds

The person with more knowledge showed up on IRC, so I'll bring this to a quicker end.

It's important to ask "why", but when you're working on your own stuff, rather than just doing exercises, you need the biggest toolbox possible to draw from.

My lesson from your question is what I do for the proof of [eq.1a].

I'm glad to know that binding a variable with \<forall> helped Sledgehammer out.

Recently, I replaced some complicated proofs with much simpler proofs, just by intelligently using a structured proof, with old-fashioned thinking, where I actually understood the proof steps I was implementing.

That's the basis of my comment in my summary. Magic tools can let us move very fast, but sometimes old-fashioned thinking is required.

Some specifics of \<forall>

Here, I make a short comment to support my comment that \<forall> is easier than \<And>.

Essentially, 3 meta-logic ops are these:

• ==, meta-equality, where it works like you expect, reflexive, symmetric, and transitive.
• ==>, meta-implication, where it works like you expect, and is used to define object logic operators and theorems. It is implication, but if I define --> with it, it's not a circular definition.
• \<And>, meta-universal-quantifier, the one without a one-liner explanation. One short answer is that it's related to schematic variables (produced after the proof), and free variables in a formula ,which are implicitly quantified with, guess what, yep, \<And>. In my experiments defining a full set of meta-logic connectives, I didn't get any help from Sledgehammer for the first few theorems using those connectives, which is far as I got. In general, variables should be left free, rather than explicitly quantifying them. And never quantified with \<forall> without a good reason, because you'll have to "unwrap" them in a step-by-step proof.

Anyway, that's just to give you the idea that in HOL.thy, \<forall> is the result of being defined with meta-logic operators.

Here is the signature at HOL.thy#l88:

All :: "('a => bool) => bool" (binder "ALL " 10)

Here is All_def, in with some other basics, HOL.thy#l187:

defs
  True_def:     "True      == ((%x::bool. x) = (%x. x))"
  All_def:      "All(P)    == (P = (%x. True))"
  Ex_def:       "Ex(P)     == !Q. (!x. P x --> Q) --> Q"
  False_def:    "False     == (!P. P)"
  not_def:      "~ P       == P-->False"
  and_def:      "P & Q     == !R. (P-->Q-->R) --> R"
  or_def:       "P | Q     == !R. (P-->R) --> (Q-->R) --> R"
  Ex1_def:      "Ex1(P)    == ? x. P(x) & (! y. P(y) --> y=x)"

Quantifiers are harder to completely figure out, because of all the binder notation.