Re: [isabelle] Error: Pending sort hypothesis



It would be nice to get a compact proof. Here is a condensed version of
Thomas's proof, getting rid of Inl/Inr:

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
  let ?I = "{i. i<size xs}"
  def g == "%n. xs ! n"
  def f == "Inv ?I g"
  have inj_g: "inj_on g ?I"
    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 : ?I ==> f (xs ! i) = i"
    unfolding f_def by (metis Inv_f_f g_def inj_g)
  have f_im: "f ` A = ?I"
    apply(auto simp add:A in_set_conv_nth f_i)
    apply (metis Collect_def f_i in_set_conv_nth rev_image_eqI mem_def)
    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

I am sure this can be improved further.

Tobias


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.