LPTerm.v 11.6 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
WIP.  
Gaspard Ferey committed
104 105 106 107 108 109 110
Definition pop_context (c:context) : context :=
  match c with
  | CEmpty     => c
  | CVar _ _ c => c
  | CRel _ _ c => c
  end.

Gaspard Ferey's avatar
Gaspard Ferey committed
111
Reserved Notation "x ':' A '∈' Γ" (at level 80, A at level 80, Γ at level 80).
112
Inductive InCtx : context -> Var -> term -> Prop :=
Gaspard Ferey's avatar
Gaspard Ferey committed
113
| INow      : forall Γ x A, x : A  (Γ, x : A)
114
| IAfterV   : forall Γ A x y B, x : A  Γ -> x : A  (Γ, y : B)
Gaspard Ferey's avatar
Gaspard Ferey committed
115
| IAfterR   : forall Γ A x t u, x : A  Γ -> x : A  (Γ, t  u)
116 117
where "x ':' A ∈ Γ" := (InCtx Γ x A).

Gaspard Ferey's avatar
Gaspard Ferey committed
118
Reserved Notation "t '≡' u '∈' Γ" (at level 80, u at level 80, Γ at level 80).
119
Inductive InRelCtx : context -> term -> term -> Prop :=
Gaspard Ferey's avatar
Gaspard Ferey committed
120
| IRNow      : forall Γ t u, t  u  (Γ, t  u)
121
| IRAfterV   : forall Γ t u y B, t  u  Γ -> t  u  (Γ, y : B)
Gaspard Ferey's avatar
Gaspard Ferey committed
122
| IRAfterR   : forall Γ t u v w, t  u  Γ -> t  u  (Γ, v  w)
123 124
where "t '≡' u ∈ Γ" := (InRelCtx Γ t u).

Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
125 126 127 128 129
Definition Defined_var Γ v := exists T, v : T  Γ.
Definition   Fresh_var Γ v := ~ (Defined_var Γ v).

(* ************ Locally nameless representation ************ *)

François Thiré's avatar
François Thiré committed
130 131
Fixpoint open_k (t u : term) (k : nat) :=
  match t with
Gaspard Ferey's avatar
Gaspard Ferey committed
132 133 134
  | TKind      => t
  | TType      => t
  | TFree n    => t
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
135
  | TBound i   => if Nat.eqb k i then u else t
Gaspard Ferey's avatar
Gaspard Ferey committed
136
  | TApp l r   => TApp (open_k l u k) (open_k r u k)
François Thiré's avatar
François Thiré committed
137
  | TAbs ty te => TAbs (open_k ty u k) (open_k te u (S k))
Gaspard Ferey's avatar
Gaspard Ferey committed
138
  | TPi ty te  => TPi (open_k ty u k) (open_k te u (S k))
François Thiré's avatar
François Thiré committed
139
  end.
Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
140 141 142
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
143

Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
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
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
192 193 194

Fixpoint subst_k (t u : term) (z : Var) : term :=
  match t with
Gaspard Ferey's avatar
Gaspard Ferey committed
195 196 197 198 199
  | 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
200
  | TAbs ty te => TAbs (subst_k ty u z) (subst_k ty u z)
Gaspard Ferey's avatar
Gaspard Ferey committed
201
  | TPi  ty te => TPi  (subst_k ty u z) (subst_k ty u z)
François Thiré's avatar
François Thiré committed
202 203 204 205
  end.

Fixpoint close_k (t : term) (k : nat) (z : Var) : term :=
  match t with
Gaspard Ferey's avatar
Gaspard Ferey committed
206 207 208 209 210
  | 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)
211 212
  | 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
213
  end.
214

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

Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
217 218 219
Notation "A '~>' B" := (TPi A B) (at level 22, right associativity).
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
220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271


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).

Notation "Γ '⊢' t '≡' u" := (Γ  t ≡βΓ  u) (at level 40, t at level 25).
Reserved Notation "Γ '⊢' t ':' A"          (at level 40, t at level 25).
Reserved Notation "Γ ✓"                    (at level 40).
272 273 274

Inductive typing : context -> term -> term -> Prop :=
| TyAxiom : forall Γ x A, Γ  -> x : A  Γ -> Γ  (# x) : A
275
| TyType  : forall Γ, Γ  -> Γ  type : kind
Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
276
| TyPi    : forall L Γ A B s,
François Thiré's avatar
François Thiré committed
277
            Γ  A : type ->
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
278
            (forall x, ~(In x L) -> Γ , x : A  B[x] : s) ->
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
279
            Γ  Π A ~ B : s
Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
280
| TyAbs   : forall L Γ A B t s,
François Thiré's avatar
François Thiré committed
281
            Γ  A : type ->
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
282 283
            (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
284
            Γ  λ A ~ t : Π A ~ B
François Thiré's avatar
François Thiré committed
285
| TyApp   : forall Γ t u A B, Γ  t : Π A ~ B -> Γ  u : A -> Γ  t @ u : B [0 <- u]
Gaspard Ferey's avatar
Gaspard Ferey committed
286
| TyConv  : forall Γ t A B s, (Γ  t : A) -> (Γ  B : s) -> Γ  A  B -> (Γ  t : B)
287 288 289
where "Γ '⊢' t ':' A" := (typing Γ t A)
with well_formed : context -> Prop :=
     | WFEmpty : [ ] 
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
290 291
     | WFVarT  : forall Γ x A, Fresh_var Γ x -> Γ  A : type -> Γ, x : A 
     | WFVarK  : forall Γ x A, Fresh_var Γ x -> Γ  A : kind -> Γ, x : A 
Gaspard Ferey's avatar
Gaspard Ferey committed
292 293
     | 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
294