Re: [isabelle] Automation is awesome; one bibliography leads to another
Mostly I am happy to see the end of proof. But if things are proved too easily, you might want to check that your definitions are correct. You might want to check that the intermediate results that need to be proved make sense.
On 31 May 2012, at 10:45, Freek Wiedijk wrote:
>> For my purposes, whatever I prove I have to understand,
> When using Coq, I regularly have had the situation that at
> the end of proving a lemma, Coq proclaimed the proof to
> be finished, while I was not there myself yet. In such
> a situation I had to decide whether to keep thinking for
> a short while or just to shrug and move on. I'm lazy:
> generally I did the latter.
> Are there other people who had the same experience?
> Of course those lemmas were easy enough that I already
> understood why they were true before I even started on the
> Coq proof. But I didn't exactly understand the final part
> of why _Coq_ got it too.
This archive was generated by a fusion of
Pipermail (Mailman edition) and