aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/ideal-features/implicit_binders.v
blob: 2ec72780805375179d70d15fa3f716c112ca9ef3 (plain)
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
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
(** * Questions de syntaxe autour de la généralisation implicite

   ** Lieurs de classes
   Aujourd'hui, les lieurs de classe [ ] et les
   lieurs {{ }} sont équivalents et on a toutes les combinaisons de { et ( pour
   les lieurs de classes (où la variable liée peut être anonyme):
   *)

Class Foo (A : Type) := foo : A -> nat.

Definition bar [ Foo A ] (x y : A) := foo x + foo y.

Definition bar₀ {{ Foo A }} (x y : A) := foo x + foo y.

Definition bar₁ {( Foo A )} (x y : A) := foo x + foo y.

Definition bar₂ ({ Foo A }) (x y : A) := foo x + foo y.

Definition bar₃ (( Foo A )) (x y : A) := foo x + foo y.

Definition bar₄ {( F : Foo A )} (x y : A) := foo x + foo y.

(** Les lieurs sont généralisés à tous les termes, pas seulement aux classes: *)

Definition relation A := A -> A -> Prop.

Definition inverse {( R : relation A )} := fun x y => R y x.

(** Autres propositions:
   [Definition inverse ..(R : relation A) := fun x y => R y x] et

   [Definition inverse ..[R : relation A] := fun x y => R y x] ou
   [Definition inverse ..{R : relation A} := fun x y => R y x]
   pour lier [R] implicitement.

   MS: Le .. empêche d'utiliser electric-terminator dans Proof General. Cependant, il existe
   aussi les caractères utf8 ‥ (two dot leader) et … (horizontal ellipsis) qui permettraient
   d'éviter ce souci moyennant l'utilisation d'unicode.

   [Definition inverse _(R : relation A) := fun x y => R y x] et

   [Definition inverse _[R : relation A] := fun x y => R y x] ou
   [Definition inverse _{R : relation A} := fun x y => R y x]

   [Definition inverse `(R : relation A) := fun x y => R y x] et

   [Definition inverse `[R : relation A] := fun x y => R y x] ou
   [Definition inverse `{R : relation A} := fun x y => R y x]


   Toujours avec la possibilité de ne pas donner le nom de la variable:
*)

Definition div (x : nat) ({ y <> 0 }) := 0.

(** Un choix à faire pour les inductifs: accepter ou non de ne pas donner de nom à
   l'argument. Manque de variables anonymes pour l'utilisateur mais pas pour le système... *)

Inductive bla [ Foo A ] : Type :=.

(** *** Les autres syntaxes ne supportent pas de pouvoir spécifier séparément les statuts
   des variables généralisées et celui de la variable liée. Ca peut être utile pour les
   classes où l'on a les cas de figure: *)

(** Trouve [A] et l'instance par unification du type de [x]. *)
Definition allimpl {{ Foo A }} (x : A) : A := x.

(** Trouve l'instance à partir de l'index explicite *)

Class SomeStruct (a : nat) := non_zero : a <> 0.

Definition instimpl ({ SomeStruct a }) : nat := a + a.

(** Donne l'instance explicitement (façon foncteur). *)

Definition foo_prod {( Foo A, Foo B )} : Foo (A * B) :=
  fun x => let (l, r) := x in foo l + foo r.

(** *** Questions:
   - Gardez les crochets [ ] pour {{ }} ?
   - Quelle syntaxe pour la généralisation ?
   - Veut-on toutes les combinaisons de statut pour les variables généralisées et la variable liée ?
   *)

(** ** Constructeur de généralisation implicite

   Permet de faire une généralisation n'importe où dans le terme: on
   utilise un produit ou un lambda suivant le scope (fragile ?).
   *)

Goal `(x + y + z = x + (y + z)).
Admitted.

(** La généralisation donne un statut implicite aux variables si l'on utilise
   `{ }. *)

Definition baz := `{x + y + z = x + (y + z)}.
Print baz.

(** Proposition d'Arthur C.: déclarer les noms de variables généralisables à la [Implicit Types]
   pour plus de robustesse (cela vaudrait aussi pour les lieurs). Les typos du genre de l'exemple suivant
   ne sont plus silencieuses: *)

Check `(foob 0 + x).

(** Utilisé pour généraliser l'implémentation de la généralisation implicite dans
   les déclarations d'instances (i.e. les deux defs suivantes sont équivalentes). *)

Instance fooa : Foo A.
Admitted.
Definition fooa' : `(Foo A).
Admitted.

(** Un peu différent de la généralisation des lieurs qui "explosent" les variables
   libres en les liant au même niveau que l'objet. Dans la deuxième defs [a] n'est pas lié dans
   la définition mais [F : Π a, SomeStruct a]. *)

Definition qux {( F : SomeStruct a )} : nat := a.
Definition qux₁ {( F : `(SomeStruct a) )} : nat := 0.

(** *** Questions
   - Autres propositions de syntaxe ?
   - Réactions sur la construction ?
   *)