Yiming Xu (Dec 14 2024 at 12:02): Yiming Xu (Dec 14 2024 at 12:02):I have made a definition involving Inf and I got very confused. I am stating my confusion here and would like mature users to help identify what I missed about critical things to know for using Inf.
I defined:
inductive height_le ::
"'a ⇒ 'm set ⇒ ('m ⇒ 'a list ⇒ bool) ⇒ 'a ⇒ nat ⇒ bool"
for r :: 'a and Op :: "'m set" and R :: "('m ⇒ 'a list ⇒ bool)"
where
root : "height_le r Op R r 0"
| rel: "height_le r Op R w n ⟹ m ∈ Op ⟹ R m (w # vl) ⟹ v ∈ set vl
⟹ height_le r Op R v (n+1)"
definition height :: "'a ⇒ 'm set ⇒ ('m ⇒ 'a list ⇒ bool) ⇒ 'a ⇒ nat" where
"height r Op R w = Inf {n. height_le r Op R w n}"
It says R is a family of relations indexed by Op. Think about just one binary relation, then in this case if we fix an element r as a root element, then r has height 0, and for each of its immediate successor, i.e. R r w, we say "w's height is at most 1". The "at most" instead of "is" is because in the case we have a 1-path [r,w] and a 2-path [r,w0,w], then we can will count w twice, through w0 or not, then we have "w has height at most 1" and "w has height at most 2", and we will take "1" as the height of w, since it is the smallest.
I then proved:
lemma height_le_root:
"height_le r τ R w 0 ≡ w = r"
using height_le.simps
by (smt (verit, ccfv_threshold) add_is_0 zero_neq_one)
But I cannot prove
lemma height_root:
"height r τ R w = 0 ⟷ w = r"
unfolding height_def
I tried:
lemma height_root:
"height r τ R w = 0 ⟷ w = r"
unfolding height_def
proof (safe)
assume a: "(Inf (Collect (height_le r τ R w)) = 0)"
have "finite (Collect (height_le r τ R w))" sorry
then have "height_le r τ R w 0"
using a height_le_root Inf_nat_def Inf_nat_def1 sledgehammer
and sledgehammer fails here. May I please ask for possible reasons?
Yiming Xu (Dec 14 2024 at 12:16):Oops. I should not have the "sorry" since it is not necessarily true. But still I am surprised that sledgehammer fails.
Yiming Xu (Dec 14 2024 at 12:17):I think an inductive argument from left and right would work, trying...
Mathias Fleury (Dec 14 2024 at 12:21):Inf is very hard for sledgehammer because the inf is not guaranteed to be in the set (well here it is, but this is hard to figure out). This is where you as a human must add extra steps.
I managed something, but I had to add an extra condition:
inductive height_le ::
"'a ⇒ 'm set ⇒ ('m ⇒ 'a list ⇒ bool) ⇒ 'a ⇒ nat ⇒ bool"
for r :: 'a and Op :: "'m set" and R :: "('m ⇒ 'a list ⇒ bool)"
where
root[intro] : "height_le r Op R r 0"
| rel: "height_le r Op R w n ⟹ m ∈ Op ⟹ R m (w # vl) ⟹ v ∈ set vl
⟹ height_le r Op R v (n+1)"
definition height :: "'a ⇒ 'm set ⇒ ('m ⇒ 'a list ⇒ bool) ⇒ 'a ⇒ nat" where
"height r Op R w = Inf {n. height_le r Op R w n}"
lemma height_le_root:
"height_le r τ R w 0 ≡ w = r"
using height_le.simps
by (smt (verit, ccfv_threshold) add_is_0 zero_neq_one)
inductive_cases heightE: ‹height_le r τ R w 0›
lemma height_root:
assumes ‹height_le r τ R w n›
shows "height r τ R w = 0 ⟷ w = r"
proof -
have ‹w=r› if ‹Inf (Collect (height_le r τ R w)) = 0›
proof -
have ‹height_le r τ R w 0›
using that
wellorder_InfI[of n ‹Collect (height_le r τ R w)›, simplified] assms
unfolding height_def
by (auto simp del: )
then show ?thesis
using wellorder_InfI[of 0 ‹Collect (height_le r τ R w)›, simplified]
by (auto elim: heightE)
qed
then show ?thesis
using cInf_eq_minimum[of 0 ‹Collect (height_le r τ R w)›]
unfolding height_def
by (auto simp del: )
qed
So I think all we need would be nonemptyness.
Yiming Xu (Dec 14 2024 at 12:24):Once the set is nonempty, we can have Inf is in the set, is that true?
Yiming Xu (Dec 14 2024 at 12:24):Oh I can just find_theorems...
Mathias Fleury (Dec 14 2024 at 12:25):For natural numbers : yes
Mathias Fleury (Dec 14 2024 at 12:25):in general : no
Yiming Xu (Dec 14 2024 at 12:25):found 4 theorem(s):
Conditionally_Complete_Lattices.wellorder_InfI: ?k ∈ ?A ⟹ Inf ?A ∈ ?A
Conditionally_Complete_Lattices.Inf_nat_def1: ?K ≠ {} ⟹ Inf ?K ∈ ?K
Zorn.Inter_in_chain: finite ?ℬ ⟹ ?ℬ ≠ {} ⟹ subset.chain ?𝒜 ?ℬ ⟹ ⋂ ?ℬ ∈ ?ℬ
Finite_Set.complete_lattice_class.finite_Inf_in:
finite ?A ⟹ ?A ≠ {} ⟹ (⋀x y. x ∈ ?A ⟹ y ∈ ?A ⟹ inf x y ∈ ?A) ⟹ Inf ?A ∈ ?A
(like integers or stuff like {x \in Q. x > sqrt(2)})
Mathias Fleury (Dec 14 2024 at 12:26):Not every set has the wellorder property
Yiming Xu (Dec 14 2024 at 12:26):Ah yes. So infiniteness is a problem from that aspect.
Yiming Xu (Dec 14 2024 at 12:28):lemma height_height_le:
" height_le r τ R w m ⟹ height r τ R w = n ⟹ height_le r τ R w n"
unfolding height_def
by (metis generated_set_height_height_le height_def height_le_generated_set)
I see, the problem is truly about nonemptyness. With the nonemptiness sledgehammer is fast enough.
Yiming Xu (Dec 14 2024 at 12:29):(does not even ask me to do an induction.)
Yiming Xu (Dec 14 2024 at 12:29):Thanks! That is good to know.
Last updated: Dec 21 2024 at 16:20 UTC