Re: [isabelle] Pending sort hypotheses



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





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