The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 04/02/2015 03:08 PM, Jonathan Leivent wrote:
> ...
> 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

I installed 8.4 to check this.  It didn't work, but was fixable 
(attached).  I had to rely on case_eq for the hard @eq case that Jason 
pointed out, even though case_eq looks like it has a bug with respect to 
the equality it generates (eq_refl = eq_refl in the @eq case) - but 
maybe that bug is just why it can handle @eq in 8.4. 8.4 also needs 
those extra arg-less instantiates.

-- 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}(h:T)(t:things)
| NoMore.

Ltac start_things H := evar (H:things).

Ltac add_thing t H := 
  instantiate; instantiate (1:=More t _) in (Value of H).

Ltac end_things H := 
  instantiate; instantiate (1:=NoMore) in (Value of H).

Ltac pose_ctors type H :=
  start_things H;
  assert ((forall T, T) -> True) as _ by
  (let Q := fresh in 
   intro Q;
   let D := fresh in
   let rec f t := first [pose (D:=Q t) | f (t (Q _))] in 
   f type;
   case_eq D;
   intros;
   lazymatch goal with 
   | _ : _ = ?c |- _ =>
     let C:=head_of c in
     add_thing C H
   end;
   exact I);
  end_things H.

(*Tests*)

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.

Inductive Strange(x: nat)(w : Weird x) : Set := 
| strange0
| strange1 (b:bool).

Lemma demo : True.
pose_ctors Weird W.
pose_ctors Strange R.
pose_ctors False F.
pose_ctors bool B.
pose_ctors nat N.
pose_ctors @eq E.
pose_ctors list L.
pose_ctors prod P.
Show Proof.
exact I.
Defined.
Print demo.
Definition demo2 := Eval lazy beta delta [demo] in demo.
Print demo2.