[isabelle] How do I prove "¬ 2 ≤ 1" and use a simple lemma?

[Ching-Tsun Chou]

First, how do I prove a "¬ 2 ≤ 1"? Neither arith nor simp nor (simp add:
eval_nat_numeral) works.

Second, I have simple inductive definition and a lemma:

inductive le :: "nat ⇒ nat ⇒ bool" (infix "⊑" 50) where
le_n: "n ⊑ n" |
le_S: "n ⊑ m ⟹ n ⊑ (Suc m)"

lemma le_leq: "n ⊑ m ⟹ n ≤ m"
apply (induction rule: le.induct)
by (simp_all)

But then when I try to prove:

lemma "¬ 2 ⊑ 1"
proof (intro notI)
assume "2 ⊑ 1"
then have "2 ≤ 1" *by (rule le_leq)*

I get stuck. I can't figure out how to use the lemma le_leq above.
Isabelle complains:

Failed to apply initial proof method⌂:
using this:
2 ⊑ 1
goal (1 subgoal):
1. 2 ≤ 1

What does that mean?

Thanks!
- Ching Tsun

[Mark Wassell]

Hello,

Have you seen what sledgehammer comes up with in these situations?

I think proving "¬ 2 ≤ 1" as it is written is problematic as the strings
"2" and "1" mean a number of things. Move the mouse over 2 and 1 in the UI
to see what I mean.

Cheers

Mark

Post by Ching-Tsun Chou
eval_nat_numeral) works.
inductive le :: "nat ⇒ nat ⇒ bool" (infix "⊑" 50) where
le_n: "n ⊑ n" |
le_S: "n ⊑ m ⟹ n ⊑ (Suc m)"
lemma le_leq: "n ⊑ m ⟹ n ≤ m"
apply (induction rule: le.induct)
by (simp_all)
lemma "¬ 2 ⊑ 1"
proof (intro notI)
assume "2 ⊑ 1"
then have "2 ≤ 1" *by (rule le_leq)*
I get stuck. I can't figure out how to use the lemma le_leq above.
2 ⊑ 1
1. 2 ≤ 1
What does that mean?
Thanks!
- Ching Tsun

[Ching-Tsun Chou]

Aha! That is indeed the problem. Once I annotate change "1" to "1::nat",
everything works.

Thanks a lot!
- Ching Tsun

Post by Mark Wassell
Hello,
Have you seen what sledgehammer comes up with in these situations?
I think proving "¬ 2 ≤ 1" as it is written is problematic as the strings
"2" and "1" mean a number of things. Move the mouse over 2 and 1 in the UI
to see what I mean.
Cheers
Mark

Post by Ching-Tsun Chou
eval_nat_numeral) works.
inductive le :: "nat ⇒ nat ⇒ bool" (infix "⊑" 50) where
le_n: "n ⊑ n" |
le_S: "n ⊑ m ⟹ n ⊑ (Suc m)"
lemma le_leq: "n ⊑ m ⟹ n ≤ m"
apply (induction rule: le.induct)
by (simp_all)
lemma "¬ 2 ⊑ 1"
proof (intro notI)
assume "2 ⊑ 1"
then have "2 ≤ 1" *by (rule le_leq)*
I get stuck. I can't figure out how to use the lemma le_leq above.
2 ⊑ 1
1. 2 ≤ 1
What does that mean?
Thanks!
- Ching Tsun