(* Algorithme d'exclusion mutuelle de Peterson. *) Require PolyList. Require Bool. Require Arith. Require ZArith. (* On a deux processus, nommes 1 et 2. Le but est de montrer que, partant chacun de l'etat NonCritique, les deux processus ne se retrouvent jamais tous les deux en meme temps en section critique, c'est-a-dire dans l'etat Critique. Ceci permet aux deux processus 1 et 2 en parallele de se partager une ressource en etant sur que l'autre processus n'est pas en train de la modifier. L'algorithme de Peterson est realise a l'aide de trois variables : - c1 est un booleen que le processus 1 peut lire et ecrire, et que le processus 2 ne peut que lire (atomiquement); il est initialement vrai. - c2 est un booleen que le processus 2 peut lire et ecrire, et que le processus 1 ne peut que lire (atomiquement); il est initialement vrai. - tour est un booleen, valant faux (=processus 1) ou vrai (=processus 2), et que les deux processus peuvent lire et ecrire de facon atomique (sans etre interrompu par l'autre processus). *) (* En graphiques (les noms entre crochets sont des etats, les fleches sont les transitions): Processus 1: Processus 2: ______________ ______________ / \ / \ / \ / \ L \ L \ [NonCritique] \ [NonCritique] \ | \ | \ c1:=true \ c2:=true \ | | | | v | v | [Pose] | [Pose] | | | | | tour:=true__ | tour:=false_ | | / \ | | / \ | v L (si c2=true | v L (si c1=true | [Attente] et tour=true) | [Attente] et tour=faux) | | \_____/ | | \_____/ | (si c2=false / (si c1=false / ou tour=false) / ou tour=true) / | / | / v / v / [Critique] / [Critique] / | / | / c1:=false / c2:=false / \ / \ / \___________/ \___________/ Le but est de montrer que, partant de l'etat NonCritique pour chaque processus, avec c1=c2=true, on ne peut jamais arriver dans l'etat ou les deux processus sont dans l'etat Critique en meme temps. *) Inductive pc : Set := (* le compteur de programme de chaque processus. *) NonCritique : pc | Critique : pc | Pose : pc | Attente : pc. Definition proc := bool. (* le type des processus, peut etre faux (=1) ou vrai (=2). *) Inductive etat : Set := Etat : bool -> bool -> pc -> pc -> proc -> etat (* c1 c2 pc1 pc2 tour *) . (* Etat : (proc -> bool) -> (proc -> pc) -> proc -> etat (* ^- pour chaque ^- pour chaque ^- la valeur de processus i, processus i, la variable la valeur de la valeur pc(i) partagee tour. c(i). de son compteur de programme. *) . *) Lemma choix_bool : (b:bool) b=true \/ b=false. Proof. Induction b. Left . Reflexivity. Right . Reflexivity. Qed. Inductive transition : etat -> etat -> Prop := prepare1 : (c1,c2:bool) (pc2:pc) (tour:proc) (transition (Etat c1 c2 NonCritique pc2 tour) (Etat true c2 Pose pc2 tour)) (* Processus 1 fait : [NonCritique] c1:=true [Pose] *) | prepare2 : (c1,c2:bool) (pc1:pc) (tour:proc) (transition (Etat c1 c2 pc1 NonCritique tour) (Etat c1 true pc1 Pose tour)) (* Processus 2 fait : [NonCritique] c2:=true [Pose] *) | pose1 : (c1,c2:bool) (pc2:pc) (tour:proc) (transition (Etat c1 c2 Pose pc2 tour) (Etat c1 c2 Attente pc2 true)) (* Processus 1 fait : [Pose] tour:=true [Attente] *) | pose2 : (c1,c2:bool) (pc1:pc) (tour:proc) (transition (Etat c1 c2 pc1 Pose tour) (Etat c1 c2 pc1 Attente false)) (* Processus 2 fait : [Pose] tour:=false [Attente] *) | attente1 : (c1,c2:bool) (pc2:pc) (tour:proc) c2=true /\ tour=true -> (transition (Etat c1 c2 Attente pc2 tour) (Etat c1 c2 Attente pc2 tour)) (* Processus 1 fait : si c2 vrai et tour vrai, [Attente] nop [Attente] *) | attente2 : (c1,c2:bool) (pc1:pc) (tour:proc) c1=true /\ tour=false -> (transition (Etat c1 c2 pc1 Attente tour) (Etat c1 c2 pc1 Attente tour)) (* Processus 2 fait : si c1 vrai et tour faux, [Attente] nop [Attente] *) | entre1 : (c1,c2:bool) (pc2:pc) (tour:proc) c2=false \/ tour=false -> (transition (Etat c1 c2 Attente pc2 tour) (Etat c1 c2 Critique pc2 tour)) (* Processus 1 fait : si c2 faux ou tour faux, [Attente] nop [Critique] *) | entre2 : (c1,c2:bool) (pc1:pc) (tour:proc) c1=false \/ tour=true -> (transition (Etat c1 c2 pc1 Attente tour) (Etat c1 c2 pc1 Critique tour)) (* Processus 2 fait : si c1 faux ou tour vrai, [Attente] nop [Critique] *) | sort1 : (c1,c2:bool) (pc2:pc) (tour:proc) (transition (Etat c1 c2 Critique pc2 tour) (Etat false c2 NonCritique pc2 tour)) (* Processus 1 fait : [Critique] c1:=false [NonCritique] *) | sort2 : (c1,c2:bool) (pc1:pc) (tour:proc) (transition (Etat c1 c2 pc1 Critique tour) (Etat c1 false pc1 NonCritique tour)) (* Processus 2 fait : [Critique] c1:=false [NonCritique] *) . Inductive exec : etat -> etat -> Prop := nop : (s1,s2:etat) s1=s2 -> (exec s1 s2) (* On peut aller de s1 a s2 en ne faisant rien, mais alors s1=s2. *) | qqch : (s1,s2,s3:etat) (exec s1 s2) -> (transition s2 s3) -> (exec s1 s3). (* Ou on peut faire une execution pour aller de s1 a s2, puis faire une etape de s2 a s3. Ceci definit une execution (non vide) de s1 a s3. *) (* On montre d'abord que quand le processus 1 est dans l'etat Pose, ou l'etat Attente, ou l'etat Critique, necessairement c1 est vrai: *) Lemma apres_prepare_c1_est_vrai : (s0,s:etat) (exec s0 s) -> (tour0:proc) s0=(Etat true true NonCritique NonCritique tour0) -> (tour:proc) (c1,c2:bool) (pc1,pc2:pc) s =(Etat c1 c2 pc1 pc2 tour) -> pc1=Pose \/ pc1=Attente \/ pc1=Critique -> c1=true. Proof. (* On fait une recurrence sur l'execution (exec s0 s): *) Intros s0 s H. Elim H. (* Focus. *) (* Cas 1: nop, execution vide. Donc s0=s, ce qui force c1=true: *) Intros. Rewrite H0 in H1. Rewrite H1 in H2. Inversion H2. Reflexivity. (* Cas 2: qqch, execution non vide. On effectue une inversion sur H2:(transition s2 s3) pour regarder tous les cas possibles pour la derniere transition effectuee, de s2 a l'etat final s3: *) Intros. Inversion H2. (* Il y a dix sous-cas, correspondant chacun a une transition possible. *) (* Cas 1.1: la derniere transition etait effectuee par le processus 1, et etait [NonCritique] c1:=true [Pose]. On a donc bien apres c1=true, parce que c'est l'effet de l'affectation c1:=true: *) Rewrite H4 in H7. Inversion H7. Reflexivity. (* Cas 1.2: la derniere transition etait effectuee par le processus 2, et etait [NonCritique] c2:=true [Pose]. Par hypothese de recurrence, c1 etait vrai dans l'etat s2 avant la transition, et l'affectation c2:=true ne change pas la valeur de c1, donc c1 est toujours true. *) Rewrite H4 in H7. Inversion H7. Rewrite H9 in H6. (* H9:c0=c1 dit que la valeur de c1 avant la transition (c0) egale celle apres la transition (c1). *) Rewrite <- H6 in H1. Apply (H1 tour0 H3 tour1 c1 c3 pc0 NonCritique). (* On applique la recurrence. *) Reflexivity. Rewrite H11. Assumption. (* Cas 1.3: la derniere transition etait effectuee par le processus 1, et etait [Pose] tour:=true [Attente]. Comme ci-dessus, ca ne change pas la valeur de c1. *) Rewrite H4 in H7. Inversion H7. Rewrite H9 in H6. Rewrite <- H6 in H1. Apply (H1 tour0 H3 tour1 c1 c3 Pose pc0). Reflexivity. Left . Reflexivity. (* Cas 1.4: la derniere transition etait effectuee par le processus 2, et etait [Pose] tour:=false [Attente]. Comme ci-dessus, ca ne change pas la valeur de c1. *) Rewrite H4 in H7. Inversion H7. Rewrite H9 in H6. Rewrite <- H6 in H1. Apply (H1 tour0 H3 tour1 c1 c3 pc0 Pose). Reflexivity. Rewrite H11. Assumption. (* Cas 1.5: la derniere transition etait effectuee par le processus 1, et etait: si c2=true et tour=true, alors [Attente] nop [Attente]. Comme ci-dessus, ca ne change pas la valeur de c1. *) Rewrite H4 in H8. Inversion H8. Rewrite H10 in H7. Rewrite <- H7 in H1. Apply (H1 tour0 H3 tour1 c1 c3 Attente pc0). Reflexivity. Right . Left . Reflexivity. (* Cas 1.6: la derniere transition etait effectuee par le processus 2, et etait: si c1=true et tour=false, alors [Attente] nop [Attente]. Comme ci-dessus, ca ne change pas la valeur de c1. *) Rewrite H4 in H8. Inversion H8. Rewrite H10 in H7. Rewrite <- H7 in H1. Apply (H1 tour0 H3 tour1 c1 c3 pc0 Attente). Reflexivity. Rewrite H12. Assumption. (* Cas 1.7: la derniere transition etait effectuee par le processus 1, et etait: si c2=false ou tour=false, alors [Attente] nop [Critique]. Comme ci-dessus, ca ne change pas la valeur de c1. *) Rewrite H4 in H8. Inversion H8. Rewrite H10 in H7. Rewrite <- H7 in H1. Apply (H1 tour0 H3 tour1 c1 c3 Attente pc0). Reflexivity. Right . Left . Reflexivity. (* Cas 1.8: la derniere transition etait effectuee par le processus 2, et etait: si c1=false ou tour=true, alors [Attente] nop [Critique]. Comme ci-dessus, ca ne change pas la valeur de c1. *) Rewrite H4 in H8. Inversion H8. Rewrite H10 in H7. Rewrite <- H7 in H1. Apply (H1 tour0 H3 tour1 c1 c3 pc0 Attente). Reflexivity. Rewrite H12. Assumption. (* Cas 1.9: la derniere transition etait effectuee par le processus 1, et etait: [Critique] c1:=false [NonCritique]. A la sortie, on n'a pas la conclusion desiree c1=true, mais ce cas est impossible en fait, puisqu'on a suppose que pc1 (apres la transition) valait Pose, Attente ou Critique, mais pas NonCritique. *) Rewrite H4 in H7. Inversion H7. Rewrite <- H11 in H5. Elim H5. Intro. Discriminate H8. Intro. Elim H8. Intro. Discriminate H14. Intro. Discriminate H14. (* Cas 1.10: la derniere transition etait effectuee par le processus 2, et etait: [Critique] c2:=false [NonCritique]. Ceci ne change pas la valeur de c1, et donc le resultat s'ensuit pas hypothese de recurrence H1. *) Rewrite H4 in H7. Inversion H7. Rewrite H9 in H6. Rewrite <- H6 in H1. Apply (H1 tour0 H3 tour1 c1 c3 pc0 Critique). Reflexivity. Rewrite H11. Assumption. Qed. (* Donc quand le processus 1 est en section critique (dans l'etat Critique), c1 vaut true: *) Lemma en_critique_c1_est_vrai : (s0,s:etat) (exec s0 s) -> (tour0:proc) s0=(Etat true true NonCritique NonCritique tour0) -> (tour:proc) (c1,c2:bool) (pc1,pc2:pc) s =(Etat c1 c2 pc1 pc2 tour) -> pc1=Critique -> c1=true. Proof. Intros. Apply (apres_prepare_c1_est_vrai s0 s H tour0 H0 tour c1 c2 pc1 pc2 H1). Right . Right . Assumption. Qed. (* On montre ensuite le lemme analogue que quand le processus 2 est dans l'etat Pose, ou l'etat Attente, ou l'etat Critique, necessairement c2 est vrai: *) Lemma apres_prepare_c2_est_vrai : (s0,s:etat) (exec s0 s) -> (tour0:proc) s0=(Etat true true NonCritique NonCritique tour0) -> (tour:proc) (c1,c2:bool) (pc1,pc2:pc) s =(Etat c1 c2 pc1 pc2 tour) -> pc2=Pose \/ pc2=Attente \/ pc2=Critique -> c2=true. Proof. (* La preuve est essentiellement la meme que pour apres_prepare_c1_est_vrai. *) Intros s0 s H. Elim H. Intros. Rewrite H0 in H1. Rewrite H1 in H2. Inversion H2. Reflexivity. Intros. Inversion H2. Rewrite H4 in H7. Inversion H7. Rewrite H10 in H6. Rewrite <- H6 in H1. Apply (H1 tour0 H3 tour1 c0 c2 NonCritique pc0). Reflexivity. Rewrite H12. Assumption. Rewrite H4 in H7. Inversion H7. Reflexivity. Rewrite H4 in H7. Inversion H7. Rewrite H10 in H6. Rewrite <- H6 in H1. Apply (H1 tour0 H3 tour1 c0 c2 Pose pc0). Reflexivity. Rewrite H12. Assumption. Rewrite H4 in H7. Inversion H7. Rewrite H10 in H6. Rewrite <- H6 in H1. Apply (H1 tour0 H3 tour1 c0 c2 pc0 Pose). Reflexivity. Left . Reflexivity. Rewrite H4 in H8. Inversion H8. Rewrite H11 in H7. Rewrite <- H7 in H1. Apply (H1 tour0 H3 tour1 c0 c2 Attente pc0). Reflexivity. Rewrite H13. Assumption. Rewrite H4 in H8. Inversion H8. Rewrite H11 in H7. Rewrite <- H7 in H1. Apply (H1 tour0 H3 tour1 c0 c2 pc0 Attente). Reflexivity. Right . Left . Reflexivity. Rewrite H4 in H8. Inversion H8. Rewrite H11 in H7. Rewrite <- H7 in H1. Apply (H1 tour0 H3 tour1 c0 c2 Attente pc0). Reflexivity. Rewrite H13. Assumption. Rewrite H4 in H8. Inversion H8. Rewrite H11 in H7. Rewrite <- H7 in H1. Apply (H1 tour0 H3 tour1 c0 c2 pc0 Attente). Reflexivity. Right . Left . Reflexivity. Rewrite H4 in H7. Inversion H7. Rewrite H10 in H6. Rewrite <- H6 in H1. Apply (H1 tour0 H3 tour1 c0 c2 Critique pc0). Reflexivity. Rewrite H12. Assumption. Rewrite H4 in H7. Inversion H7. Rewrite <- H12 in H5. Elim H5. Intro. Discriminate H8. Intro. Elim H8. Intro. Discriminate H14. Intro. Discriminate H14. Qed. (* Donc quand le processus 2 est en section critique (dans l'etat Critique), c2 vaut true: *) Lemma en_critique_c2_est_vrai : (s0,s:etat) (exec s0 s) -> (tour0:proc) s0=(Etat true true NonCritique NonCritique tour0) -> (tour:proc) (c1,c2:bool) (pc1,pc2:pc) s =(Etat c1 c2 pc1 pc2 tour) -> pc2=Critique -> c2=true. Proof. Intros. Apply (apres_prepare_c2_est_vrai s0 s H tour0 H0 tour c1 c2 pc1 pc2 H1). Right . Right . Assumption. Qed. (* On remarque que si le processus 1 est dans l'etat Critique, et le processus 2 n'est pas dans l'etat Pose, alors des que c2 est vrai, tour est faux: *) Lemma en_critique1_tour_est_faux : (s0,s:etat) (exec s0 s) -> (tour0:proc) s0=(Etat true true NonCritique NonCritique tour0) -> (tour:proc) (c1,c2:bool) (pc1,pc2:pc) s =(Etat c1 c2 pc1 pc2 tour) -> pc1=Critique -> ~pc2=Pose -> c2=true -> tour=false. Proof. (* On fait une recurrence sur l'execution (exec s0 s): *) Intros s0 s H. Elim H. (* Focus. *) (* Cas 1: nop, execution vide. Donc s0=s, ce qui force le processus 1 a etre a la fois dans l'etat NonCritique (initial) et Critique (parce que pc1=Critique). Ce cas est donc impossible (donc trivialement correct). *) Intros. Rewrite H3 in H2. Rewrite H0 in H1. Rewrite H1 in H2. Discriminate H2. (* Cas 2: qqch, execution non vide. On effectue une inversion sur H2:(transition s2 s3) pour regarder tous les cas possibles pour la derniere transition effectuee, de s2 a l'etat final s3: *) Intros. Inversion H2. (* Il y a dix sous-cas, correspondant chacun a une transition possible. *) (* Cas 1.1: la derniere transition etait effectuee par le processus 1, et etait [NonCritique] c1:=true [Pose]. Ceci force pc1=Pose, ce qui contredit pc1=Critique. Le cas est donc impossible, donc trivialement correct. *) Rewrite H5 in H4. Rewrite H4 in H9. Discriminate H9. (* Cas 1.2: la derniere transition etait effectuee par le processus 2, et etait [NonCritique] c2:=true [Pose]. Ceci force pc2=Pose, qui a ete explicitement exclu (cf. l'hypothese ~pc2=Pose). *) Rewrite H4 in H9. Inversion H9. Rewrite <- H14 in H6. Absurd Pose=Pose. Assumption. Reflexivity. (* Cas 1.3: la derniere transition etait effectuee par le processus 1, et etait [Pose] tour:=true [Attente]. Encore une fois, c'est un cas impossible, comme pour le sous-cas 1.1. *) Rewrite H5 in H4. Rewrite H4 in H9. Discriminate H9. (* Cas 1.4: la derniere transition etait effectuee par le processus 2, et etait [Pose] tour:=false [Attente]. Mais ceci met tour a false, et demontre donc la conclusion tour=false. *) Rewrite H4 in H9. Inversion H9. Reflexivity. (* Cas 1.5: la derniere transition etait effectuee par le processus 1, et etait: si c2=true et tour=true, alors [Attente] nop [Attente]. C'est un cas impossible, comme 1.1 et 1.3. *) Rewrite H4 in H10. Rewrite H5 in H10. Discriminate H10. (* Cas 1.6: la derniere transition etait effectuee par le processus 2, et etait: si c1=true et tour=false, alors [Attente] nop [Attente]. Non seulement ca ne change pas la valeur de tour, mais si la transition a ete franchie, c'est qu'en particulier tour=false comme demande. *) Rewrite H5 in H4. Rewrite H4 in H10. Inversion H10. Elim H8. Rewrite H16. Trivial. (* Cas 1.7: la derniere transition etait effectuee par le processus 1, et etait: si c2=false ou tour=false, alors [Attente] nop [Critique]. On a deux cas (Elim H8): - si c2=false, ca contredit l'hypothese que c2=true; - donc tour=false, qui est la conclusion demandee. *) Rewrite H4 in H10. Inversion H10. Elim H8. Rewrite H13. Rewrite H7. Intro. Discriminate H11. Rewrite H16. Trivial. (* Cas 1.8: la derniere transition etait effectuee par le processus 2, et etait: si c1=false ou tour=true, alors [Attente] nop [Critique]. Ici, tour ne change clairement pas, et on applique l'hypothese de recurrence H1. *) Rewrite H4 in H10. Rewrite H5 in H10. Inversion H10. Rewrite <- H9 in H1. Rewrite H10 in H1. Rewrite H16 in H1. Apply (H1 tour0 H3 tour c0 c3 pc0 Attente). Reflexivity. Assumption. Unfold not. Intro. Discriminate H11. Rewrite H13. Assumption. (* Cas 1.9: la derniere transition etait effectuee par le processus 1, et etait: [Critique] c1:=false [NonCritique]. Ce cas est impossible, car pc1=Critique et pas NonCritique. *) Rewrite H4 in H9. Rewrite H5 in H9. Discriminate H9. (* Cas 1.10: la derniere transition etait effectuee par le processus 2, et etait: [Critique] c2:=false [NonCritique]. Ce cas est aussi impossible, parce qu'il aurait mis c2 a false, mais on a suppose que c2 valait true. *) Rewrite H7 in H4. Rewrite H4 in H9. Discriminate H9. Qed. (* On montre ensuite le lemme analogue que quand le processus 2 est dans l'etat Critique, et le processus 1 n'est pas dans l'etat Pose, alors des que c1 est vrai, tour est vrai: *) Lemma en_critique2_tour_est_vrai : (s0,s:etat) (exec s0 s) -> (tour0:proc) s0=(Etat true true NonCritique NonCritique tour0) -> (tour:proc) (c1,c2:bool) (pc1,pc2:pc) s =(Etat c1 c2 pc1 pc2 tour) -> pc2=Critique -> ~pc1=Pose -> c1=true -> tour=true. Proof. Intros s0 s H. Elim H. Intros. Rewrite H3 in H2. Rewrite H0 in H1. Rewrite H1 in H2. Discriminate H2. Intros. Inversion H2. Rewrite H4 in H9. Inversion H9. Absurd pc1=Pose. Assumption. Rewrite H13. Reflexivity. Rewrite H5 in H4. Rewrite H4 in H9. Discriminate H9. Rewrite H5 in H4. Rewrite H4 in H9. Inversion H9. Reflexivity. Rewrite H5 in H4. Rewrite H4 in H9. Discriminate H9. Rewrite H4 in H10. Inversion H10. Elim H8. Rewrite H16. Trivial. Rewrite H5 in H4. Rewrite H4 in H10. Discriminate H10. Rewrite H5 in H4. Rewrite H4 in H10. Inversion H10. Rewrite <- H9 in H1. Rewrite H16 in H1. Apply (H1 tour0 H3 tour c0 c3 Attente pc0). Reflexivity. Assumption. Unfold not. Intro. Discriminate H11. Rewrite H12. Assumption. Rewrite H4 in H10. Inversion H10. Rewrite H12 in H8. Rewrite H16 in H8. Elim H8. Rewrite H7. Intro. Discriminate H11. Trivial. Rewrite H4 in H9. Rewrite H7 in H9. Discriminate H9. Rewrite H5 in H4. Rewrite H4 in H9. Discriminate H9. Qed. Lemma exclusion_mutuelle : (s0,s:etat) (exec s0 s) -> (tour0,tour:proc) (c1,c2:bool) s0=(Etat true true NonCritique NonCritique tour0) -> ~s =(Etat c1 c2 Critique Critique tour). (* Il n'est pas possible, partant d'un etat initial ou c1=c2=true, pc1=pc2=NonCritique, d'arriver a un etat ou les deux processus sont en section critique en meme temps (pc1=pc2=Critique). *) Proof. (* L'idee de la demonstration est la suivante : supposons que l'on soit arrive a l'etat pc1=pc2=Critique, en partant de s0 un etat initial. Par en_critique_c1_est_vrai, c1 est vrai. On peut donc utiliser en_critique2_tour_est_vrai et conclure que tour est vrai. D'autre part, par en_critique_c2_est_vrai, c2 est vrai. On peut donc utiliser en_critique1_tour_est_faux et conclure que tour est faux. Mais le fait que tour soit a la fois vrai et faux est contradictoire. *) Unfold not. Intros. Cut tour=false. Intro. (* On va montrer que tour est faux. *) Cut tour=true. Intro. (* On va aussi montrer que tour est vrai. *) Rewrite H2 in H3. Discriminate H3. (* Pour montrer que tour est vrai, on applique en_critique2_tour_est_vrai avec les arguments qui vont bien : *) Apply (en_critique2_tour_est_vrai s0 s H tour0 H0 tour c1 c2 Critique Critique H1). Reflexivity. Unfold not. Intro. Discriminate H3. (* Il ne reste qu'a montrer que c1 est vrai, par en_critique_c1_est_vrai : *) Apply (en_critique_c1_est_vrai s0 s H tour0 H0 tour c1 c2 Critique Critique). Assumption. Reflexivity. (* Pour montrer que tour est vrai, on applique en_critique1_tour_est_faux avec les arguments qui vont bien : *) Apply (en_critique1_tour_est_faux s0 s H tour0 H0 tour c1 c2 Critique Critique). Assumption. Reflexivity. Unfold not. Intro. Discriminate H2. (* Il ne reste qu'a montrer que c2 est vrai, par en_critique_c2_est_vrai : *) Apply (en_critique_c2_est_vrai s0 s H tour0 H0 tour c1 c2 Critique Critique). Assumption. Reflexivity. Qed.