The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 08/01/2014 04:48 PM, Enrico Tassi wrote:
> On Fri, Aug 01, 2014 at 04:28:44PM -0400, Jonathan wrote:
> > Goal mytype.
> > econstructor.
> >
> > produces the goal like:
> >
> > 1 subgoals
> > , subgoal 1 (ID 4)
> >
> >    ============================
> >     P ?3
> Sure, but I don't see why you can't prove as a forward step (pt := P t)
> and applt (Mytype pt), or just apply (@Mytype t).
> Is t so horrible that you cannot construct it by hand?
>
> I feel so naive, but I don't get if it is actually necessary to play
> with evars this way or it just that people find it convenient.
>
> I have some examples where one really needs an evar floating around, but
> this one does not seem of that kind (I' thinking at the big enough library
> by Cyril Cohen, or at the [: ] patterns of ssr to spill subproofs).
>
> Thanks for the patience,

Certainly, for every instance of backward chaining which creates a new 
evar, one could substitute a forward chaining step that instead provided 
hand-constructed arguments to the otherwise evar-producing fields.  I 
have no argument with that (excuse the pun).

However, I think that forward chaining is always hidden backward 
chaining.  In order for you to determine in advance the right form of 
any constrained arguments, such as px above (or, rather, more complex 
variations in more useful types), you are doing some backward chaining 
in your head, and using Coq to check the step's validity.  Coq is for 
that step then just a proof checker and not a proof assistant.  
Furthermore, the backward chaining thought process you used in that step 
is not recorded, unless in a comment - but certainly not formally.

My motivation is to find techniques whereby interactive 
dependently-typed systems such as Coq (or Agda, or Idris, or Matita if 
it was still being maintained) can be used by people whose expertise 
isn't in proving.  I recall a marketing executive at a former company  
that used to boast that he wanted to "reduce the IQ of our customer base 
by 25%".  I guess I have a similar motivation here, although I am unsure 
of the percentages :)

The advantage of backward chaining and producing evars in this case over 
forward chaining is just how much mental effort is involved. Does the 
goal currently tell you in an obvious way what you need to know to 
instantiate evars (or provide arguments to prevent them)? If not, 
continue refining the goal until it becomes obvious.  Where "obvious" is 
a very subjective measure.

I have an example of backward chaining in my github project that 
uncovered a new algorithm that I didn't believe existed, or know how it 
worked, until the proof was finished.  I don't think I would have been 
able to accomplish that with just forward chaining steps.

-- Jonathan