The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 04/02/2015 10:11 AM, Jonathan Leivent wrote:
> ...  Roughly - the 8.4 version uses refine instead of tactic-in-term 
> to build constrs out of tactics - as the "collect_things" technique 
> used in these tactics requires a constr to be built that contains the 
> inductive type's match expression. However, the alternate evar-based 
> mechanism I referred to would perhaps also work in 8.4, but not as 
> easily (I don't have an 8.4 version of Coq available to test - so I am 
> saying this based only on faulty memory).  That evar-based mechanism 
> avoids the context searches by directly building a "list" of the 
> constructor names by selective instantiation of an evar, and avoiding 
> the need for context searching a constr - hence no need for the constr.

Here's a version that should work in 8.4 (I only have 8.5 installed, so 
I can't check it), and which uses the evar direct-list trick instead of 
context searches.  Because it does not use tactic-in-term, proof term 
impact is quite large, but it beta reduces out easily - as can be seen 
in the demo.

-- Jonathan

Ltac head_of term :=
  lazymatch term with
  | ?H _ => head_of H
  | _ => term
  end.

Ltac get_value H := eval cbv delta [H] in H.

Inductive things : Prop := 
| More{T}(head:T)(tail:things)
| NoMore.

Ltac elaborate term Q :=
  match I with
  | _ => elaborate (term (Q _)) Q
  | _ => term
  end.

Ltac pose_ctors type H :=
evar (H:things);
assert ((forall T, T) -> True) as _ by
(intro Q;
 let type':=elaborate type Q in
 let D:=fresh in
 assert type' as D by apply Q;
 pose D as D2;
 destruct D;
 let c:=get_value D2 in
 let C:=head_of c in
 instantiate (1:=(More C _)) in (Value of H);
 exact I);
instantiate (1:=NoMore) in (Value of H). 

Inductive Weird : nat -> Set :=
| weird0 : Weird 0
| weird1(b : bool) : Weird 1
| weird2(n : nat) : Weird (n - 2)
| weird3(n : nat)(w : Weird (S n)) : n > 2 -> Weird n.

Lemma demo : True.
pose_ctors Weird W.
pose_ctors things T.
pose_ctors False F.
pose_ctors (@eq) E.
pose_ctors bool B.
pose_ctors nat N.
Show Proof.
exact I.
Defined.
Print demo.
Definition demo2 := Eval lazy beta delta [demo] in demo.
Print demo2.