Coq/LPTerm.v

@@ -59,7 +59,7 @@ Fixpoint   closed (t:term) := match t with
   | TApp t u => (closed t) /\ (closed u)
 end.
 
-Theorem close_FV : forall t, (closed t) <-> (FV t) = nil.
+Theorem closed_FV : forall t, (closed t) <-> (FV t) = nil.
 Proof.
   intro. split ; intros.
   - induction t ; intros ; try easy.
@@ -132,7 +132,7 @@ Fixpoint open_k (t u : term) (k : nat) :=
   | TKind      => t
   | TType      => t
   | TFree n    => t
-  | TBound i   => if Nat.eq_dec k i then u else t
+  | TBound i   => if Nat.eqb k i then u else t
   | TApp l r   => TApp (open_k l u k) (open_k r u k)
   | TAbs ty te => TAbs (open_k ty u k) (open_k te u (S k))
   | TPi ty te  => TPi (open_k ty u k) (open_k te u (S k))
@@ -141,6 +141,54 @@ Notation "t '[' k '<-' u ']'" := (open_k t u k) (at level 24).
 
 Definition open (t u : term) := t [ 0 <- u ].
 
+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.
+
+
+
 
 Fixpoint subst_k (t u : term) (z : Var) : term :=
   match t with
@@ -227,12 +275,12 @@ Inductive typing : context -> term -> term -> Prop :=
 | TyType  : forall Γ, Γ ✓ -> Γ ⊢ type : kind
 | TyPi    : forall L Γ A B s,
             Γ ⊢ A : type ->
-            (forall x, ~(In x L) -> Γ , x : A ⊢ (close B x) : s) ->
+            (forall x, ~(In x L) -> Γ , x : A ⊢ B[x] : s) ->
             Γ ⊢ Π A ~ B : s
 | TyAbs   : forall L Γ A B t s,
             Γ ⊢ A : type ->
-            (forall x, ~ (In x L) -> Γ, x : A ⊢ (close B x) : s) ->
-            (forall x, ~ (In x L) -> Γ, x : A ⊢ (close t x) : (close B x)) ->
+            (forall x, ~ (In x L) -> Γ, x : A ⊢ B[x] : s) ->
+            (forall x, ~ (In x L) -> Γ, x : A ⊢ t[x] : B[x]) ->
             Γ ⊢ λ A ~ t : Π A ~ B
 | TyApp   : forall Γ t u A B, Γ ⊢ t : Π A ~ B -> Γ ⊢ u : A -> Γ ⊢ t @ u : B [0 <- u]
 | TyConv  : forall Γ t A B s, (Γ ⊢ t : A) -> (Γ ⊢ B : s) -> Γ ⊢ A ≡ B -> (Γ ⊢ t : B)
@@ -243,3 +291,4 @@ with well_formed : context -> Prop :=
      | WFVarK  : forall Γ x A, Fresh_var Γ x -> Γ ⊢ A : kind -> Γ, x : A ✓
      | WFRel   : forall Γ A s t u, Γ ⊢ A : s -> Γ ⊢ t : A -> Γ ⊢ u : A -> Γ ✓ -> Γ, t ≡ u ✓
 where "Γ ✓" := (well_formed Γ).
+

Coq/WF.v

@@ -4,14 +4,86 @@ Require Import List.
 Require Import LPTerm.
 
 
-Theorem not_in_not_eq {A:Type} : forall (x v : A) l, ~ (In x (v::l)) -> x <> v.
+Theorem types_WF : forall Γ t u, Γ ⊢ t : u -> Γ ✓.
+Proof. intros. induction H; easy. Qed.
+
+Theorem vardecl_WF : forall Γ x A, Γ, x : A ✓ -> Γ ✓.
 Proof.
   intros.
-  intro.
-  apply H.
-  now left.
+  remember (Γ, x : A) as Γ2.
+  induction H; inversion HeqΓ2; subst; eapply types_WF; apply H0.
 Qed.
 
+Theorem ruldecl_WF : forall Γ t u, Γ, t ≡ u ✓ -> Γ ✓.
+Proof.
+  intros.
+  remember (Γ, t ≡ u) as Γ2.
+  induction H; inversion HeqΓ2; subst; eapply types_WF; apply H0.
+Qed.
+
+
+
+Inductive weaker : context -> context -> Prop :=
+| WeakRefl        : forall Γ       , weaker Γ Γ
+| WeakVarDecl     : forall Γ    x A, weaker Γ (Γ, x : A)
+| WeakRulDecl     : forall Γ    t u, weaker Γ (Γ, t ≡ u)
+| WeakNextVarDecl : forall Γ Γ' x A, weaker Γ Γ' -> weaker (Γ, x : A) (Γ', x : A)
+| WeakNextRulDecl : forall Γ Γ' t u, weaker Γ Γ' -> weaker (Γ, t ≡ u) (Γ', t ≡ u).
+
+
+Theorem subset_var_decl : forall Γ Γ' x A, weaker Γ Γ' -> x : A ∈ Γ -> x : A ∈ Γ'.
+Proof.
+  intros.
+  induction H.
+  - easy.
+  - apply IAfterV. easy.
+  - apply IAfterR. easy.
+  - remember (Γ, x0 : A0) as Γ2. induction H0.
+    + inversion HeqΓ2. subst. apply INow.
+    + inversion HeqΓ2. subst. apply IAfterV. apply IHweaker. easy.
+    + inversion HeqΓ2.
+  - remember (Γ, t ≡ u) as Γ2. induction H0 ; inversion HeqΓ2.
+    subst. apply IAfterR. apply IHweaker. easy.
+Qed.
+
+Theorem subset_rul_decl : forall Γ Γ' t u, weaker Γ Γ' -> t ≡ u ∈ Γ -> t ≡ u ∈ Γ'.
+Proof.
+  intros.
+  induction H.
+  - easy.
+  - apply IRAfterV. easy.
+  - apply IRAfterR. easy.
+  - remember (Γ, x : A) as Γ2. induction H0.
+    + inversion HeqΓ2.
+    + inversion HeqΓ2. subst. apply IRAfterV. apply IHweaker. easy.
+    + inversion HeqΓ2.
+  - remember (Γ, t0 ≡ u0) as Γ2. induction H0; inversion HeqΓ2.
+    + subst. econstructor.
+    + inversion HeqΓ2. subst. apply IRAfterR. apply IHweaker. easy.
+Qed.
+
+Theorem fresh_vars_weaker : forall Γ Γ' x, weaker Γ Γ' -> Fresh_var Γ' x -> Fresh_var Γ x.
+Proof.
+  intros. intro. apply H0. destruct H1. exists x0. eapply subset_var_decl. apply H. easy.
+Qed.
+
+
+Theorem weak : forall Γ Γ' t u, Γ ⊢ t : u -> weaker Γ Γ' -> Γ' ✓ -> Γ' ⊢ t : u.
+Proof.
+  intros.
+  generalize dependent Γ'.
+  induction H; intros.
+  - apply TyAxiom. easy. eapply subset_var_decl. apply H1. easy.
+  - apply TyType. easy.
+  - eapply TyPi.
+    + apply IHtyping. easy. easy.
+    + intro. intro. apply H1. apply H4. apply WeakNextVarDecl. easy. econstructor.
+      Admitted.
+      
+
+Theorem not_in_not_eq {A:Type} : forall (x v : A) l, ~ (In x (v::l)) -> x <> v.
+Proof. intros. intro. apply H. now left. Qed.
+
 Theorem FV_close : forall x y t, In x (FV t) -> x <> y -> forall n, In x (FV (close_k t n y)).
 Proof.
   intros x y t H x_neq_y.