The Coq mailing list

[Arnaud Spiwack <arnaud AT spiwack.net>]

Vladimir Voevodsky wrote:

This should not be too hard to implement and it would make many proofs easier.

Unfortunately for my health, but fortunately for those who want this feature, I held a similar belief when I started the endeavour of implementing dependent subgoals in Coq… 7 years ago. (of course, it's far from the only thing I've done in the last seven years, but it should speak of how non-obvious this was. Arguably though, I've put much more in the new proof engine than just dependent subgoals, and it probably has slowed the whole enterprise significantly ).

Matthieu Sozeau wrote:

Long story short, the previous proof engine used an ad-hoc tree with leaves representing the subgoals, instead of using directly the term tree structure + holes/existentials.

In fact, the problem is easier to see in the type of tactics (they go hand to hand, but the tactics showcase it best). The previously used tactic was based on Milner's tactic type for LCF:

type tactic = goal -> (goal list * (theorem list -> theorem))

Where theorem is an abstract type. The idea was to give a basic set of tactics which, then, become the only way to construct theorem, if the basic tactics are correct then all theorems are indeed theorem. This was an immensely good idea and has proven to have unexpected applications (for instance, for a cartesian closed category 𝓒, there is a category where the objects are pairs (A,A') of objects of 𝓒, and whose morphisms (A,A')⟶(B,B') are morphisms A⟶B×(B'⇒A') of 𝓒. This has been used to analyse Gödel's Dialectica interpretation. See Valeria de Paiva's The Dialectica categories [ http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-213.pdf ] ).

The former type of tactics of Coq was pretty similar (up to some boilerplate for existential variables) except that the abstract theorem type was not needed (as there is a more primitive notion of theorems), and was replaced by the concrete tree type which Matthieu is referring to. In a sense these proof trees are an implementation of terms with holes. And the basic tactics a set of typing rules for them.

It it clear when watching the (former) type of tactics closely that it assumes the goals to be independent. Which is not the case of dependent subgoals (the name gives it away of course). Basically, a subgoals which appears as an existential variable in another subgoal can be solved by side effect, but resulting in fewer goals than expected passed to the theorem list -> theorem function, and proof reconstruction failing.

Beta Ziliani wrote:

Nevertheless, with eapply and Grab
Existential Variables you can get the existentials as goals, the
problem is that the ordering is opposite to what one would expect

Indeed. As it happens, Grab Existential Variables can work because, under the hood, v8.4 uses the new proof engine. Unfortunately, Ltac was in its own bubble and couldn't fully leverage the new capabilities: it is the reason why Grab Existential Variables can only be called when the proof is completed. Trunk fixes that.

Andrea Asperti wrote:

Well, you have just to pass to Matita instead of using Coq ... :-)

Hehe :) . In fact, the new proof engine is partially inspired by Matita. At the very least I knew of Matita's approach for dependent subgoals when I set myself to implement dependent subgoals in Coq. It also has multiple goals to multiple goals tactics, but it was conceived and designed independently.

Benjamin Grégoire wrote:

"eapply Iconstr" do no works ?

It's not quite what Vladimir is after, actually. To make things clear, here is a corresponding example (which works in trunk):

Record AbGr := {
  El :> Type ;
  equ : El -> El -> Prop
    where "a ≡ b" := (equ a b);
  equ_equiv : Equivalence equ ;
  zero : El
    where "0" := zero;
  plus : El -> El -> El
    where "x +  y" := (plus x y);
  plus_proper : Proper (equ ==> equ ==> equ) plus ;
  minus : El -> El
    where "- x" := (minus x);
  minus_proper : Proper (equ ==> equ) minus ;

  plus_assoc : forall x y z, (x+y)+z ≡ x+(y+z) ;
  plus_comm : forall x y, x+y ≡ y+x ;
  zero_neutral : forall x, x+0 ≡ x ;
  minus_inverse : forall x, x+(-x) ≡ 0
}.
(* 12 fields including 7 proof obligations. *)

Goal forall (P:AbGr->Prop), exists G, P G.
Proof.
  intros *.
  refine (ex_intro _ _ _).
  - refine {|
      El := Z.t;
      equ n p := Z.eqb n p = true;
      zero := 0%Z;
      plus := Z.add;
      minus := Z.opp
    |}.

(The proof isn't complete, of course)