The Coq mailing list

[Anders Lundstedt <anders AT anderslundstedt.se>]

Background: I am formalizing some first order logic. Any term in n
variables can naturally also be seen as a a term in m variables for
m>n.

I have played around with coercions and identity coercions to solve
the following, but with no success. Reading the manual I get the
impression that at least the first two problems should be possible to
solve.

Consider the following.

  Parameter term : nat -> Type. (* n-ary terms *)
  Parameter tuple : nat -> Type. (* tuple n is a tuple of n-ary terms *)
  Parameter makeTuple : forall n, term n -> term n -> tuple n.

(1) In particular, I would like to be able to solve the following
problem of coercing constants to unary terms
(http://pastebin.com/TBYEi2V6):

  Parameter constToUnary : term 0 -> term 1. (* constant term to unary term *)

  Parameter c : term 0.
  Parameter x : term 1.

  Check (makeTuple 1 (constToUnary c) x). (* OK *)
  Check (makeTuple 1 c x). (* how do I get c coerced to a unary term here? *)

(2) More generally I would like to coerce any n-ary term to a
(n+1)-ary term (http://pastebin.com/UQY1Xw99):

    Parameter promote : forall {n}, term n -> term (S n). (* n-ary to
(n+1)-ary *)

    Parameter c : term 0.
    Parameter x : term 1.

    Check (makeTuple 1 (promote c) x). (* OK *)
    Check (makeTuple 1 c x). (* how do I get c coerced to a unary term here? 
*)

(3) Even more generally, is it possible to get all coercions term n
>-> term m for m>n using the promote function from (2)
(http://pastebin.com/YGnNF1NH):

    Parameter c : term 0.
    Parameter x : term 2.

    Check (makeTuple 2 (promote (promote c)) x). (* OK *)
    Check (makeTuple 2 c x). (* how do I get c coerced from constant
to unary to binary? *)


Best regards,

Anders Lundstedt