coercion

logsem · Jan 30, 2024 · d5cbc77 · d5cbc77
1 parent 733ff1d
commit d5cbc77
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 0 deletions.
diff --git a/theories/gitree/reify.v b/theories/gitree/reify.v
@@ -31,6 +31,26 @@ Section reifier.
     }.
 End reifier.
 
+Section reifier_coercion.
+  Context {A} `{!Cofe A}.
+  #[local] Open Scope type.
+  Program Definition sReifier_NotCtxDep_CtxDep (r : sReifier NotCtxDep)
+    : sReifier CtxDep :=
+    {|
+      sReifier_ops := sReifier_ops _ r;
+      sReifier_state := sReifier_state _ r;
+      sReifier_re x xc op :=
+        (λne y, (optionO_map (prodO_map y.2 idfun)
+                   (sReifier_re _ r op (y.1.1, y.1.2))));
+        sReifier_inhab := sReifier_inhab _ r;
+      sReifier_cofe := sReifier_cofe _ r;
+    |}.
+  Next Obligation.
+    intros.
+    repeat intro; repeat f_equiv; assumption.
+  Qed.
+End reifier_coercion.
+
 Section reifier_cofe_inst.
   Context {A} `{!Cofe A}.
   #[local] Open Scope type.

diff --git a/theories/lang_generic.v b/theories/lang_generic.v
@@ -26,6 +26,19 @@ Section interp.
     solve_proper.
   Qed.
 
+  Definition interp_scope_split {S1 S2 : Set} :
+    interp_scope (sum S1 S2) -n> interp_scope S1 * interp_scope S2.
+  Proof.
+    simple refine (λne (f : interp_scope (sum S1 S2)), _).
+    - split.
+      + simple refine (λne x, _).
+        apply (f (inl x)).
+      + simple refine (λne x, _).
+        apply (f (inr x)).
+    - repeat intro; simpl.
+      repeat f_equiv; intro; simpl; f_equiv; assumption.
+  Defined.
+
   Global Instance interp_var_proper {S : Set} (v : S) : Proper ((≡) ==> (≡)) (interp_var v).
   Proof. apply ne_proper. apply _. Qed.