Re: [isabelle] Error: Pending sort hypothesis



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.