coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 :
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
- [Coq-Club] Force automation to ignore a hypothesis, Joey Dodds, 02/01/2015
- Re: [Coq-Club] Force automation to ignore a hypothesis, Jonathan Leivent, 02/01/2015
- Re: [Coq-Club] Force automation to ignore a hypothesis, Jonathan Leivent, 02/01/2015
- Re: [Coq-Club] Force automation to ignore a hypothesis, Abhishek Anand, 02/01/2015
- Message not available
- Re: [Coq-Club] Force automation to ignore a hypothesis, Joey Dodds, 02/01/2015
- Re: [Coq-Club] Force automation to ignore a hypothesis, Abhishek Anand, 02/01/2015
- Re: [Coq-Club] Force automation to ignore a hypothesis, Joey Dodds, 02/01/2015
- Re: [Coq-Club] Force automation to ignore a hypothesis, Jonathan Leivent, 02/01/2015
Archive powered by MHonArc 2.6.18.