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 (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.