The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/01/2015 03:58 PM, Jonathan Leivent wrote:
> On 02/01/2015 03:43 PM, Joey Dodds 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
>
> I have a way to do this in 8.5, but it's a bit of a hack (again). I 
> also requested this feature as enhancement #3845.
>
> I'll extract the hiding tactic from some other stuff I'm working on, 
> and post it momentarily...
>
> -- Jonathan

Attached.  Unfortunately, this specific tactic includes a lot of the 
infrastructure I'm still building.  The example at the very end uses the 
tactic "vgoal" (included) to display the current goal with two 
hypotheses (n2 and n3) hidden.  To use, just substitute some other tac 
in the invocation "hyps {non-empyt list of hyps to hide} => hide_hyps tac"

Note that this hiding technique should be able to prevent any automation 
from using the hidden hypotheses.  Here's the output with n2 and n3 hidden:

n0 : nat
n1 : nat
hidden : (Type -> Type)
n2 : (hidden nat)
n3 : (hidden nat)
n4 : nat
======
True

Since the hidden function is bodyless in this goal, there is no way for 
automation to make use of the hidden hyps.  The "hack" involves how to 
recover those hidden hypotheses.

-- Jonathan

Ltac lasthyp :=
  lazymatch goal with H:_ |- _ => constr:(H) end.

Ltac revert_clearbody1 H := try clearbody H; revert H.

Ltac harvest_hyps harvester :=
  constr:($(harvester; constructor)$ : True).

Tactic Notation "harvest" tactic3(harvester) "=>" tactic3(tac) :=
  let hs := harvest_hyps harvester in
  tac hs.

Ltac revert_clearbody_all :=
  repeat revert_clearbody1 lasthyp.

Ltac allhyps := harvest_hyps revert_clearbody_all.

Tactic Notation "hyps" "=>" tactic3(tac) :=
  harvest revert_clearbody_all => tac.

Tactic Notation "hyps" ne_hyp_list(hs) "=>" tactic3(tac) :=
  harvest generalize hs => tac.

Ltac next_hyp hs step last := 
  lazymatch hs with 
  | (?hs' ?H) => step H hs'
  | _ => last
  end.

Ltac loop tac hs :=
  idtac;
  let rec step H hs := tac H; next_hyp hs step idtac in
  next_hyp hs step idtac.

Ltac reorder hs :=
  let totop H := try move H at top in
  loop totop hs.

Tactic Notation "Reorder" tactic4(tac) :=
  hyps => fun hs => tac; reorder hs.
  
Ltac intro_to H :=
  intro;
  first [constr_eq H lasthyp | intro_to H].

Ltac eclear_except hs :=
  let stop:=fresh "stop" in
  generalize I as stop;
  (repeat let H:=lasthyp in
    lazymatch hs with 
    | context[H] => revert H 
    | _ => first [clear H|revert H]
    end);
  intro_to stop;
  clear stop.

Ltac hide_hyps tac hs :=
  try (is_evar ?__Unhider;
       fail 1 "hide_hyps: The evar name ?__Unhider is being used");
  let hider := fresh "hidden" in
  pose (hider := (fun T=>T): Type -> Type);
  let hidetype H := let T := type of H in
                    change T with (hider T) in H in
  loop hidetype hs;
  assert True as _;
  [eclear_except hider|];
  [|clearbody hider; tac];
  [refine (let unhide := ?[__Unhider] : hider=fun T=>T in _) | ..];
  [| |Reorder pose proof ?__Unhider as -> ..];
  [reflexivity|exact I|..].
  
Ltac get_value H := eval cbv delta [H] in H.
  
Ltac vgoal := 
  idtac; (*prevents early eval*)
  match reverse goal with
    | H : ?T |- _ => 
      first[let v := get_value H in 
            idtac H ":=" v ":" T
           |idtac H ":" T];
      fail
    | |- ?G => 
      idtac "======"; idtac G; idtac ""
  end.


Goal True.
do 5 pose proof 0 as ?n0.
hyps n2 n3 => hide_hyps vgoal.