coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coercing a type to different constructors of an inductive type

From: Erkki Luuk <erkkil AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Coercing a type to different constructors of an inductive type
Date: Sat, 8 Apr 2017 21:52:53 +0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=erkkil AT gmail.com; spf=Pass smtp.mailfrom=erkkil AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f176.google.com
Ironport-phdr: 9a23:ZN/avxHOVp0pjS59PALeAJ1GYnF86YWxBRYc798ds5kLTJ79ocuwAkXT6L1XgUPTWs2DsrQf2raQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbQhFgDWwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOT43/m/Ul8J+kr5UrQm7qBBj2YPZep2ZOOZ8c67bYNgURXBBXsFUVyFZDY28dYgPD+kAPe1FqYf9ukYOrRijDgSrGuzv0DxIhnz33a0+yOkhHgTG0xYhH9IKqnjbsNL1NKILXO2z0aLGzi3DYutI1Tvh7IXEaBMsrPGWUb5ubMbcyFMjGx7Hg1iRr4HuIimb2f4Xs2eB6uptTeKvhHAjqwF2ujWvw90jiojNho4M01DE6Tl1zJ87JdGlSkN2YMSoEJRXtyGdOIt2Rt0tT3t0tyY9z70KoZ+7fC4Ux5Q73xPTdeCLfoyS7h/gVOudOyl0iG9kdb6lmhq/80mtxvX5Vsau0VZKqiRFksPLtnAIzxHc9NKHSvh+/keg3TaCzA/T6uReLkA1karXMYIuwrk1lpYLq0TMAjf2mFnqjK+Rbkgr5u+o6/3+brr6op+cKpR7hxrlMqUun8y/Gf43PhIPX2id4+S81afs8Vf3QLVQ3bUKlfzSt4mfLsAGrIa4BRVU28At8UWRFTCjhfkCnnoGZHZYZRHP24XzOFLPJNj3CP6+hxKnlzI9lKOOBaHoHpiYdiuLq7zmZ7sos0M=

Dear all

Is it possible to coerce a type A to different constructors of an inductive type B? The problem arises in various contexts (the coerced type can be e.g. a record, subset or fixpoint). Below is a minimal example w/ a record:

Inductive R := r | s.

Variable rt:> R -> Type.

Record RS := { c:> r; c0:> s }.

Variable rs:RS.

Check rs:r. Fail Check rs:s. (*!*)

Print Graph. (* [rt] : R >-> Sortclass. [c] : RS >-> rt *)

There's no warning or error, but c0 isn't registered (presumably because it would have the same path as c)

Kind regards

Erkki

[Coq-Club] Coercing a type to different constructors of an inductive type, Erkki Luuk, 04/08/2017