Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Force automation to ignore a hypothesis

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Force automation to ignore a hypothesis


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Force automation to ignore a hypothesis
  • Date: Sun, 1 Feb 2015 16:04:17 -0500

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,

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




Archive powered by MHonArc 2.6.18.

Top of Page