The Coq mailing list

[Pierre Casteran <casteran AT labri.u-bordeaux.fr>]

Hello, I made a draft proof of your Theorem. It certainly can be written
more elegantly,
but it works. I began to derive an induction scheme for your both
relationships, then used
many inversions to finish the proof .


Please notice i changed slightly to order of your quantifiers to make
easier the proof by induction,
but that doesn't change the result at all.

Here is the complete proof.

Best regards,
Pierre



Require PolyList.


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

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



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'))
.


Check RelAB_ind.
Check RelListAB_ind.
Scheme induc1 := Minimality for RelAB Sort Prop
with   induc2 := Minimality for RelListAB Sort Prop.

Check induc1.
(*
    : (P:(DefA->DefB->Prop); P0:((list DefA)->(list DefB)->Prop))
        (P Abase Bbase)
        ->((L:(list DefA); L':(list DefB))
            (RelListAB L L')->(P0 L L')->(P (Anext L) (Bnext L')))
        ->(P0 (nil DefA) (nil DefB))
        ->((a:DefA; b:DefB; L:(list DefA); L':(list DefB))
            (RelAB a b)
            ->(P a b)
            ->(RelListAB L L')
            ->(P0 L L')
            ->(P0 (cons a L) (cons b L')))
        ->(d:DefA; d0:DefB)(RelAB d d0)->(P d d0)
*)

Theorem relfunc
  : (a:DefA; b:DefB)
    (RelAB a b) ->
    (b':DefB)(RelAB a b') ->
    b=b'.
Proof.
 Intros a b  H.
 Apply induc1 with P0 := [L:(list DefA); L':(list DefB)] 
                          (L'':(list DefB))(RelListAB L L'')->L'=L''
                   P := [a:DefA ; b : DefB](b':DefB)(RelAB a b')->b=b' .
 Intros.
 Inversion H;Auto.
 Inversion_clear H0;Auto.
 Inversion_clear H0. 
 Auto.
 Intros.
 Inversion_clear H2;Intros.
 Elim (H1 L'0 H3);Auto.
 Intros.
 Inversion H0;Auto.
 Intros.
 Inversion_clear H4;Intros.
 Elim (H1 b1 H5).
 Elim (H3 L'0 H6).
 Auto.
 Auto.
Qed.





Nadeem Abdul Hamid a écrit :
> 
> 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

-- 
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |   
351 Cours de la Liberation        |   
F-33405 TALENCE Cedex             |   
France                            |   
tel : (+ 33) 5 56 84 69 31
fax : (+ 33) 5 56 84 66 69
email: Pierre . Casteran @ labri . u-bordeaux . fr  (but whithout white
space)
www: http://dept-info.labri.u-bordeaux.fr/~casteran