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.
| (* {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 a où a est une preuve de A, soit right b où b est une preuve de B. Une valeur de type A \/ B vit dans Prop et est soit or_introl a où a est une preuve de A, soit or_intror b où b 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.
