Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Trouble with coercions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Trouble with coercions


Chronological Thread 
  • From: Gabriel Scherer <gabriel.scherer AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Trouble with coercions
  • Date: Sat, 27 Sep 2014 19:18:30 +0200

Situation (1) (coercion from n to n+1) works by just declaring the coercion as the manual says:
  http://coq.inria.fr/coq/refman/Reference-Manual021.html

  Coercion promote : term >-> term.
 
  Check (makeTuple 1 c x). (* 0->1: ok *)
  Check (makeTuple 2 x x). (* 1->2: ok *)
  Check (makeTuple 2 c x). (* 0->2: fails *)

You should think of coercions as a mechanism for convenience only -- rather than expect it will always work in the ideal way.


On Sat, Sep 27, 2014 at 6:48 PM, Anders Lundstedt <anders AT anderslundstedt.se> wrote:
Here is another example, which I think is closely related to my
problem (1). http://pastebin.com/CWwWvPRu

  Parameter A : nat -> Type.
  SubClass A0 := A 0.
  SubClass A1 := A 1.
  Parameter A0toA1 :> A0 -> A1.
  Print Graph.
  (* we now have coercions A0,A1 >-> A and A0  >-> A1 *)

  Parameter (a0 : A 0) (a1 : A 1).
  Parameter (a0' : A0) (a1' : A1).
  Parameter f : A 1 -> Type.
  Parameter f' : A1 -> Type.

  (* term of type A0 when term of type A1 expected: *)
  Check (f' a0'). (* OK *)

  (* possible to avoid casts below, e.g. get "f a0'" to typecheck? *)

  (* term of type A0 when type of A 1 expected: *)
  Check (f (a0' : A1)).

  (* term of type A 0 when term of type A1 expected: *)
  Check (f' (a0 : A0)).

  (* term of type A 0 when term of type A 1 expected: *)
  Check (f ((a0 : A0) : A1)). (* note: double cast needed! *)




Archive powered by MHonArc 2.6.18.

Top of Page