The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Here's one way to build an inductive type and one of it's constructors given its FQ name and the index of the constructor, with example code that I wrote for sigT, which you can modify as needed. Zero guarantees it's up-to-date or the best way but hopefully it gets you somewhere.

let coq_init_specif = ModPath.MPfile (DirPath.make (List.map Id.of_string ["Specif"; "Init"; "Coq"]))
                                     
let sigT =
  mkInd (MutInd.make1 (KerName.make2 coq_init_specif (Label.make "sigT")), 0)

let existT =
  mkConstruct (fst (destInd sigT), 1)

On Mon, Apr 9, 2018, 6:44 PM Kenneth Roe <kendroe AT hotmail.com> wrote:

I am writing a tactic to simplify expressions.  As an example consider the following:

Fixpoint beq a b :=

    match a,b with

    | 0,0 => true

    | (S x),(S y) => beq x y

    | _,_ => false

    end.

Fixpoint blt a b :=

    match a,b with

    | _,0 => false

    | (S x),(S y) => blt x y

    | 0,(S x) => true

    end.

Theorem test: forall x y, q(x,y) = orb (negb (beq x y)) (negb(blt x y)).

Proof.

    arewrite.

The "arewrite" tactic can reduce this theorem to "forall x y, q(x,y) = true".  The tactic needs to construct the inductive term "true".  I tried the following piece of ml code which did not work:

let true_term = Term.mkApp (mkConstructorUi (Lib_coq.init_constant ["Coq"; "Init"; "Datatypes"] "bool") 1) [||]

The problem seems to be that I need to convert a constr object to a pinductive object.  Can someone give me a piece of ml code to construct the term "true"?

                                   - Ken