Email Gateway (Aug 19 2022 at 16:18): Email Gateway (Aug 19 2022 at 16:18):From: Amarin Phaosawasdi <phaosaw2@illinois.edu>
Hello,
I have a series of short, related questions regarding reasoning with
even and odd numbers.
There are a lot of examples on the inductive definitions of even
numbers, such as the following from the book Concrete Semantics.
inductive ev :: "nat ⇒ bool" where
ev0: "ev 0" |
evSS: "ev n ⟹ ev (n + 2)"
Proving that 4 is even can be done like this.
lemmas four_is_even = evSS[OF evSS[OF ev0]]
lemma "ev (Suc(Suc(Suc(Suc 0))))"
by (rule four_is_even[simplified])
Q1: Is there anyway to simplify "evSS[OF evSS[OF ev0]]" on the fly such
that I don't need the lemma "four_is_even"?
Q2: I am not able to prove "ev 4". The closest that I got is this.
lemma "ev 4"
apply (subgoal_tac "ev (0 + 2 + 2)")
sorry
Simplification just yields "ev (Suc(Suc(Suc(Suc 0))))", not "ev 4".
How can I prove "ev 4"?
Q3: I also wanted to prove that "¬ev 1", so I tried modifying the
inductive definition as follows.
inductive ev :: "nat ⇒ bool" where
ev0: "ev 0" |
evS: "¬ev n ⟹ ev (n + 1)" |
evSS: "ev n ⟹ ev (n + 2)"
Isabelle told me that proof failed for the goal.
mono (λp x. x = 0 ∨ (∃n. x = n + 1 ∧ ¬ p n) ∨ (∃n. x = n + 2 ∧ p n))
What's going on? If I can't define ev this way, what's the best way to
prove "¬ev 1"
Maybe the questions weren't that short, sorry about that.
Any help on any of the questions are much appreciated.
Thank you,
Amarin
Email Gateway (Aug 19 2022 at 16:18):From: Tobias Nipkow <nipkow@in.tum.de>
On 15/10/2014 05:37, Amarin Phaosawasdi wrote:
Hello,
I have a series of short, related questions regarding reasoning with even and
odd numbers.There are a lot of examples on the inductive definitions of even numbers, such
as the following from the book Concrete Semantics.inductive ev :: "nat ⇒ bool" where
ev0: "ev 0" |
evSS: "ev n ⟹ ev (n + 2)"
For a start, note that a bit further down, in the section "In Isabelle", the
"+2" is replaced by "Suc(Suc". The "+2" version was just an intuitive starter.
Proving that 4 is even can be done like this.
lemmas four_is_even = evSS[OF evSS[OF ev0]]
lemma "ev (Suc(Suc(Suc(Suc 0))))"
by (rule four_is_even[simplified])Q1: Is there anyway to simplify "evSS[OF evSS[OF ev0]]" on the fly such that I
don't need the lemma "four_is_even"?
Yes, you can combine attributes with ",":
evSS[OF evSS[OF ev0], simplified]
Q2: I am not able to prove "ev 4". The closest that I got is this.
Numerals are distinct from Suc terms.
lemma "ev 4"
apply (subgoal_tac "ev (0 + 2 + 2)")
sorrySimplification just yields "ev (Suc(Suc(Suc(Suc 0))))", not "ev 4".
How can I prove "ev 4"?
One possibility:
lemma "ev 4"
using evSS[OF evSS[OF ev0]]
by(simp add: numeral_eq_Suc)
where numeral_eq_Suc expands numerals to Sc terms. There may also exist a set of
rules that performs the opposite conversion.
Q3: I also wanted to prove that "¬ev 1", so I tried modifying the inductive
definition as follows.inductive ev :: "nat ⇒ bool" where
ev0: "ev 0" |
evS: "¬ev n ⟹ ev (n + 1)" |
evSS: "ev n ⟹ ev (n + 2)"
Rule evS violates the format for inductive definitions (see 4.5.3).
Isabelle told me that proof failed for the goal.
mono (λp x. x = 0 ∨ (∃n. x = n + 1 ∧ ¬ p n) ∨ (∃n. x = n + 2 ∧ p n))What's going on? If I can't define ev this way, what's the best way to prove
"¬ev 1"
You have to rephrase it such that you can apply induction, eg
ev n ==> n ~= 1
Tobias
Maybe the questions weren't that short, sorry about that.
Any help on any of the questions are much appreciated.
Thank you,
Amarin
Email Gateway (Aug 19 2022 at 16:18):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
On 15/10/14 05:37, Amarin Phaosawasdi wrote:
Q1: Is there anyway to simplify "evSS[OF evSS[OF ev0]]" on the fly
such that I don't need the lemma "four_is_even"?
By ‘simplify’, you probably mean ‘derive automatically’. evSS[OF evSS[OF
ev0]] is basically a ‘hand-crafted proof’ where you put together the
existing lemmas by hand to derive a new lemma. Isabelle proof methods
like simp and auto basically do the same thing automatically in the
background.
You have correctly deduced that the problem here is that in order to
apply the introduction rules for ev (ev0 and evSS), the goal must be in
the shape ‘ev 0’ or ‘ev (n + 2)’. This is what your subgoal_tac achieves.
When the goal /is/ in that shape, you can simply apply the introduction
rules for ev to solve it:
apply (rule evSS)
apply (rule evSS)
apply (rule ev0)
Or shorter:
apply (rule evSS ev0)+
Or even shorter:
apply (intro evSS ev0)
Or this:
apply (intro ev.intros)
The entire proof:
lemma "ev 4"
proof-
have "(4::nat) = 0 + 2 + 2" by simp
also have "ev (0 + 2 + 2)" by (intro ev.intros)
finally show ?thesis .
qed
Now, as for the matter of getting from ‘4’ to ‘Suc (Suc (Suc (Suc 0)))’:
the representation of numeral constants (such as 4) in Isabelle is a bit
tricky for technical reasons. There is a collection of rewrite rules to
convert something like ‘4’ into its ‘Suc’ notation. It is called
eval_nat_numeral. If you write
lemma "ev 4"
apply (simp only: eval_nat_numeral)
you get the new goal "ev (Suc (Suc (Suc (Suc 0))))". You can usually
also use ‘simp add: eval_nat_numeral’, the ‘only’ just means that /only/
the given rules will be applied, which can be useful sometimes.
The problem is that evSS cannot be applied then, because they want the
form ‘ev (n + 2)’. Therefore, I would recommend to define the inductive
differently:
inductive ev :: "nat ⇒ bool" where
ev0: "ev 0" |
evSS: "ev n ⟹ ev (Suc (Suc n))"
Then you can simply prove even ‘ev 1000’ easily:
lemma "ev 1000"
by (auto simp: eval_nat_numeral intro!: ev.intros)
Alternatively, if you don't want to define the inductive differently,
you could just prove a derived introduction rule:
lemma evSS': "ev n ⟹ ev (Suc (Suc n))"
using evSS by simp
And then you can prove your lemmas with that.
On 15/10/14 05:37, Amarin Phaosawasdi wrote:
Isabelle told me that proof failed for the goal.
mono (λp x. x = 0 ∨ (∃n. x = n + 1 ∧ ¬ p n) ∨ (∃n. x = n + 2 ∧ p n))
As far as I know: inductive definitions require the properties to be
monotonic, i.e. among other things you can't have something like ‘¬ev n’
anywhere in it. This is not an inductive property anymore, you could
otherwise define something silly like ‘¬ev n ⟹ ev n’.
Regardless, you don't need this rule anyway. First of all, it is already
subsumed by the other rules and secondly, it does not help you at all in
proving ‘¬ev 1’. For that, ‘¬ev _’ would have to be on the right-hand
side of the implication.
The way to prove ‘¬ev 1’ is by case distinction: if ‘ev 1’ were to hold,
then either 1 = 0, which is obviously false, or 1 = Suc (Suc n), which
is also obviously false. The idea here is that ev is the ‘smallest’
predicate that fulfils the introduction rules given in its definition,
so if ‘ev n’ cannot be derived by ev0 and evSS, it is false.
A simple way to do this case distinction is by using the simplification
rules for ev, ev.simps:
lemma "¬ev 1"
by (subst ev.simps) auto
Using ev.simps with the ‘simp’ method is not a good idea because it will
probably cause the simplifier to loop.
For more complicated examples, you can prove the following (intuitively
obvious) lemma:
lemma ev_imp_not_ev_Suc: "ev n ⟹ ¬ev (Suc n)"
I will not give you the proof – it can be proven by induction over the
inductive definition of ‘ev’ and I think it makes a nice exercise. You
may also want to look up the ev.cases rule and the ‘inductive_cases’
command.
With that lemma, if you want to prove that something is not even, you
can just rewrite it to ‘Suc’ notation with ‘eval_nat_numeral’, apply
ev_imp_not_ev_Suc, and thus reduce the problem to proving that the
predecessor of the number is even – which you have already done.
As a side note: with the command ‘code_pred ev .’, you can generate
executable code for the predicate ‘ev’. Then you can check evenness with
‘value "ev 3"’ and even prove or disprove it by using the ‘eval’ method.
lemma "ev 4" by eval
lemma "¬ev 3" by eval
Note that, for technical reasons, a proof involving ‘eval’ is arguably
not as nice as a ‘normal’ proof.
Cheers,
Manuel
Q2: I am not able to prove "ev 4". The closest that I got is this.
lemma "ev 4"
apply (subgoal_tac "ev (0 + 2 + 2)")
sorrySimplification just yields "ev (Suc(Suc(Suc(Suc 0))))", not "ev 4".
How can I prove "ev 4"?
Q3: I also wanted to prove that "¬ev 1", so I tried modifying the
inductive definition as follows.inductive ev :: "nat ⇒ bool" where
ev0: "ev 0" |
evS: "¬ev n ⟹ ev (n + 1)" |
evSS: "ev n ⟹ ev (n + 2)"Isabelle told me that proof failed for the goal.
mono (λp x. x = 0 ∨ (∃n. x = n + 1 ∧ ¬ p n) ∨ (∃n. x = n + 2 ∧ p n))What's going on? If I can't define ev this way, what's the best way to
prove "¬ev 1"Maybe the questions weren't that short, sorry about that.
Any help on any of the questions are much appreciated.
Thank you,
Amarin
Email Gateway (Aug 19 2022 at 16:18):From: Lawrence Paulson <lp15@cam.ac.uk>
Other people have answered your questions in detail, but I just wanted to stress one point about inductive definitions. They give you rules for building up the elements of a set (equivalently, for constructing elements were a predicate is true), but the negative cases are implicit. Therefore, once you have defined the notion of even, you have also defined the notion of odd. And inductive references in the rules can only be positive. You should regard the rules as stating “0 is even”; “if N is even then so is N 2”; "there are no other even numbers”. A statement such as “if N is odd then N+1 is even” should be provable.
Larry Paulson
Email Gateway (Aug 19 2022 at 16:20):From: Amarin Phaosawasdi <phaosaw2@illinois.edu>
Thank you.
Is there a difference between using a proof vs adding it to simp like this?
lemma "ev 4"
by (simp add: numeral_eq_Suc evSS[OF evSS[OF ev0]])
Amarin
Email Gateway (Aug 19 2022 at 16:20):From: Amarin Phaosawasdi <phaosaw2@illinois.edu>
Ah, this makes things clearer, thank you.
Amarin
Email Gateway (Aug 19 2022 at 16:20):From: Amarin Phaosawasdi <phaosaw2@illinois.edu>
I definitely learned a lot here. Thanks.
Here's one way I did it.
lemma suc0:"¬ev (Suc 0)"
by (subst ev.simps, simp)
lemma sucSS:"⋀n. ev n ⟹ ¬ ev (Suc n) ⟹ ¬ ev (Suc (Suc (Suc n)))"
by (erule ev.cases) (subst ev.simps, simp)+
lemma "ev n ⟹ ¬ev (Suc n)"
by (induction rule: ev.induct) (simp add: suc0 sucSS)+
The other way, as you hinted, was adding the elimination rules so that
auto can use them.
inductive_cases evE[elim!]: "ev n"
lemma "ev n ⟹ ¬ev (Suc n)"
by (induction rule: ev.induct) auto
I'm a little curious though.
How did evE[elim!] help me with, for example, "¬ev (Suc 0)"?
As you can see above, without evE, I would prove it as follows.
lemma "¬ev (Suc 0)"
by (subst ev.simps, simp)
But with it, I can simply do.
lemma "¬ev (Suc 0)"
by auto
How would I prove "¬ev (Suc 0)" using evE (or ev.cases) explicitly the
way that auto is presumably using behind the scenes?
Amarin
Email Gateway (Aug 19 2022 at 16:20):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
The typical way of proving negations is by assuming the statement holds
and deriving False. You can do
this with the rule notI:
lemma "¬ev (Suc 0)"
apply (rule notI)
This leaves you with
goal (1 subgoal):
1. ev (Suc 0) ⟹ False
Now you can use evE to perform a case distinction on ‘ev (Suc 0)’: if
‘ev (Suc 0)’ holds, it was either derived by ev0 (in which case ‘Suc 0’
would have to be ‘0’) or it was derived by evSS (in which case ‘Suc 0’
would have to be ‘Suc (Suc n)’ for some n). Both are trivially false and
can be discharged by ‘simp_all’.
lemma "¬ev (Suc 0)"
apply (rule notI)
apply (erule evE)
apply simp_all
done
It should be mentioned that your evE is the same as the
automatically-proved ev.cases. inductive_cases is for deriving more
specialised elimination rules, i.e. ones where you don't have ‘ev n’,
but something more restricted, such as ‘ev 0’ or ‘ev (Suc n)’ or ‘ev
(Suc (Suc n))’. inductive_cases simply uses the ev.cases rule and
performs some simplification on it. In your case, you could do the
following:
inductive_cases evS: "ev (Suc n)"
Then, in the above proof of ‘¬ev (Suc 0)’, you applying the elimination
rule would leave you with the goal ‘Suc 0 = 0’. In this case, it doesn't
make much difference though – you might as well just use ev.cases.
Also, I would like to say that declaring rules as elimination rules
([elim]), especially safe ones ([elim!]) should be done with care. The
evE rule you defined is probably not a good choice for an automatic
elimination rule, since it doesn't always make the goal ‘simpler’ and
can be applied infinitely often, blowing the goal up indefinitely. In
these examples, it all works out, but in more complicated ones, auto
(and force, blast, etc.) might loop because of it, applying the rule
infinitely often.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 16:21):From: Tobias Nipkow <nipkow@in.tum.de>
On 19/10/2014 19:52, Amarin Phaosawasdi wrote:
One possibility:
lemma "ev 4"
using evSS[OF evSS[OF ev0]]
by(simp add: numeral_eq_Suc)Thank you.
Is there a difference between using a proof vs adding it to simp like this?
Yes, with "using" the fact becomes part of the proof state and is simplified itself.
Tobias
lemma "ev 4"
by (simp add: numeral_eq_Suc evSS[OF evSS[OF ev0]])Amarin
Last updated: Apr 19 2024 at 12:27 UTC