Set Warnings "-notation-overridden,-parsing".
From Coq Require Import Strings.String.
From PLF Require Import Maps.
From PLF Require Import Imp.
From PLF Require Import Smallstep.
From PLF Require Import Stlc.

       t ::=                          项：
           | {i1=t1, ..., in=tn}         记录
           | t.i                         投影
           | ...

       v ::=                          值：
           | {i1=v1, ..., in=vn}         记录值
           | ...

       T ::=                          类型：
           | {i1:T1, ..., in:Tn}         记录类型
           | ...

Module STLCExtendedRecords.

Module FirstTry.

---

Definition alist (X : Type) := list (string × X).

---

Inductive ty : Type :=
  | Base : string → ty
  | Arrow : ty → ty → ty
  | TRcd : (alist ty) → ty.

(* Check ty_ind.
   ====>
    ty_ind :
      forall P : ty -> Prop,
        (forall i : id, P (Base i)) ->
        (forall t : ty, P t -> forall t₀ : ty, P t₀
                            -> P (Arrow t t₀)) ->
        (forall a : alist ty, P (TRcd a)) ->    (* ??? *)
        forall t : ty, P t
*)

---

End FirstTry.

Inductive ty : Type :=
  | Base : string → ty
  | Arrow : ty → ty → ty
  | RNil : ty
  | RCons : string → ty → ty → ty.

Inductive tm : Type :=
  | var : string → tm
  | app : tm → tm → tm
  | abs : string → ty → tm → tm
  (* 记录体 *)
  | rproj : tm → string → tm
  | trnil : tm
  | rcons : string → tm → tm → tm.

Open Scope string_scope.

---

Notation a := "a".
Notation f := "f".
Notation g := "g".
Notation l := "l".
Notation A := (Base "A").
Notation B := (Base "B").
Notation k := "k".
Notation i₁ := "i₁".
Notation i₂ := "i₂".

(* Check (RCons i₁ A RNil). *)

(* Check (RCons i₁ (Arrow A B)
           (RCons i₂ A RNil)). *)

Definition weird_type := RCons X A B.

Inductive record_ty : ty → Prop :=
  | RTnil :
        record_ty RNil
  | RTcons : ∀ i T₁ T₂,
        record_ty (RCons i T₁ T₂).

Inductive well_formed_ty : ty → Prop :=
  | wfBase : ∀ i,
        well_formed_ty (Base i)
  | wfArrow : ∀ T₁ T₂,
        well_formed_ty T₁ →
        well_formed_ty T₂ →
        well_formed_ty (Arrow T₁ T₂)
  | wfRNil :
        well_formed_ty RNil
  | wfRCons : ∀ i T₁ T₂,
        well_formed_ty T₁ →
        well_formed_ty T₂ →
        record_ty T₂ →
        well_formed_ty (RCons i T₁ T₂).

---

Hint Constructors record_ty well_formed_ty.

Inductive record_tm : tm → Prop :=
  | rtnil :
        record_tm trnil
  | rtcons : ∀ i t₁ t₂,
        record_tm (rcons i t₁ t₂).

---

Hint Constructors record_tm.

Fixpoint subst (x:string) (s:tm) (t:tm) : tm :=
  match t with
  | var y ⇒ if eqb_string x y then s else t
  | abs y T t₁ ⇒ abs y T
                     (if eqb_string x y then t₁ else (subst x s t₁))
  | app t₁ t₂ ⇒ app (subst x s t₁) (subst x s t₂)
  | rproj t₁ i ⇒ rproj (subst x s t₁) i
  | trnil ⇒ trnil
  | rcons i t₁ tr₁ ⇒ rcons i (subst x s t₁) (subst x s tr₁)
  end.

---

Notation "'[' x ':=' s ']' t" := (subst x s t) (at level 20).

Inductive value : tm → Prop :=
  | v_abs : ∀ x T₁₁ t₁₂,
      value (abs x T₁₁ t₁₂)
  | v_rnil : value trnil
  | v_rcons : ∀ i v₁ vr,
      value v₁ →
      value vr →
      value (rcons i v₁ vr).

---

Hint Constructors value.

Fixpoint tlookup (i:string) (tr:tm) : option tm :=
  match tr with
  | rcons i' t tr' ⇒ if eqb_string i i' then Some t else tlookup i tr'
  | _ ⇒ None
  end.

Reserved Notation "t₁ '-->' t₂" (at level 40).

---

Inductive step : tm → tm → Prop :=
  | ST_AppAbs : ∀ x T₁₁ t₁₂ v₂,
         value v₂ →
         (app (abs x T₁₁ t₁₂) v₂) --> ([x:=v₂]t₁₂)
  | ST_App1 : ∀ t₁ t₁' t₂,
         t₁ --> t₁' →
         (app t₁ t₂) --> (app t₁' t₂)
  | ST_App2 : ∀ v₁ t₂ t₂',
         value v₁ →
         t₂ --> t₂' →
         (app v₁ t₂) --> (app v₁ t₂')
  | ST_Proj1 : ∀ t₁ t₁' i,
        t₁ --> t₁' →
        (rproj t₁ i) --> (rproj t₁' i)
  | ST_ProjRcd : ∀ tr i vi,
        value tr →
        tlookup i tr = Some vi →
        (rproj tr i) --> vi
  | ST_Rcd_Head : ∀ i t₁ t₁' tr₂,
        t₁ --> t₁' →
        (rcons i t₁ tr₂) --> (rcons i t₁' tr₂)
  | ST_Rcd_Tail : ∀ i v₁ tr₂ tr₂',
        value v₁ →
        tr₂ --> tr₂' →
        (rcons i v₁ tr₂) --> (rcons i v₁ tr₂')

where "t₁ '-->' t₂" := (step t₁ t₂).

---

Notation multistep := (multi step).
Notation "t₁ '-->*' t₂" := (multistep t₁ t₂) (at level 40).

---

Hint Constructors step.

Fixpoint Tlookup (i:string) (Tr:ty) : option ty :=
  match Tr with
  | RCons i' T Tr' ⇒
      if eqb_string i i' then Some T else Tlookup i Tr'
  | _ ⇒ None
  end.

---

Definition context := partial_map ty.

---

Reserved Notation "Gamma '⊢' t '∈' T" (at level 40).

---

Inductive has_type : context → tm → ty → Prop :=
  | T_Var : ∀ Gamma x T,
      Gamma x = Some T →
      well_formed_ty T →
      Gamma ⊢ (var x) \in T
  | T_Abs : ∀ Gamma x T₁₁ T₁₂ t₁₂,
      well_formed_ty T₁₁ →
      (update Gamma x T₁₁) ⊢ t₁₂ \in T₁₂ →
      Gamma ⊢ (abs x T₁₁ t₁₂) \in (Arrow T₁₁ T₁₂)
  | T_App : ∀ T₁ T₂ Gamma t₁ t₂,
      Gamma ⊢ t₁ \in (Arrow T₁ T₂) →
      Gamma ⊢ t₂ \in T₁ →
      Gamma ⊢ (app t₁ t₂) \in T₂
  (* records: *)
  | T_Proj : ∀ Gamma i t Ti Tr,
      Gamma ⊢ t \in Tr →
      Tlookup i Tr = Some Ti →
      Gamma ⊢ (rproj t i) \in Ti
  | T_RNil : ∀ Gamma,
      Gamma ⊢ trnil \in RNil
  | T_RCons : ∀ Gamma i t T tr Tr,
      Gamma ⊢ t \in T →
      Gamma ⊢ tr \in Tr →
      record_ty Tr →
      record_tm tr →
      Gamma ⊢ (rcons i t tr) \in (RCons i T Tr)

where "Gamma '⊢' t '∈' T" := (has_type Gamma t T).

---

Hint Constructors has_type.

Lemma typing_example_2 :
  empty ⊢
    (app (abs a (RCons i₁ (Arrow A A)
                      (RCons i₂ (Arrow B B)
                       RNil))
              (rproj (var a) i₂))
            (rcons i₁ (abs a A (var a))
            (rcons i₂ (abs a B (var a))
             trnil))) \in
    (Arrow B B).
Proof.
  (* 请在此处解答 *) Admitted.

---

Example typing_nonexample :
  ¬ ∃ T,
      (update empty a (RCons i₂ (Arrow A A)
                                RNil)) ⊢
               (rcons i₁ (abs a B (var a)) (var a)) \in
               T.
Proof.
  (* 请在此处解答 *) Admitted.

---

Example typing_nonexample_2 : ∀ y,
  ¬ ∃ T,
    (update empty y A) ⊢
           (app (abs a (RCons i₁ A RNil)
                     (rproj (var a) i₁))
                   (rcons i₁ (var y) (rcons i₂ (var y) trnil))) \in
           T.
Proof.
  (* 请在此处解答 *) Admitted.

Lemma wf_rcd_lookup : ∀ i T Ti,
  well_formed_ty T →
  Tlookup i T = Some Ti →
  well_formed_ty Ti.

Lemma step_preserves_record_tm : ∀ tr tr',
  record_tm tr →
  tr --> tr' →
  record_tm tr'.

Lemma has_type__wf : ∀ Gamma t T,
  Gamma ⊢ t \in T → well_formed_ty T.

Lemma lookup_field_in_value : ∀ v T i Ti,
  value v →
  empty ⊢ v \in T →
  Tlookup i T = Some Ti →
  ∃ ti, tlookup i v = Some ti ∧ empty ⊢ ti \in Ti.

Theorem progress : ∀ t T,
     empty ⊢ t \in T →
     value t ∨ ∃ t', t --> t'.

Inductive appears_free_in : string → tm → Prop :=
  | afi_var : ∀ x,
      appears_free_in x (var x)
  | afi_app1 : ∀ x t₁ t₂,
      appears_free_in x t₁ → appears_free_in x (app t₁ t₂)
  | afi_app2 : ∀ x t₁ t₂,
      appears_free_in x t₂ → appears_free_in x (app t₁ t₂)
  | afi_abs : ∀ x y T₁₁ t₁₂,
        y ≠ x →
        appears_free_in x t₁₂ →
        appears_free_in x (abs y T₁₁ t₁₂)
  | afi_proj : ∀ x t i,
     appears_free_in x t →
     appears_free_in x (rproj t i)
  | afi_rhead : ∀ x i ti tr,
      appears_free_in x ti →
      appears_free_in x (rcons i ti tr)
  | afi_rtail : ∀ x i ti tr,
      appears_free_in x tr →
      appears_free_in x (rcons i ti tr).

---

Hint Constructors appears_free_in.

---

Lemma context_invariance : ∀ Gamma Gamma' t S,
     Gamma ⊢ t \in S →
     (∀ x, appears_free_in x t → Gamma x = Gamma' x) →
     Gamma' ⊢ t \in S.

Lemma free_in_context : ∀ x t T Gamma,
   appears_free_in x t →
   Gamma ⊢ t \in T →
   ∃ T', Gamma x = Some T'.

Lemma substitution_preserves_typing : ∀ Gamma x U v t S,
     (update Gamma x U) ⊢ t \in S →
     empty ⊢ v \in U →
     Gamma ⊢ ([x:=v]t) \in S.
Proof with eauto.
  (* 定理：若 x⊢>U;Gamma ⊢ t : S 且 empty ⊢ v : U，则
     Gamma ⊢ (x:=vt) S。 *)
  intros Gamma x U v t S Htypt Htypv.
  generalize dependent Gamma. generalize dependent S.
  (* 证明：通过对项 t 作归纳可得。大部分情况下，结论可以从归纳假设直接得到，
     只有 var、abs 和 rcons 的情况需要额外证明。无法自动得到前两者，
     是因为我们必须处理变量之间的相互作用。对于 rcons 的情况，
     我们必须额外证明在项中作代换不改变它是否为一个记录项。 *)
  induction t;
    intros S Gamma Htypt; simpl; inversion Htypt; subst...
  - (* var *)
    simpl. rename s into y.
    (* 若 t = y，我们知道
         empty ⊢ v : U 且
         x⊢>U; Gamma ⊢ y : S
       经反演可得 update Gamma x U y = Some S。
       我们需要证明 Gamma ⊢ [x:=v]y : S。

       有两种情况需要考虑：x=y 或 x≠y。 *)
    unfold update, t_update in H₀.
    destruct (eqb_stringP x y) as [Hxy|Hxy].
    + (* x=y *)
    (* 若 x = y，那么我们知道 U = S，以及 [x:=v]y = v。
       因此我们必须证明若 empty ⊢ v : U 则 Gamma ⊢ v : U。
       我们已经证明了此定理更一般的版本，即上下文不变性！ *)
      subst.
      inversion H₀; subst. clear H₀.
      eapply context_invariance...
      intros x Hcontra.
      destruct (free_in_context _ _ S empty Hcontra)
        as [T' HT']...
      inversion HT'.
    + (* x<>y *)
    (* 若 x ≠ y，则 Gamma y = Some S 且代换没有效果。我们可以根据
       T_Var 证明 Gamma ⊢ y : S。 *)
      apply T_Var...
  - (* abs *)
    rename s into y. rename t into T₁₁.
    (* 若 t = abs y T₁₁ t₀，那么我们知道
         x⊢>U; Gamma ⊢ abs y T₁₁ t₀ : T₁₁→T₁₂
         x⊢>U; y⊢>T₁₁; Gamma ⊢ t₀ : T₁₂
         empty ⊢ v : U
       根据归纳假设，我们知道对于所有的 S Gamma，
         x⊢>U; Gamma ⊢ t₀ : S → Gamma ⊢ [x:=v]t₀ S.

       我们可以计算出
        [x:=v]t = abs y T₁₁ (if eqb_string x y then t₀ else [x:=v]t₀) ，
       此时我们必须证明 Gamma ⊢ [x:=v]t : T₁₁→T₁₂。我们知道可以用
       T_Abs 来证明它，因此接下来需要证明的就是：
         y⊢>T₁₁; Gamma ⊢ if eqb_string x y then t₀ else [x:=v]t₀ : T₁₂
       我们考虑两种情况：x = y 和 x ≠ y。 *)
    apply T_Abs...
    destruct (eqb_stringP x y) as [Hxy|Hxy].
    + (* x=y *)
      (* 若 x = y，则代换没有作用。上下文不变性保证了
         y:U,y:T₁₁ 和 Gamma,y:T₁₁ 等价。在前者的上下文中有 t₀ : T₁₂ ，
         那么在后者中也是这样。 *)
      eapply context_invariance...
      subst.
      intros x Hafi. unfold update, t_update.
      destruct (eqb_string y x)...
    + (* x<>y *)
      (* 若 x ≠ y，那么归纳假设和上下文不变性能让我们证明
           x⊢>U; y⊢>T₁₁; Gamma ⊢ t₀ : T₁₂       =>
           y⊢>T₁₁; x⊢>U; Gamma ⊢ t₀ : T₁₂       =>
           y⊢>T₁₁; Gamma ⊢ [x:=v]t₀ : T₁₂ *)
      apply IHt. eapply context_invariance...
      intros z Hafi. unfold update, t_update.
      destruct (eqb_stringP y z)...
      subst. rewrite false_eqb_string...
  - (* rcons *)
    apply T_RCons... inversion H₇; subst; simpl...
Qed.

---

Theorem preservation : ∀ t t' T,
     empty ⊢ t \in T →
     t --> t' →
     empty ⊢ t' \in T.
Proof with eauto.
  intros t t' T HT.
  (* 定理：若 empty ⊢ t : T 且 t --> t'，则
     empty ⊢ t' : T. *)
  remember (@empty ty) as Gamma. generalize dependent HeqGamma.
  generalize dependent t'.
  (* 证明：对给定的定型导出式来归纳。很多情况是矛盾的（T_Var、T_Abs）
     或可直接从归纳假设得出（T_RCons），我们只需证明那些“有趣”的情况。 *)
  induction HT;
    intros t' HeqGamma HE; subst; inversion HE; subst...
  - (* T_App *)
    (* 若使用的最后一条规则为 T_App，那么 t = t₁ t₂。
       证明 t --> t' 可能用到的三条规则是 ST_App1、ST_App2 和 ST_AppAbs。
       在前两种情况下，结果可直接从归纳假设得出。 *)
    inversion HE; subst...
    + (* ST_AppAbs *)
      (* 对于第三种情况，假设
           t₁ = abs x T₁₁ t₁₂
         且
           t₂ = v₂。我们必须证明 empty ⊢ [x:=v₂]t₁₂ : T₂。
         根据假设我们知道
             empty ⊢ abs x T₁₁ t₁₂ : T₁→T₂
         经反演可得
             x:T₁ ⊢ t₁₂ : T₂
         我们已经证明了 substitution_preserves_typing，又根据假设，有
             empty ⊢ v₂ : T₁
         故此分支证明完毕。 *)
      apply substitution_preserves_typing with T₁...
      inversion HT₁...
  - (* T_Proj *)
    (* 若 T_Proj，则 t = rproj t₁ i。
       证明 t --> t' 需要两条规则：T_Proj1 和 T_ProjRcd。
       t' 的定型可从前面情况中的归纳假设得出，因此我们只需考虑
       T_ProjRcd  即可。

       这里我们知道 t 为记录体值。由于使用了规则 T_Proj，
       我们知道对于某些 i 和 Tr 有 empty ⊢ t \in Tr 且
       Tlookup i Tr = Some Ti。接着可以应用引理 lookup_field_in_value
       来查找该投影步骤所得的记录元素。 *)
    destruct (lookup_field_in_value _ _ _ _ H₂ HT H)
      as [vi [Hget Htyp]].
    rewrite H₄ in Hget. inversion Hget. subst...
  - (* T_RCons *)
    (* 若最后一条规则为 T_RCons，那么对于某些 i、t 和满足
       record_tm tr 的 tr，有 t = rcons i t tr。若该步骤为
       ST_Rcd_Head，则结果可由归纳假设直接得出。若该步骤为
       ST_Rcd_Tail，那么对于某些 tr₂' 有 tr --> tr₂'，
       我们还需要使用引理 step_preserves_record_tm 来证明 record_tm tr₂'。 *)
    apply T_RCons... eapply step_preserves_record_tm...
Qed.
☐

End STLCExtendedRecords.

---

(* 2022-03-14 05:28:24 (UTC+00) *)