*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Infinitely recursive lambda expression or not?*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Wed, 18 Dec 2013 16:55:03 -0600*In-reply-to*: <op.w723lrn9ule2fv@cardamome>*References*: <op.w72usxweule2fv@cardamome> <C743CBFE-029F-4E49-9A56-3695338394B8@cantab.net> <52AC4D87.9030304@gmx.com> <op.w723lrn9ule2fv@cardamome>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 12/14/2013 7:26 AM, Yannick Duchêne (Hibou57) wrote:

I wanted to check if had an issue with binding (indeed, I did hadissues with implicit operations in some cases), so tried this:lemma "f = (λa. False ∨ f False) ⟹ (f False = False)"It still says it find a counter example, with “f False = True”.Precisely, what I don't understand, is why it suppose this may beTrue. “a” is not used, and the only constant used in f is False.I must be missing something important, or else it's just AutoQuickcheck which is not made for this kind of infinite expression.

Regards, GB (******************************************************************************) theory i131216a__isaU_eq_is_not_assignment imports Complex_Main (*"../../../iHelp/i"*) begin (*SHOWING THAT "=" IS HOL.eq, RATHER THAN PROGRAMMING LANGUAGE ASSIGNMENT*) (*

has been axiomatized to have certain properties, such as substitution.

pertinent theorem is this: *) theorem "(f = g) <-> (!x. f x = g x)" by(rule fun_eq_iff) (*

Also, this shows that there's no recursion, unless for a particular f, f has

named fix_f: *) function fix_f :: "bool => bool" where "fix_f a = (%x. x | fix_f x) a" by(auto) (*

on it.

if HOL implements a short-circuited or, it would simplify to "True". You might think that "(fix_f False)" should be an infinite loop, because

hasn't been proved.

and isar-ref.pdf. *) function fix_g :: "bool => bool" where "fix_g a = (%x. x | fix_g x) a" by pat_completeness auto termination by lexicographic_order

order.*) fun fix_h :: "bool => bool" where "fix_h a = (%x. x | fix_h x) a" (*ERROR: Same error as for "function".*) primrec fix_i :: "bool => bool" where "fix_i a = (%x. x | fix_i x) a" (*ERROR: primrec only defines functions that use datatype.*) (*********************************************************************) (*SHOWING THAT RECURSIVE FUNCTIONS DON'T GET "COMPUTED" AUTOMATICALLY*) (*********************************************************************) fun sumXp :: "nat => nat" where "sumXp 0 = 0" |"sumXp n = n + sumXp(n - 1)" find_theorems "sumXp" thm sumXp.simps (* Prints the simp rules created for sumXp: sumXp.simps(1), sumXp.simps(2) *) value "sumXp 4" (* The code generator prints the successor form of 10. Doing an import of "~~/src/HOL/Library/Code_Target_Nat" will print 10, but the fact that the successor form is being used is needed information here. *) theorem "sumXp 4 = 10" apply(simp) oops (* But simp here doesn't do any magic computation, even though sumXp.simps(1) and sumXp.simps(2) are automatically declared as simp rules. *) theorem "(!!f::(nat => nat). !!a. f = (%x. f x) ==> f a = a) ==> False" by(auto) (* EXAMPLE: This example, similar to yours, will be made concrete with sumXp. *) theorem "sumXp = (%x. sumXp x)" by(rule eta_contract_eq) (* Checking that the left-hand side will be true. *) theorem "sumXp = (%x. sumXp x) ==> sumXp 4 = 10" using[[simp_trace]] apply(simp) oops (* After simp is applied, the goal is "sumXp 4 = 10". The RHS hasn't been simplified any at all. Computations like this are a result of simp rule substitutions (rewriting), and simp rules are picky. *) theorem "sumXp = (%x. sumXp x) ==> sumXp (Suc (Suc (Suc (Suc 0)))) = (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))" (* Happy simp rules make for happy computations... *) using[[simp_trace]] by(simp) (* ...by means of rewriting. With the right form of natural numbers, the simp

the rewriting of which can be seen at the end of the simp trace. *) (*declare[[simp_trace]]*) value "sumXp 4" (*

using to compute `value "sumXp 4"`.

It's also using a lot of other rewrite rules. *) term "nat_of_num" theorem "sumXp 4 = 10" apply(simp add: nat_of_num.simps) oops (* The message is that nat_of_num.simps are duplicate rewrite rules. It will be easier just to ask what needs to be done to be able to prove a theorem which uses an expression like "sumXp 4 = 10". *) (******************************************************************************) end

theory i131216a__isaU_eq_is_not_assignment imports Complex_Main (*"../../../iHelp/i"*) begin (*SHOWING THAT "=" IS HOL.eq, RATHER THAN PROGRAMMING LANGUAGE ASSIGNMENT*) (* You're treating "=" as if it's assignment or definition, such as "val x = 1", but it's not, it's the application of the function HOL.eq::('a => 'a => bool), which has been axiomatized to have certain properties, such as substitution. The expression "f = (%a. a | f a)" is a statement of function equality, and the pertinent theorem is this: *) theorem "(f = g) <-> (!x. f x = g x)" by(rule fun_eq_iff) (* To prove your theorem wrong, I only need one function of type (bool => bool), and I choose (%x. True), with the result that "(%x. True) = (%a. a | (%x. True) a)" is True by fun_eq_iff. There are only two values, True and False, that need to be tested to determine whether (%x. True) is equal to (%a. a | (%x. True) a). Also, this shows that there's no recursion, unless for a particular f, f has been defined to be recursive. Here, it appears I've defined a recursive function named fix_f: *) function fix_f :: "bool => bool" where "fix_f a = (%x. x | fix_f x) a" by(auto) (* Of note is that the "=" used is still HOL.eq, which can be seen by cntl-clicking on it. You might think that "(fix_f True)" should return "(True | fix_f True)", where if HOL implements a short-circuited or, it would simplify to "True". You might think that "(fix_f False)" should be an infinite loop, because the first iteration will return "(False | fix_f False)", and so on, to infinity. You can try to use fix_f in theorems, but it's not usable because termination hasn't been proved. Your options for defining recursive functions are function, fun, and primrec, none of which will work for fix_f. The applicable documents are functions.pdf and isar-ref.pdf. *) function fix_g :: "bool => bool" where "fix_g a = (%x. x | fix_g x) a" by pat_completeness auto termination by lexicographic_order (*ERROR: Unfinished goal "1. False". Could not find lexicographic termination order.*) fun fix_h :: "bool => bool" where "fix_h a = (%x. x | fix_h x) a" (*ERROR: Same error as for "function".*) primrec fix_i :: "bool => bool" where "fix_i a = (%x. x | fix_i x) a" (*ERROR: primrec only defines functions that use datatype.*) (*********************************************************************) (*SHOWING THAT RECURSIVE FUNCTIONS DON'T GET "COMPUTED" AUTOMATICALLY*) (*********************************************************************) fun sumXp :: "nat => nat" where "sumXp 0 = 0" |"sumXp n = n + sumXp(n - 1)" find_theorems "sumXp" thm sumXp.simps (* Prints the simp rules created for sumXp: sumXp.simps(1), sumXp.simps(2) *) value "sumXp 4" (* The code generator prints the successor form of 10. Doing an import of "~~/src/HOL/Library/Code_Target_Nat" will print 10, but the fact that the successor form is being used is needed information here. *) theorem "sumXp 4 = 10" apply(simp) oops (* But simp here doesn't do any magic computation, even though sumXp.simps(1) and sumXp.simps(2) are automatically declared as simp rules. *) theorem "(!!f::(nat => nat). !!a. f = (%x. f x) ==> f a = a) ==> False" by(auto) (* EXAMPLE: This example, similar to yours, will be made concrete with sumXp. *) theorem "sumXp = (%x. sumXp x)" by(rule eta_contract_eq) (* Checking that the left-hand side will be true. *) theorem "sumXp = (%x. sumXp x) ==> sumXp 4 = 10" using[[simp_trace]] apply(simp) oops (* After simp is applied, the goal is "sumXp 4 = 10". The RHS hasn't been simplified any at all. Computations like this are a result of simp rule substitutions (rewriting), and simp rules are picky. *) theorem "sumXp = (%x. sumXp x) ==> sumXp (Suc (Suc (Suc (Suc 0)))) = (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))" (* Happy simp rules make for happy computations... *) using[[simp_trace]] by(simp) (* ...by means of rewriting. With the right form of natural numbers, the simp rules can compute what is needed to obtain the necessary "HOL.eq a b == True", the rewriting of which can be seen at the end of the simp trace. *) (*declare[[simp_trace]]*) value "sumXp 4" (* Going back, I'd like to see if simp_trace can tell me what simp rule "value" is using to compute `value "sumXp 4"`. It's using the function Num.nat_of_num, which cntl-clicking will take you to. It's also using a lot of other rewrite rules. *) term "nat_of_num" theorem "sumXp 4 = 10" apply(simp add: nat_of_num.simps) oops (* The message is that nat_of_num.simps are duplicate rewrite rules. It will be easier just to ask what needs to be done to be able to prove a theorem which uses an expression like "sumXp 4 = 10". *) (******************************************************************************) end

**Follow-Ups**:**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Gottfried Barrow

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

**References**:**[isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*John Wickerson

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Gottfried Barrow

**Re: [isabelle] Infinitely recursive lambda expression or not?***From:*Yannick Duchêne (Hibou57)

- Previous by Date: Re: [isabelle] "(!!P. P::bool) ==> PROP P" with auto methods hangs PIDE
- Next by Date: [isabelle] Instantiating type classes
- Previous by Thread: Re: [isabelle] Infinitely recursive lambda expression or not?
- Next by Thread: Re: [isabelle] Infinitely recursive lambda expression or not?
- Cl-isabelle-users December 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list