The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

On Tue, Jan 7, 2014 at 10:04 PM, Matthieu Sozeau 
<mattam AT mattam.org>
 wrote:
> That's not doable in 8.4 but is in trunk thanks to Arnaud Spiwack's new
> proof engine. 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.

Then I'm curious to know why refine does the job in 8.4:

"
Inductive I := Iconstr :  forall ( x0 : Type ) ( x1 : x0 ) , I .

Goal I.
refine (Iconstr _ _).
refine 0.
Qed.
"



>
> Le mardi 7 janvier 2014, Vladimir Voevodsky a écrit :
>
>> Is there a reason why Coq's proof engine does not accept a possibility of
>> dependent goals? For example if I need to provide an object of an inductive
>> type
>>
>> Inductive I := Iconstr :  forall ( x0 : T0 ) ( x1 : T1 ) , I .
>>
>> where T1 in general depends on x0, I would like to say "apply Iconstr."
>> and get provided first with the goal to fill in x0 in T0 and then with the
>> goal to fill in x1 in the appropriately substituted T1.
>>
>> This should not be too hard to implement and it would make many proofs
>> easier.
>>
>> Vladimir.
>
>
>
> --
> -- Matthieu