The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I stumbled on an interesting trick that uses admit.  It combines admit 
with the fact that Ltac local definitions that are not directly used to 
solve part of the goal don't become anything that the proof depends on.  
Hence, using admit in such terms doesn't make the ongoing proof depend 
on admit.  If those terms use $(...)$, then we can analyze the resulting 
admitted constr to see the results of tactics within the $(...)$ without 
having to properly "solve" them.

For example, one can use this trick within a tactic to uncover the names 
and args of all constructors of an inductive type merely by destructing 
an instance of that type and collecting the types of the resulting subgoals:

(*some synonyms of admit to make searching by context easier:*)
Definition myadmit(T : Type) : T := $(admit)$.
Definition myadmit' := myadmit.
Opaque myadmit myadmit'.

Ltac revert_all := repeat lazymatch goal with H:_ |- _ => revert H end.

(*analyze will return a tuple of the resulting subgoal types generated 
by tac
  given the initial conclusion targtype.  It will return 0 if tac 
leaves no subgoals.*)
Ltac analyze tac targtype :=
  let x := eval simpl in ($(tac; revert_all; apply myadmit)$ : targtype) in
  (*each subgoal left over by tac will get "solved" by myadmit*)
  let rec f pt x := (*find the myadmits in x and tuplize their args*)
      match x with
        | context W[myadmit ?T] =>
          let pt' := match pt with
                       | 0 => T
                       | _ => constr:((pt , T))
                     end in
          (*replace myadmit by myadmit' so that this recursion terminates*)
          let x' := context W[myadmit' T] in
          f pt' x'
        | _ => pt
      end in
  f 0 x.

(* Demo:*)

Inductive foo : nat -> Set :=
| Foo1 : foo 1
| Foo2(b : bool) : foo 2
| Foo3 : foo 3
| Foo4(n : nat)(f : foo n) : foo 4.

Lemma demo : True.
let x := analyze ltac:(clear; intros n f; destruct f eqn:?) (forall n, 
foo n->True) in
idtac x. (*Print out the constructor info for foo*)
exact I.
Qed.

Print Assumptions demo. (*Closed under the global context - no 
dependency on proof_admitted axiom*)

-- Jonathan