The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users,

using Jonathan Leivant's ideas on the split tactic, I created a tactic which 
produces for simple enumeration style inductive types a list of all values 
(see attached Coq script). It works fine, just the returned "proof term" 
contains some unnecessary overhead (a function definition which is never 
used). I wonder if there is a way to modify the tactic such that the 
resulting "proof term" is just the list, without the overhead.

E.g. what I want is the term: 

ValList1b = a :: b :: c :: nil
     : list Test1 

but what I get is the equivalent but much longer term:

ValList1 = 
let result := a :: b :: c :: nil in
(fun _ : forall x : Test1, x = x => result)
  (fun x : Test1 =>
   match x as t return (t = t) with
   | a => let tmp := b :: c :: nil in eq_refl
   | b => let tmp := c :: nil in eq_refl
   | c => let tmp := nil in eq_refl
   end)
     : list Test1

Thanks & best regards,

Michael

Attachment: MakeValList.v
Description: MakeValList.v