[Coq] établir preuve : équivalence de 2 ordres

[minhkhue]

J'ai commencé à peine 1 semaine avec Coq. Je dois établir des preuves pour prouver l'équivalence deux notions.

Code :

1
2
3
4
5
Inductive sorted_i : list nat -> Prop :=
    sorted_i_nil : sorted_i nil
  | sorted_i_cons : forall (a : nat) (l : list nat),
                    (forall b : nat, In b l -> a <= b) ->
                    sorted_i l -> sorted_i (a :: l)

et

Code :

1
2
3
4
5
6
sorted_d = 
fun l : list nat =>
forall i j : nat,
i < j ->
forall a b : nat, nth_error l i = Some a -> nth_error l j = Some b -> a <= b
     : list nat -> Prop

Donc je dois montrer un Lemme qui est :

Code :

Lemma sortedEq : forall l, sorted_i l <-> sorted_d l.

J'ai commencé par :

Code :

1
2
3
Proof.
split.
intros.

pour découper l'équivalence, et puis monter les introductions.
Mais ensuite, je me suis bloqué car je n'ai aucune idée pour quel tactique sur quel truc à applique.
J'ai essayé avec

Code :

intros sorted_d.

Coq l'a monté comme un sorted_d : nat en haut et laisse en bas le corps de sorted_d.
Mais après, vraiment, je suis perdu. Quelqu'un pourrait me donner un coup de main?

[SpiceGuid]

Quand on a une propriété construite de façon inductive, généralement (ma connaissance de Coq est très très superficielle et très empirique) on la détruit avec induction.
induction l
Après on doit prouver le lemme pour le cas de base sorted_i_nil puis pour le cas inductif sorted_i_cons.

Après, je dis ça je dis rien hein, si c'est pas ça alors c'est autre chose, va savoir quoi

Envoyé par minhkhue

Mais ensuite, je suis bloqué car je n'ai aucune idée pour quelle tactique sur quel truc à appliquer.

Alors on est au moins deux !
Quand tu sens que tu es allé dans une impasse tu peux annuler la(les) dernière(s) commande(s) avec Undo.

[gorgonite]

tu connais forcément replace

connais-tu la commande unfold ?
http://coq.inria.fr/V8.1/tutorial.html

selon moi, il te faudra aussi inversion
http://coq.inria.fr/refman/Reference...013.html#toc75

et prouver

Code :

1
2
Lemma egal_some: (T:Set) (a,b:T) ((Some ? a)=(Some ? b)) -> (a=b).

au passage es-tu sûr de sorted_d ?

je verrais plutôt ceci :

Code :

1
2
3
4
5
6
7
Definition sorted_d : list nat -> Prop := 
fun l : list nat => l = nil \/ 
forall i j : nat, 
i < j ->
forall a b : nat, nth_error l i = Some a -> nth_error l j = Some b -> a <= b    
.

penses aussi à regarder le_refl dans Coq.Arith.Le

[gorgonite]

pour infos, j'ai essayé de la faire en entier... et je suis tombé sur un point non constructible :'(

mais peut-être y a-t-il une autre manière de procéder... je ne suis pas expert en Coq

[gasche]

Le problème ici est un problème de bibliothèques. Les spécifications utilisent d'une part "nth_error" et de l'autre "In", mais évidemment dans la lib standard de Coq il n'y a rien de déjà prêt sur le lien entre "nth_error" et "In", il faut faire à la main le lien entre "nth_error" et "nth", ce qui est très pénible (parce que "nth" est laid pour commencer), et ensuite passer de "In" à "nth". Ou alors faire directement la preuve soi-même.
Mais bref tout ça c'est réimplémenter un petit bout de la bibliothèque standard, et ça n'a rien à avoir avec le domaine qui nous concerne qui est de parler de listes triées.

gorgonite > ton ajout de "l = nil \/" n'est pas nécessaire puisque `sorted_d` est vraie en particulier pour une liste vide.

Je n'ai pas essayé donc je ne sais pas pour la constructivité, mais à priori c'est plutôt une question de comment les définitions sont posées. Normalement comme les deux listes sont finies on doit pouvoir tout faire constructivement.

[gorgonite]

Envoyé par bluestorm

gorgonite > ton ajout de "l = nil \/" n'est pas nécessaire puisque `sorted_d` est vraie en particulier pour une liste vide.

mathématiquement oui... pour la preuve, je ne vois pas trop comment m'en sortir pour démontrer en Coq qu'une chose est vraie pour tout élément d'un ensemble vide

Envoyé par bluestorm

Le problème ici est un problème de bibliothèques. Les spécifications utilisent d'une part "nth_error" et de l'autre "In", mais évidemment dans la lib standard de Coq il n'y a rien de déjà prêt sur le lien entre "nth_error" et "In", il faut faire à la main le lien entre "nth_error" et "nth", ce qui est très pénible (parce que "nth" est laid pour commencer), et ensuite passer de "In" à "nth". Ou alors faire directement la preuve soi-même.
Mais bref tout ça c'est réimplémenter un petit bout de la bibliothèque standard, et ça n'a rien à avoir avec le domaine qui nous concerne qui est de parler de listes triées.

[...]

Je n'ai pas essayé donc je ne sais pas pour la constructivité, mais à priori c'est plutôt une question de comment les définitions sont posées. Normalement comme les deux listes sont finies on doit pouvoir tout faire constructivement.

justement c'est cela que j'ai essayé... et je suis tombé sur un problème de constructivité, mais il y a peut-être une manière plus subtile

EDIT: en gros, une fois que je prouve ce lemme, je m'en sors... mais je n'y arrive pas

Code :

1
2
3
4
Lemma nth_not_error_impl_In :
  forall (b : nat) l,
  (exists n, nth_error l n = value b) ->
  In b l.

enfin, c'est dans ces situations où l'on comprend pourquoi il ne faut pas utiliser Coq si la constructivité n'est pas nécessaire... Isabelle/HOL est nettement plus adaptée pour faire des preuves non corrélées à des implantations

[gasche]

Non, c'est toi qui est obsédé par la constructivité. Si tu veux juste raisonner comme d'habitude sans te prendre la tête, tu ajoutes le tiers exclu, on en a déjà parlé, c'est consistent, c'est prévu par la bibliothèque standard (qui apporte des tactiques de raisonnement classique), etc. Sur ce point ton raisonnement n'est pas rationnel.
(Par ailleurs si tu t'intéresses à Isabelle/HOL c'est très bien, hein, il faut avoir une vision un peu large et essayer des alternatives; je veux bien croire qu'Isabelle/HOL soit plus agréable à utiliser que Coq, je n'en sais rien malheureusement, je n'ai pas encore essayé ces outils. Mais l'argument n'est pas "bouh on n'a pas le tiers exclu".)

mathématiquement oui... pour la preuve, je ne vois pas trop comment m'en sortir pour démontrer en Coq qu'une chose est vraie pour tout élément d'un ensemble vide

Ce n'est pas ce qu'il faut montrer ici. On te donne deux indices qui "ont des éléments" (nth_error renvoie Some) dans la liste vide, et on te demande de montrer quelque chose. Mais nth_error sur la liste vide renvoie toujours None, donc l'hypothèse qu'ils ont des éléments est fausse, donc implique n'importe quoi.

Code :

1
2
Goal sorted_d nil.
  intros i j Hij a b Ha Hb.

En regardant le code de nth_error on voit qu'il pattern-matche d'abord sur l'indice (si c'est 0 ou pas) et ensuite sur la liste, et que dans les deux branches du filtrage, la liste vide renvoie None. Pour exhiber la contradiction il faut donc commencer par détruire l'indice.

Code :

destruct i. simpl in Ha.

On a alors l'hypothèse ("error" veut dire None ici, c'est son nom dans la monade d'exception) :

Ha : error = Some a

La tactique `discriminate` voit la contradiction (deux constructeurs différents d'un inductif ne peuvent être égaux). En fait on peut l'utiliser dans les deux branches.

Code :

1
2
3
4
Goal sorted_d nil.
  intros i j Hij a b Ha Hb.
  destruct i; discriminate Ha.
Qed.

justement c'est cela que j'ai essayé... et je suis tombé sur un problème de constructivité, mais il y a peut-être une manière plus subtile.

Comme je l'ai déjà dit, il n'est pas nécessaire de se poser des questions philosophiques sur la constructivité en Coq. Si on a l'impression d'avoir un problème et qu'on ne veut *pas* se prendre la tête, on admet le tiers-exclu.
Cependant, ici, si tu as envie de faire ton puriste constructiviste, et c'est intéressant aussi, tu vois que la preuve qu'on te demande repose fondamentalement sur un objet fini. Tu as une liste "l" finie et tu veux montrer que si une condition décidable est vraie, alors une autre condition décidable est vraie. Il n'y a rien de non-constructif là-dedans, et un bon moyen de ne pas avoir d'ennui et de raisonner sur la liste qu'on sait finie.

Code :

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Lemma nth_not_error_impl_In :
  forall (b : nat) l n, nth_error l n = value b -> In b l.
  induction l.
  (* Cas nil *) destruct n; discriminate.
  (* Cas a::l *)
    destruct n.
    (* Cas 0 *)
      injection 1; intro H0.
      constructor; exact H0.
    (* Cas (S n) *)
      intro Hn.
      right.
      apply (IHl _ Hn).
Qed.

NB: j'ai viré le "exists" là parce qu'il alourdit la preuve en forçant à empaqueter/dépaqueter des types existentiels et qu'on n'en a de toute façon pas besoin dans l'exercice demandé, mais ça ne change rien à la prouvabilité.

[gorgonite]

Envoyé par bluestorm

Non, c'est toi qui est obsédé [... ] Sur ce point ton raisonnement n'est pas rationnel.

j'ai réservé ma place à l'asile, mais il y a une longue liste d'attente

Envoyé par bluestorm

Mais l'argument n'est pas "bouh on n'a pas le tiers exclu".

l'argument serait plutôt... quand j'ai besoin de quelque chose, y a sûrement le système logique ad-hoc déjà tout prêt à utiliser

Envoyé par bluestorm

La tactique `discriminate` voit la contradiction (deux constructeurs différents d'un inductif ne peuvent être égaux). En fait on peut l'utiliser dans les deux branches.

ok c'est celle qui me manquait... depuis si longtemps

Envoyé par bluestorm

Cependant, ici, si tu as envie de faire ton puriste constructiviste, et c'est intéressant aussi,

ben c'est à mes yeux le seul intérêt de Coq... pour le reste il y a d'autres outils plus agréables selon moi

Envoyé par bluestorm

tu vois que la preuve qu'on te demande repose fondamentalement sur un objet fini. Tu as une liste "l" finie et tu veux montrer que si une condition décidable est vraie, alors une autre condition décidable est vraie. Il n'y a rien de non-constructif là-dedans, et un bon moyen de ne pas avoir d'ennui et de raisonner sur la liste qu'on sait finie.

j'étais parti aussi sur cette voie, mais différemment... à croire que j'adore me recréer le même pattern planteur

en tout cas, tu utilises des tactiques de plus haut niveau que moi, ce qui raccourcit considérablement les preuves. il faut avouer que je me sers juste des bases... c'est carrément pas mon domaine (je suis plus dans l'interprétation abstraite et l'exécution symbolique )

Envoyé par bluestorm

NB: j'ai viré le "exists" là parce qu'il alourdit la preuve en forçant à empaqueter/dépaqueter des types existentiels et qu'on n'en a de toute façon pas besoin dans l'exercice demandé, mais ça ne change rien à la prouvabilité.

ok ce n'était pas l'exercice ici, mais aurais-tu un lien qui montre cet alourdissement ?

[gasche]

Code :

1
2
3
4
5
6
7
8
9
10
11
12
Lemma nth_not_error_impl_In_exists :
  forall (b : nat) l, (exists n, nth_error l n = value b) -> In b l.
  induction l.
  (* Cas nil *)
    destruct 1 as [n Hn]. destruct n; discriminate.
  (* Cas a::l *)
    destruct 1 as [n Hn]. destruct n.
      injection Hn; intro H0.
      constructor; exact H0.
      right. apply IHl.
      exists n. apply Hn.
Qed.

[gorgonite]

au fait minhkhue, où en es-tu ?

parce qu'on parle (j'ai un peu fait digressé le sujet), mais on ne sait pas si de ton côté ça avance ?

as-tu au moins compris où allait servir nth_not_error_impl_In ?

en gros, à un moment, avec les tactiques que je t'ai citées (bluestorm ferait sûrement mieux en moins de ligne mais bon ), tu vas arriver à un stade de ce style:

Code :

1
2
3
4
5
6
7
8
9
10
11
a : nat
l : list nat
H : sorted_i (a :: l)
a0 : nat
b : nat
H2 : nth_error (a :: l) (S n) = value b
H4 : a = a0
H5 : nth_error l n = value b
H7 : forall b : nat, In b l -> a <= b
______________________________________(1/3)
a0 <= b

c'est juste un petit coup de pouce (les grandes lignes pour arriver jusqu'à un point où son utilité saute aux yeux)

dis-nous où tu en es...

[gasche]

PS : je suis flatté d'entendre dire de mon code Coq "il utilise des techniques avancées, moi je fais avec les outils de base", parce que c'est ce que je passe mon temps à me dire du code *des autres*. Comme quoi tout est une question de point de vue :p

Je ne l'ai pas fait dans le code de mon développement ci-dessus, car c'était juste un petit hack temporaire pour vérifier (et de préférence contredire hein, sinon c'est pas drôle) ce que disait gorgonite, mais j'encourage l'utilisation des macros "Case", que je tire du cours Software Foundations de Benjamin Pierce (c'est LE document pour apprendre Coq par la pratique, avec le Coq'Art éventuellement si vous avez la chance d'avoir une copie papier). La définition des macros en question est ici, et ça s'utilise comme ça :

Code :

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Lemma nth_not_error_impl_In :
  forall (b : nat) l n, nth_error l n = value b -> In b l.
  induction l.
  Case "nil". destruct n; discriminate.
  Case "a::l".
    destruct n.
    SCase "0".
      injection 1; intro H0.
      constructor; exact H0.
    SCase "S n".
      intro Hn.
      right.
      apply (IHl _ Hn).
Qed.

[gorgonite]

Envoyé par bluestorm

cours Software Foundations de Benjamin Pierce (c'est LE document pour apprendre Coq par la pratique, avec le Coq'Art éventuellement si vous avez la chance d'avoir une copie papier).

au fait y a-t-il une version pdf de ce cours en ligne ?

[TropMDR]

Envoyé par gorgonite

mathématiquement oui... pour la preuve, je ne vois pas trop comment m'en sortir pour démontrer en Coq qu'une chose est vraie pour tout élément d'un ensemble vide

Euh, vraiment ?

Code :

1
2
3
4
5
6
7
8
9
10
11
12
13
Goal forall A (x:A) P, In x nil -> P x.
Proof.
  intros * IN.
  inversion IN.
Qed.

Require Import Ensembles.

Goal forall A (x:A) P, In _ (Empty_set A) x -> P x.
Proof.
  intros * IN.
  inversion IN.
Qed.

Envoyé par gorgonite

justement c'est cela que j'ai essayé... et je suis tombé sur un problème de constructivité, mais il y a peut-être une manière plus subtile

Ca m'intéresserait beaucoup de tomber sur un "problème de constructivité" quand tu fais une preuve sur les listes. Ce sont des ensembles finis, que l'on peut trivialement parcourir.

Envoyé par gorgonite

enfin, c'est dans ces situations où l'on comprend pourquoi il ne faut pas utiliser Coq si la constructivité n'est pas nécessaire... Isabelle/HOL est nettement plus adaptée pour faire des preuves non corrélées à des implantations

Dans toutes les preuves que j'ai faites, la constructivité n'a pour ainsi dire jamais été un problème. Les seuls axiomes dont j'ai eu besoin, ça a été extensionnalité et proof irrelevence. Je veux bien que tu me cites des "vrais" problèmes...

[TropMDR]

Envoyé par gorgonite

au fait y a-t-il une version pdf de ce cours en ligne ?

Ca ne correspondrait pas du tout à l'esprit, qui est de jouer le code et de compléter les preuves.

[gasche]

D'ailleurs TropMDR je me souviens être tombé il y a quelques temps sur une page assez cool liée à Software Foundations, des gens avaient codé une variante de "coqdoc" telle que quand on passe la souris sur la preuve, à côté tu as les buts qui défilent selon la tactique sur laquelle tu es. Malheureusement j'ai cherché à retrouver cette démo récemment, et pas moyen.... Si jamais tu as un lien, ça m'intéresse.

[TropMDR]

Proof general 4 fait ça. Pour le reste, je ne sais pas !