Email Gateway (Aug 22 2022 at 09:25): Email Gateway (Aug 22 2022 at 09:25):From: "W. Douglas Maurer" <maurer@gwu.edu>
As a first example of explaining to my students what a subproof is,
without complicating the matter by doing one with cases or with
induction, I prepared the following (contrived) proof that 6 is the
factorial of 3:
lemma "fact(3::nat) = 6" proof-
have "(3::nat) = (2::nat)+1" by simp
then have "fact(3::nat) = fact((2::nat)+1)" by (rule arg_cong)
also have 1: "... = ((2::nat)+1)*fact(2) by (rule fact_plus_one_nat)
have "fact(2::nat) = 2" proof-
have "(2::nat) = 1+(1::nat)" by simp
then have "fact(2::nat)=fact(1+(1::nat))" by (rule arg_cong)
also have "... = (1+1)*fact(1)" by (rule fact_plus_one_nat)
finally show ?thesis by simp
qed
with 1 have "fact(3::nat) = ((2::nat)+1)*2" by simp
then show ?thesis by simp
qed
This works, but it's ugly. I would much rather have a proof that
somehow proceeds automatically from fact(3) = 6 to fact(Suc 2) = 6 to
(Suc 2)fact(2) = 6 to (Suc 2)fact(Suc 1) = 6 to (Suc 2)*(Suc
1)fact(1) = 6 to (Suc 2)(Suc 1)fact(Suc 0) = 6 to (Suc 2)(Suc
1)(Suc 0)fact(0) = 6 to 321*1 = 6, all in one step. As a first
try, after a few iterations, I wrote:
theory FactDef imports Main Fact begin
lemma "fact(3::nat) = 6" by (auto simp add: fact_nat_def)
end
which didn't work (I didn't necessarily expect it to), but the
message I got was:
Failed to finish proof: goal (1 subgoal): 1. fact_nat_sumC 3 = 6
So my question now is: What is this sumC? I searched for it in
"Isabelle/HOL --- Higher-Order Logic" and in the Isabelle/Isar
Reference Manual, and it wasn't in either place. -Douglas
Email Gateway (Aug 22 2022 at 09:25):From: Lars Hupel <hupel@in.tum.de>
Hello,
This works, but it's ugly. I would much rather have a proof that somehow
proceeds automatically from fact(3) = 6 to fact(Suc 2) = 6 to (Suc
2)fact(2) = 6 to (Suc 2)fact(Suc 1) = 6 to (Suc 2)(Suc 1)fact(1) = 6
to (Suc 2)(Suc 1)fact(Suc 0) = 6 to (Suc 2)(Suc 1)(Suc 0)*fact(0) =
6 to 321*1 = 6, all in one step.
I'm not sure I fully understand the requirement. Are you looking for a
proof method which can solve the full goal automatically? If so, you can
try 'code_simp' or 'eval'.
Perhaps a better way to understand what's going on internally is to
first convert the numeral notation to 'Suc ... 0' notation of natural
numbers:
lemma "fact 3 = 6"
unfolding eval_nat_numeral BitM.simps
At this point, the subgoal looks like this:
fact (Suc (Suc (Suc 0))) = Suc (Suc (Suc (Suc (Suc (Suc 0)))))
This goal can be solved 'by simp'. Of course, you can also add that rule
to the simpset:
lemma "fact 3 = 6"
by (simp add: eval_nat_numeral)
Does that help?
As a first try, after a few
iterations, I wrote:
theory FactDef imports Main Fact begin
lemma "fact(3::nat) = 6" by (auto simp add: fact_nat_def)
end
which didn't work (I didn't necessarily expect it to), but the message I
got was:
Failed to finish proof: goal (1 subgoal): 1. fact_nat_sumC 3 = 6
So my question now is: What is this sumC?
It's an internal definition of the function command. See here for an
older discussion:
<http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/10667>.
Cheers
Lars
Email Gateway (Aug 22 2022 at 09:26):From: "W. Douglas Maurer" <maurer@gwu.edu>
Where is code_simp described? It's not in "Programming and Proving in
Isabelle/HOL"; it's not in "The Isabelle/Isar Reference Manual"; it's
not in "The Isabelle/Isar Implementation"; it's not in "Isabelle/HOL
-- A Proof Assistant for Higher-Order Logic." Are there other manuals
or tutorials I should try?
Email Gateway (Aug 22 2022 at 09:26):From: Lars Hupel <hupel@in.tum.de>
Can you give the definition of your 'fact' function? I was assuming
something along those lines:
fun fact :: "nat => nat" where
"fact 0 = 1" |
"fact (Suc n) = (Suc n) * fact n"
Email Gateway (Aug 22 2022 at 09:26):From: Lars Hupel <hupel@in.tum.de>
Both 'eval' and 'code_simp' use the code generator, which is why they're
described in the code generator manual, section 6.
Cheers
Lars
Email Gateway (Aug 22 2022 at 09:29):From: Lars Hupel <hupel@in.tum.de>
I searched the code generation manual for code-simp and eval. Code-simp
appears in only one place in that manual, and it's in the Schematic
Diagram (section 6.3), which hardly qualifies as a description.
It's slightly more detailed in §6.1.
Having said this, though, it doesn't look as if I'll be able to use
these, anyway. The Abstract to the code generation manual says that "the
code generator facilities of Isabelle/HOL...empower the user to turn HOL
specifications into corresponding executable programs in the languages
SML, OCaml, Haskell and Scala." I'm based in the US, and my only
exposure to functional languages has been to Lisp. (Maybe that's
chauvinistic, since Lisp was developed in the US.) I've been studying
Paulson's ML book, but I haven't actually used ML yet.
The 'code_simp' and 'eval' methods are using code generator
infrastructure, but are not actually generating code (at least not
observably). They are completely embedded in Isabelle and have nothing
to do with any of the targets the code generator supports.
Cheers
Lars
Email Gateway (Aug 22 2022 at 09:29):From: Lars Hupel <hupel@in.tum.de>
After digging a bit, it turns out that the Fact theory is part of HOL in
Isabelle2014, but not anymore in Isabelle2015-RC*.
I couldn't reproduce the tactic failure, though. 'simp add:
eval_nat_numeral' solves the goal just fine.
Cheers
Lars
Email Gateway (Aug 22 2022 at 09:30):From: Larry Paulson <lp15@cam.ac.uk>
The theory Fact was combined with Binomial and is now included in Complex_Main. The integer version of the factorial function no longer exists. See NEWS:
The factorial function, "fact", now has type "nat = 'a" (of sort semiring_char_0, which admits numeric types including nat, int, real and complex. INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type constraint, and the combination "real (fact k)" is likely to be unsatisfactory. If a type conversion is still necessary, then use "of_nat (fact k)" or "real_of_nat (fact k)”.
Larry Paulson
Last updated: Apr 20 2024 at 08:16 UTC