Lambda.v 2.6 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11

(* A link with Lambda Calculus. *)

Require Import Defs Mix List.
Import ListNotations.

Open Scope list.

Inductive term :=
  | Var : nat -> term
  | App : term -> term -> term
12
13
  | Abs : term -> term
  | Nabla : term -> term.
14
15
16

Inductive type :=
  | Arr : type -> type -> type
17
18
  | Atom : name -> type
  | Bot : type.
19
20
21
22
23
24

Definition context := list type.

Inductive typed : context -> term -> type -> Prop :=
  | Type_Ax : forall Γ τ n, nth_error Γ n = Some τ -> typed Γ (Var n) τ
  | Type_App : forall Γ u v σ μ, typed Γ u (Arr σ μ) -> typed Γ v σ -> typed Γ (App u v) μ
25
26
  | Type_Abs : forall Γ u σ μ,  typed (σ :: Γ) u μ -> typed Γ (Abs u) (Arr σ μ)
  | Type_Nabla : forall Γ u τ, typed Γ u Bot -> typed Γ (Nabla u) τ.
27
28

Notation "u @ v" := (App u v) (at level 20) : lambda_scope.
29
Notation "∇ u" := (Nabla u) (at level 20) : lambda_scope.
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
Notation "σ -> μ" := (Arr σ μ) : lambda_scope.
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 []
45
    | Bot => False
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
  end.

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

Lemma In_in τ Γ :
  In τ Γ -> In (to_form τ) (to_ctxt Γ).
Proof.
  induction Γ.
  - intros. inversion H.
  - intros.
    assert (a :: Γ = [a] ++ Γ). { easy. }
    rewrite H0 in H. clear H0.
    apply in_app_or in H.
    destruct H.
    + inversion H; [ | inversion H0 ].
      unfold to_ctxt. rewrite List.map_cons.
      rewrite H0.
      apply in_eq.
    + unfold to_ctxt. rewrite List.map_cons.
      apply in_cons.
      apply IHΓ. assumption.
Qed.

Theorem CurryHoward Γ u τ :
  typed Γ u τ -> Pr Intuiti (to_ctxt Γ  to_form τ).
Proof.
  revert Γ. revert τ.
  induction u.
  - intros.
    inversion H. clear Γ0 τ0 n0 H1 H0 H3.
    apply R_Ax.
    apply In_in.
    apply nth_error_In with (n := n); auto.
  - intros.
    inversion H. clear H2 H0 H1 H4.
    apply R_Imp_e with (A := to_form σ).
    + specialize IHu1 with (τ := σ -> τ) (Γ := Γ).
      cbn in IHu1.
      intuition.
    + specialize IHu2 with (τ := σ) (Γ := Γ).
      intuition.
  - intros.
    inversion H. clear Γ0 u0 H1 H0.
    rewrite<- H3 in H. clear H3.
    specialize IHu with (τ := μ) (Γ := σ :: Γ).
    cbn. apply R_Imp_i.
    intuition.
93
94
95
96
97
  - intros.
    inversion H. clear Γ0 u0 τ0 H1 H0 H3.
    specialize IHu with (τ := Bot) (Γ := Γ). cbn in IHu.
    apply R_Fa_e.
    intuition.
98
Qed.