implemented from_nat

Metalib/MetatheoryAtom.v

@@ -44,6 +44,8 @@ Module Type ATOM <: UsualDecidableType.
 
   Parameter nat_of : atom -> nat.
 
+  Parameter from_nat : nat -> atom.
+
   Hint Resolve eq_dec.
 
   Include HasUsualEq <+ UsualIsEq <+ UsualIsEqOrig.
@@ -102,6 +104,8 @@ Module Atom : ATOM.
 
   Definition nat_of := fun (x : atom) => x.
 
+  Definition from_nat : nat -> atom := fun x => x.
+
   Include HasUsualEq <+ UsualIsEq <+ UsualIsEqOrig.
 
   (* end hide *)

Tutorial/STLC.v

@@ -120,18 +120,20 @@ Definition demo_rep2 := abs typ_base (abs typ_base (app 0 1)).
 
 *)
 
-(** <<
 
-Definition two :=
+
+Definition two := abs (typ_arrow typ_base typ_base) (abs typ_base (app 0 (app 0 1))).
   (* FILL IN HERE *)
 
-Definition COMB_K :=
+Definition COMB_K := abs typ_base (abs typ_base 1).
   (* FILL IN HERE *)
 
 Definition COMB_S :=
+  abs (typ_arrow typ_base (typ_arrow typ_base typ_base))
+      (abs (typ_arrow typ_base typ_base)
+           (abs typ_base (app (app 2 0) (app 1 0)))).
    (* FILL IN HERE *)
 
->> *)
 
 (** There are two important advantages of the locally nameless
     representation:
@@ -229,13 +231,16 @@ Qed.
 Lemma subst_eq_var: forall (x : atom) u,
   [x ~> u]x = u.
 Proof.
-  (* OPTIONAL EXERCISE *) Admitted.
+  intros. unfold subst.
+  destruct (x == x); congruence.
+Qed.
 
 Lemma subst_neq_var : forall (x y : atom) u,
   y <> x -> [x ~> u]y = y.
 Proof.
-  (* OPTIONAL EXERCISE *) Admitted.
-
+  intros. unfold subst.
+  destruct (y == x); congruence.
+Qed.
 
 (*************************************************************************)
 (** * Free variables *)
@@ -306,7 +311,10 @@ Qed.
 Lemma subst_fresh : forall (x : atom) e u,
   x `notin` fv e -> [x ~> u] e = e.
 Proof.
-  (* FILL IN HERE (and delete "Admitted") *) Admitted.
+  intros. generalize dependent u. generalize dependent x.
+  induction e; intros; simpl in *; try f_equal; auto.
+  destruct (a == x); fsetdec.
+Qed.
 
 (* Take-home Demo: Prove that free variables are not introduced by
    substitution.
@@ -327,22 +335,8 @@ Lemma subst_notin_fv : forall x y u e,
    x `notin` fv ([y ~> u]e).
 Proof.
   intros x y u e Fr1 Fr2.
-  induction e; simpl in *.
-  Case "bvar".
-    assumption.
-  Case "fvar".
-  destruct (a == y).
-      assumption.
-      simpl. assumption.
-  Case "abs".
-    apply IHe. assumption.
-  Case "app".
-    destruct_notin.
-    apply notin_union.
-    apply IHe1.
-    assumption.
-    apply IHe2.
-    assumption.
+  induction e; simpl in *; auto.
+  destruct (a == y); auto.
 Qed.
 
 
@@ -412,7 +406,8 @@ Lemma demo_open :
   open (app (abs typ_base (app 1 0)) 0) Y =
        (app (abs typ_base (app Y 0)) Y).
 Proof.
-Admitted.
+  reflexivity.
+Qed.
 (* HINT for demo: To show the equality of the two sides below, use the
    tactics [unfold], which replaces a definition with its RHS and
    reduces it to head form, and [simpl], which reduces the term the
@@ -466,6 +461,19 @@ Hint Constructors lc.
     outside of this part of the tutorial so we make it a local
     notation, confined to this section. *)
 
+
+Ltac destruct_eq :=
+  destruct_notin;
+  match goal with
+    | [ |- context[if ?x == ?y then _ else _]] => destruct (x == y)
+  end.
+
+Ltac equality :=
+  simpl in *; try congruence;
+  destruct_eq;
+  auto; try congruence.
+
+
 Section BasicOperations.
 Local Notation "{ k ~> u } t" := (open_rec k u t) (at level 67).
 
@@ -480,13 +488,7 @@ Lemma open_rec_lc_0 : forall k u e,
   e = {k ~> u} e.
 Proof.
   intros k u e LC.
-  induction LC.
-  Case "lc_fvar".
-    simpl.
-    auto.
-  Case "lc_abs".
-    simpl.
-    f_equal.
+  induction LC; simpl in *; try f_equal; auto.
 Admitted.
 
 (** At this point there are two problems.  Our goal is about
@@ -617,7 +619,13 @@ Lemma subst_open_rec : forall e1 e2 u (x : atom) k,
   lc u ->
   [x ~> u] ({k ~> e2} e1) = {k ~> [x ~> u] e2} ([x ~> u] e1).
 Proof.
-  (* OPTIONAL EXERCISE *) Admitted.
+  intro e1.
+  induction e1; intros;
+    unfold subst in *; unfold open_rec in *;
+      repeat destruct_eq; subst; simpl in *;
+        try f_equal; try apply open_rec_lc;
+          auto.
+Qed.
 
 
 (** *** Exercise [subst_open_var] *)
@@ -635,8 +643,10 @@ Lemma subst_open_var : forall (x y : atom) u e,
   y <> x ->
   lc u ->
   open ([x ~> u] e) y = [x ~> u] (open e y).
-Proof.
-  (* FILL IN HERE (and delete "Admitted") *) Admitted.
+Proof with auto.
+  intros. unfold open. rewrite subst_open_rec...
+  rewrite subst_neq_var...
+Qed.
 
 (** *** Take-home Exercise [subst_intro] *)
 
@@ -653,7 +663,13 @@ Lemma subst_intro : forall (x : atom) u e,
   x `notin` (fv e) ->
   open e u = [x ~> u](open e x).
 Proof.
-  (* OPTIONAL EXERCISE *) Admitted.
+  unfold open. generalize 0.
+  intros n x u e.
+  generalize dependent n. generalize dependent x. generalize dependent u.
+  induction e; intros; simpl in *;
+    try destruct_eq; simpl in *; try f_equal; try equality;
+      destruct_notin; auto.
+Qed.
 
 End BasicOperations.
 
@@ -760,6 +776,17 @@ Hint Constructors lc_c.
 (* Reintroduce notation for [open_rec] so that we can reprove
    properties about it and the new version of lc_c. *)
 
+Tactic Notation "gen" ident(x) := generalize dependent x.
+Tactic Notation "gen" ident(x) ident(y) := gen x; gen y.
+Tactic Notation "gen" ident(x) ident(y) ident(z) := gen x y; gen z.
+Tactic Notation "gen" ident(x) ident(y) ident(z) ident(w) := gen x y z; gen w.
+
+Ltac discharge :=
+  intros;
+  simpl in *; try destruct_eq; simpl in *; try f_equal; subst; auto;
+  try equality; try congruence.
+
+
 Section CofiniteQuantification.
 Local Notation "{ k ~> u } t" := (open_rec k u t) (at level 67).
 
@@ -805,14 +832,24 @@ Lemma subst_open_rec_c : forall e1 e2 u (x : atom) k,
   lc_c u ->
   [x ~> u] ({k ~> e2} e1) = {k ~> [x ~> u] e2} ([x ~> u] e1).
 Proof.
-(* OPTIONAL EXERCISE *) Admitted.
+  intro e1.
+  induction e1; discharge.
+  rewrite <- open_rec_lc_c; auto.
+Qed.
+
 
 Lemma subst_open_var_c : forall (x y : atom) u e,
   y <> x ->
   lc_c u ->
   open ([x ~> u] e) y = [x ~> u] (open e y).
 Proof.
-  (* OPTIONAL EXERCISE *) Admitted.
+  unfold open. generalize 0.
+  intros n x y u e. gen n x y. gen u.
+  induction e; intros;
+    simpl in *; try destruct_eq; simpl in *; try f_equal; subst; auto.
+  - equality.
+  - rewrite <- open_rec_lc_c; auto.
+Qed.
 
 (* Exercise [subst_lc_c]:
 
@@ -830,15 +867,11 @@ Lemma subst_lc_c : forall (x : atom) u e,
   lc_c ([x ~> u] e).
 Proof.
   intros x u e He Hu.
-  induction He.
-  Case "lc_var_c".
-   simpl.
-   destruct (x0 == x).
-     auto.
-     auto.
-  Case "lc_abs_c".
-    simpl.
-    (* FILL IN HERE (and delete "Admitted") *) Admitted.
+  induction He; simpl in *; try destruct_eq; auto.
+  econstructor; auto.
+  instantiate (1 := (L `union` singleton x)). intros.
+  rewrite subst_open_var_c; auto.  
+Qed.
 
 End CofiniteQuantification.
 
@@ -1213,8 +1246,14 @@ Proof.
   remember (G ++ E) as E'.
   generalize dependent G.
   induction H; intros G Eq Uniq; subst.
- (* FILL IN HERE (and delete "Admitted") *) Admitted.
-
+  - constructor. assumption.
+    apply binds_weaken. assumption.
+  - pick fresh y and apply typing_abs_c.
+    rewrite_env (((y ~ T1) ++ G) ++ F ++ E).
+    apply H0; auto.
+    simpl_env. auto.
+  - econstructor; eauto.
+Qed.
 
 
 (** *** Example
@@ -1289,7 +1328,13 @@ Lemma typing_subst_var_case : forall (E F : env) u S T (z x : atom),
 Proof.
   intros E F u S T z x H J K.
   simpl.
- (* FILL IN HERE (and delete "Admitted") *) Admitted.
+  destruct_eq.
+  - subst. apply binds_mid_eq in H; auto. subst.
+    apply typing_c_weakening; auto.
+    eapply uniq_remove_mid. eauto.
+  - econstructor. eapply uniq_remove_mid; eauto.
+    eapply binds_remove_mid; eauto.
+Qed.
 
 (** *** Note
 
@@ -1337,8 +1382,18 @@ Lemma typing_c_subst : forall (E F : env) e u S T (z : atom),
   typing_c E u S ->
   typing_c (F ++ E) ([z ~> u] e) T.
 Proof.
-(* FILL IN HERE (and delete "Admitted") *) Admitted.
-
+  intros. gen u. remember (F ++ [(z, S)] ++ E) as E'.
+  gen E F.
+  induction H; intros; subst.
+  - eapply typing_subst_var_case; eauto.
+  - simpl in *.
+    pick fresh x and apply typing_abs_c.
+    pose proof H1. apply typing_c_to_lc_c in H2.
+    rewrite subst_open_var_c; auto.
+    rewrite_env (((x ~ T1) ++ F) ++ E0).
+    eapply H0; eauto. 
+  - simpl in *. econstructor; eauto.
+Qed.
 
 (** *** Exercise
 
@@ -1354,7 +1409,9 @@ Lemma typing_c_subst_simple : forall (E : env) e u S T (z : atom),
   typing_c E u S ->
   typing_c E ([z ~> u] e) T.
 Proof.
-(* FILL IN HERE (and delete "Admitted") *) Admitted.
+  intros. rewrite_env (nil ++ E).
+  eapply typing_c_subst; eauto.
+Qed.
 
 (*************************************************************************)
 (** * Values and Evaluation *)