The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Hi Clément,

I have tried variants of your proposal, but I don't like the additional 
note-taking hypotheses - both because they complicate the goals, and 
because they create dependencies between hypotheses that can cause other 
tactics to fail when they try to eliminate or alter depended-on hypotheses.

Also, having Extern hints that use the learn tactic means that they will 
be triggered much more often than needed, in most cases just failing 
after doing their search for Learnt hyps - which slows down (e)auto.

My proposal is just that - if ad-hoc workarounds for this deficiency are 
common, but they all suffer similar drawbacks - maybe the better 
solution is to provide the missing ingredient in some way.  And the 
missing ingredient seems to be the ability to automatically trigger a 
tactic after a new hypothesis of some type is added to a goal (also 
perhaps when the type of an existing hypothesis changes).

-- Jonathan

On 11/05/2015 01:03 AM, Clément Pit--Claudel wrote:
> 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.