Composed-shortcut-laws

fx.experimental.desc-interp.composed-shortcut-laws: six H.refl lemmas — state's three canonical ops on inl and error's three strategies on inr — anchoring composedHandlerShortcut soundness. Each chains composeHandlersInl/InrLemma, the per-effect uniform-shortcut lemma, and inner sumElim ι; all three reductions are conv-decidable.

errorCollectingInrLemma

H.refl proof of errorCollectingInrLemmaTy. Resume payload := tt; new s_B := cons E payload s_B.

errorCollectingInrLemmaTy

Π E S_A A. Π H_A. Π payload:E. Π s_A:S_A. Π s_B:List E. composeHandlers … H_A uniformOf_collecting (inr (error E payload)) (pair s_A s_B) ≡ mkResumeAt … tt (pair s_A (cons E payload s_B)).

errorResultInrLemma

H.refl proof of errorResultInrLemmaTy. Abort channel Sum E A_inner carries inl payload.

errorResultInrLemmaTy

Π E S_A S_B A_inner. Π H_A. Π payload:E. Π s_A:S_A. Π s_B:S_B. composeHandlers … H_A uniformOf_result (inr (error E payload)) (pair s_A s_B) ≡ mkAbortAt … (Sum E A_inner) (inl E A_inner payload) (pair s_A s_B).

errorStrictInrLemma

H.refl proof of errorStrictInrLemmaTy. Strict always aborts; abort payload := payload.

errorStrictInrLemmaTy

Π E S_A S_B. Π H_A. Π payload:E. Π s_A:S_A. Π s_B:S_B. composeHandlers … H_A uniformOf_strict (inr (error E payload)) (pair s_A s_B) ≡ mkAbortAt … E payload (pair s_A s_B).

stateGetInlLemma

H.refl proof of stateGetInlLemmaTy. handle_State (get S) s_A ι→ inl(pair s_A s_A); inner sumElim ι folds to the composed mkResumeAt.

stateGetInlLemmaTy

Π E S_A A. Π H_B. Π s_A:S_A. Π s_B:List E. composeHandlers … handle_State H_B (inl (get S_A)) (pair s_A s_B) ≡ mkResumeAt … (inl (get S_A)) A s_A (pair s_A s_B).

stateModifyInlLemma

H.refl proof of stateModifyInlLemmaTy. New sub-state := fn s_A; resume payload := tt.

stateModifyInlLemmaTy

Π E S_A A. Π H_B. Π fn:S_A→S_A. Π s_A:S_A. Π s_B:List E. composeHandlers … handle_State H_B (inl (modify S_A fn)) (pair s_A s_B) ≡ mkResumeAt … tt (pair (fn s_A) s_B).

statePutInlLemma

H.refl proof of statePutInlLemmaTy. New sub-state := param; resume payload := tt.

statePutInlLemmaTy

Π E S_A A. Π H_B. Π param s_A:S_A. Π s_B:List E. composeHandlers … handle_State H_B (inl (put S_A param)) (pair s_A s_B) ≡ mkResumeAt … tt (pair param s_B).