Re: [isabelle] Verify the legitimacy of a proof?



Unfortunately, it is very easy to circumvent this. I don't recall who
found this originally, but you can hide the âtaintâ of a theorem by
going through a type class instantiation:

lemma one_add_1_eq_3:
  "(1::nat) + 1 = 3"
  sorry
   
class foo = semiring_1 +
  assumes foo: "1 + 1 = 3"

instance nat :: foo
  by intro_classes (rule one_add_1_eq_3)

lemmas one_add_1_eq_3' = foo [where ?'a = nat]

check_sorry one_add_1_eq_3'


Cheers,

Manuel


On 2017-07-08 11:47, Simon Wimmer wrote:
> Hi Scott,
>
> you can also check which oracles a theorem depends on from the ML level.
> A hack to look for the oracle that is used to implement sorry can look like
> this:
>
> theory Scratch
>   imports Main
>   keywords "check_sorry" :: diag
> begin
>
> ML â
> val get_oracles = Proofterm.all_oracles_of o Proofterm.strip_thm o
> Thm.proof_body_of
>
> val contains_sorry = exists (fn (a, _) => a = "Pure.skip_proof") o
> get_oracles
>
> fun report_sorry ctxt =
>   if Context_Position.is_visible ctxt then
>     Output.report [Markup.markup Markup.bad "Proof arises from sorry
> oracle!"]
>   else ();
>
> fun check_sorry ctxt th =
>     if contains_sorry th then report_sorry ctxt else ()
>
> fun check_sorry_cmd thm_ref st =
>   let
>     val ctxt = Toplevel.context_of st
>     val th = Proof_Context.get_fact_single ctxt thm_ref
>   in check_sorry ctxt th end
>
> val _ =
>   Outer_Syntax.command @{command_keyword check_sorry} "Check theorem for
> sorry"
>     (Parse.thm >> (fn (th, _) => Toplevel.keep (check_sorry_cmd th)));
> â
>
> (* Usage: *)
> lemma one_add_1_eq_3:
>   "1 + 1 = 3"
>   sorry
>
> check_sorry HOL.refl
> check_sorry one_add_1_eq_3
>
> Cheers,
> Simon
>
> On Fri, Jul 7, 2017 at 8:28 PM C. Diekmann <diekmann at in.tum.de> wrote:
>
>>> That is, I want to ensure that no lemma in the
>>> proof tree ended with "sorry",
>> If you make a command line run with `isabelle build`, every use of `sorry`
>> is counted as cheating and makes the build fail (but only at the end of the
>> build, not at the time when the thy with the sorry is processed).
>>
>> This raises a new question: can I enable cheating (quick_and_dirty) mode in
>> a command line build?
>>
>> One question answered, one not answered, one new problem ;-)
>>
>> Cheers,
>>   Cornelius
>>




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