Re: [isabelle] reasoning with even and odd numbers



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)")
> 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
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.