Lambda.v 6.65 KB
Newer Older
1

2
(** * A link with Lambda Calculus *)
3

4
(** The NatDed development, Pierre Letouzey, Samuel Ben Hamou, 2019-2020.
5
6
    This file is released under the CC0 License, see the LICENSE file *)

Pierre Letouzey's avatar
Pierre Letouzey committed
7
Require Import Utils Defs Mix Meta.
8
Import ListNotations.
Pierre Letouzey's avatar
Pierre Letouzey committed
9
10
Local Open Scope list.
Local Open Scope eqb_scope.
11
12
13
14

Inductive term :=
  | Var : nat -> term
  | App : term -> term -> term
15
  | Abs : term -> term
Pierre Letouzey's avatar
Pierre Letouzey committed
16
  | One : term
17
18
19
  | Nabla : term -> term
  | Couple : term -> term -> term
  | Pi1 : term -> term
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
20
21
22
23
  | Pi2 : term -> term
  | Case : term -> term -> term -> term
  | I1 : term -> term
  | I2 : term -> term.
24
25
26

Inductive type :=
  | Arr : type -> type -> type
27
  | Atom : name -> type
28
  | Bot : type
Pierre Letouzey's avatar
Pierre Letouzey committed
29
  | Unit : type
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
30
31
  | And : type -> type -> type
  | Or : type -> type -> type.
32
33
34
35

Definition context := list type.

Inductive typed : context -> term -> type -> Prop :=
36
37
38
  | Type_Var : forall Γ τ n, nth_error Γ n = Some τ -> typed Γ (Var n) τ
  | Type_App : forall Γ u v σ τ, typed Γ u (Arr σ τ) -> typed Γ v σ -> typed Γ (App u v) τ
  | Type_Abs : forall Γ u σ τ,  typed (σ :: Γ) u τ -> typed Γ (Abs u) (Arr σ τ)
Pierre Letouzey's avatar
Pierre Letouzey committed
39
  | Type_One : forall Γ, typed Γ One Unit
40
  | Type_Nabla : forall Γ u τ, typed Γ u Bot -> typed Γ (Nabla u) τ
41
42
  | Type_Couple : forall Γ u v σ τ, typed Γ u σ -> typed Γ v τ ->
                                    typed Γ (Couple u v) (And σ τ)
43
  | Type_Pi1 : forall Γ u σ τ, typed Γ u (And σ τ) -> typed Γ (Pi1 u) σ
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
44
  | Type_Pi2 : forall Γ u σ τ, typed Γ u (And σ τ) -> typed Γ (Pi2 u) τ
45
46
  | Type_Case : forall Γ u v1 v2 τ1 τ2 σ, typed Γ u (Or τ1 τ2) -> typed (τ1 :: Γ) v1 σ ->
                                          typed (τ2 :: Γ) v2 σ -> typed Γ (Case u v1 v2) σ
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
47
48
  | Type_I1 : forall Γ u σ τ, typed Γ u σ -> typed Γ (I1 u) (Or σ τ)
  | Type_I2 : forall Γ u σ τ, typed Γ u τ -> typed Γ (I2 u) (Or σ τ).
49

Pierre Letouzey's avatar
Pierre Letouzey committed
50
51
Hint Constructors typed.

52
Notation "u @ v" := (App u v) (at level 20) : lambda_scope.
53
Notation "∇ u" := (Nabla u) (at level 20) : lambda_scope.
Pierre Letouzey's avatar
Pierre Letouzey committed
54
(*Notation "u , v" := (Couple u v) (at level 20) : lambda_scope. *)
55
56
Notation "σ -> τ" := (Arr σ τ) : lambda_scope.
Notation "σ /\ τ" := (And σ τ) : lambda_scope.
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
57
Notation "σ \/ τ" := (Or σ τ) : lambda_scope.
58
59
60
61
62
63
64
65
66
67
68
69
70
71
Notation "# n" := (Var n) (at level 20, format "# n") : lambda_scope.

Delimit Scope lambda_scope with lam.
Bind Scope lambda_scope with term.

Open Scope lambda_scope.

Coercion Var : nat >-> term.
Check Abs 0 @ 0.

Fixpoint to_form (t : type) : formula :=
  match t with
    | Arr u v => ((to_form u) -> (to_form v))%form
    | Atom a => Pred a []
Pierre Letouzey's avatar
Pierre Letouzey committed
72
    | Unit => True
73
    | Bot => False
74
    | And u v => ((to_form u) /\ (to_form v))%form
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
75
    | Or u v => ((to_form u) \/ (to_form v))%form
76
77
78
79
80
81
82
  end.

Definition to_ctxt (Γ : context) := List.map to_form Γ.

Theorem CurryHoward Γ u τ :
  typed Γ u τ -> Pr Intuiti (to_ctxt Γ  to_form τ).
Proof.
Pierre Letouzey's avatar
Pierre Letouzey committed
83
  induction 1; cbn.
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
84
85
  - apply R_Ax.
    apply in_map.
86
    apply nth_error_In with (n := n); auto.
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
87
88
  - apply R_Imp_e with (A := to_form σ); intuition.
  - apply R_Imp_i. intuition.
Pierre Letouzey's avatar
Pierre Letouzey committed
89
  - apply R_Tr_i.
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
90
91
92
93
  - apply R_Fa_e. intuition.
  - apply R_And_i; intuition.
  - apply R_And_e1 with (B := to_form τ). intuition.
  - apply R_And_e2 with (A := to_form σ). intuition.
Pierre Letouzey's avatar
Pierre Letouzey committed
94
95
96
  - eapply R_Or_e; eauto.
  - now apply R_Or_i1.
  - now apply R_Or_i2.
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
97
98
99
100
Qed.

Lemma ex : Pr Intuiti ([]  (Pred "A" [] /\ Pred "B" []) -> (Pred "A" [] \/ Pred "B" [])).
Proof.
Pierre Letouzey's avatar
Pierre Letouzey committed
101
102
  set (typ := Atom "A" /\ Atom "B" -> Atom "A" \/ Atom "B").
  change (Pr J (to_ctxt []  to_form typ)).
Samuel Ben Hamou's avatar
Samuel Ben Hamou committed
103
104
105
106
107
108
  apply CurryHoward with (u := (Abs (I1 (Pi1 (#0))))).
  unfold typ.
  apply Type_Abs.
  apply Type_I1.
  apply Type_Pi1 with (τ := Atom "B").
  apply Type_Var.
Pierre Letouzey's avatar
Pierre Letouzey committed
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
  easy.
Qed.

Instance eqb_type : Eqb type :=
 fix eqb_type (u v:type) :=
   match u, v with
   | Unit, Unit | Bot, Bot => true
   | Atom a, Atom b => a =? b
   | Arr u1 u2, Arr v1 v2
   | And u1 u2, And v1 v2
   | Or u1 u2, Or v1 v2 => eqb_type u1 v1 && eqb_type u2 v2
   | _, _ => false
   end.

Instance eqbspec_type : EqbSpec type.
Proof.
 red. induction x; destruct y; cbn; try constructor; try easy.
 - destruct (IHx1 y1), (IHx2 y2); cbn; constructor; congruence.
 - case eqbspec; constructor; congruence.
 - destruct (IHx1 y1), (IHx2 y2); cbn; constructor; congruence.
 - destruct (IHx1 y1), (IHx2 y2); cbn; constructor; congruence.
Qed.

Lemma list_index_nth_error {A} `(EqbSpec A) n x l :
  list_index x l = Some n -> nth_error l n = Some x.
Proof.
 revert n. induction l; intros n; cbn; try easy.
 case eqbspec. now intros -> [= <-].
 intros N. destruct (list_index x l); try easy. cbn.
 intros [= <-]. cbn; auto.
Qed.

Fixpoint of_form (f : formula) : type :=
  match f with
  | True => Unit
  | False => Bot
  | Pred a _ => Atom a
  | Not A => Arr (of_form A) Bot
  | (A->B) => Arr (of_form A) (of_form B)
  | (A/\B) => And (of_form A) (of_form B)
  | (A\/B) => Or (of_form A) (of_form B)
  | Quant _ A => of_form A
  end%form.

Definition of_ctxt (Γ : Mix.context) := List.map of_form Γ.

Lemma of_to_form T : of_form (to_form T) = T.
Proof.
 induction T; cbn; now f_equal.
Qed.

Lemma of_form_bsubst n t A :
 of_form (bsubst n t A) = of_form A.
Proof.
 revert n t; induction A; cbn; intros; auto.
 - now f_equal.
 - destruct o; f_equal; auto.
Qed.

Theorem CurryHoward_recip seq :
  Pr Intuiti seq ->
  let '(Γ  A) := seq in exists u, typed (of_ctxt Γ) u (of_form A).
Proof.
 induction 1; cbn in *.
 - unfold of_ctxt.
   apply (in_map of_form) in H.
   rewrite <- list_index_in in H.
   destruct (list_index (of_form A) (map of_form Γ)) eqn:E; try easy.
   exists (Var n). constructor.
   apply list_index_nth_error; eauto with *.
 - exists One; auto.
 - destruct IHPr as (u,P). exists (Nabla u); auto.
 - destruct IHPr as (u,P). exists (Abs u); auto.
 - destruct IHPr1 as (u,P), IHPr2 as (v,Q). exists (v @ u); eauto.
 - destruct IHPr1 as (u,P), IHPr2 as (v,Q). exists (Couple u v); eauto.
 - destruct IHPr as (u,P). exists (Pi1 u); eauto.
 - destruct IHPr as (u,P). exists (Pi2 u); eauto.
 - destruct IHPr as (u,P). exists (I1 u); auto.
 - destruct IHPr as (u,P). exists (I2 u); auto.
 - destruct IHPr1 as (u,P), IHPr2 as (v,Q), IHPr3 as (w,R).
   exists (Case u v w); eauto.
 - destruct IHPr as (u,P). exists (Abs u); auto.
 - destruct IHPr1 as (u,P), IHPr2 as (v,Q). exists (u @ v); eauto.
 - destruct IHPr as (u,P). rewrite of_form_bsubst in P.
   now exists u.
 - destruct IHPr as (u,P). exists u. now rewrite of_form_bsubst.
 - destruct IHPr as (u,P). exists u. now rewrite of_form_bsubst in P.
 - destruct IHPr1 as (u,P), IHPr2 as (v,Q).
   rewrite of_form_bsubst in Q. exists (Abs v @ u); eauto.
 - easy.
Qed.

Theorem CurryHoward_recip' Γ A :
  Pr Intuiti (Γ  A) -> exists u, typed (of_ctxt Γ) u (of_form A).
Proof.
 apply CurryHoward_recip.
205
Qed.