coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Building a constructive term from inside an ML tactic, Kenneth Roe, 04/10/2018
- Re: [Coq-Club] Building a constructive term from inside an ML tactic, Talia Ringer, 04/10/2018
- Re: [Coq-Club] Building a constructive term from inside an ML tactic, Emilio Jesús Gallego Arias, 04/11/2018
- Re: [Coq-Club] Building a constructive term from inside an ML tactic, Talia Ringer, 04/10/2018
Archive powered by MHonArc 2.6.18.