Email Gateway (Aug 18 2022 at 20:17): Email Gateway (Aug 18 2022 at 20:17):From: Henri DEBRAT <Henri.Debrat@loria.fr>
Hi all,
I am trying to define a randomized algorithm in order to prove it is correct. On this purpose, I defined following objects:
"bernoulli p ≡ point_measure (UNIV :: bool set) (% True => p | False => 1 - p)"
interpretation rs:product_prob_space "(λi. bernoulli p)" "UNIV::(nat × Proc) set" for p
proof (unfold_locales, auto)
have "(UNIV :: bool set) = { True, False }" by auto
thus "emeasure (bernoulli p) (space (bernoulli p)) = ∞ ⟹ False"
using emeasure_point_measure_finite finite_UNIV
proof (unfold bernoulli_def, blast) qed
...
Proof goes fine (just ends with "no subgoals") but at "qed" I obtain the following error:
Pending sort hypotheses:
{finite,perfect_space,real_normed_vector}
Does anyone have any idea on how to solve this issue ?
Thanks in advance,
Henri.
Email Gateway (Aug 18 2022 at 20:29):From: Henri DEBRAT <Henri.Debrat@loria.fr>
Thanks a lot for your help, Makarius.
Unfolding the definition...Hum, I feel a little silly here...
Your solution works...partially. That is, it solves the sort_contraint goal. However, when closing the proof block, here is the error I get :
exception TERM raised (line 137 of "more_thm.ML"):
dest_equals
SORT_CONSTRAINT(?'a∷{finite,perfect_space,real_normed_vector})
any idea ?
H.
Email Gateway (Aug 18 2022 at 20:30):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Donnerstag, den 28.06.2012, 12:40 +0200 schrieb Henri DEBRAT:
Hi all,
I am trying to define a randomized algorithm in order to prove it is correct. On this purpose, I defined following objects:
"bernoulli p ≡ point_measure (UNIV :: bool set) (% True => p | False => 1 - p)"
interpretation rs:product_prob_space "(λi. bernoulli p)" "UNIV::(nat × Proc) set" for p
proof (unfold_locales, auto)
have "(UNIV :: bool set) = { True, False }" by auto
thus "emeasure (bernoulli p) (space (bernoulli p)) = ∞ ⟹ False"
using emeasure_point_measure_finite finite_UNIV
proof (unfold bernoulli_def, blast) qed
...Proof goes fine (just ends with "no subgoals") but at "qed" I obtain the following error:
Pending sort hypotheses:
{finite,perfect_space,real_normed_vector}
Huh, where does this come from? There should be no additional sort
constraint.
Does anyone have any idea on how to solve this issue ?
The interpretation as you try it will unfortunately not work. You need
to clamp the probability p between 0 and 1:
definition clamp :: "real ⇒ real" where "clamp p = min 0 (max 1 p)"
definition
"bernoulli p ≡ point_measure (UNIV :: bool set) (% True => ereal (clamp p) | False => 1 - ereal (clamp p))"
Important note: If p is a real the following proofs are much simpler!
The next is: For product_prob_space you just need to show that
"bernoulli p" is a probabilty space. This does work directly with
unfold_locales, but with prob_spaceI which is a default rule. This is a
little ugly but saves a couple of sublocales in the probability theory.
interpretation rs: product_prob_space "(λi. bernoulli p)" "UNIV::(nat × nat) set" for p :: real
proof -
have "emeasure (bernoulli p) (space (bernoulli p)) =
(∑i∈UNIV. case i of True => clamp p | False => 1 - clamp p)"
by (simp add: bernoulli_def space_point_measure emeasure_point_measure_finite
clamp_def max_def min_def split: bool.split)
also have "… = 1"
by (simp add: UNIV_bool one_ereal_def)
finally interpret prob_space "bernoulli p"
by rule -- {* Here prob_spaceI is applied *}
show "product_prob_space (λi. bernoulli p)"
.. -- {* This is also unfold_locales, but this time the interpret from above is used *}
qed
Maybe even better is:
interpretation bernoulli: "bernoulli p" for p :: real
proof -
have "emeasure (bernoulli p) (space (bernoulli p)) =
(∑i∈UNIV. case i of True => clamp p | False => 1 - clamp p)"
by (simp add: bernoulli_def space_point_measure emeasure_point_measure_finite
clamp_def max_def min_def split: bool.split)
also have "… = 1"
by (simp add: UNIV_bool one_ereal_def)
finally show "prob_space (bernoulli p)"
by rule -- {* Here prob_spaceI is applied *}
qed
interpretation rs: product_prob_space "(λi. bernoulli p)" "UNIV::(nat × nat) set" for p :: real ..
Thanks in advance,
Henri.
Email Gateway (Aug 19 2022 at 07:50):From: Henri DEBRAT <Henri.Debrat@loria.fr>
Thanks a lot, Johannes. The code you provide me with does work, thanks a lot.
You are right, I had some axiomatic constraints on p so that it is in ] 0 ; 1[ I just forgot to say it.
Yet, some great mystery lies here concerning sort_constraint and the exception it raises.
In case it might be an interesting issue to solve, I copy here two piece of code.
They look pretty similar, however, the first goes fine while the second raise the famous sort_constraint error.
typedecl Proc
arities Proc :: finite
axiomatization
bp::real
where
bpdef:"bp > 0 ∧ bp < 1"
definition
"bernoulli ≡ point_measure (UNIV :: bool set) (% True => ereal bp | False => 1 - ereal bp)"
**** CODE WHICH FAILS AT THE LAST "QED" (sort_constraint error):
interpretation rs:product_prob_space "(λi::nat × Proc. bernoulli)" "UNIV::(nat × Proc) set"
where "SORT_CONSTRAINT('a::{finite,perfect_space,real_normed_vector} )"
proof(unfold_locales, auto)
have "UNIV = { True, False }" by auto
thus "emeasure bernoulli (space bernoulli) = 1"
using space_point_measure finite_UNIV
by (blast dest:emeasure_point_measure_finite)
next
have "UNIV = { True, False }" by auto
thus "emeasure bernoulli (space bernoulli) = ∞ ⟹ False"
using finite_UNIV space_point_measure
by (blast dest:emeasure_point_measure_finite)
next
have "UNIV = { True, False }" by auto
moreover
obtain A where "A = (λi::nat. if i = 0 then space bernoulli else {})" by auto
hence "range A ⊆ sets bernoulli" and "(⋃x::nat. A x) = space bernoulli"
by auto
ultimately
show "∃A. range A ⊆ sets bernoulli ∧ (⋃x::nat. A x)
= space bernoulli ∧ (∀i. emeasure bernoulli (A i) ≠ ∞)"
using finite_UNIV
by (blast dest:emeasure_point_measure_finite)
qed
*** CODE WHICH ENDS FINE (thanks to Johannes) :
interpretation rs:product_prob_space "(λi. bernoulli)" "UNIV::(nat × Proc) set"
proof(unfold_locales, auto)
from bpdef show "emeasure bernoulli (space bernoulli) = 1"
by (auto simp: UNIV_bool one_ereal_def bernoulli_def
space_point_measure emeasure_point_measure_finite split: bool.split)
next
from bpdef show "emeasure bernoulli (space bernoulli) = ∞ ⟹ False"
by (auto simp: UNIV_bool one_ereal_def bernoulli_def
space_point_measure emeasure_point_measure_finite split: bool.split)
next
obtain A where Adef:"A = (λi::nat. if i = 0 then space bernoulli else {})" by auto
hence "range A ⊆ sets bernoulli" and "(⋃x::nat. A x) = space bernoulli"
by auto
moreover
from Adef bpdef have "∀i. emeasure bernoulli (A i) ≠ ∞"
by(auto simp: UNIV_bool one_ereal_def bernoulli_def
space_point_measure emeasure_point_measure_finite split: bool.split)
ultimately
show "∃A. range A ⊆ sets bernoulli ∧ (⋃x::nat. A x)
= space bernoulli ∧ (∀i. emeasure bernoulli (A i) ≠ ∞)"
by auto
qed
I hope this might be useful.
H.
Email Gateway (Aug 19 2022 at 07:51):From: Henri DEBRAT <Henri.Debrat@loria.fr>
Oh, I forgot to say that if i start the first proof with "proof (unfold_locales, auto simp:sort_constraint_def)", as suggested by Makarius, the exception still raises :
exception TERM raised (line 137 of "more_thm.ML"):
dest_equals
SORT_CONSTRAINT
(?'a∷{finite,perfect_space,real_normed_vector})
H.
Email Gateway (Aug 19 2022 at 07:56):From: Lars Noschinski <noschinl@in.tum.de>
On 03.07.2012 18:53, Henri DEBRAT wrote:
Yet, some great mystery lies here concerning sort_constraint and the exception it raises.
In case it might be an interesting issue to solve, I copy here two piece of code.
The first proof does not go through for me (Isabelle 2012) -- the proof
of obtains in the 3rd block fails and there is some remaining goal.
definition
"bernoulli ≡ point_measure (UNIV :: bool set) (% True => ereal bp | False => 1 - ereal bp)"
[...]
interpretation rs:product_prob_space "(λi::nat × Proc. bernoulli)" "UNIV::(nat × Proc) set"
where "SORT_CONSTRAINT('a::{finite,perfect_space,real_normed_vector} )"
proof(unfold_locales, auto)
have "UNIV = { True, False }" by auto
thus "emeasure bernoulli (space bernoulli) = 1"
using space_point_measure finite_UNIV
by (blast dest:emeasure_point_measure_finite)
This looks already a bit suspicious -- you proof something about
bernoulli without ever using its definition (definitions are not
unfolded automatically). Indeed it turns out, that you can prove False here:
interpretation rs:product_prob_space "(λi::nat × Proc. bernoulli)"
"UNIV::(nat × Proc) set"
where "SORT_CONSTRAINT('a::{finite,perfect_space,real_normed_vector} )"
proof(unfold_locales, auto)
have A: "UNIV = { True, False }" by auto
then have False using finite_UNIV
by (blast dest:emeasure_point_measure_finite)
This means, you assumptions are inconsistent. The SORT_CONSTRAINT you
gave adds the assumption, that there exists a type, which is finite, a
perfect_space, and a real_normed_vector. I guess such a type does not
exist -- maybe somebody more familiar with this field can confirm this?
These sort constraints are necessary to keep the system consistent, when
type variables vanish from a term: If you have a type class c with
inconsistent assumptions, then you can easily derive False from it. But
the term False does not contain references to c anymore. Hence, Isabelle
attaches the additional sort constraint "c" to this theorem. This
basically encodes "If the type class c is not empty, then this theorem
holds". If there is already an instance of this class, the additional
sort constraint is automatically discharged.
So, in your case, somehow blast is able to find a proof which basically
runs into above situation -- i.e., it is not really a proof.
-- Lars
Email Gateway (Aug 19 2022 at 07:57):From: Johannes Hölzl <hoelzl@in.tum.de>
real_normed_vector includes open_dist, which together with finite
forces it to be a discrete topology, i.e. "!!x. open {x}".
The opposite of a perfect space "!!x. ~ open {x}".
However, I have now idea how blast can deduce False by itself. I don't
think there is any theorem in the library which relates finite with
topology.
Email Gateway (Aug 19 2022 at 08:00):From: Lars Noschinski <noschinl@in.tum.de>
I had now a look in the proof terms. One can see, that this proof uses
in particular the following three theorems:
not_bounded_univ:
"¬bounded (UNIV :: ('a :: {perfect_space,real_normed_vector}) set)"
finite_imp_bounded:
"finite (S :: ('a :: metric_space) set) ⟹ bounded S"
finite_UNIV:
"finite (UNIV :: ('a :: finite) set)"
If there existed a type 'a satisfying these four sorts, we could prove
false (a real_normed_vector is in particular a metric space, so we only
need to mention three sorts explicitly):
lemma Y:
assumes S:
"SORT_CONSTRAINT('a::{finite,perfect_space,real_normed_vector})"
shows False
proof -
from finite_UNIV have "bounded (UNIV :: 'a set)"
by (rule finite_imp_bounded)
moreover have "¬bounded (UNIV :: 'a set)"
by (rule not_bounded_UNIV)
ultimately show False by metis
qed
So, blast did not really find a proof for you, it just gave you an error
message which might lead you into thinking it found a proof.
-- Lars
Email Gateway (Aug 19 2022 at 08:01):From: Henri.Debrat@loria.fr
Hi,
Thanks a lot for all your previous explanations.
Now, let's try some really dummy test.
lemma univbool_a: "UNIV = { True, False }" by auto
(* this is nothing but the standard UNIV_bool theorem *)
lemma univbool_b: "UNIV = { False, True }" by auto
lemma test_a: "False" using univbool_a finite_UNIV
by (blast dest:emeasure_point_measure_finite)
lemma test_b: "False" using univbool_b finite_UNIV
by (blast dest:emeasure_point_measure_finite)
The proof of test_a ends with the usual sort_contraint error, while test_b just makes the CPU go mad. I just cannot understand what is happening here !
H.
Email Gateway (Aug 19 2022 at 08:05):From: Henri.Debrat@loria.fr
Hi all,
Ok, I solved my problem all by myself :-)
Just in case it might be useful to someone, here is the solution:
interpretation rs:product_prob_space "(λi. bernoulli bp)" "UNIV::(nat × Proc) set"
where "SORT_CONSTRAINT('a::{finite,perfect_space,real_normed_vector} )"
proof [...]
H
Email Gateway (Aug 19 2022 at 08:08):From: Makarius <makarius@sketis.net>
I am impressed. How did you figure that out?
The pro-forma proposition "SORT_CONSTRAINT('a::sort)" is indeed the way to
help out in situations where certain sort occurrences in a proof need to
be specified statically in the result, to avoid the "Pending sort
hypotheses" problem.
This vacous proposition is later stripped away in the HHF normalization of
Isabelle rule statements. So it does its job of introducing sorts
formally, without changing the result. It occurs in are situations as
'assumes' in the standard collection of Isabelle applications shipped with
the release.
Makarius
Email Gateway (Aug 19 2022 at 08:10):From: Henri DEBRAT <Henri.Debrat@loria.fr>
Hi,
Well, I used the grep command to discover the word "sort" in the Isabelle directory : doing this, I discovered some lemmas had "assumes SORT_CONSTRAINT" in their header.
Then I have seen in the old isar-ref.pdf file that interpretation could take an optional "where" clause...and I tried to mix up the whole thing ! Kind of a dirty method, I admit.
Anyway, that is not so magic. It does not fully solve my issue: in the end, I discovered that a new goal had appeared in the "proof" block of the interpretation command. And guess what, this new goal is:
"SORT_CONSTRAINT('a::{finite,perfect_space,real_normed_vector} )"
So I am blocked again, even thought I could put an end to all other goals, which is already a little step forward.
By the way, I do not know what "HHF normalization" stands for so I do not really understand what's happening here.
Thanks a lot for your help !
H.
Email Gateway (Aug 19 2022 at 08:11):From: Makarius <makarius@sketis.net>
OK, I was half suspecting that, but did not try your example. This is how
you can establish these vacuous propositions as conclusions:
lemma "SORT_CONSTRAINT('a::ord)" unfolding sort_constraint_def .
lemma "SORT_CONSTRAINT('a::ord)" by (rule sort_constraintI)
The first form works, because it reveals the definition of this trick in
terms of TERM/TYPE wrappers in Isabelle/Pure: a TERM proposition is always
implicitly provable via ".", ie. "by this".
The second is the more explicit direct introduction. I am considering to
make this a default intro in Pure, so that one could write ".." instead
next time.
Makarius
Last updated: Apr 27 2024 at 01:05 UTC