Re: [isabelle] Error: Pending sort hypothesis

Hi Thomas,

My hope was that ATP would find a proof based on the lemma
"finite_imp_nat_seg_image_inj_on" that is, in some sense, the inverse of
my lemma.

In the meantime, I proved the lemma directly with induction over the
finite set (no idea whether this is more elegant ;) ):

  -- "Finite sets have an injective mapping to an initial segments of the
      natural numbers"
lemma finite_imp_inj_to_nat_seg:
  fixes A :: "'a set"
  assumes A: "finite A"
  obtains f::"'a \<Rightarrow> nat" and n::"nat" where
    "f`A = {i. i<n}"
    "inj_on f A"

proof -
  from A have "\<exists>f (n::nat). f`A = {i. i<n} \<and> inj_on f A"
  proof (induct)
    case empty thus ?case by auto
    case (insert x A)
    then obtain f and n::nat where
      IH: "f`A = {i. i<n}" "inj_on f A" by auto
    let ?fs = "f(x:=n)"
    from IH insert(2) have
      "?fs`(insert x A) = {i. i<Suc n}"
      "inj_on ?fs (insert x A)"
      apply -
      apply force
      apply simp
      apply (rule inj_onI)
      apply (auto dest: inj_onD split: split_if_asm)
    thus ?case by blast
  with that show ?thesis by blast


Thomas Sewell wrote:
> Hi Peter.
> I agree with Tobias, it's highly unlikely that the automated theorem
> provers will find an instantiation that solves your problem. I was
> fiddling with your problem out of interest, and did find a proof, but
> it's not especially elegant. The rule finite_distinct_list tells you
> that a list exists which puts A in order, giving you (roughly) the
> inverse of the function f you want. The problem is inverting back to f
> since we don't have an injective function. To do this I had to extend
> into the sum type to force injectivity - maybe someone can see an
> easier way?
> Yours,
>    Thomas.
> lemma
>  fixes A :: "'a set"
>  assumes finA: "finite A"
>  obtains f::"'a => nat" and n::"nat" where
>    "f`A = {i. i<n}"
>    "inj_on f A"
> proof -
>  obtain xs where dist: "distinct xs" and A: "A = set xs"
>    using finite_distinct_list[OF finA] by auto
>  obtain g where g_def: "g == (%n. if n < length xs then Inl (xs ! n)
> else Inr n)" ..
>  obtain f where f_def: "f == inv g o Inl" ..
>  have inj_g: "inj g"
>    unfolding g_def
>    apply (rule inj_onI)
>    apply (auto simp: nth_eq_iff_index_eq[OF dist] split: split_if_asm)
>    done
>  have f_i: "!!i. i < length xs ==> f (xs ! i) = i"
>    unfolding f_def
>    apply (cut_tac x=i in inv_f_f[OF inj_g])
>    apply (clarsimp simp: g_def)
>    done
>  have f_im: "f ` A = {i. i < length xs}"
>    apply safe
>     apply (clarsimp simp: A in_set_conv_nth f_i)
>    apply (simp add: A)
>    apply (rule image_eqI[OF sym], erule f_i)
>    apply simp
>    done
>  have f_inj: "inj_on f A"
>    apply (rule inj_onI)
>    apply (auto simp: A in_set_conv_nth f_i)
>    done
>  show ?thesis
>    using prems f_im f_inj by auto
> qed
> Tobias Nipkow wrote:
>> I am surprised you got any answer from sledgehammer, I failed.
>> Unfortunately the proof you got is not a real proof: the ATPs are give a
>> problem with some type information omitted for efficiency reasons. This
>> allows them sometimes to find proofs that do not replay in Isabelle
>> because of typing problems. Yours is most likely of that kind.
>> The development version has a Settings item ATP: Full Types that gives
>> the ATPs the full type information which you can try in such situations.
>> It will avoid these unsound proofs but also reduces the success rate of
>> the ATPs. In you example I am sceptical that the ATPs will find a real
>> proof because of the non-trivial witnesses required.
>> Tobias
>> Peter Lammich schrieb:
>>> Hi all,
>>> I wanted to prove the following lemma:
>>> lemma
>>>   fixes A :: "'a set"
>>>   assumes "finite A"
>>>   obtains f::"'a => nat" and n::"nat" where
>>>     "f`A = {i. i<n}"
>>>     "inj_on f A"
>>>   (* Sledgehammer found a proof: *)
>>>   apply (metis finite finite_imageD id_apply inj_on_inverseI
>>> infinite_UNIV_char_0)
>>>   (* Here, Isabelle sais: No subgoals
>>>   However, when finnishing the proof: *)
>>>   done
>>>   (* I get the error:
>>> *** Pending sort hypotheses: {finite,semiring_char_0}
>>> *** At command "done".
>>> *)
>>> Ok, I wondered how to prove the theorem from the lemmas given to metis.
>>> But what is happening here behind the scenes, how do these
>>> typeclasses(?) enter the game?
>>> Regards,
>>>   Peter

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