Discussion :

[SpiceGuid]

Comme semble-t-il beaucoup de débutants en Coq j'ai moi aussi commencé à jouer avec les axiomes de groupe.
Et comme tous les débutants en Coq j'arrive à faire tout ce qui est facile mais je butte à la première vraie difficulté.

D'abord quelques banalités.

Code Coq :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
Module Relation.
  
  Section relations.
  
  Variable U : Set.
  Definition Relation := U -> U -> Prop.
  Variable R : Relation.
  
  Definition reflexive :=
    forall x, R x x.  
  Definition transitive :=
    forall x y z, R x y -> R y z -> R x z.
  Definition symmetric :=
    forall x y, R x y -> R y x.
  
  End relations. 
 
End Relation.

Code Coq :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
Module Operation.

  Section operations.
  
  Variable U : Set.
  Definition Operation := U -> U -> U.
  Variable Op : Operation.

  Definition associative :=
    forall x y z, Op x (Op y z) = Op (Op x y) z.  
  Definition commutative :=
    forall x y, Op x y = Op y x.
  Definition neutral e :=
    forall x, Op e x = x.
  Definition symmetric S e :=
    forall x, Op (S x) x = e.

  End operations. 
 
End Operation.

Le type-module des groupes:

Code Coq :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Module Type Group.

  Import Operation.

  Parameter U: Set.  
  Parameter law:  Operation U.  
  Parameter unit: U.
  Parameter inverse: U -> U.

  Axiom group_associative: associative U law. 
  Axiom group_neutral:     neutral U law unit. 
  Axiom group_symmetric:   symmetric U law inverse unit.
 
End Group.

Enfin, le groupe des transformations du Rubik's Cube (le petit modèle Rubik Pocket 2 x 2 x 2):

Code Coq :

Sélectionner tout - Visualiser dans une fenêtre à part

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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
Module Rubik2Group <: Group.

  (* les suites de rotations *)
  Inductive transform : Set :=
    | Take:   transform  (* prendre le cube et ne rien faire *)  
    | Back:   transform -> transform 
    | Right:  transform -> transform 
    | Down:   transform -> transform
    | Back':  transform -> transform 
    | Right': transform -> transform 
    | Down':  transform -> transform.

  Definition U := transform.

  (* les simplifications sur les rotations *)
  Axiom involutive_back:   forall x, Back (Back' x) = x.  
  Axiom involutive_right:  forall x, Right (Right' x) = x.  
  Axiom involutive_down:   forall x, Down (Down' x) = x.  
  Axiom involutive_back':  forall x, Back' (Back x) = x.  
  Axiom involutive_right': forall x, Right' (Right x) = x.  
  Axiom involutive_down':  forall x, Down' (Down x) = x.

  (* la loi est la composition de deux transformations *)
  Fixpoint law t1 t2 {struct t1} :=
    match t1 with
    | Take     => t2
    | Back t   => Back   (law t t2)
    | Right t  => Right  (law t t2)
    | Down t   => Down   (law t t2)
    | Back' t  => Back'  (law t t2)
    | Right' t => Right' (law t t2)
    | Down' t  => Down'  (law t t2)
    end.

  (* le neutre est la transformation identité *)
  Definition unit := Take.

  Fixpoint rev_law t1 t2 {struct t1} :=
    match t1 with
    | Take     => t2
    | Back t   => rev_law t (Back' t2)
    | Right t  => rev_law t (Right' t2)
    | Down t   => rev_law t (Down' t2)
    | Back' t  => rev_law t (Back t2)
    | Right' t => rev_law t (Right t2)
    | Down' t  => rev_law t (Down t2)
    end.

  (* l'inverse *)
  Definition inverse t := rev_law t Take.

  Import Operation.

  Definition group_associative: associative U law.
    Proof.
    unfold associative. intros.
    induction x.
    simpl. reflexivity.
    simpl. rewrite IHx. reflexivity.
    simpl. rewrite IHx. reflexivity.
    simpl. rewrite IHx. reflexivity.
    simpl. rewrite IHx. reflexivity.
    simpl. rewrite IHx. reflexivity.
    simpl. rewrite IHx. reflexivity.
    Qed.
  Definition group_neutral: neutral U law unit.
    Proof.
    unfold neutral. intros.
    unfold unit. unfold law.
    reflexivity.
    Qed.
  Lemma lemma1: forall x, rev_law x x = unit.
    Proof.
    intro. unfold unit. induction x.
    simpl. reflexivity.
    simpl. rewrite involutive_back'.  exact IHx.
    simpl. rewrite involutive_right'. exact IHx.
    simpl. rewrite involutive_down'.  exact IHx.
    simpl. rewrite involutive_back.   exact IHx.
    simpl. rewrite involutive_right.  exact IHx.
    simpl. rewrite involutive_down.   exact IHx.
    Qed.
  Lemma lemma2: forall x, law (rev_law x Take) x = rev_law x x.
    Proof.
    intro. induction x.
    simpl. reflexivity.
    simpl. rewrite involutive_back'.
    Admitted.
  Definition group_symmetric: symmetric U law inverse unit.
    Proof.
    unfold symmetric. intro.
    unfold inverse.
    rewrite <- (lemma1 x). exact (lemma2 x).
    Qed.

End Rubik2Group.

Le type transform a une certaine similarité avec les types nat et list.
Pourtant je bloque sur la preuve de lemma2, je n'arrive pas à réécrire de façon à pouvoir utiliser les axiomes involutive_****.

Merci pour vos commentaires.

[dividee]

Il est parfois nécessaire de généraliser le théorème; cela permet d'avoir une hypothèse d'induction plus forte:

Code Coq :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
  Lemma lemma2_aux: forall x y, law (rev_law x Take) y = rev_law x y.
  Proof.
    induction x; simpl; intro y.
    reflexivity.
    rewrite <- IHx. rewrite <- group_associative. simpl. apply IHx.
    rewrite <- IHx. rewrite <- group_associative. simpl. apply IHx.
    rewrite <- IHx. rewrite <- group_associative. simpl. apply IHx.
    rewrite <- IHx. rewrite <- group_associative. simpl. apply IHx.
    rewrite <- IHx. rewrite <- group_associative. simpl. apply IHx.
    rewrite <- IHx. rewrite <- group_associative. simpl. apply IHx.
  Qed.

  Lemma lemma2: forall x, law (rev_law x Take) x = rev_law x x.
  Proof.
    intro x. apply lemma2_aux.
  Qed.

On voit d'ailleurs que cette propriété ne dépend pas des axiomes involutive_****.

[SpiceGuid]

Il est parfois nécessaire de généraliser le théorème; cela permet d'avoir une hypothèse d'induction plus forte

Il va me falloir un sacré bout de temps pour méditer cette phrase.

[Steki-kun]

Il va me falloir un sacré bout de temps pour méditer cette phrase.

Bonjour, j'étais pas venu ici depuis des lustres mais comme il y a un sujet Coq je me sens obligé d'intervenir, même s'il est marqué résolu

Même si le conseil de dividee est très pertinent en général, je crois qu'il faut surtout méditer sur le fait que ton contexte est inconsistent ici. Ainsi, je te propose un petit lemme qui rendra bcp plus facile la suite du fichier ;-)

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
Lemma assert_false : False.
assert (Take = Back (Back' Take)) 
  by (rewrite involutive_back; reflexivity).
discriminate.
Qed.

Blague à part, tu ne peux pas supposer que deux constructeurs différents d'inductifs sont égaux, c'est comme écrire le même type en Caml et essayer de convaincre Pervasives.compare que deux objets différents sont syntaxiquement égaux.

De manière générale, tu ne devrais jamais écrire 'Axiom' sauf

• dans une signature de module
• pour la proof irrelevance, l'EM, l'axiome du choix, et autres bizarreries logiques

Dans le cas présent, si tu veux une représentation canonique, tu peux par exemple définir une fonction de normalisation (tu obtiendras tes axiomes, mais par conversion et non par supposition) et raisonner sur les formes normales en utilisant une égalité setoide. Pour une autre solution, tu peux regarder le très bon papier de Laurent Théry à TPHOLs'08 sur le Rubiks cube 2x2x2 ftp://ftp-sop.inria.fr/marelle/Laurent.Thery/Rubik.ps.

SK

[SpiceGuid]

il faut surtout méditer sur le fait que ton contexte est inconsistent

De manière générale, tu ne devrais jamais écrire 'Axiom' sauf

• dans une signature de module
• pour la proof irrelevance, l'EM, l'axiome du choix, et autres bizarreries logiques

Le fait que j'utilise Axiom dans la signature du module Group a beaucoup contribué à le banaliser dans mon esprit.

tu peux par exemple définir une fonction de normalisation (tu obtiendras tes axiomes, mais par conversion et non par récriture) et raisonner sur les formes normales en utilisant une égalité setoide.

En fait c'est la direction que j'avais prise au départ, avec un type de module Setoid, l'associativité n'était plus définie à l'aide de l'égalité mais à l'aide de la relation d'équivalence du setoid porteur du groupe.

Comme ça m'a vite paru trop technique et que je ne savais pas où je mettais les pieds j'ai vite cédé à la facilité en posant comme une égalité ce qui n'est effectivement qu'une équivalence d'interprétation.

La différence entre Coq et Caml c'est qu'avec Coq on n'a plus le droit de ne pas être un peu logicien alors que Caml ne demande que d'être un programmeur soigneux. Honnêtement, je ne pense pas que je vais investir davantage de temps dans une compétence aussi radicalement nouvelle.
Néanmoins je te remercie pour ton intervention.

Je connaissais le papier de Laurent Théry, il est plus calculatoire (orienté vers la résolution), je lui ai emprunté le codage de l'état du Rubik's cube dans mon dernier article.