new example: f(f(n))<f(n+1)

parent 5b15206e
(* Let f be a function over natural numbers such that, for all n
f(f(n)) < f(n)+1
Show that f(n)=n for all n. *)
theory Puzzle
use import int.Int
function f int: int
axiom H1: forall n: int. 0 <= n -> 0 <= f n
axiom H2: forall n: int. 0 <= n -> f (f n) < f (n+1)
(* k <= f(n+k) by induction over k *)
predicate p (k: int) = forall n: int. 0 <= n -> k <= f(n+k)
clone int.SimpleInduction as I1
with predicate p = p, lemma base, lemma induction_step
lemma L3: forall n: int. 0 <= n -> n <= f n
lemma L4: forall n: int. 0 <= n -> f n < f (n+1)
(* so f is increasing, that is *)
predicate p' (k: int) = forall n m: int. 0 <= n <= m <= k -> f n <= f m
clone int.SimpleInduction as I2
with predicate p = p', lemma base, lemma induction_step
lemma L4cor: forall n m: int. 0 <= n <= m -> f n <= f m
lemma L5: forall n: int. 0 <= n -> f n < n+1
goal G: forall n: int. 0 <= n -> f n = n
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="Alt-Ergo"
version="0.95"/>
<prover
id="2"
name="Spass"
version="3.7"/>
<prover
id="3"
name="Z3"
version="3.2"/>
<file
name="../f_puzzle.why"
verified="true"
expanded="true">
<theory
name="Puzzle"
locfile="../f_puzzle.why"
loclnum="6" loccnumb="7" loccnume="13"
verified="true"
expanded="true">
<goal
name="base"
locfile="../../share/theories/int.why"
loclnum="421" loccnumb="8" loccnume="12"
sum="ed78c9fb65e77c70c6620657d70585f3"
proved="true"
expanded="true"
shape="apc0">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="induction_step"
locfile="../../share/theories/int.why"
loclnum="423" loccnumb="8" loccnume="22"
sum="245c3be7001b98c7db290e437e6be588"
proved="true"
expanded="true"
shape="apainfix +V0c1IapV0Iainfix &lt;=c0V0F">
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal
name="L3"
locfile="../f_puzzle.why"
loclnum="20" loccnumb="8" loccnume="10"
sum="58bd5c2b0f5c1d9c12651652ffebfd10"
proved="true"
expanded="true"
shape="ainfix &lt;=V0afV0Iainfix &lt;=c0V0F">
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal
name="L4"
locfile="../f_puzzle.why"
loclnum="22" loccnumb="8" loccnume="10"
sum="c4aa04ae9120b08b2384cbfebd9f02bd"
proved="true"
expanded="true"
shape="ainfix &lt;afV0afainfix +V0c1Iainfix &lt;=c0V0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="base"
locfile="../../share/theories/int.why"
loclnum="421" loccnumb="8" loccnume="12"
sum="dcdb5e521974a78d89381bcd99c2076a"
proved="true"
expanded="true"
shape="ap&apos;c0">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="induction_step"
locfile="../../share/theories/int.why"
loclnum="423" loccnumb="8" loccnume="22"
sum="2f88f4598c42a29ff1753666b723745e"
proved="true"
expanded="true"
shape="ap&apos;ainfix +V0c1Iap&apos;V0Iainfix &lt;=c0V0F">
<proof
prover="1"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
</proof>
</goal>
<goal
name="L4cor"
locfile="../f_puzzle.why"
loclnum="28" loccnumb="8" loccnume="13"
sum="1e8c64e74d3ab2a23f4359575310b094"
proved="true"
expanded="true"
shape="ainfix &lt;=afV0afV1Iainfix &lt;=V0V1Aainfix &lt;=c0V0F">
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="L5"
locfile="../f_puzzle.why"
loclnum="30" loccnumb="8" loccnume="10"
sum="77670682cc8babaa2a551be587eb4fb8"
proved="true"
expanded="true"
shape="ainfix &lt;afV0ainfix +V0c1Iainfix &lt;=c0V0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="G"
locfile="../f_puzzle.why"
loclnum="32" loccnumb="7" loccnume="8"
sum="74e23d8234ec2dc48c6b0e54f7801f2f"
proved="true"
expanded="true"
shape="ainfix =afV0V0Iainfix &lt;=c0V0F">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
</file>
</why3session>
......@@ -412,6 +412,20 @@ integers greater or equal a given bound.
*)
theory SimpleInduction
use import Int
predicate p int
axiom base: p 0
axiom induction_step: forall n:int. 0 <= n -> p n -> p (n+1)
lemma SimpleInduction : forall n:int. 0 <= n -> p n
end
theory Induction
use import Int
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment