Pre

I had thought I understand how to prove progress in Coq for some simple semantic ..... until I saw one of our QE question

Link is here
https://eng-cs.syr.edu/wp-content/uploads/2018/10/CISE-QE-1-January-8-2018.pdf

Semantic

operational semantic

It looks quite straight forward. Interesting part of this semantic is raise and handle. if exception in raise body is not handled, language will run into the case of a direct raise γ which very similar to a abort. And looks quite easy to formalize it in Coq.

Inductive expr : Type :=
| Tru
| Fls
| If (e0 : expr) (e1 : expr) (e2 : expr)
| Raise (γ : string)
| Handle (e1 : expr) (γ : string) (e2 : expr).

(* bool is the only type here *)
Inductive ty : Type :=
| TBool : ty.

Inductive eval : expr -> expr -> Prop :=
| E_If_t : forall e2 e3, eval (If Tru e2 e3) e2
| E_If_f : forall e2 e3, eval (If Fls e2 e3) e3
| E_If_g : forall e1 e1' e2 e3,
    eval e1 e1' ->
    eval (If e1 e2 e3) (If e1' e2 e3)
| E_If_r : forall e2 e3 γ,
    eval (If (Raise γ) e2 e3) (Raise γ)
| E_handle_t : forall γ e2, eval (Handle Tru γ e2) Tru
| E_handle_f : forall γ e2, eval (Handle Fls γ e2) Fls
| E_handle_r : forall γ e2, eval (Handle (Raise γ) γ e2) e2
| E_handle_e : forall e1 e1' γ e2,
    eval e1 e1' ->
    eval (Handle e1 γ e2) (Handle e1' γ e2)
| E_handle_h : forall γ γ' e2,
    γ <> γ' ->
    eval (Handle (Raise γ) γ' e2) (Raise γ).

in order to make sure of every raise is handled, we also has following typing rule:

Typing

Inductive value : expr -> Prop :=
| v_t : value Tru
| v_f : value Fls.

Inductive has_type : context -> expr -> ty -> Prop :=
| T_Tru : forall Γ, has_type Γ Tru TBool
| T_Fls : forall Γ, has_type Γ Fls TBool
| T_Raise : forall Γ γ, (Γ γ) = 1 -> has_type Γ (Raise γ) TBool
| T_If : forall Γ e1 e2 e3,
    has_type Γ e1 TBool ->
    has_type Γ e2 TBool ->
    has_type Γ e3 TBool ->
    has_type Γ (If e1 e2 e3) TBool
| T_Handle : forall Γ γ e1 e2,
    (Γ γ) = 0 ->
    has_type (γ !-> 1 ; Γ) e1 TBool ->
    has_type Γ e2 TBool ->
    has_type Γ (Handle e1 γ e2) TBool.

My Coq knowledge is very limited, so I use a total map to simulate set, since the core of this this problem is not proving properties of set. So my plan is just leave and use addmited on that part of proof. (TvT)/

Progress

finally this QE question ask me to prove progress properties of above semantic. However, since we also has raise here. So this language can finally run into either a value or a raise.

Theorem e_progress : forall e T Γ,
    has_type Γ e T ->
    value e \/ (exists γ, (Γ γ) = 1 -> e = Raise γ) \/ exists e', eval e e'.
Proof with eauto.
  intros.
  induction H...
  - right. right.
    destruct IHhas_type1.
    inversion H2; subst...
    destruct H2.
    inversion H; subst... 
    (* stuck *)

My proof start from induction on type relation, True, False and Raise case is trivial. First interesting case is If case. If e1 e2 e3 of course should step to something. But the second clause of my inductive hypothesis really annoy me, a or case. It is easy to see value If ... of course is impossible and can be eliminated, but second clause which is an exists one can't be discriminated! My proof context looks like this:

H2 looks like an impossible case, because If of course can't equal to a Raise. But if I want to get that , I need to show γ in set of Γ ! this is not in any of context.... and my proof stuck....

....

my failure code is here....
https://github.com/StarGazerM/my-foolish-code/blob/master/qe/pl2018.v