chap9: init

src/chap9.v

@@ -0,0 +1,353 @@
+From Stdlib Require Import
+  Strings.String
+  FSets.FMapInterface
+  FSets.FMapList
+  FSets.FMapFacts
+  Structures.OrderedTypeEx.
+
+Module Chap9.
+  (*
+    NOTE: a lot of the definitions of stlc done here were
+          taken from https://softwarefoundations.cis.upenn.edu/plf-current/Stlc.html
+          and adapted to fit the contents from the book.
+  *)
+
+  Inductive type : Type :=
+    | type_Bool : type
+    | type_Arrow : type -> type -> type.
+
+  Scheme Equality for type.
+
+  Inductive term : Type :=
+    | term_var : string -> term
+    | term_app : term -> term -> term
+    | term_abs : string -> type -> term -> term
+    | term_true : term
+    | term_false : term
+    | term_if : term -> term -> term -> term.
+
+  Scheme Equality for term.
+
+  Declare Scope stlc_scope.
+  Delimit Scope stlc_scope with stlc.
+  Open Scope stlc_scope.
+
+  Declare Custom Entry stlc_type.
+  Declare Custom Entry stlc_term.
+
+  Notation "x" := x (in custom stlc_type at level 0, x global) : stlc_scope.
+  Notation "<{{ x }}>" := x (x custom stlc_type).
+  Notation "( t )" := t (in custom stlc_type at level 0, t custom stlc_type) : stlc_scope.
+  Notation "S -> T" := (type_Arrow S T) (in custom stlc_type at level 99, right associativity) : stlc_scope.
+  Notation "$( t )" := t (in custom stlc_type at level 0, t constr) : stlc_scope.
+  Notation "'Bool'" := type_Bool (in custom stlc_type at level 0) : stlc_scope.
+  Notation "'if' x 'then' y 'else' z" :=
+    (term_if x y z) (in custom stlc_term at level 200,
+                      x custom stlc_term,
+                      y custom stlc_term,
+                      z custom stlc_term at level 200,
+                      left associativity).
+  Notation "'true'"  := true (at level 1).
+  Notation "'true'"  := term_true (in custom stlc_term at level 0).
+  Notation "'false'"  := false (at level 1).
+  Notation "'false'"  := term_false (in custom stlc_term at level 0).
+
+  Notation "$( x )" := x (in custom stlc_term at level 0, x constr, only parsing) : stlc_scope.
+  Notation "x" := x (in custom stlc_term at level 0, x constr at level 0) : stlc_scope.
+  Notation "<{ e }>" := e (e custom stlc_term at level 200) : stlc_scope.
+  Notation "( x )" := x (in custom stlc_term at level 0, x custom stlc_term) : stlc_scope.
+  Notation "x y" := (term_app x y) (in custom stlc_term at level 10, left associativity) : stlc_scope.
+  Notation "\ x : t , y" :=
+    (term_abs x t y) (in custom stlc_term at level 200, x global,
+                      t custom stlc_type,
+                      y custom stlc_term at level 200,
+                      left associativity).
+
+  Coercion term_var : string >-> term.
+  Arguments term_var _%_string.
+
+  Definition f : string := "f".
+  Definition x : string := "x".
+  Definition y : string := "y".
+  Definition z : string := "z".
+  Hint Unfold f : core.
+  Hint Unfold x : core.
+  Hint Unfold y : core.
+  Hint Unfold z : core.
+
+  Inductive value : term -> Prop :=
+    | v_abs : forall (x : string) (T2 : type) (t1 : term),
+        value <{\x:T2, t1}>
+    | v_true :
+        value <{true}>
+    | v_false :
+        value <{false}>.
+
+  Hint Constructors value : core.
+
+  Reserved Notation "'[' x ':=' s ']' t" (in custom stlc_term at level 5, x global, s custom stlc_term,
+        t custom stlc_term at next level, right associativity).
+  Fixpoint subst (x : string) (s : term) (t : term) : term :=
+    match t with
+    | term_var y =>
+        if String.eqb x y then s else t
+    | <{\y:T, t1}> =>
+        if String.eqb x y then t else <{\y:T, [x:=s] t1}>
+    | <{t1 t2}> =>
+        <{[x:=s] t1 [x:=s] t2}>
+    | <{true}> =>
+        <{true}>
+    | <{false}> =>
+        <{false}>
+    | <{if t1 then t2 else t3}> =>
+        <{if [x:=s] t1 then [x:=s] t2 else [x:=s] t3}>
+    end
+  where "'[' x ':=' s ']' t" := (subst x s t) (in custom stlc_term).
+
+  Reserved Notation "t '--->' t'" (at level 40).
+  Inductive step : term -> term -> Prop :=
+    | E_App1 : forall t1 t1' t2,
+          t1 ---> t1' ->
+          <{t1 t2}> ---> <{t1' t2}>
+    | E_App2 : forall v1 t2 t2',
+          value v1 ->
+          t2 ---> t2' ->
+          <{v1 t2}> ---> <{v1 t2'}>
+    | E_AppAbs : forall x T t v,
+          value v ->
+          <{(\x:T, t) v}> ---> <{ [x:=v]t }>
+    | E_IfTrue : forall t1 t2,
+        <{if true then t1 else t2}> ---> t1
+    | E_IfFalse : forall t1 t2,
+        <{if false then t1 else t2}> ---> t2
+    | E_If : forall t1 t1' t2 t3,
+        t1 ---> t1' ->
+        <{if t1 then t2 else t3}> ---> <{if t1' then t2 else t3}>
+  where "t '--->' t'" := (step t t').
+
+  Hint Constructors step : core.
+
+  Module M := FMapList.Make(String_as_OT).
+  Definition context := M.t type.
+  Definition empty_ctx : context := @M.empty type.
+
+  Notation "x ')>' v ';' m " := (M.add x v m)
+    (in custom stlc_term at level 0, x constr at level 0, v custom stlc_type, right associativity) : stlc_scope.
+  Notation "x ')>' v " := (M.add x v empty_ctx)
+    (in custom stlc_term at level 0, x constr at level 0, v custom stlc_type) : stlc_scope.
+  Notation "'empty'" := empty_ctx (in custom stlc_term) : stlc_scope.
+
+  Reserved Notation "<{ Γ '|-' t '∈' T }>"
+              (at level 0, Γ custom stlc_term at level 200, t custom stlc_term, T custom stlc_type).
+  Inductive has_type : context -> term -> type -> Prop :=
+    | T_Var : forall (Γ : context) (x : string) (T1 : type),
+        M.find x Γ = Some T1 ->
+        <{ Γ |- x ∈ T1 }>
+    | T_Abs : forall (Γ : context) (x : string) (T1 T2 : type) (t1 : term),
+        <{ x )> T1; Γ |- t1 ∈ T2 }> ->
+        <{ Γ |- \x:T1, t1 ∈ T1 -> T2 }>
+    | T_App : forall (Γ : context) (t1 t2 : term) (T1 T2 : type),
+        <{ Γ |- t1 ∈ T2 -> T1 }> ->
+        <{ Γ |- t2 ∈ T2 }> ->
+        <{ Γ |- t1 t2 ∈ T1 }>
+    | T_True : forall Γ,
+        <{ Γ |- true ∈ Bool }>
+    | T_False : forall Γ,
+        <{ Γ |- false ∈ Bool }>
+    | T_If : forall t1 t2 t3 T1 Γ,
+        <{ Γ |- t1 ∈ Bool }> ->
+        <{ Γ |- t2 ∈ T1 }> ->
+        <{ Γ |- t3 ∈ T1 }> ->
+        <{ Γ |- if t1 then t2 else t3 ∈ T1 }>
+  where "<{ Γ '|-' t '∈' T }>" := (has_type Γ t T) : stlc_scope.
+
+  Hint Constructors has_type : core.
+
+  (* Notation multistep := (multi step).
+  Notation "t1 '-->*' t2" := (multistep t1 t2) (at level 40). *)
+
+  Example typing_example_1' :
+    <{ empty |- \x:Bool, x ∈ Bool -> Bool }>.
+  Proof. eauto. Qed.
+
+  (* End of definitions Software Foundations definitions of STLC *)
+
+  (* 9.2.2 *)
+
+  Example typing_example_1 :
+    <{ f )> Bool -> Bool |- f (if false then true else false) ∈ Bool }>.
+  Proof.
+  Admitted.
+
+  Example typing_example_2 :
+    <{ f )> Bool -> Bool |- \x:Bool, f (true) ∈ Bool -> Bool }>.
+  Proof.
+  Admitted.
+
+  (* 9.2.3 *)
+  Lemma fxy_bool_iff :
+    forall Γ,
+      <{ Γ |- f x y ∈ Bool }> <->
+      exists T1 T2,
+           M.find f Γ = Some <{{ T1 -> T2 -> Bool }}>
+        /\ M.find x Γ = Some T1
+        /\ M.find y Γ = Some T2.
+  Proof.
+    split.
+    - intros H.
+      inversion H.
+  Admitted.
+
+  (* 9.3.1 *)
+  Lemma type_inv_var :
+    forall (Γ : context) (x : string) (R : type),
+      <{ Γ |- x ∈ R }> ->
+      exists T', M.find x Γ = Some T'.
+  Proof.
+    intros Γ x R H.
+    inversion H.
+    exists R.
+    assumption.
+  Qed.
+
+  Lemma type_inv_abs :
+    forall (Γ : context) (x : string) (T1 R : type) (t2 : term),
+      <{ Γ |- \x:T1, t2 ∈ R }> ->
+      exists R2,
+        R = <{{ T1 -> R2 }}> /\
+        <{ x )> T1; Γ |- t2 ∈ R2 }>.
+  Proof.
+    intros Γ x T1 R t2 H.
+    inversion H.
+    exists T2.
+    split.
+    - reflexivity.
+    - assumption.
+  Qed.
+
+  Lemma type_inv_app :
+    forall (Γ : context) (t1 t2 : term) (T11 R : type),
+      <{ Γ |- t1 t2 ∈ R }> ->
+      exists T12,
+        <{ Γ |- t1 ∈  T12 -> R }> /\
+        <{ Γ |- t2 ∈ T12 }>.
+  Proof.
+    intros Γ t1 t2 T11 R H.
+    inversion H.
+    exists T2.
+    split.
+    - assumption.
+    - assumption.
+  Qed.
+
+  Lemma type_inv_true :
+    forall (Γ : context) (R : type),
+      <{ Γ |- true ∈ R }> ->
+      R = type_Bool.
+  Proof.
+    intros Γ R H.
+    inversion H.
+    reflexivity.
+  Qed.
+
+  Lemma type_inv_false :
+    forall (Γ : context) (R : type),
+      <{ Γ |- false ∈ R }> ->
+      R = type_Bool.
+  Proof.
+    intros Γ R H.
+    inversion H.
+    reflexivity.
+  Qed.
+
+  Lemma type_inv_if :
+    forall (Γ : context) (t1 t2 t3 : term) (R : type),
+      <{ Γ |- if t1 then t2 else t3 ∈ R }> ->
+      <{ Γ |- t1 ∈ Bool }> /\
+      <{ Γ |- t2 ∈ R }> /\
+      <{ Γ |- t3 ∈ R }>.
+  Proof.
+    intros Γ t1 t2 t3 R H.
+    inversion H.
+    split.
+    - assumption.
+    - split.
+      + assumption.
+      + assumption.
+  Qed.
+
+  (* 9.3.2 *)
+
+  Lemma unique_context_content :
+    forall (Γ : context) (x : string) (T1 T2 : type),
+      <{ Γ |- x ∈ T1 }> ->
+      <{ Γ |- x ∈ T2 }> ->
+      T1 = T2.
+  Proof.
+    intros Γ x T1 T2 H1 H2.
+    inversion H1.
+    inversion H2.
+    subst.
+    rewrite H3 in H7.
+    inversion H7.
+    reflexivity.
+  Qed.
+
+  Lemma no_self_arrow :
+    forall T U,
+      type_Arrow T U <> T.
+  Proof.
+    induction T; intros U H.
+    - discriminate H.
+    - inversion H.
+      apply IHT1 in H1.
+      contradiction.
+  Qed.
+
+  Lemma no_x_x_T :
+    forall (Γ : context) (x : string) (T : type),
+    ~(exists Γ T, <{ Γ |- x x ∈ T }>).
+  Proof.
+    intros Γ x T H.
+    destruct H as [Γ' [T' H']].
+    inversion H'.
+    apply unique_context_content with
+      (Γ := Γ') (x := x) (T1 := T2) (T2 := <{{ T2 -> T' }}>) in H2.
+    - symmetry in H2.
+      apply no_self_arrow in H2.
+      contradiction.
+    - assumption.
+  Qed.
+
+  (* 9.3.3 *)
+  Lemma unique_bag_content :
+    forall (Γ : context) (x : string) (T1 T2 : type),
+      M.find x Γ = Some T1 ->
+      M.find x Γ = Some T2 ->
+      T1 = T2.
+  Proof.
+    intros Γ x T1 T2 H1 H2.
+    rewrite H1 in H2.
+    inversion H2.
+    reflexivity.
+  Qed.
+
+  Lemma uniqueness_of_types :
+    forall (Γ : context) (t : term) (T1 T2 : type),
+      <{ Γ |- t ∈ T1 }> ->
+      <{ Γ |- t ∈ T2 }> ->
+      T1 = T2.
+  Proof.
+    intros Γ t T1 T2 H1 H2.
+    generalize dependent T2.
+    induction H1.
+    - intros T2 H2.
+      inversion H2.
+      apply unique_bag_content with
+        (Γ := Γ) (x := x0) (T1 := T1) (T2 := T2) in H.
+      + assumption.
+      + assumption.
+    - intros R.
+  Admitted.
+
+End Chap9.