systemf: logrel & free theorems

_CoqProject

@@ -9,6 +9,7 @@
 theories/lib/maps.v
 theories/lib/sets.v
 theories/lib/debruijn.v
+theories/lib/facts.v
 
 # STLC
 theories/stlc/lang.v
@@ -42,6 +43,10 @@ theories/systemf/types.v
 theories/systemf/tactics.v
 theories/systemf/bigstep.v
 theories/systemf/church_encodings.v
+theories/systemf/parallel_subst.v
+theories/systemf/logrel.v
+theories/systemf/free_theorems.v
+
 
 # By removing the # below, you can add the exercise sheets to make
 # theories/warmup/sheet0.v

theories/lib/facts.v

+From stdpp Require Export relations.
+From stdpp Require Import binders gmap.
+
+Lemma if_iff P Q R S:
+  (P ↔ Q) →
+  (R ↔ S) →
+  ((P → R) ↔ (Q → S)).
+Proof.
+  naive_solver.
+Qed.
+
+Lemma list_subseteq_cons {X} (A B : list X) x : A ⊆ B → x :: A ⊆ x :: B.
+Proof. intros Hincl. intros y. rewrite !elem_of_cons. naive_solver. Qed.
+Lemma list_subseteq_cons_binder A B x : A ⊆ B → x :b: A ⊆ x :b: B.
+Proof. destruct x; [done|]. apply list_subseteq_cons. Qed.
+Lemma list_subseteq_cons_l {X} (A B : list X) x : A ⊆ x :: B → x :: A ⊆ x :: B.
+Proof. 
+  intros Hincl. intros y. rewrite elem_of_cons. intros [-> | ?]. 
+  - left.
+  - apply Hincl. naive_solver. 
+Qed.
+
+Lemma list_subseteq_cons_elem {X} (A B : list X) x :
+  x ∈ B → A ⊆ B → (x :: A) ⊆ B.
+Proof.
+  intros Hel Hincl.
+  intros a [-> | ?]%elem_of_cons; [done|].
+  by apply Hincl.
+Qed.
+
+Lemma elements_subseteq `{EqDecision A} `{Countable A} (X Y : gset A):
+  X ⊆ Y → elements X ⊆ elements Y.
+Proof.
+  rewrite elem_of_subseteq.
+  intros Ha a. rewrite !elem_of_elements.
+  apply Ha.
+Qed.
+Lemma list_subseteq_cons_r {X} (A B : list X) x :
+  A ⊆ B → A ⊆ (x :: B).
+Proof.
+  intros Hincl. trans B; [done|].
+  intros b Hel. apply elem_of_cons; by right.
+Qed.

theories/systemf/free_theorems.v

+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.lib Require Export debruijn.
+From semantics.systemf Require Import lang notation parallel_subst types bigstep tactics logrel.
+From Equations Require Import Equations.
+
+(** * Free Theorems *)
+Implicit Types
+  (Δ : nat)
+  (Γ : typing_context)
+  (v : val)
+  (α : var)
+  (e : expr)
+  (A : type).
+
+Lemma not_every_type_inhabited : ¬ ∃ e, TY 0; ∅ ⊢ e : (∀: #0).
+Proof.
+  intros (e & Hty%sem_soundness).
+  specialize (Hty ∅ δ_any). simp type_interp in Hty.
+  destruct Hty as (v & Hb & Hv).
+  { constructor. }
+  simp type_interp in Hv. destruct Hv as (e' & -> & Hcl & Ha).
+  (* [specialize_sem_type] defines a semantic type, spawning a subgoal for the closedness sidecondition *)
+  specialize_sem_type Ha with (λ _, False) as τ; first done.
+  simp type_interp in Ha. destruct Ha as (v' & He' & Hv').
+  simp type_interp in Hv'. simpl in Hv'.
+  done.
+Qed.
+
+Lemma all_identity :
+  ∀ e,
+  TY 0; ∅ ⊢ e : (∀: #0 → #0) →
+  ∀ v, is_closed [] v → big_step (e <> (of_val v)) v.
+Proof.
+  intros e Hty%sem_soundness v0 Hcl_v0.
+  specialize (Hty ∅ δ_any). simp type_interp in Hty.
+  destruct Hty as (v & Hb & Hv).
+  { constructor. }
+
+  simp type_interp in Hv. destruct Hv as (e' & -> & Hcl & Hv).
+  specialize_sem_type Hv with (λ v, v = v0) as τ.
+  { intros v ->; done. }
+  simp type_interp in Hv.
+
+  destruct Hv as (v & He & Hv).
+  simp type_interp in Hv.
+  destruct Hv as (x & e'' & -> & Hcl' & Hv).
+  specialize (Hv v0 ltac:(done)).
+
+  simp type_interp in Hv. destruct Hv as (v & Hb' & Hv).
+  simp type_interp in Hv; simpl in Hv. subst v.
+
+  rewrite subst_map_empty in Hb.
+  eauto using big_step_of_val.
+Qed.

theories/systemf/parallel_subst.v

+From stdpp Require Import prelude.
+From iris Require Import prelude.
+From semantics.systemf Require Import lang.
+From semantics.lib Require Import maps.
+
+Fixpoint subst_map (xs : gmap string expr) (e : expr) : expr :=
+  match e with
+  | Lit l => Lit l
+  | Var y => match xs !! y with Some es => es | _ =>  Var y end
+  | App e1 e2 => App (subst_map xs e1) (subst_map xs e2)
+  | Lam x e => Lam x (subst_map (binder_delete x xs) e)
+  | UnOp op e => UnOp op (subst_map xs e)
+  | BinOp op e1 e2 => BinOp op (subst_map xs e1) (subst_map xs e2)
+  | If e0 e1 e2 => If (subst_map xs e0) (subst_map xs e1) (subst_map xs e2)
+  | TApp e => TApp (subst_map xs e)
+  | TLam e => TLam (subst_map xs e)
+  | Pack e => Pack (subst_map xs e)
+  | Unpack x e1 e2 => Unpack x (subst_map xs e1) (subst_map (binder_delete x xs) e2)
+  | Pair e1 e2 => Pair (subst_map xs e1) (subst_map xs e2)
+  | Fst e => Fst (subst_map xs e)
+  | Snd e => Snd (subst_map xs e)
+  | InjL e => InjL (subst_map xs e)
+  | InjR e => InjR (subst_map xs e)
+  | Case e e1 e2 => Case (subst_map xs e) (subst_map xs e1) (subst_map xs e2)
+  end.
+
+Lemma subst_map_empty e :
+  subst_map ∅ e = e.
+Proof.
+  induction e; simpl; f_equal; eauto.
+  all: destruct x; simpl; [done | by rewrite !delete_empty..].
+Qed.
+
+Lemma subst_map_is_closed X e xs :
+  is_closed X e →
+  (∀ x : string, x ∈ dom xs → x ∉ X) →
+  subst_map xs e = e.
+Proof.
+  intros Hclosed Hd.
+  induction e in xs, X, Hd, Hclosed |-*; simpl in *;try done.
+  all: repeat match goal with
+  | H : Is_true (_ && _)  |- _ => apply andb_True in H as [ ? ? ]
+              end.
+  { (* Var *)
+    apply bool_decide_spec in Hclosed.
+    assert (xs !! x = None) as ->; last done.
+    destruct (xs !! x) as [s | ] eqn:Helem; last done.
+    exfalso; eapply Hd; last apply Hclosed.
+    apply elem_of_dom; eauto.
+  }
+  { (* lambdas *)
+    erewrite IHe; [done | done |].
+    intros y. destruct x as [ | x]; first apply Hd.
+    simpl.
+    rewrite dom_delete elem_of_difference not_elem_of_singleton.
+    intros [Hnx%Hd Hneq]. rewrite elem_of_cons. intros [? | ?]; done.
+  }
+  8: { (* Unpack *)
+    erewrite IHe1; [ | done | done].
+    erewrite IHe2; [ done | done | ].
+    intros y. destruct x as [ | x]; first apply Hd.
+    simpl.
+    rewrite dom_delete elem_of_difference not_elem_of_singleton.
+    intros [Hnx%Hd Hneq]. rewrite elem_of_cons. intros [? | ?]; done.
+  }
+  (* all other cases *)
+  all: repeat match goal with
+       | H : ∀ _ _, _ → _ → subst_map _ _ = _ |- _ => erewrite H; clear H
+       end; done.
+Qed.
+
+Lemma subst_map_subst map x (e e' : expr) :
+  is_closed [] e' →
+  subst_map map (subst x e' e) = subst_map (<[x:=e']>map) e.
+Proof.
+  intros He'.
+  revert x map; induction e; intros xx map; simpl;
+  try (f_equal; eauto).
+  - case_decide.
+    + simplify_eq/=. rewrite lookup_insert.
+      rewrite (subst_map_is_closed []); [done | apply He' | ].
+      intros ? ?. apply not_elem_of_nil.
+    + rewrite lookup_insert_ne; done.
+  - destruct x; simpl; first done.
+    + case_decide.
+      * simplify_eq/=. by rewrite delete_insert_delete.
+      * rewrite delete_insert_ne; last by congruence. done.
+  - destruct x; simpl; first done.
+    + case_decide.
+      * simplify_eq/=. by rewrite delete_insert_delete.
+      * rewrite delete_insert_ne; last by congruence. done.
+Qed.
+
+Definition subst_is_closed (X : list string) (map : gmap string expr) :=
+  ∀ x e, map !! x = Some e → closed X e.
+Lemma subst_is_closed_subseteq X map1 map2 :
+  map1 ⊆ map2 → subst_is_closed X map2 → subst_is_closed X map1.
+Proof.
+  intros Hsub Hclosed2 x e Hl. eapply Hclosed2, map_subseteq_spec; done.
+Qed.
+
+Lemma subst_subst_map x es map e :
+  subst_is_closed [] map →
+  subst x es (subst_map (delete x map) e) =
+  subst_map (<[x:=es]>map) e.
+Proof.
+  revert map es x; induction e; intros map v0 xx Hclosed; simpl;
+  try (f_equal; eauto).
+  - destruct (decide (xx=x)) as [->|Hne].
+    + rewrite lookup_delete // lookup_insert //. simpl.
+      rewrite decide_True //.
+    + rewrite lookup_delete_ne // lookup_insert_ne //.
+      destruct (_ !! x) as [rr|] eqn:Helem.
+      * apply Hclosed in Helem.
+        by apply subst_is_closed_nil.
+      * simpl. rewrite decide_False //.
+  - destruct x; simpl; first by auto.
+    case_decide.
+    + simplify_eq. rewrite delete_idemp delete_insert_delete. done.
+    + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. apply IHe.
+      eapply subst_is_closed_subseteq; last done.
+      apply map_delete_subseteq.
+  - destruct x; simpl; first by auto.
+    case_decide.
+    + simplify_eq. rewrite delete_idemp delete_insert_delete. done.
+    + rewrite delete_insert_ne //; last congruence. rewrite delete_commute. apply IHe2.
+      eapply subst_is_closed_subseteq; last done.
+      apply map_delete_subseteq.
+Qed.
+
+Lemma subst'_subst_map b (es : expr) map e :
+  subst_is_closed [] map →
+  subst' b es (subst_map (binder_delete b map) e) =
+  subst_map (binder_insert b es map) e.
+Proof.
+  destruct b; first done.
+  apply subst_subst_map.
+Qed.
+
+Lemma closed_subst_weaken e map X Y :
+  subst_is_closed [] map →
+  (∀ x, x ∈ X → x ∉ dom map → x ∈ Y) →
+  closed X e →
+  closed Y (subst_map map e).
+Proof.
+  induction e in X, Y, map |-*; rewrite /closed; simpl; intros Hmclosed Hsub Hcl; first done.
+  all: repeat match goal with
+  | H : Is_true (_ && _)  |- _ => apply andb_True in H as [ ? ? ]
+              end.
+  { (* vars *)
+    destruct (map !! x) as [es | ] eqn:Heq.
+    + apply is_closed_weaken_nil. by eapply Hmclosed.
+    + apply bool_decide_pack. apply Hsub; first by eapply bool_decide_unpack.
+      by apply not_elem_of_dom.
+  }
+  { (* lambdas *)
+    eapply IHe; last done.
+    + eapply subst_is_closed_subseteq; last done.
+      destruct x; first done. apply map_delete_subseteq.
+    + intros y. destruct x as [ | x]; first by apply Hsub.
+      rewrite !elem_of_cons. intros [-> | Hy] Hn; first by left.
+      destruct (decide (y = x)) as [ -> | Hneq]; first by left.
+      right. eapply Hsub; first done. set_solver.
+  }
+  8: { (* unpack *)
+    apply andb_True; split; first naive_solver.
+    eapply IHe2; last done.
+    + eapply subst_is_closed_subseteq; last done.
+      destruct x; first done. apply map_delete_subseteq.
+    + intros y. destruct x as [ | x]; first by apply Hsub.
+      rewrite !elem_of_cons. intros [-> | Hy] Hn; first by left.
+      destruct (decide (y = x)) as [ -> | Hneq]; first by left.
+      right. eapply Hsub; first done. set_solver.
+  }
+  (* all other cases *)
+  all: repeat match goal with
+         | |- Is_true (_ && _) => apply andb_True; split
+              end.
+  all: naive_solver.
+Qed.