use 'atom' in debruijn terms & complete proofs about type subst / open

coq/FSetNotin.v

@@ -6,7 +6,6 @@
 
 Set Implicit Arguments.
 Require Import FSetInterface.
-Require Import AdditionalTactics.
 Require AdditionalTactics.
 
 (* *********************************************************************** *)

coq/terms_debruijn.v

@@ -1,12 +1,17 @@
 From Coq Require Import Strings.String.
 From Coq Require Import Lists.List.
 Import ListNotations.
+From Coq Require Import Arith.EqNat.
 
+Local Open Scope nat_scope.
+Require Import Atom.
+Require Import Metatheory.
+Require Import FSetNotin.
 Require Import terms.
 
 Inductive type_DeBruijn : Type :=
   | ty_id : string -> type_DeBruijn
-  | ty_fvar : string -> type_DeBruijn
+  | ty_fvar : atom -> type_DeBruijn
   | ty_bvar : nat -> type_DeBruijn
   | ty_univ : type_DeBruijn -> type_DeBruijn
   | ty_spec : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
@@ -16,35 +21,36 @@ Inductive type_DeBruijn : Type :=
 .
 
 Inductive expr_DeBruijn : Type :=
-  | ex_var : nat -> expr_DeBruijn
+  | ex_fvar : atom -> expr_DeBruijn
+  | ex_bvar : nat -> expr_DeBruijn
   | ex_ty_abs : expr_DeBruijn -> expr_DeBruijn
   | ex_ty_app : expr_DeBruijn -> type_DeBruijn -> expr_DeBruijn
   | ex_abs   : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
   | ex_morph : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
   | ex_app : expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
-  | varlet : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
+  | ex_let : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
   | ex_ascend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
   | ex_descend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
 .
 
 (* get the list of all free variables in a type term *)
-Fixpoint type_fv (τ : type_DeBruijn) {struct τ} : (list string) :=
+Fixpoint type_fv (τ : type_DeBruijn) {struct τ} : atoms :=
   match τ with
-  | ty_id s => []
+  | ty_id s => {}
-  | ty_fvar α => [α]
+  | ty_fvar α => singleton α
-  | ty_bvar x => []
+  | ty_bvar x => {}
   | ty_univ τ => (type_fv τ)
-  | ty_spec σ τ => (type_fv σ) ++ (type_fv τ)
+  | ty_spec σ τ => (type_fv σ) `union` (type_fv τ)
-  | ty_func σ τ => (type_fv σ) ++ (type_fv τ)
+  | ty_func σ τ => (type_fv σ) `union` (type_fv τ)
-  | ty_morph σ τ => (type_fv σ) ++ (type_fv τ)
+  | ty_morph σ τ => (type_fv σ) `union` (type_fv τ)
-  | ty_ladder σ τ => (type_fv σ) ++ (type_fv τ)
+  | ty_ladder σ τ => (type_fv σ) `union` (type_fv τ)
   end.
 
 (* substitute free variable x with type σ in τ *)
-Fixpoint subst_type (x:string) (σ:type_DeBruijn) (τ:type_DeBruijn) {struct τ} : type_DeBruijn :=
+Fixpoint subst_type (x:atom) (σ:type_DeBruijn) (τ:type_DeBruijn) {struct τ} : type_DeBruijn :=
   match τ with
   | ty_id s => ty_id s
-  | ty_fvar s => if eqb x s then σ else τ
+  | ty_fvar s => if x == s then σ else τ
   | ty_bvar y => ty_bvar y
   | ty_univ τ => ty_univ (subst_type x σ τ)
   | ty_spec τ1 τ2 => ty_spec (subst_type x σ τ1) (subst_type x σ τ2)
@@ -54,10 +60,10 @@ Fixpoint subst_type (x:string) (σ:type_DeBruijn) (τ:type_DeBruijn) {struct τ}
   end.
 
 (* replace a free variable with a new (dangling) bound variable *)
-Fixpoint type_bind_fvar (x:string) (n:nat) (τ:type_DeBruijn) {struct τ} : type_DeBruijn :=
+Fixpoint type_bind_fvar (x:atom) (n:nat) (τ:type_DeBruijn) {struct τ} : type_DeBruijn :=
   match τ with
   | ty_id s => ty_id s
-  | ty_fvar s => if eqb x s then ty_bvar n else τ
+  | ty_fvar s => if x == s then ty_bvar n else τ
   | ty_bvar n => ty_bvar n
   | ty_univ τ1 => ty_univ (type_bind_fvar x (S n) τ1)
   | ty_spec τ1 τ2 => ty_spec (type_bind_fvar x n τ1) (type_bind_fvar x n τ2)
@@ -71,7 +77,7 @@ Fixpoint type_open_rec (k:nat) (σ:type_DeBruijn) (τ:type_DeBruijn) {struct τ}
   match τ with
     | ty_id s => ty_id s
     | ty_fvar s => ty_fvar s
-    | ty_bvar i => if Nat.eqb k i then σ else τ
+    | ty_bvar i => if k === i then σ else τ
     | ty_univ τ1 => ty_univ (type_open_rec (S k) σ τ1)
     | ty_spec τ1 τ2 => ty_spec (type_open_rec k σ τ1) (type_open_rec k σ τ2)
     | ty_func τ1 τ2 => ty_func (type_open_rec k σ τ1) (type_open_rec k σ τ2)
@@ -88,7 +94,7 @@ Inductive type_lc : type_DeBruijn -> Prop :=
   | Tlc_Id : forall s, type_lc (ty_id s)
   | Tlc_Var : forall s, type_lc (ty_fvar s)
   | Tlc_Univ : forall τ1 L,
-      (forall x, ~ (In x L) -> type_lc (type_open (ty_fvar x) τ1)) ->
+      (forall x, (x `notin` L) -> type_lc (type_open (ty_fvar x) τ1)) ->
       type_lc (ty_univ τ1)
   | Tlc_Spec : forall τ1 τ2, type_lc τ1 -> type_lc τ2 -> type_lc (ty_spec τ1 τ2)
   | Tlc_Func : forall τ1 τ2, type_lc τ1 -> type_lc τ2 -> type_lc (ty_func τ1 τ2)
@@ -109,10 +115,12 @@ Fixpoint type_debruijn_depth (τ:type_DeBruijn) : nat :=
   | ty_ladder s t => max (type_debruijn_depth s) (type_debruijn_depth t)
   end.
 
+
+(*
 Fixpoint type_named2debruijn (τ:type_term) {struct τ} : type_DeBruijn :=
   match τ with
   | type_id s => ty_id s
-  | type_var s => ty_fvar s
+  | type_var s => ty_fvar (pick fresh )
   | type_univ x t => let t':=(type_named2debruijn t) in (ty_univ (type_bind_fvar x 0 t'))
   | type_spec s t => ty_spec (type_named2debruijn s) (type_named2debruijn t)
   | type_fun s t => ty_func (type_named2debruijn s) (type_named2debruijn t)
@@ -121,48 +129,16 @@ Fixpoint type_named2debruijn (τ:type_term) {struct τ} : type_DeBruijn :=
   end.
 
 Coercion type_named2debruijn : type_term >-> type_DeBruijn.
-
+*)
-Lemma list_in_tail : forall x (E:list string) f,
-  In x E ->
-  In x (cons f E).
-Proof.
-  intros.
-  simpl.
-  right.
-  apply H.
-Qed.
-
-Lemma list_in_concatA : forall x (E:list string) (F:list string),
-  In x E ->
-  In x (E ++ F).
-Proof.
-Admitted.
-
-Lemma list_in_concatB : forall x (E:list string) (F:list string),
-  In x F ->
-  In x (E ++ F).
-Proof.
-  intros.
-  induction E.
-  auto.
-  apply list_in_tail.
-  
-Admitted.
-
-Lemma list_notin_singleton : forall (x:string) (y:string),
-  ((eqb x y) = false) -> ~ In x [ y ].
-Proof.
-Admitted.
-
-Lemma list_elim_notin_singleton : forall (x:string) (y:string),
-  ~ In x [y] -> ((eqb x y) = false).
-Proof.
-Admitted.
 
 
-Lemma subst_fresh_type : forall (x : string) (τ:type_DeBruijn) (σ:type_DeBruijn),
+
-  ~(In x (type_fv τ)) ->
+(*
-  (subst_type x σ τ) = τ
+ * Substitution has no effect if the variable is not free
+ *)
+Lemma subst_fresh_type : forall (x : atom) (τ:type_DeBruijn) (σ:type_DeBruijn),
+  x `notin` (type_fv τ) ->
+  ([ x ~> σ ] τ) = τ
 .
 Proof.
   intros.
@@ -171,9 +147,9 @@ Proof.
   - reflexivity.
 
   - unfold type_fv in H.
-    apply list_elim_notin_singleton in H.
+    apply AtomSetNotin.elim_notin_singleton in H.
     simpl.
-    case_eq (x =? s)%string.
+    case_eq (x == a).
     congruence.
     reflexivity.
 
@@ -183,99 +159,169 @@ Proof.
     reflexivity.
     apply H.
 
-  - simpl. rewrite IHτ1, IHτ2.
+  - simpl; rewrite IHτ1, IHτ2.
     reflexivity.
-    simpl type_fv in H.
+    simpl type_fv in H; fsetdec.
-    contradict H. apply list_in_concatB, H.
+    simpl type_fv in H; fsetdec.
-    contradict H. apply list_in_concatA, H.
 
   - simpl. rewrite IHτ1, IHτ2.
     reflexivity.
-    contradict H. apply list_in_concatB, H.
+    simpl type_fv in H; fsetdec.
-    contradict H. apply list_in_concatA, H.
+    simpl type_fv in H; fsetdec.
 
   - simpl. rewrite IHτ1, IHτ2.
     reflexivity.
-    contradict H. apply list_in_concatB, H.
+    simpl type_fv in H; fsetdec.
-    contradict H. apply list_in_concatA, H.
+    simpl type_fv in H; fsetdec.
 
   - simpl. rewrite IHτ1, IHτ2.
     reflexivity.
-    contradict H. apply list_in_concatB, H.
+    simpl type_fv in H; fsetdec.
-    contradict H. apply list_in_concatA, H.
+    simpl type_fv in H; fsetdec.
 Qed.
 
 
 
-Lemma open_rec_lc_core : forall τ j σ1 i σ2,
+Lemma open_rec_lc_core : forall τ i σ1 j σ2,
   i <> j ->
-  {j ~> σ1} τ = {i ~> σ2} ({j ~> σ1} τ) ->
+  {i ~> σ1} τ = {j ~> σ2} ({i ~> σ1} τ) ->
-  τ = {i ~> σ1} τ.
+  ({j ~> σ2} τ) = τ.
 
-Proof with (eauto with *).
+Proof with eauto*.
   induction τ;
-  intros j v i u Neq H;
+  intros i σ1 j σ2 Neq H.
-  simpl in *; try solve [inversion H; f_equal; eauto].
 
-(*  case (ty_bvar).*)
+  (* id *)
-    destruct (Nat.eqb j n)...
+  - reflexivity.
-    destruct (Nat.eqb i n)...
   
-Admitted.
+  (* free var *)
+  - reflexivity.
+  
+  (* bound var *)
+  - simpl in *.
+    destruct (j === n).
+    destruct (i === n).
+    3:reflexivity.
+
+    rewrite e,e0 in Neq.
+    contradiction Neq.
+    reflexivity.
+
+    rewrite H,e.
+    simpl.
+    destruct (n===n).
+    reflexivity.
+    contradict n1.
+    reflexivity.
+
+  (* univ *)
+  - simpl in *.
+    inversion H.
+    f_equal.
+    apply IHτ with (i:=S i) (j:=S j) (σ1:=σ1).
+    auto.
+    apply H1.
+
+  (* spec *)
+  - simpl in *.
+    inversion H.
+    f_equal.
+    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H1.
+    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H2.
+
+  (* func *)
+  - simpl in *.
+    inversion H.
+    f_equal.
+    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H1.
+    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H2.
+
+
+  (* morph *)
+  - simpl in *.
+    inversion H.
+    f_equal.
+    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H1.
+    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H2.
+
+  (* ladder *)
+  - simpl in *.
+    inversion H.
+    f_equal.
+    * apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H1.
+    * apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
+      auto.
+      apply H2.
+
+Qed.
 
 
 Lemma type_open_rec_lc : forall k σ τ,
   type_lc τ ->
-  { k ~> σ } τ = τ.
+  ({ k ~> σ } τ) = τ
+.
 Proof.
   intros.
   generalize dependent k.
   induction H.
-  - auto.
-  - auto.
-  - intro k.
-    unfold type_open in *.
-    (*
-    pick fresh x for L.
-    apply open_rec_lc_core with (i := S k) (j := 0) (u := u) (v := x). auto. auto.
-    *)
-    admit.
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-Admitted.
-
-Lemma type_subst_open_rec : forall τ1 τ2 σ x k,
-  type_lc σ ->
-  [x ~> σ] ({k ~> τ2} τ1) = {k ~> [x ~> σ] τ2} ([x ~> σ] τ1).
-Proof.
-  intros.
-  induction τ1.
 
   (* id *)
   - auto.
 
   (* free var *)
-  - simpl.
+  - auto.
-    case_eq (eqb x s).
-    intro.
-    apply eq_sym.
-    apply type_open_rec_lc, H.
-    auto.
-
-  (* bound var *)
-  - simpl.
-    case_eq (Nat.eqb k n).
-    auto.
-    auto.
 
   (* univ *)
   - simpl.
-    admit.
+    intro k.
+    f_equal.
+    unfold type_open in *.
+    pick fresh x for L.
+    apply open_rec_lc_core with
+      (i := 0) (σ1 := (ty_fvar x))
+      (j := S k) (σ2 := σ).
+    trivial.
+    apply eq_sym, H0, Fr.
 
-  - simpl. rewrite IHτ1_1. rewrite IHτ1_2. reflexivity.
+  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-  - simpl. rewrite IHτ1_1. rewrite IHτ1_2. reflexivity.
+  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-  - simpl. rewrite IHτ1_1. rewrite IHτ1_2. reflexivity.
+  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-  - simpl. rewrite IHτ1_1. rewrite IHτ1_2. reflexivity.
+  - simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
-Admitted.
+Qed.
+
+Lemma type_subst_open_rec : forall τ σ1 σ2 x k,
+  type_lc σ2 ->
+
+  [x ~> σ2] ({k ~> σ1} τ)
+  =
+  {k ~> [x ~> σ2] σ1} ([x ~> σ2] τ).
+Proof.
+  induction τ;
+  intros; simpl; f_equal; auto.
+
+  (* free var *)
+  - destruct (x == a).
+    subst.
+    apply eq_sym, type_open_rec_lc.
+    assumption.
+    trivial.
+
+  (* bound var *)
+  - destruct (k === n).
+    reflexivity.
+    trivial.
+Qed.