Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Building a constructive term from inside an ML tactic

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Building a constructive term from inside an ML tactic


Chronological Thread 
  • From: Kenneth Roe <kendroe AT hotmail.com>
  • To: Coq-Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Building a constructive term from inside an ML tactic
  • Date: Tue, 10 Apr 2018 01:43:56 +0000
  • Accept-language: en-US
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kendroe AT hotmail.com; spf=Pass smtp.mailfrom=kendroe AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM03-BY2-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:1bjOohcVqPxJWcFteGtGUNJHlGMj4u6mDksu8pMizoh2WeGdxcu9bB7h7PlgxGXEQZ/co6odzbaO6Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahb75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM38H/ZhNFsjKxVoxyuuxNwzpXOb42JKPZzZL/Rcc8HSWdHQ81fVzZBAoS5b4YXCuQOI+BYr4/jqFsSrRu1GBWiBOTxxTRVgXL23rM10+I8HgHc2wwvAckDsHTTrNXpMacdS+G1zK3SwTrfaPNW3C7w5Y7VeR4iufGBRb19fdbLxUQrCQ/JlFSdpZbkMj6UzugNvXaU4ul8We+qjmMnpQF8rzezycopiYTEh4AYxU7B+Cpn3Yk4KsO0RUt1YdOnE5ZQuSeXPJZsTMw4WWFnoiM6x6UGuZGleCgKz4wqyQbDZvKAb4SF7AvvWfuTLjtmnX5lf6mwiAio/Uin1+38StK70FFXripDj9bArGgN1wbU6sibVPRy4luh2TeI1wDV8O1EJl00lbbfK54mxb4wlYAfvljEHi/zgEn2jamWeVs4+uWw5Onrfq/qq5uCO4NuiwzyKKUjl82nDeQ9KAcOXmyb+eqm1L3k+E30WLZKgeMwkqbEqpDaItoUq7W5Aw9SzoYj7gywDzai0NgCgXYHK1dFdAqdj4f1I1HOPOz4DfCnjluwlzdr3unKMaHlApXQNXfOi6zhfLZ4605E0gU/19Ff55ROCrEAOv3/QEHxtMaLRiM+Ziez2qPMDMh3ntcVXnvKCauEOovTt0WJ76QhOb/fSpUSvWPeJv4j6uLuxUU+lBdJfqSv0YEQZVi4GehjKkSdJ3Hrh4FSQi8xogMiQbmy2xW5WjlJaiPqBvNu1nQAEIujSLz7aMWoib2F0j28G8QNNGBBFlWFEHOufIKBCa5VNHCiZ/R5mzlBboCPDpc73Ej15g/9179uL+6S8Sod58q6iYpFotbLnBR3zgRaSsSQ12bREDNSt0ZQHHoc7fo6pkZwjFCezaJ/nvpUU8RJ4O9EWRs7MpiayPFmD9f1WUTKedLbEVs=

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




Archive powered by MHonArc 2.6.18.

Top of Page