Prove a function on option

theories/typing/lib/option.v

@@ -39,7 +39,7 @@ Section option.
     eqtype E L (option_ty ty) (option_ty ty') (option_map f) (option_map g).
   Proof. move=> [??]. split; by apply option_subtype. Qed.
 
-(*
+
   (* Variant indices. *)
   Definition none := 0%nat.
   Definition some := 1%nat.
@@ -50,30 +50,72 @@ Section option.
       let: "r" := new [ #2 ] in
     withcont: "k":
       case: !"o'" of
-        [ "r" <-{Σ none} ();; "k" [];
-          "r" <-{Σ some} "o'" +ₗ #1;; "k" [] ]
+        [ "r" <-{Σ none} ();; jump: "k" [];
+          "r" <-{Σ some} "o'" +ₗ #1;; jump: "k" [] ]
     cont: "k" [] :=
       delete [ #1; "o"];; return: ["r"].
 
-  Lemma option_as_mut_type τ :
+  Lemma tctx_extract_ctx_eq {𝔄 𝔅l ℭl} tr tr' E L
+      (t: _ 𝔄) (T1: tctx 𝔅l) (T2: tctx ℭl) :
+      tctx_extract_elt E L t T1 T2 tr' → tr = tr' → tctx_extract_elt E L t T1 T2 tr.
+Proof. by move=> ? ->. Qed.
+  From iris.proofmode Require Import environments.
+
+  Lemma option_as_mut_type {𝔄} (τ : _ 𝔄) :
     typed_val
-      option_as_mut (fn(∀ α, ∅; &uniq{α} (option τ)) → option (&uniq{α}τ)).
+      option_as_mut (fn<α>(∅; &uniq{α} (option_ty τ)) → option_ty (&uniq{α} τ))
+      (λ (post : of_syn_type (predₛ (optionₛ (_ * _))))  '-[a], match a with
+        | (Some a, Some a') => post (Some (a, a'))
+        | (None, None) => post None
+        | _ => False
+      end).
   Proof.
-    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !>". iIntros (α ϝ ret p).
-      inv_vec p=>o. simpl_subst.
-    iApply type_deref; [solve_typing..|]. iIntros (o'). simpl_subst.
+    eapply type_fn; [solve_typing|]. iIntros (α ϝ ret [o []]). simpl_subst. via_tr_impl.
+    iApply type_deref; [solve_extract|solve_typing..|]. iIntros (o'). simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
-    iApply (type_cont [] [ϝ ⊑ₗ []] (λ _, [o ◁ _; r ◁ _])) ; [solve_typing..| |].
-    - iIntros (k). simpl_subst.
-      iApply type_case_uniq; [solve_typing..|].
-        constructor; last constructor; last constructor; left.
-      + iApply (type_sum_unit (option $ &uniq{α}τ)%T); [solve_typing..|].
-        iApply type_jump; solve_typing.
-      + iApply (type_sum_assign (option $ &uniq{α}τ)%T); [try solve_typing..|].
-        iApply type_jump; solve_typing.
+    iApply (type_cont [] (λ _, +[o ◁ _ ; r ◁ _ ]) [ϝ ⊑ₗ []]).
+    iIntros (k). simpl_subst. set E := fp_E _ _. set L := [ϝ ⊑ₗ []].
+    - iApply (type_case_uniq (𝔄l := [_ ; _ ]) +[inl _; inl _] _ _ _ _ +[_; _] _ α +[unit_ty; τ]);
+      [ solve_typing | solve_typing | | solve_typing | ].
+      eapply tctx_extract_elt_further, tctx_uniq_mod_ty_out'; [apply _| solve_typing].
+      constructor; last constructor; last constructor.
+      +
+      iStartProof;
+      match goal with |- envs_entails _ (typed_body _ _ [k ◁cont{_, _} ?c; _] ?T _ _) =>
+        let TypeT := type of T in
+        match eval hnf in TypeT with (hlist _ ?𝔄l) =>
+          iApply (typed_body_impl (𝔄l:=𝔄l) (λ post '-[e; f; d], c post -[d; _] )); last first
+        end
+      end.
+
+        iApply (type_sum_unit _ +[unit_ty ; (&uniq{α} τ)%T] 0 _ _ _  _  _  _ _  _ _  _  _ eq_refl); [solve_typing..|].
+        iApply type_jump; [solve_typing|solve_extract|solve_typing].
+        rewrite /compose /= => ? [? [? [ ? [? ?]]]]  //.
+      +
+        iStartProof;
+        match goal with |- envs_entails _ (typed_body _ _ [k ◁cont{_, _} ?c; _] ?T _ _) =>
+          let TypeT := type of T in
+          match eval hnf in TypeT with (hlist _ ?𝔄l) =>
+            iApply (typed_body_impl (𝔄l:=𝔄l) (λ post '-[e; f; d], c post -[d; inr (inl e)] )); last first
+          end
+        end.
+        iApply (type_sum_assign _ +[() ; &uniq{α} τ]%T 1 _ _ _); [try solve_typing..|].
+        iApply type_jump; [solve_typing|solve_extract|solve_typing].
+        rewrite /compose /= => ? [? [? [? []]]] //.
     - iIntros "/= !>". iIntros (k args). inv_vec args. simpl_subst.
-      iApply type_delete; [solve_typing..|].
-      iApply type_jump; solve_typing.
+      iApply (typed_body_impl (𝔄l := [() ; Σ! [(); _]]%ST) (𝔅 := optionₛ _) (λ post '-[_; b], post (sum'_to_option b))); last first.
+      iApply type_delete; [solve_extract|solve_typing..|].
+      iApply type_jump; [solve_typing| |solve_typing].
+      eapply tctx_extract_ctx_elt; last solve_extract.
+      eapply tctx_extract_elt_here, own_subtype, mod_ty_in.
+      rewrite /compose /= => ? [? [b []]] //.
+    - move => ? [[+ +] []] + ?? ++ [|[|i]] //=.
+      + move => [?|] [?|] // _  ++ ?? [= ??]. by subst.
+      + move => [?|] [?|] // ? ++ ?? [= ??]; subst; try done.
+        move => [= <-] [= <-] //.
+      + move => ?? _ _ _ [[] _].
+    Unshelve.
+    by eapply option_ty, prod_ty.
   Qed.
 
   Definition option_unwrap_or τ : val :=