The Coq mailing list

[Joey Dodds <jdodds AT princeton.edu>]

Thanks Abishek,
That's pretty close to what I tried. What was a little surprising to me is that the following still succeeds

Opaque ltac_something.

 

Goal forall P, P -> P.

intros. hide_hyp X. auto.

Qed.

Unification doesn't seem to mind unfolding opaque symbols, so this approach doesn't quite work for me.

On Sun Feb 01 2015 at 4:04:51 PM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

I think I originally got these from :

http://www.cis.upenn.edu/~bcpierce/sf/current/LibTactics.html

Definition ltac_something (P:Type) (e:P) := e.

Notation "'Something'" := 

  (@ltac_something _ _).

Lemma ltac_something_eq : forall (e:Type),

  e = (@ltac_something _ e).

Proof. auto. Qed.

Lemma ltac_something_hide : forall (e:Type),

  e -> (@ltac_something _ e).

Proof. auto. Qed.

Lemma ltac_something_show : forall (e:Type),

  (@ltac_something _ e) -> e.

Proof. auto. Qed.

Ltac show_hyp H :=

  apply ltac_something_show in H.

Ltac hide_hyp H :=

  apply ltac_something_hide in H.

Ltac show_hyps :=

  repeat match goal with

    H: @ltac_something _ _ |- _ => show_hyp H end.

These worked for me, but maybe your automation is smarter and can fool this hiding mechanism.

Regards,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Sun, Feb 1, 2015 at 3:43 PM, Joey Dodds <jdodds AT princeton.edu> wrote:

Hi,

I'm trying to do a mutually inductive proof where Coq puts the lemmas you are trying to prove above the line and you have to be careful where to apply them or you will fail to QED. 

My automation keeps using them, and I was wondering if there was a way to define a tactic to temporarily make them unusable. My first attempt was rewriting them into an opaque identity function, but it seems like auto and apply are happy to ignore opacity and unfold the definition anyways.

Thanks,

Joey