The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

Hello again all,

I am trying to prove some properties about relations that are defined as
inductive definitions and am not sure how it works. I have looked in the
previous Coq archives and found some discussion of the Scheme command for
generating the more general induction principles but I don't know how to
apply it correctly in my situation, described below:

First, I have two isomorphic inductive definitions with a simple
"base" constructor and a second constructor that takes as argument a list
of the set. (So you need to "Require PolyList." - I give the complete code
of my example at the end of this email):

Inductive DefA : Set
  := Abase : DefA
  |  Anext : (list DefA) -> DefA.

Inductive DefB : Set
  := Bbase : DefB
  |  Bnext : (list DefB) -> DefB.


Next, I define a relation which maps objects of one type to the other: but
this is actually two mutually recursive relations because of the list:

Mutual
Inductive RelAB : DefA -> DefB -> Prop
  := rel_base : (RelAB Abase Bbase)
  |  rel_next : (L:(list DefA); L':(list DefB))
               (RelListAB L L') ->
  (RelAB (Anext L) (Bnext L'))
with
RelListAB : (list DefA) -> (list DefB) -> Prop
  := rell_nil : (RelListAB (nil ?) (nil ?))
  | rell_cons : (a:DefA; b:DefB; L:(list DefA); L':(list DefB))
               (RelAB a b) ->
               (RelListAB L L') ->
  (RelListAB (cons a L) (cons b L'))
.


Now, what I want to prove is that this relation is actually a function:

Theorem relfunc
  : (a:DefA; b,b':DefB)
    (RelAB a b) ->
    (RelAB a b') ->
    b=b'.

I know in this case the mapping can probably be defined directly as mutual
Fixpoint functions, but what I'm really trying to do is a bit more complex
that the example given above. If someone's willing to look at the more
complicated thing I'm trying to do, I'll be more than willing to send you
the problem.

Thanks for all help,
--- nadeem