Preuves avec propriétés inductives

L'auteur de ce sujet a trouvé une solution à son problème.
Auteur du sujet

Bonjour à tous,

J'essaie de me (re)mettre intensivement à Coq, notamment en me mangeant le Coq'Art. Je commence à jouer avec les propriétés inductives, mais j'ai beaucoup de mal à les utiliser dans le cadre de preuves.

Un exemple « simple » de mon problème.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
Inductive last (A:Set)(a:A): list A  Prop :=
  | lastone: last a (a :: nil)
  | lastx:  x l, last a l  last a (x :: l).

Fixpoint last_fun (A:Set)(l:list A) :=
  match l with
    | nil => None
    | a :: nil => Some a
    | a :: r => last_fun r
  end.

Lemma last_last:  A:Set,  l:list A,  a:A, last a l  last_fun l = Some a.
Proof.
  intros A l a H.
  induction l.
  inversion H.

Qed.

Je me retrouve avec ce but :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
1 subgoal

A : Set
a0 : A
l : list A
a : A
H : last a (a0 :: l)
IHl : last a l → last_fun l = Some a

======================== ( 1 / 1 )
last_fun (a0 :: l) = Some a

Un peu d'aide ? ;_;

Merci beaucoup d'avance !

Édité par lethom

Staff

Cette réponse a aidé l'auteur du sujet

Tu devrais corriger tes définitions. Voici ce que j'ai utilisé :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
Require Export List.


Inductive last (A:Set)(a:A): list A -> Prop :=
  | lastone: last A a (a :: nil)
  | lastx: forall x l, last A a l -> last A a (x :: l).

Fixpoint last_fun (A:Set)(l:list A) :=
  match l with
    | nil => None
    | a :: nil => Some a
    | a :: r => last_fun A r
  end.

Ensuite, j'avoue que je ne suis jamais allé trop loin dans Coq'Art, j'ai toujours préféré Software Foundations. Et ce dernier donne un conseil pour ce genre de preuve : ton induction, tu ne veux pas la faire sur ta liste, mais sur ta définition inductive directement.

C'est à dire que tu feras quelque chose du genre

1
induction H

Il y a une bonne raison pour cela mais il faudrait que je retrouve le lien car à froid je ne aurais l'expliquer.

+0 -0

Cette réponse a aidé l'auteur du sujet

Lu'!

Du coup j'ai refait du Coq (je te hais).

La preuve est effectivement plus facile en faisant l'induction sur la propriété, mais tu as quand même une analyse par cas à faire sur la liste. Dans l'idée :

  • induction sur "last",
  • premier cas trivial,
  • deuxième cas : deux possibilités
  • le reste de la liste est vide, une hypothèse est fausse.
  • il reste des choses dans la liste, on la réécrit en appliquant un tour de last_func et on obtient une des hypothèse.

First : Always RTFM - "Tout devrait être rendu aussi simple que possible, mais pas plus." A.Einstein

+0 -0

Cette réponse a aidé l'auteur du sujet

Bonjour,

Quand tu as un prédicat inductif ça donne des preuves plus simples de faire l'induction dessus quand c'est possible. Ci-dessous deux preuves de ta propriété, l'une par induction sur le prédicat et l'autre sur la liste.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
Require Import Coq.Unicode.Utf8.
Require Import Coq.Lists.List.
Import ListNotations.

Inductive last {A:Set} (a:A): list A  Prop :=
  | lastone: last a (a :: nil)
  | lastx:  x l, last a l  last a (x :: l).

Fixpoint last_fun {A:Set} (l:list A) :=
  match l with
    | nil => None
    | a :: nil => Some a
    | a :: r => last_fun r
  end.

Lemma last_last:  (A:Set) (l:list A) (a:A), last a l  last_fun l = Some a.
Proof.
  intros A l a H.
  induction H as [|a'].
  + simpl.
    reflexivity.
  + destruct l as [|a'' l'].
    * exfalso.
      inversion H.
    * simpl.
      simpl in IHlast.
      assumption.
Qed.

Lemma last_last_alt:  (A:Set) (l:list A) (a:A), last a l  last_fun l = Some a.
Proof.
  intros A l a H.
  induction l as [|h t].
  + exfalso.
    inversion H.
  + destruct t as [|h' t'].
    * simpl.
      inversion H.
      - reflexivity.
      - exfalso.
        inversion H1.
    * inversion H.
      pose (IHt H1) as IH.
      simpl.
      simpl in IH.
      assumption.
Qed.

Après tu te compliques la vie car avec le prédicat défini comme il l'est, à chaque fois que tu auras un lastx tu vas avoir besoin de justifier que ton l ne peut pas être la liste vide puisqu'on a last a l (c'est pourquoi j'ai des exfalso qui trainent)… Ce serait plus simple de rendre cette information explicite :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
Require Import Coq.Unicode.Utf8.
Require Import Coq.Lists.List.
Import ListNotations.

Inductive last {A:Set} (a:A): list A  Prop :=
  | lastone: last a (a :: nil)
  | lastx:  h h' t', last a (h' :: t')  last a (h :: h' :: t').

Fixpoint last_fun {A:Set} (l:list A) :=
  match l with
    | nil => None
    | a :: nil => Some a
    | a :: r => last_fun r
  end.

Lemma last_last:  (A:Set) (l:list A) (a:A), last a l  last_fun l = Some a.
  intros A l a H.
  induction H as [|h h' t'].
  + simpl.
    reflexivity.
  + simpl.
    simpl in IHlast.
    assumption.
Qed.

Note que ça rend les inversions plus simples dans le cas où on a H : last a (x :: nil), maintenant on sait directement que H a forcément été construit avec lastone.

Édité par dentuk

+1 -0
Auteur du sujet

Merci ! Je ne savais pas si j'allais avoir des réponses, mais je suis heureux de voir que des gens touchent à Coq dans le coin. Je risque de venir vous embêter souvent :3.

@Saroupille : je ne vois pas trop la différence entre ta version et la mienne, à part que j'utilise l'UTF8 ;o.

@Ksass`Peuk : intuitivement, je voyais en effet qu'il fallait faire ça, mais il me manque encore les bons automatismes pour conduire correctement mes preuves.

@dentuk : Eh, merci pour les explications. Déjà, j'avais oublié comment présenter correctement mes preuves, mais les + ou *, ça rend les choses vraiment lisibles.

Je vais étudier vos différentes preuves à tête reposée, dans tous les cas. Ça me fera du bien de voir un peu du code coq d'autres gensses.

Auteur du sujet

C'est encore moi ;D.

Nouvelle difficulté et après avoir bien cherché par moi-même (merci encore pour vos différentes réponses, d'ailleurs !), je rends les armes.

Je veux prouver que deux entiers sont soit égaux, soit différents. J'ai donc décidé de faire une induction sur ces deux entiers (je ne vois pas comment commencer autrement).

Peu importe ma façon de faire, j'arrive à résoudre les trois premiers sous-buts, mais pas le dernier. Un peu d'aide serait appréciée <3.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
Definition eq_dec(A:Type) :=  x y:A, {x = y}+{x  y}.

(* TODO *)
Lemma eq_nat_dec: eq_dec nat.
Proof.
  induction x; induction y.
  + left; trivial.
  + right; discriminate.
  + right; discriminate.
  + inversion IHy.
    * rewrite H.
      right; omega.
    * (* ?? *)

Le but sur lequel je coince :

1
2
3
4
5
6
7
IHx : ∀ y : nat, {x = y} + {x ≠ y}
y : nat
IHy : {S x = y} + {S x ≠ y}
H : S x ≠ y

======================== ( 1 / 1 )
{S x = S y} + {S x ≠ S y}

Cette réponse a aidé l'auteur du sujet

Un peu de lecture liée : https://fr.wikipedia.org/wiki/Logique_intuitionniste et https://fr.wikipedia.org/wiki/Calcul_des_constructions . Ça ne s'applique en fait pas ici, parce que pour nat l'égalité est décidable, mais dans le cas général note que tu ne peux pas montrer ça en Coq sans ajouter un axiome.

Edit : pour ta preuve, la solution est de garder b généralisé quand tu fais l'induction sur a, et de ne l'introduire qu'après. Un exemple :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
Lemma eq_neq : forall a b : nat, {a = b} + {a <> b}.

Proof.
intro a.
induction a; intro b; destruct b.
left. trivial.
right. discriminate.
right. discriminate.
elim (IHa b); intro.
left. rewrite a0. trivial.
right. injection. intro. contradict b0. assumption.
Qed.

Édité par anonyme

+0 -0
Auteur du sujet

Encore une petite question o/. Je ne comprends finalement pas la notation { _ } + { _ } et surtout ce qu'elle a à faire avec le côté décidable.

Après tout, j'arrive à prouver ça :

1
2
3
4
Lemma try: { True } + { True }.
Proof.
  intuition.
Qed.

On s'attendrait plutôt à ce que ça soit impossible, non ? (et que ça se comporte plutôt comme un xor booléan)

Cette réponse a aidé l'auteur du sujet

Salut,

{A} + {B} a exactement la même définition que A \/ B à ceci près que le premier vit dans Set et le second dans Prop.

1
2
3
4
5
6
7
(* {A} + {B} *)
Inductive sumbool (A B : Prop) : Set :=
    left : A -> sumbool A B | right : B -> sumbool A B.

(* A \/ B *)
Inductive or (A B : Prop) : Prop :=
    or_introl : A -> or A B | or_intror : B -> or A B.

Une valeur de type {A} + {B} (on parle d'habitant du type) vit dans Set et est soit left aa est une preuve de A, soit right bb est une preuve de B. Une valeur de type A \/ B vit dans Prop et est soit or_introl aa est une preuve de A, soit or_intror bb est une preuve de B.

Lors de l'extraction de programmes, tout ce qui vit dans Prop disparaît. C'est la partie dédiée à la spécification du programme, une fois qu'elle a été vérifiée par Coq elle encombre inutilement les calculs. Dans le cas de A \/ B, donc, or_introl b et or_intror a deviennent confondus, tu peux voir ça comme s'ils devenaient tous les deux () de type unit (en pratique __ de type __ qui sera viré à chaque fois que c'est possible). Dans le cas de { A } + { B } en revanche, on a left a qui devient Left et right b qui devient Right (a et b disparaissent bien, comme eux vivent dans Prop, mais pas les constructeurs qui eux vivent dans Set).

Pour que tout cela soit cohérent, il faut des restrictions lorsqu'on définit quelque chose qui vit dans Set : ce qu'on définit doit garder du sens une fois que tout ce qui vit dans Prop a disparu. Par exemple, on ne peut analyser une preuve de A \/ B que dans un contexte logique (i.e. pour définir quelque chose qui vivra également dans Prop), tandis qu'un habitant de { A } + { B } va pouvoir être détruit dans un contexte calculatoire (i.e. pour définir quelque chose qui vivra dans Set) pour regarder si c'est un left _ ou un right _.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
Definition foo : { True } + { ~ True } := left I.

Extraction foo.

(** val foo : sumbool **)

(**
let foo =
  Left
**)

Definition bar : True \/ (~ True) := or_introl I.

Extraction bar.

(** val bar : __ **)

(**
let bar =
  __
 **)

Definition foobar : nat :=
  match foo with
    | left _ => 0
    | right _ => 1
  end.

Extraction foobar.

(** val foobar : nat **)

(**
let foobar =
  match foo with
  | Left -> O
  | Right -> S O
**)

Fail Definition barfoo : nat :=
  match bar with
    | or_introl _ => 0
    | or_intror _ => 1
  end.

(**
The command has indeed failed with message:
=> Error:
   Incorrect elimination of "bar" in the inductive type "or":
   the return type has sort "Set" while it should be "Prop".
   Elimination of an inductive object of sort Prop
   is not allowed on a predicate in sort Set
   because proofs can be eliminated only to build proofs.
**)

Le rapport avec la décidabilité c'est quand, pour P : Prop, tu regardes P \/ (~ P) et { P } + { ~ P}. Est-ce que tu peux définir des habitants pour ces types ? Si oui P est décidable, soit au niveau logique pour \/, soit au niveau calculatoire pour { _ } + { _ }.

En effet si tu as un habitant de P \/ (~ P), c'est soit une preuve de P, soit une preuve de ~ P. Donc cet habitant témoigne de lui-même de la décidabilité de P : si tu l'as, alors dans n'importe quel contexte logique tu peux décider si P est vraie ou si ~ P est vraie en détruisant cet habitant.

C'est exactement la même chose avec { P } + { ~ P } sauf que maintenant tu vas pouvoir utiliser l'information dans tes calculs, en regardant si l'habitant est un left _ (dans ce cas on sait que P est vraie) ou un right _ (on sait que ~ P est vraie).

NB: J'ai pris une vue centrée sur l'extraction de programmes car c'est comme ça que je comprends ces distinctions mais il y sûrement d'autres raisonnements plus mathématiques.

Édité par dentuk

+0 -0
Staff

@Dentuk : Même si je comprend ton exemple, tu as un exemple concret où cette différence joue un rôle ? C'est à dire dans un cas tu préfères vivre dans la sorte Prop et dans l'autre cas, tu préfères être dans Set (par rapport à ce point de vue de décidabilité.

+0 -0

Cette réponse a aidé l'auteur du sujet

@Dentuk : Même si je comprend ton exemple, tu as un exemple concret où cette différence joue un rôle ? C'est à dire dans un cas tu préfères vivre dans la sorte Prop et dans l'autre cas, tu préfères être dans Set (par rapport à ce point de vue de décidabilité.

Saroupille

A priori dans le cas de la décidabilité, quand c'est possible, tu as tout intérêt à la définir en termes de { P } + { ~ P }, car on peut passer de { A } + { B } à A \/ B sans problème (c'est dans l'autre sens que ça coince).

1
2
3
4
Lemma comp_dec_imp_log_dec : forall (P:Prop), { P } + { ~ P } -> P \/ ~ P.
Proof.
  intros P [p|np]; [left | right]; assumption.
Qed.

Le cas qui me vient à l'esprit où ça ne serait pas possible d'utiliser { P } + { ~ P }, c'est celui où ta preuve de P \/ ~ P requiert elle-même de détruire quelque chose qui vit dans Prop. Dans ce cas tu ne peux pas l'écrire en termes de { P } + { ~ P } qui vit dans Set. Par exemple, si tu veux travailler en logique classique et que du coup tu t'autorises le tiers-exclus dans Prop, tu ne pourras pas l'exploiter pour des preuves de { P } + { ~ P}, car ça te demanderait de faire une analyse par cas sur quelque chose qui vit dans Prop pour définir un résultat dans Set. Par contre tu n'auras aucun problème à prouver P \/ ~ P par définition du tiers-exclus.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
Axiom excluded_middle : forall (P:Prop), P \/ ~ P.

Lemma comp_excluded_middle : forall (P:Prop), { P } + { ~ P }.
Proof.
  intros P.
  pose (excluded_middle P) as H.
  Fail destruct H.
(*
The command has indeed failed with message:
=> Error: Case analysis on sort Set is not allowed for inductive definition
   or.
 *)
Abort.

Édité par dentuk

+0 -0
Vous devez être connecté pour pouvoir poster un message.
Connexion

Pas encore inscrit ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte