LPTerm.v 12.4 KB
Newer Older
François Thiré's avatar
François Thiré committed
1
(** Start to implement lambda pi modulo with pretty printing.
2 3 4 5 6 7
    TODO:
    - Have a better pretty printing for binders
    - no substitution
    - Try a localy nameless representation, but not implemented
*)

François Thiré's avatar
François Thiré committed
8
Require Import PeanoNat.
François Thiré's avatar
François Thiré committed
9
Require Import List.
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
10

11 12 13 14
Parameter Var : Set.

Axiom var_dec : forall (x y:Var), {x = y} + {x <> y}.

Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
15 16
Axiom var_inf : forall l, exists x:Var, ~ (In x l).

Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
17 18
(* ************ Terms ************ *)

19
Inductive term : Set :=
Gaspard Ferey's avatar
Gaspard Ferey committed
20 21
| TKind  : term
| TType  : term
22
| TFree  : Var  -> term
Gaspard Ferey's avatar
Gaspard Ferey committed
23
| TBound : nat    -> term
24 25 26 27
| TPi    : term -> term -> term
| TAbs   : term -> term -> term
| TApp   : term -> term -> term.

Gaspard Ferey's avatar
Gaspard Ferey committed
28 29 30 31 32
Notation "'#' x" := (TFree  x) (at level 20).
Notation "'?' x" := (TBound x) (at level 20).
Notation "'Π' A '~' B" := (TPi A B) (at level 22, right associativity).
Notation "'λ' A '~' u" := (TAbs A u) (at level 22).
Notation "t '@' u" := (TApp t u) (at level 21, left associativity).
33

Gaspard Ferey's avatar
Gaspard Ferey committed
34 35
Definition type : term := TType.
Definition kind : term := TKind.
36

Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
37 38 39

(* ************ Free variables ************ *)

Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
40 41 42 43 44 45 46 47 48 49 50
Fixpoint FV (t:term) : list Var :=
  match t with
  | TKind    => nil
  | TType    => nil
  | TFree v  => cons v nil
  | TBound _ => nil
  | TPi  A B => (FV A) ++ (FV B)
  | TAbs A B => (FV A) ++ (FV B)
  | TApp t u => (FV t) ++ (FV u)
  end.

Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
51 52 53 54 55 56 57 58 59 60 61

Fixpoint   closed (t:term) := match t with
  | TKind    => True
  | TType    => True
  | TFree v  => False
  | TBound _ => True
  | TPi  A B => (closed A) /\ (closed B)
  | TAbs A B => (closed A) /\ (closed B)
  | TApp t u => (closed t) /\ (closed u)
end.

Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
62
Theorem closed_FV : forall t, (closed t) <-> (FV t) = nil.
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
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
Proof.
  intro. split ; intros.
  - induction t ; intros ; try easy.
    + destruct H. simpl.
      assert (FV t1 = nil); auto.
      assert (FV t2 = nil); auto.
      rewrite H1. rewrite H2. easy.
    + destruct H. simpl.
      assert (FV t1 = nil); auto.
      assert (FV t2 = nil); auto.
      rewrite H1. rewrite H2. easy.
    + destruct H. simpl.
      assert (FV t1 = nil); auto.
      assert (FV t2 = nil); auto.
      rewrite H1. rewrite H2. easy.
  - induction t ; try easy.
    + econstructor.
      * apply IHt1. apply (proj1 (app_eq_nil (FV t1) (FV t2) H)).
      * apply IHt2. apply (proj2 (app_eq_nil (FV t1) (FV t2) H)).
    + econstructor.
      * apply IHt1. apply (proj1 (app_eq_nil (FV t1) (FV t2) H)).
      * apply IHt2. apply (proj2 (app_eq_nil (FV t1) (FV t2) H)).
    + econstructor.
      * apply IHt1. apply (proj1 (app_eq_nil (FV t1) (FV t2) H)).
      * apply IHt2. apply (proj2 (app_eq_nil (FV t1) (FV t2) H)).
Qed.




Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
93 94
(* ************ Contexts ************ *)

95 96 97 98 99
Inductive context : Set :=
| CEmpty : context
| CVar   : Var -> term -> context -> context
| CRel   : term -> term -> context -> context.

Gaspard Ferey's avatar
Gaspard Ferey committed
100 101 102
Notation "[ ]" := CEmpty (at level 0).
Notation "Γ ',' x ':' A" := (CVar x A Γ) (at level 30, x at level 30).
Notation "Γ ',' t '≡' u" := (CRel t u Γ) (at level 30, t at level 30).
103

Gaspard Ferey's avatar
Gaspard Ferey committed
104 105 106 107 108 109 110 111 112 113 114 115
Definition pop_context (Γ:context) : context :=
  match Γ with
  | CEmpty     => Γ
  | CVar _ _ Γ => Γ
  | CRel _ _ Γ => Γ
  end.

Fixpoint defined_vars (Γ:context) : list Var :=
  match Γ with
  | CEmpty     => nil
  | CVar x _ Γ => cons x (defined_vars Γ)
  | CRel _ _ Γ => (defined_vars Γ)
Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
116 117
  end.

Gaspard Ferey's avatar
Gaspard Ferey committed
118
Reserved Notation "x ':' A '∈' Γ" (at level 80, A at level 80, Γ at level 80).
119
Inductive InCtx : context -> Var -> term -> Prop :=
Gaspard Ferey's avatar
Gaspard Ferey committed
120
| INow      : forall Γ x A, x : A  (Γ, x : A)
Gaspard Ferey's avatar
Gaspard Ferey committed
121
| IAfterV   : forall Γ A x y B, x : A  Γ -> x <> y -> x : A  (Γ, y : B)
Gaspard Ferey's avatar
Gaspard Ferey committed
122
| IAfterR   : forall Γ A x t u, x : A  Γ -> x : A  (Γ, t  u)
123 124
where "x ':' A ∈ Γ" := (InCtx Γ x A).

Gaspard Ferey's avatar
Gaspard Ferey committed
125
Reserved Notation "t '≡' u '∈' Γ" (at level 80, u at level 80, Γ at level 80).
126
Inductive InRelCtx : context -> term -> term -> Prop :=
Gaspard Ferey's avatar
Gaspard Ferey committed
127
| IRNow      : forall Γ t u, t  u  (Γ, t  u)
128
| IRAfterV   : forall Γ t u y B, t  u  Γ -> t  u  (Γ, y : B)
Gaspard Ferey's avatar
Gaspard Ferey committed
129
| IRAfterR   : forall Γ t u v w, t  u  Γ -> t  u  (Γ, v  w)
130 131
where "t '≡' u ∈ Γ" := (InRelCtx Γ t u).

Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
132 133 134
Definition Defined_var Γ v := exists T, v : T  Γ.
Definition   Fresh_var Γ v := ~ (Defined_var Γ v).

Gaspard Ferey's avatar
Gaspard Ferey committed
135 136 137
Notation "x '∈' Γ" := (Defined_var Γ x) (at level 90).
Notation "x '∉' Γ" := (Fresh_var   Γ x) (at level 90).

Gaspard Ferey's avatar
Gaspard Ferey committed
138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155
Theorem defined_eq : forall Γ v, Defined_var Γ v <-> In v (defined_vars Γ).
Proof.
  intros.
  split; intros.
  - induction H. induction H.
    + left. easy.
    + right. easy.
    + easy.
  - induction Γ.
    + contradiction H.
    + destruct (var_dec v v0).
      * subst. econstructor. econstructor.
      * assert (v  Γ). apply IHΓ. destruct H. contradiction n. easy. easy.
        destruct H0. econstructor. apply IAfterV. apply H0. easy.
    + assert (v  Γ). apply IHΓ. exact H.
      destruct H0. econstructor. apply IAfterR. apply H0.
Qed.

Gaspard Ferey's avatar
Gaspard Ferey committed
156

Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
157 158
(* ************ Locally nameless representation ************ *)

François Thiré's avatar
François Thiré committed
159 160
Fixpoint open_k (t u : term) (k : nat) :=
  match t with
Gaspard Ferey's avatar
Gaspard Ferey committed
161 162 163
  | TKind      => t
  | TType      => t
  | TFree n    => t
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
164
  | TBound i   => if Nat.eqb k i then u else t
Gaspard Ferey's avatar
Gaspard Ferey committed
165
  | TApp l r   => TApp (open_k l u k) (open_k r u k)
François Thiré's avatar
François Thiré committed
166
  | TAbs ty te => TAbs (open_k ty u k) (open_k te u (S k))
Gaspard Ferey's avatar
Gaspard Ferey committed
167
  | TPi ty te  => TPi (open_k ty u k) (open_k te u (S k))
François Thiré's avatar
François Thiré committed
168
  end.
Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
169 170 171
Notation "t '[' k '<-' u ']'" := (open_k t u k) (at level 24).

Definition open (t u : term) := t [ 0 <- u ].
François Thiré's avatar
François Thiré committed
172

Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
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 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220
Theorem open_k_FV : forall t u x k, In x (FV (open_k t u k)) -> In x (FV t) \/ In x (FV u).
Proof.
  intro. intro. intro.  induction t.
  - intros. contradict H.
  - intros. contradict H.
  - intros. destruct H. rewrite H. left. left. easy. contradict H.
  - intros. destruct (Nat.eq_dec k n); subst.
    + right. assert ((n =? n) = true).
      eapply Nat.eqb_eq ; easy.
      cbn in H. rewrite H0 in H. easy.
    + cbn in H. assert (~ (k =? n) = true).
      * intro. apply n0. eapply Nat.eqb_eq. easy.
      * pose proof (Bool.not_true_is_false (k =? n) H0). cbn in H. rewrite H1 in H. left. easy.
  - intros. simpl.
    pose proof (in_app_or (FV (t1 [k <- u])) (FV (t2 [S k <- u])) x H). destruct H0.
    + simpl. pose proof (IHt1 k     H0). destruct H1.
      left. apply in_or_app. left. easy. right. easy.
    + simpl. pose proof (IHt2 (S k) H0). destruct H1.
      left. apply in_or_app. right. easy. right. easy.
  - intros. simpl. cbn in H.
    pose proof (in_app_or (FV (t1 [k <- u])) (FV (t2 [S k <- u])) x H). destruct H0.
    + simpl. pose proof (IHt1 k     H0). destruct H1.
      left. apply in_or_app. left. easy. right. easy.
    + simpl. pose proof (IHt2 (S k) H0). destruct H1.
      left. apply in_or_app. right. easy. right. easy.
  - intros. simpl. cbn in H.
    pose proof (in_app_or (FV (t1 [k <- u])) (FV (t2 [k <- u])) x H). destruct H0.
    + simpl. pose proof (IHt1 k H0). destruct H1.
      left. apply in_or_app. left. easy. right. easy.
    + simpl. pose proof (IHt2 k H0). destruct H1.
      left. apply in_or_app. right. easy. right. easy.
Qed.


(* Substitute DB_0 with a named var. *)
Definition open_v (t : term) (v : Var) := t [0 <- # v].
Notation "t '[' v ']'" := (open_v t v) (at level 24).
  
Theorem open_FV : forall t v x, In x (FV (open_v t v)) -> x = v \/ In x (FV t).
Proof.
  intros. cbn in H.
  destruct (open_k_FV t (# v) x 0 H).
  + right. easy.
  + left. destruct H0 ; easy.
Qed.



François Thiré's avatar
François Thiré committed
221 222 223

Fixpoint subst_k (t u : term) (z : Var) : term :=
  match t with
Gaspard Ferey's avatar
Gaspard Ferey committed
224 225 226 227 228
  | TKind      => t
  | TType      => t
  | TBound i   => t
  | TFree x    => if var_dec x z then u else t
  | TApp l  r  => TApp (subst_k l  u z) (subst_k r  u z)
François Thiré's avatar
François Thiré committed
229
  | TAbs ty te => TAbs (subst_k ty u z) (subst_k ty u z)
Gaspard Ferey's avatar
Gaspard Ferey committed
230
  | TPi  ty te => TPi  (subst_k ty u z) (subst_k ty u z)
François Thiré's avatar
François Thiré committed
231 232 233 234
  end.

Fixpoint close_k (t : term) (k : nat) (z : Var) : term :=
  match t with
Gaspard Ferey's avatar
Gaspard Ferey committed
235 236 237 238 239
  | TKind      => t
  | TType      => t
  | TBound i   => t
  | TFree x    => if var_dec x z then TBound k else t
  | TApp l r   => TApp (close_k l  k z) (close_k r  k     z)
240 241
  | TAbs ty te => TAbs (close_k ty k z) (close_k te (S k) z)
  | TPi ty te  => TPi  (close_k ty k z) (close_k te (S k) z)
François Thiré's avatar
François Thiré committed
242
  end.
243

Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
244
Definition close (t : term) (z : Var) : term := close_k t 0 z.
245

Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
246 247
Notation "x ';' A '~>' B" := (TPi A (close B x))  (at level 22, A at level 21, right associativity).
Notation "x ';' A '=>' B" := (TAbs A (close B x)) (at level 22, A at level 21, right associativity).
Gaspard Ferey's avatar
Gaspard Ferey committed
248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296


Definition ConvScheme := context -> term -> term -> Prop.

Inductive RW_Head_Beta : ConvScheme :=
  RWBeta : forall Γ A t u,           RW_Head_Beta  Γ ((λ A ~ t) @ u) (open_k t u 0).
Inductive RW_Head_Gamma : ConvScheme :=
  RWRel  : forall Γ t u, t  u  Γ -> RW_Head_Gamma Γ t u.

Inductive ContextClosure (Cv:ConvScheme) : ConvScheme :=
| CCHere  : forall Γ t u  , Cv Γ t u -> ContextClosure Cv Γ t u
| CCApp1  : forall Γ f g t, Cv Γ f g -> ContextClosure Cv Γ (TApp f t) (TApp g t)
| CCApp2  : forall Γ f t u, Cv Γ t u -> ContextClosure Cv Γ (TApp f t) (TApp f u)
| CCAbs1  : forall Γ A B t, Cv Γ A B -> ContextClosure Cv Γ (TAbs A t) (TApp B t)
| CCAbs2  : forall Γ A t u, Cv Γ t u -> ContextClosure Cv Γ (TAbs A t) (TAbs A u)
| CCPi1   : forall Γ A B C, Cv Γ A B -> ContextClosure Cv Γ (TPi  A C) (TApp B C)
| CCPi2   : forall Γ A B C, Cv Γ B C -> ContextClosure Cv Γ (TPi  A B) (TApp A C).

Inductive ConvUnion (C1:ConvScheme) (C2:ConvScheme) : ConvScheme :=
| CV1 : forall Γ t u  , C1 Γ t u -> ConvUnion C1 C2 Γ t u
| CV2 : forall Γ t u  , C2 Γ t u -> ConvUnion C1 C2 Γ t u.

Inductive RTClosure (C:ConvScheme) : ConvScheme :=
| RWRule  : forall Γ t u  , C Γ t u -> RTClosure C Γ t u
| RWRefl  : forall Γ t    , RTClosure C Γ t t
| RWTrans : forall Γ t u v, RTClosure C Γ t u -> RTClosure C Γ u v -> RTClosure C Γ t v.

Inductive RSTClosure (C:ConvScheme) : ConvScheme :=
| CVRefl  : forall Γ t    , RSTClosure C Γ t t
| CVSym   : forall Γ t u  , RSTClosure C Γ t u -> RSTClosure C Γ u t
| CVTrans : forall Γ t u v, RSTClosure C Γ t u -> RSTClosure C Γ u v -> RSTClosure C Γ t v
| CVRule  : forall Γ t u  , C Γ t u -> RSTClosure C Γ t u.

Definition RW_Beta       : ConvScheme := ContextClosure RW_Head_Beta.
Definition RW_Gamma      : ConvScheme := ContextClosure RW_Head_Gamma.
Definition RW_Beta_Gamma : ConvScheme := ConvUnion RW_Beta RW_Gamma.

Notation "Γ '⊢' t '→β'   u" := ( RW_Head_Beta              Γ t u) (at level 40, t at level 25).
Notation "Γ '⊢' t '→Γ'   u" := ( RW_Head_Gamma             Γ t u) (at level 40, t at level 25).
Notation "Γ '⊢' t '↪β'   u" := ( RW_Beta                   Γ t u) (at level 40, t at level 25).
Notation "Γ '⊢' t '↪Γ'   u" := ( RW_Gamma                  Γ t u) (at level 40, t at level 25).
Notation "Γ '⊢' t '↪βΓ'  u" := ( RW_Beta_Gamma             Γ t u) (at level 40, t at level 25).
Notation "Γ '⊢' t '↪β*'  u" := ((RTClosure  RW_Beta      ) Γ t u) (at level 40, t at level 25).
Notation "Γ '⊢' t '↪Γ*'  u" := ((RTClosure  RW_Gamma     ) Γ t u) (at level 40, t at level 25).
Notation "Γ '⊢' t '↪βΓ*' u" := ((RTClosure  RW_Beta_Gamma) Γ t u) (at level 40, t at level 25).
Notation "Γ '⊢' t '≡β'   u" := ((RSTClosure RW_Beta      ) Γ t u) (at level 40, t at level 25).
Notation "Γ '⊢' t '≡Γ'   u" := ((RSTClosure RW_Gamma     ) Γ t u) (at level 40, t at level 25).
Notation "Γ '⊢' t '≡βΓ'  u" := ((RSTClosure RW_Beta_Gamma) Γ t u) (at level 40, t at level 25).

Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
297
Notation "Γ '⊢' t '≡' u" := (Γ  t ≡βΓ u)  (at level 40, t at level 25).
Gaspard Ferey's avatar
Gaspard Ferey committed
298 299
Reserved Notation "Γ '⊢' t ':' A"          (at level 40, t at level 25).
Reserved Notation "Γ ✓"                    (at level 40).
300 301 302

Inductive typing : context -> term -> term -> Prop :=
| TyAxiom : forall Γ x A, Γ  -> x : A  Γ -> Γ  (# x) : A
303
| TyType  : forall Γ, Γ  -> Γ  type : kind
Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
304
| TyPi    : forall L Γ A B s,
François Thiré's avatar
François Thiré committed
305
            Γ  A : type ->
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
306
            (forall x, ~(In x L) -> Γ , x : A  B[x] : s) ->
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
307
            Γ  Π A ~ B : s
Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
308
| TyAbs   : forall L Γ A B t s,
François Thiré's avatar
François Thiré committed
309
            Γ  A : type ->
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
310 311
            (forall x, ~ (In x L) -> Γ, x : A  B[x] : s) ->
            (forall x, ~ (In x L) -> Γ, x : A  t[x] : B[x]) ->
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
312
            Γ  λ A ~ t : Π A ~ B
François Thiré's avatar
François Thiré committed
313
| TyApp   : forall Γ t u A B, Γ  t : Π A ~ B -> Γ  u : A -> Γ  t @ u : B [0 <- u]
Gaspard Ferey's avatar
Gaspard Ferey committed
314
| TyConv  : forall Γ t A B s, Γ  t : A -> Γ  B : s -> Γ  A  B -> Γ  t : B
315 316 317
where "Γ '⊢' t ':' A" := (typing Γ t A)
with well_formed : context -> Prop :=
     | WFEmpty : [ ] 
Gaspard Ferey's avatar
Gaspard Ferey committed
318 319
     | WFVarT  : forall Γ x A, x  Γ -> Γ  A : type -> Γ, x : A 
     | WFVarK  : forall Γ x A, x  Γ -> Γ  A : kind -> Γ, x : A 
Gaspard Ferey's avatar
Gaspard Ferey committed
320 321
     | WFRel   : forall Γ A s t u, Γ  A : s -> Γ  t : A -> Γ  u : A -> Γ  -> Γ, t  u 
where "Γ ✓" := (well_formed Γ).
Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
322