The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Hi,

While trying to investigate why CoqIDE (Windows 8.5pl3) was not checking my opaque proofs asynchronously (in a background thread),  I found that

the section variables often (always?) prevent CoqIDE from checking opaque proofs asynchronously. 

This behaviour of CoqIDE does not surprise me anymore.

The fundamental property that enabled asynchronous proof checking was that the exact content between Proof....Qed does not matter, as long as the content is correct. Section variables break this invariant,

because at the end of a section, the types of its lemmas depends on the section variables used in the proofs. This is illustrated in the example below. The types of [useEqq] and [noUseEqq] are different 

at the end of the section, even though they were identical inside. 

Is there a way to get both the brevity enabled by section variables, and

the significant productivity-boost enabled by asynchronous proof checking? 

An easy fix could be a switch to make the types of lemmas of a section depend on all section variables, and thus regain the invariant enabling asynchronous proof checking?

Section NoAsynch.

Variables a b:nat.

Hypothesis eqq : a=b.

Lemma useEqq :a=a.

Proof.

  rewrite eqq.

  reflexivity.

Qed.

Lemma noUseEqq :a=a.

Proof.

  reflexivity.

Qed.

End NoAsynch.

Check useEqq.

(*useEqq

     : forall a b : nat, a = b -> a = a *)

Check noUseEqq.

(*noUseEqq

     : forall a : nat, a = a*)

Indeed, when section variables are eliminated, as below,

CoqIDE checks the proofs below asynchronously.

Section Asynch.

Lemma useEqqA (a b:nat) (eqq:a=b) :a=a.

Proof.

  rewrite eqq. 

  reflexivity.

Qed.

Lemma noUseEqqA (a b:nat) (eqq:a=b) :a=a.

Proof.

  reflexivity.

Qed.

End Asynch.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/