The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

Jean Goubault-Larrecq me fait remarquer a juste titre que mon
affirmation 
  " si nat n'etait pas le plus petit ensemble clos par O et S,
    alors on pourrait construire un terme tel que n=(S n) "
est erronee
Ce qui est correct est que 
        si nat est le plus grand point fixe avec O et S comme
constructeurs (CoInductive en Coq) alors on peut
construire un terme tel que n = (S n)
et que la preuve de n <> S n s'appuie sur le principe d'induction.

Christine Paulin

Christine Paulin writes:
 > Ce n'est pas une preuve evidente, mais le lemme existe dans la
 > bibliotheque n_Sn : (n:nat)n<>Sn
 > Apply (n_Sn n); Auto devrait resoudre votre but
 > 
 > Discriminate fonctionne sur une hypothese de la forme 
 >      c1=c2 
 > ou c1 et c2 debutent par des constructeurs differents 
 > ce qui n'est pas votre cas.
 > 
 > En fait si nat n'etait pas le plus petit ensemble clos par O et S,
 > alors on pourrait construire un terme tel que n=(S n)
 > La preuve que ce n'est pas possible s'appuie donc sur la structure
 > inductive de nat.
 > Pour n=O : O<>S O est resolu par discriminate
 > puis sion suppose  n<>(S n), on montre (S n)<>(S (S n)) 
 > en supposant (S n)=(S (S n)) dont on deduit n=(S n) (Tactique
 > Injection) et finalement une contradiction avec l'hypothese de
 > recurrence.
 > 
 > Christine Paulin
 >      
 > -- 
 >   Christine Paulin-Mohring             mailto : 
 >Â Christine.Paulin AT lri.fr
 >   LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
 >   tel : (+33) (0)1 69 15 66 35         fax : (+33) (0)1 69 15 65 86
 > 
 > 
 > 
 > 
 > 
 > 
 > 
 > --------------------------------------------------------
 > Bug reports: http://coq.inria.fr/bin/coq-bugs
 > Archives: http://pauillac.inria.fr/pipermail/coq-club
 >           http://pauillac.inria.fr/bin/wilma/coq-club
 > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  tel : (+33) (0)1 69 15 66 35         fax : (+33) (0)1 69 15 65 86