From 73df1945b31c0beee88cf4476df4ccd09d31403b Mon Sep 17 00:00:00 2001 From: Rutger Broekhoff Date: Wed, 26 Jun 2024 20:50:18 +0200 Subject: Import Coq project --- sem.v | 167 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 167 insertions(+) create mode 100644 sem.v (limited to 'sem.v') diff --git a/sem.v b/sem.v new file mode 100644 index 0000000..6560b82 --- /dev/null +++ b/sem.v @@ -0,0 +1,167 @@ +Require Import Coq.Strings.String. +From stdpp Require Import gmap. +From mininix Require Import binop expr matching relations. + +Definition attrset := is_Some ∘ maybe V_Attrset. + +Reserved Infix "-->base" (right associativity, at level 55). + +Inductive base_step : expr → expr → Prop := + | E_Force (sv : strong_value) : + X_Force sv -->base sv + | E_Closed e : + X_Closed e -->base e + | E_Placeholder x e : + X_Placeholder x e -->base e + | E_MSelect bs x ys : + X_Select (V_Attrset bs) (nonempty_cons x ys) -->base + X_Select (X_Select (V_Attrset bs) (nonempty_singleton x)) ys + | E_Select e bs x : + X_Select (V_Attrset (<[x := e]>bs)) (nonempty_singleton x) -->base e + | E_SelectOr bs x e : + X_SelectOr (V_Attrset bs) (nonempty_singleton x) e -->base + X_Cond (X_HasAttr (V_Attrset bs) x) + (* if true *) + (X_Select (V_Attrset bs) (nonempty_singleton x)) + (* if false *) + e + | E_MSelectOr bs x ys e : + X_SelectOr (V_Attrset bs) (nonempty_cons x ys) e -->base + X_Cond (X_HasAttr (V_Attrset bs) x) + (* if true *) + (X_SelectOr + (X_Select (V_Attrset bs) (nonempty_singleton x)) + ys e) + (* if false *) + e + | E_Rec bs : + X_Attrset bs -->base V_Attrset (rec_subst bs) + | E_Let e bs : + X_LetBinding bs e -->base subst (closed (rec_subst bs)) e + | E_With e bs : + X_Incl (V_Attrset bs) e -->base subst (placeholders bs) e + | E_WithNoAttrset v1 e2 : + ¬ attrset v1 → + X_Incl v1 e2 -->base e2 + | E_ApplySimple x e1 e2 : + X_Apply (V_Fn x e1) e2 -->base subst {[x := X_Closed e2]} e1 + | E_ApplyAttrset m e bs bs' : + bs ~ m ~> bs' → + X_Apply (V_AttrsetFn m e) (V_Attrset bs) -->base + X_LetBinding bs' e + | E_ApplyFunctor e1 e2 bs : + X_Apply (V_Attrset (<["__functor" := e2]>bs)) e1 -->base + X_Apply (X_Apply e2 (V_Attrset (<["__functor" := e2]>bs))) e1 + | E_IfTrue e2 e3 : + X_Cond true e2 e3 -->base e2 + | E_IfFalse e2 e3 : + X_Cond false e2 e3 -->base e3 + | E_Op op v1 v2 u : + v1 ⟦op⟧ v2 -⊚-> u → + X_Op op v1 v2 -->base u + | E_OpHasAttrTrue bs x : + is_Some (bs !! x) → + X_HasAttr (V_Attrset bs) x -->base true + | E_OpHasAttrFalse bs x : + bs !! x = None → + X_HasAttr (V_Attrset bs) x -->base false + | E_OpHasAttrNoAttrset v x : + ¬ attrset v → + X_HasAttr v x -->base false + | E_Assert e2 : + X_Assert true e2 -->base e2 +where "e -->base e'" := (base_step e e'). + +Notation "e '-->base*' e'" := (rtc base_step e e') + (right associativity, at level 55). + +Hint Constructors base_step : core. + +Variant is_ctx_item : bool → bool → (expr → expr) → Prop := + | IsCtxItem_Select uf_ext xs : + is_ctx_item uf_ext false (λ e1, X_Select e1 xs) + | IsCtxItem_SelectOr uf_ext xs e2 : + is_ctx_item uf_ext false (λ e1, X_SelectOr e1 xs e2) + | IsCtxItem_Incl uf_ext e2 : + is_ctx_item uf_ext false (λ e1, X_Incl e1 e2) + | IsCtxItem_ApplyL uf_ext e2 : + is_ctx_item uf_ext false (λ e1, X_Apply e1 e2) + | IsCtxItem_ApplyAttrsetR uf_ext m e1 : + is_ctx_item uf_ext false (λ e2, X_Apply (V_AttrsetFn m e1) e2) + | IsCtxItem_CondL uf_ext e2 e3 : + is_ctx_item uf_ext false (λ e1, X_Cond e1 e2 e3) + | IsCtxItem_AssertL uf_ext e2 : + is_ctx_item uf_ext false (λ e1, X_Assert e1 e2) + | IsCtxItem_OpL uf_ext op e2 : + is_ctx_item uf_ext false (λ e1, X_Op op e1 e2) + | IsCtxItem_OpR uf_ext op v1 : + is_ctx_item uf_ext false (λ e2, X_Op op (X_V v1) e2) + | IsCtxItem_OpHasAttrL uf_ext x : + is_ctx_item uf_ext false (λ e, X_HasAttr e x) + | IsCtxItem_Force uf_ext : + is_ctx_item uf_ext true (λ e, X_Force e) + | IsCtxItem_ForceAttrset bs x : + is_ctx_item true true (λ e, X_V (V_Attrset (<[x := e]>bs))). + +Hint Constructors is_ctx_item : core. + +Inductive is_ctx : bool → bool → (expr → expr) → Prop := + | IsCtx_Id uf : is_ctx uf uf id + | IsCtx_Compose E1 E2 uf_int uf_aux uf_ext : + is_ctx_item uf_ext uf_aux E1 → + is_ctx uf_aux uf_int E2 → + is_ctx uf_ext uf_int (E1 ∘ E2). + +Hint Constructors is_ctx : core. + +(* /--> This is required because the standard library definition of "-->" + | (in Coq.Classes.Morphisms, for `respectful`) defines that this operator + | uses right associativity. Our definition must match exactly, as Coq + | will give an error otherwise. + \-------------------------------------\ + | | *) +Reserved Infix "-->" (right associativity, at level 55). + +Variant step : expr → expr → Prop := + E_Ctx e1 e2 E uf_int : + is_ctx false uf_int E → + e1 -->base e2 → + E e1 --> E e2 +where "e --> e'" := (step e e'). + +Hint Constructors step : core. + +Notation "e '-->*' e'" := (rtc step e e') (right associativity, at level 55). + +(** Theories for contexts *) + +Lemma is_ctx_once uf_ext uf_int E : + is_ctx_item uf_ext uf_int E → is_ctx uf_ext uf_int E. +Proof. intros. eapply IsCtx_Compose; [done | constructor]. Qed. + +Lemma is_ctx_item_ext_imp E uf_int : + is_ctx_item false uf_int E → is_ctx_item true uf_int E. +Proof. intros H. inv H; constructor. Qed. + +Lemma is_ctx_ext_imp E1 E2 uf_aux uf_int : + is_ctx_item false uf_aux E1 → + is_ctx uf_aux uf_int E2 → + is_ctx true uf_int (E1 ∘ E2). +Proof. + intros H1 H2. + revert E1 H1. + induction H2; intros. + - inv H1; eapply IsCtx_Compose; constructor. + - eapply IsCtx_Compose. + + by apply is_ctx_item_ext_imp in H1. + + by eapply IsCtx_Compose. +Qed. + +Lemma is_ctx_uf_false_impl_true E uf_int : + is_ctx false uf_int E → + is_ctx true uf_int E ∨ E = id. +Proof. + intros Hctx. inv Hctx. + - by right. + - left. eapply is_ctx_ext_imp; [apply H | apply H0]. +Qed. -- cgit v1.2.3