The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Hi Jonathan,

In my current project I use the following tactic as an alternative to pose 
proof (simplified):

    Inductive Learnt {A: Type} (a: A) :=
      | AlreadyKnown : Learnt a.

    Ltac learn fact :=
      lazymatch goal with
      | [ H: Learnt fact |- _ ] => fail 0 "fact" fact "already learnt"
      | _ => pose proof (AlreadyKnown fact); pose proof fact
      end.

Instead of looking for duplicates in the context, [learn] explicitly records 
each call, ensuring that work can't be duplicated (see below for a slightly 
better tactic). This solves the problem that you described of destruction 
causing loops; here's an example that will get in a loop with [pose proof], 
even after using [fail_if_redundant]:

    Parameter P : nat -> Prop.
    Parameter Q R : nat -> nat -> Prop.

    Axiom P_Q : forall {x}, P x -> exists y, Q x y.
    Axiom Q_R : forall {x y}, P x -> Q x y -> R y x.

    Goal forall x, P x -> exists y, R y x.
    Proof.
      repeat match goal with
             | _ => progress intros
             | [ H: _ /\ _ |- _ ] => destruct H
             | [ H: exists _, _ |- _ ] => destruct H
             | [ H: P _ |- _ ] => learn (P_Q H)
             | [ H: P ?x, H': Q ?x _ |- _ ] => learn (Q_R H H')
             | [  |- exists _, _ ] => eexists
             | _ => eassumption
             end.
    Qed.

This approach feels very SMT-y to me (if suffers from similar pitfalls, too, 
such as matching loops arising from axioms such that [forall x, P x -> exists 
y, P y]); it works well for complex top-down proofs where eauto isn't 
sufficiently fast or flexible, but it does tend to create large goals with 
many hypotheses.

Cheers,
Clément.

[1] The full tactic actually looks more like this:

    Ltac learn fact :=
      lazymatch goal with
      | [ H: Learnt fact |- _ ] => fail 0 "fact" fact "has already been 
learnt"
      | _ => let type := type of fact in
            lazymatch goal with
            | [ H: @Learnt type _ |- _ ] => fail 0 "fact" fact "of type" type 
"was already learnt through" H
            | _ => pose proof (AlreadyKnown fact); pose proof fact
            end
      end.

On 11/04/2015 09:29 PM, Jonathan Leivent wrote:
> Could a type of automation hint be added to Coq that helps with forward 
> chaining?
> 
> Of course, (e)auto Extern hints are general enough to be used to do forward 
> chaining.  One can write something like this:
> 
> Hint Extern 10 => match goal with H : T |- _=> pose proof (Lem H) end.
> 
> so that during (e)auto, whenever a hypothesis of type T is present, the 
> automation will add a new hypothesis based on lemma Lem. However, this 
> slows automation significantly, because nothing stops it from adding 
> duplicates of that new hypothesis, with these duplicates needlessly adding 
> to the backtracking strain.  Also, this only produces one parameterization 
> of Lem, not all of them.
> 
> It's possible to do this instead:
> 
> Hint Extern 10 => repeat match goal with H : T |- _=> let H':=fresh in pose 
> proof (Lem H) as H'; fail_if_redundant H' end.
> 
> where fail_if_redundant (see below) checks to see if another hyp with the 
> same type as H' already exists, and fails if one does. This produces all 
> parameterizations of Lem without duplicates, but slows automation a lot due 
> to repeated useless attempts at firing this hint, and the internal 
> backtracking for duplicate prevention. Also, if some further (e)auto 
> processing of the goal purposefully removed one such new hypothesis (by 
> some elimination - like destruct), this hint would make it re-materialize, 
> perhaps causing even more costly needless proof searching to get triggered.
> 
> The problem is that there is currently no way to trigger an action to occur 
> only when a new hypothesis of a certain type is added to a goal.  But 
> suppose there was such a mechanism.  The interface might look like this:
> 
> Hint FChain (H : T) =>  pose proof (Lem H).
> 
> The semantics would be - during (e)auto, if a new hypothesis H with a type 
> matching the type pattern T is added to the goal, then trigger the rhs 
> tactic of each applicable FChain hint immediately after the completion of 
> the hint that added H.  The same hint wouldn't get triggered twice for the 
> same hypothesis.  It might make sense to add a cost to each FChain hint, 
> which would delay the triggering of that FChain hint until just before 
> other non-FChain hints of similar cost - so that the general form would be:
> 
> Hint FChain <cost> <hyp pattern> => <tactic> : <dbs>.
> 
> For hypotheses that already exist in the goal at the time the (e)auto 
> tactic is started, they are all considered new, and so all will trigger any 
> applicable FChain hints.  One could also have a tactic [autofchain with 
> dbs] that, like autounfold and autorewrite, used the hints outside the 
> context of (e)auto.
> 
> Does a feature like this sound useful?
> 
> Maybe typeclasses might be able to do things similar to this, but I'm no 
> typeclass expert.  Do any typeclass experts know if (and how) it can?
> 
> -- Jonathan
> 
> 
> Note:
> 
> Ltac fail_if_redundant H :=
>   let T:=type of H in
>   try (clear H; lazymatch goal with _: T |- _ => fail 1 | _ => fail end).
> 
>

Attachment: signature.asc
Description: OpenPGP digital signature