catala/doc/formalization/Catala.Translation.Helpers.fst

module Catala.Translation.Helpers

open Catala.LambdaCalculus
module T = FStar.Tactics

(*** Default translation *)

let process_exceptions_f (tau: ty) : Tot exp =
  EAbs (TOption tau) (EAbs (TArrow TUnit tau) (
    EApp (EAbs (TOption tau) (
      EMatchOption (EVar 2) tau
        (EVar 0)
        (EAbs tau (
          EMatchOption (EVar 1) tau
            (EVar 3)
            (EAbs tau (ELit (LError ConflictError)))
        ))
    ))
    (ECatchEmptyError (ESome (EApp (EVar 0) (ELit LUnit) TUnit)) ENone)
    (TOption tau)
  ))

let typ_process_exceptions_f (g: env) (tau: ty)
    : Lemma (typing g (process_exceptions_f tau)
      (TArrow (TOption tau) (TArrow (TArrow TUnit tau) (TOption tau))))
  =
  assert_norm(typing g (process_exceptions_f tau)
      (TArrow (TOption tau) (TArrow (TArrow TUnit tau) (TOption tau))))

let build_default_translation
  (exceptions: list exp)
  (acc: exp)
  (just: exp)
  (cons: exp)
  (tau: ty)
  =
  EMatchOption
    (EFoldLeft
      (process_exceptions_f tau)
      acc (TOption tau)
      (EList exceptions) (TArrow TUnit tau))
    tau
    (EIf
      just cons
      (ELit (LError EmptyError)))
    (EAbs tau (EVar 0))

#push-options "--fuel 1 --ifuel 0"
let build_default_translation_typing
  (exceptions: list exp)
  (acc: exp)
  (just: exp)
  (cons: exp)
  (tau: ty)
  (g: env)
    : Lemma
      (requires (
        typing_list g exceptions (TArrow TUnit tau) /\
        typing g acc (TOption tau) /\
        typing g just TBool /\
        typing g cons tau))
      (ensures (typing g (build_default_translation exceptions acc just cons tau) tau))
  =
  typ_process_exceptions_f g tau;
  assert_norm(typing g (build_default_translation exceptions acc just cons tau) tau)
#pop-options

#push-options "--fuel 9 --ifuel 0"
let process_exceptions_untouched_by_subst (s: var_to_exp) (tau: ty) : Lemma
    (subst s (process_exceptions_f tau) == process_exceptions_f tau)
  =
  ()
#pop-options

(*** Lambda calculus stepping lemmas *)

let well_typed_terms_invariant_by_subst (s: var_to_exp) (e: exp) (tau: ty) : Lemma
  (requires (typing empty e tau))
  (ensures (subst s e == e))
  =
  (* Classic lambda calculus result for terms that do not contain free variables *)
  admit()

(*** Step lifting framework *)

let typed_l_exp (tau: ty) = e:exp{typing empty e tau}

let rec take_l_steps (tau: ty) (e: typed_l_exp tau) (fuel: nat)
    : Tot (option (typed_l_exp tau))
      (decreases fuel) =
  if fuel = 0 then Some e else
  match step e with
  | None -> None
  | Some e' ->
    preservation e tau;
    take_l_steps tau e' (fuel - 1)

#push-options "--fuel 2 --ifuel 1"
let rec take_l_steps_transitive (tau: ty) (e1 e2: typed_l_exp tau) (n1 n2: nat)
    : Lemma
      (requires (take_l_steps tau e1 n1 == Some e2))
      (ensures (take_l_steps tau e1 (n1 + n2) == take_l_steps tau e2 n2))
      (decreases n1)
  =
  if n1 = 0 then () else begin
    match step e1 with
      | None -> ()
      | Some e1' ->
        preservation e1 tau;
        take_l_steps_transitive tau e1' e2 (n1 - 1) n2
  end
#pop-options

let not_l_value (tau: ty) = e:exp{not (is_value e) /\ typing empty e tau}
let l_value (tau: ty) = e:exp{is_value e /\ typing empty e tau}

let stepping_context (tau tau': ty) = typed_l_exp tau -> not_l_value tau'

let step_lift_commute_non_value
  (tau tau': ty)
  (f: stepping_context tau tau')
  (e: typed_l_exp tau)
    : prop
  =
  progress e tau;
  if is_value e then true else begin
    preservation e tau;
    step (f e) == Some (f (Some?.v (step e)))
  end

let is_stepping_agnostic_lift
  (tau tau': ty)
  (f:stepping_context tau tau')
    : prop
  =
  forall (e: typed_l_exp tau). step_lift_commute_non_value tau tau' f e

let stepping_agnostic_lift
  (tau tau': ty)
  : Type
  = f:(stepping_context tau tau'){is_stepping_agnostic_lift tau tau' f}

let rec l_values_dont_step (e: exp) : Lemma
    (requires (is_value e))
    (ensures (step e = None))
    (decreases %[e; 1])
  =
  match e with
  | EAbs _ _ -> ()
  | EThunk _ -> ()
  | ELit _ -> ()
  | ENone -> ()
  | ESome e' -> l_values_dont_step e'
  | EList [] -> ()
  | EList l -> l_values_dont_step_list e l
  | _ -> ()
and l_values_dont_step_list (e: exp) (l: list exp{l << e /\ Cons? l}) : Lemma
    (requires (is_value_list l))
    (ensures (step_list e l = Bad))
    (decreases %[e; 0; l])
  =
  match l with
  | [hd] -> l_values_dont_step hd
  | hd::tl ->
    l_values_dont_step hd;
    l_values_dont_step_list e tl

#push-options "--z3rlimit 50 --fuel 2 --ifuel 1"
let rec lift_multiple_l_steps
  (tau tau': ty)
  (e1: typed_l_exp tau)
  (e2: typed_l_exp tau)
  (n: nat)
  (f : stepping_agnostic_lift tau tau')
    : Lemma
      (requires (take_l_steps tau e1 n == Some e2))
      (ensures (take_l_steps tau' (f e1) n == Some (f e2)))
      (decreases n)
  =
  match step e1 with
  | None -> ()
  | Some e1' ->
    progress e1 tau;
    preservation e1 tau;
    if is_value e1 then
      l_values_dont_step e1
    else if n = 0 then
      ()
    else
      lift_multiple_l_steps tau tau' e1' e2 (n-1) f
#pop-options


(*** Lifts *)

let if_cond_lift'
  (tau: ty)
  (e2 e3: typed_l_exp tau)
    : stepping_context TBool tau
  =
  fun e1 -> EIf e1 e2 e3

let if_cond_lift_is_stepping_agnostic
  (tau: ty)
  (e2 e3: typed_l_exp tau)
  (e: typed_l_exp TBool)
    : Lemma
      (requires (True))
      (ensures (step_lift_commute_non_value TBool tau (if_cond_lift' tau e2 e3) e))
  =
  progress e TBool; if is_value e then () else preservation e TBool

let if_cond_lift
  (tau: ty)
  (e2 e3: typed_l_exp tau)
    : stepping_agnostic_lift TBool tau
  =
  Classical.forall_intro (if_cond_lift_is_stepping_agnostic tau e2 e3);
  if_cond_lift' tau e2 e3


let app_f_lift'
  (tau_arg tau: ty)
  (e2: typed_l_exp tau_arg)
    : stepping_context (TArrow tau_arg tau) tau
  =
  fun e1 -> EApp e1 e2 tau_arg

let app_f_lift_is_stepping_agnostic
  (tau_arg tau: ty)
  (e2: typed_l_exp tau_arg)
  (e: typed_l_exp (TArrow tau_arg tau))
    : Lemma
      (requires (True))
      (ensures (
        step_lift_commute_non_value (TArrow tau_arg tau) tau (app_f_lift' tau_arg tau e2) e))
  =
  progress e  (TArrow tau_arg tau);
  if is_value e then () else preservation e  (TArrow tau_arg tau)

let app_f_lift
  (tau_arg tau: ty)
  (e2: typed_l_exp tau_arg)
    : stepping_agnostic_lift (TArrow tau_arg tau) tau
  =
  Classical.forall_intro (app_f_lift_is_stepping_agnostic tau_arg tau e2);
  app_f_lift' tau_arg tau e2

let app_arg_lift'
  (tau_arg tau: ty)
  (e1: l_value (TArrow tau_arg tau))
    : stepping_context tau_arg tau
  =
  fun e2 -> EApp e1 e2 tau_arg

let app_arg_lift_is_stepping_agnostic
  (tau_arg tau: ty)
  (e1: l_value (TArrow tau_arg tau){match e1 with ELit (LError _) -> False | _ -> True})
  (e2: typed_l_exp tau_arg)
    : Lemma
      (requires (True))
      (ensures (
        step_lift_commute_non_value tau_arg tau (app_arg_lift' tau_arg tau e1) e2))
  =
  progress e2 tau_arg;
  if is_value e2 then () else preservation e2 tau_arg

let app_arg_lift
  (tau_arg tau: ty)
  (e1: l_value (TArrow tau_arg tau){match e1 with ELit (LError _) -> False | _ -> True})
    : stepping_agnostic_lift tau_arg tau
  =
  Classical.forall_intro (app_arg_lift_is_stepping_agnostic tau_arg tau e1);
  app_arg_lift' tau_arg tau e1

#push-options "--fuel 9 --ifuel 2 --z3rlimit 30"
let exceptions_head_lift'
  (tau: ty)
  (tl: list exp{typing_list empty tl (TArrow TUnit tau)})
  (acc: typed_l_exp (TOption tau))
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))
  : stepping_context tau tau
  =
  fun (hd: typed_l_exp tau) ->
    typ_process_exceptions_f empty tau;
    typing_empty_can_be_extended acc (TOption tau) (extend empty (TOption tau));
    typing_empty_can_be_extended acc (TOption tau)
      (extend (extend empty (TOption tau)) tau);
    EMatchOption
    (EFoldLeft
      (process_exceptions_f tau)
      (EApp
        (EAbs (TOption tau) (
          EMatchOption acc tau
            (EVar 0)
            (EAbs tau (
              EMatchOption (EVar 1) tau
                acc
                (EAbs tau (ELit (LError ConflictError)))
            ))
         ))
         (ECatchEmptyError
           (ESome hd) ENone)
         (TOption tau)
      )
      (TOption tau)
      (EList tl) (TArrow TUnit tau))
    tau
    (EIf
      just cons
      (ELit (LError EmptyError)))
    (EAbs tau (EVar 0))
#pop-options

let exceptions_head_lift_is_stepping_agnostic
  (tau: ty)
  (tl: list exp{typing_list empty tl (TArrow TUnit tau)})
  (acc: typed_l_exp (TOption tau))
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))
  (hd: typed_l_exp tau)
    : Lemma (step_lift_commute_non_value tau tau (exceptions_head_lift' tau tl acc just cons) hd)
  =
  progress hd tau;
  if is_value hd then () else begin
    preservation hd tau;
    assert_norm(step (exceptions_head_lift' tau tl acc just cons hd) == Some
      (exceptions_head_lift' tau tl acc just cons (Some?.v (step hd))))
  end

let exceptions_head_lift
  (tau: ty)
  (tl: list exp{typing_list empty tl (TArrow TUnit tau)})
  (acc: typed_l_exp (TOption tau))
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))
  : stepping_agnostic_lift tau tau
  =
  Classical.forall_intro (exceptions_head_lift_is_stepping_agnostic tau tl acc just cons);
  exceptions_head_lift' tau tl acc just cons

#push-options "--fuel 3 --ifuel 0"
let exceptions_init_lift'
  (tau: ty)
  (tl: list exp{typing_list empty tl (TArrow TUnit tau)})
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))
  : stepping_context (TOption tau) tau
  =
  fun (init: typed_l_exp (TOption tau)) ->
    typ_process_exceptions_f empty tau;
    EMatchOption
    (EFoldLeft
      (process_exceptions_f tau)
      init
      (TOption tau)
      (EList tl) (TArrow TUnit tau))
    tau
    (EIf
      just cons
      (ELit (LError EmptyError)))
    (EAbs tau (EVar 0))
#pop-options

let exceptions_init_lift_is_stepping_agnostic
  (tau: ty)
  (tl: list exp{typing_list empty tl (TArrow TUnit tau)})
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))
  (init: typed_l_exp (TOption tau))
    : Lemma (
      step_lift_commute_non_value (TOption tau) tau (exceptions_init_lift' tau tl just cons) init)
  =
  progress init (TOption tau);
  if is_value init then () else begin
    preservation init (TOption tau);
    assert_norm(step (exceptions_init_lift' tau tl just cons init) == Some
      (exceptions_init_lift' tau tl just cons (Some?.v (step init))))
  end

let exceptions_init_lift
  (tau: ty)
  (tl: list exp{typing_list empty tl (TArrow TUnit tau)})
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))
  : stepping_agnostic_lift (TOption tau) tau
  =
  Classical.forall_intro (exceptions_init_lift_is_stepping_agnostic tau tl just cons);
  exceptions_init_lift' tau tl just cons


#push-options "--fuel 7 --ifuel 2 --z3rlimit 50"
let lift_multiple_l_steps_exceptions_head
  (tau: ty)
  (tl: list exp{typing_list empty tl (TArrow TUnit tau) /\ is_value_list tl})
  (acc: typed_l_exp (TOption tau))
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))
  (n_hd: nat)
  (hd: typed_l_exp tau)
  (final_hd: typed_l_exp tau)
    : Lemma
      (requires (take_l_steps tau hd n_hd == Some final_hd /\ is_value acc))
      (ensures (
        build_default_translation_typing
          ((EThunk hd)::tl) acc just cons tau empty;
        take_l_steps tau
          (build_default_translation ((EThunk hd)::tl) acc just cons tau)
          (n_hd + 4) ==
            Some (exceptions_head_lift tau tl acc just cons final_hd)))
  =
  build_default_translation_typing ((EThunk hd)::tl) acc just cons tau empty;
  typing_empty_can_be_extended acc (TOption tau) (extend empty (TOption tau));
  typing_empty_can_be_extended acc (TOption tau)
   (extend (extend empty (TOption tau)) tau);
  typ_process_exceptions_f empty tau;
  let init0 : typed_l_exp (TOption tau) = EApp
    (EApp (process_exceptions_f tau) acc (TOption tau))
    (EThunk hd) (TArrow TUnit tau)
  in
  let init3 : typed_l_exp (TOption tau) = EApp (EAbs (TOption tau) (
    EMatchOption acc tau (EVar 0) (EAbs tau (
      EMatchOption (EVar 1) tau acc (EAbs tau
        (ELit (LError ConflictError))
      )
    ))))
    (ECatchEmptyError (ESome hd) ENone) (TOption tau)
  in
  let acc_invariant (s: var_to_exp) : Lemma (subst s acc == acc) [SMTPat (subst s acc)] =
    well_typed_terms_invariant_by_subst s acc (TOption tau)
  in
  let hd_invariant (s: var_to_exp) : Lemma (subst s hd == hd)
    [SMTPat (subst s hd)] =
    well_typed_terms_invariant_by_subst s hd tau
  in
  assume(take_l_steps (TOption tau) init0 3 == Some init3);
  (* F* cannot prove these rather trivial substitutions automatically, might have to do it
    manually. This proof will use well_typed_terms_invariant_by_subst *)
  let default_translation0 : typed_l_exp tau =
    build_default_translation ((EThunk hd)::tl) acc just cons tau
  in
  let default_translation1 : typed_l_exp tau = EMatchOption
    (EFoldLeft
      (process_exceptions_f tau)
      init0 (TOption tau)
      (EList tl) (TArrow TUnit tau))
    tau
    (EIf
      just cons
      (ELit (LError EmptyError)))
    (EAbs tau (EVar 0))
  in
  assert(take_l_steps tau default_translation0 1 == Some default_translation1);
  assert(default_translation1 == exceptions_init_lift tau tl just cons init0);
  lift_multiple_l_steps (TOption tau) tau init0 init3 3
    (exceptions_init_lift tau tl just cons);
  take_l_steps_transitive tau default_translation0 default_translation1 1 3;
  assert(take_l_steps tau default_translation0 4 ==
    Some (exceptions_init_lift tau tl just cons init3));
  assert(exceptions_init_lift tau tl just cons init3 ==
    exceptions_head_lift tau tl acc just cons hd);
  lift_multiple_l_steps tau tau hd final_hd n_hd (exceptions_head_lift tau tl acc just cons);
  take_l_steps_transitive tau default_translation0
    (exceptions_head_lift tau tl acc just cons hd) 4 n_hd

(*** Various lambda calculus steps *)

let process_exceptions_applied
  (tau: ty)
  (acc: typed_l_exp (TOption tau))
  (hd: typed_l_exp tau)
    : Tot (typed_l_exp (TOption tau))
  =
  typ_process_exceptions_f empty tau;
  typing_empty_can_be_extended hd tau (extend empty TUnit);
  EApp
   (EApp (process_exceptions_f tau) acc (TOption tau))
   (EThunk hd) (TArrow TUnit tau)


#push-options "--fuel 7 --ifuel 2"
let process_exceptions_applied_stepped
  (tau: ty)
  (acc: typed_l_exp (TOption tau))
  (hd: typed_l_exp tau)
    : Tot (typed_l_exp (TOption tau))
  =
  typing_empty_can_be_extended acc (TOption tau) (extend empty (TOption tau));
  typing_empty_can_be_extended acc (TOption tau)
   (extend (extend empty (TOption tau)) tau);
  EApp (EAbs (TOption tau) (
    EMatchOption acc tau (EVar 0) (EAbs tau (
      EMatchOption (EVar 1) tau acc (EAbs  tau
        (ELit (LError ConflictError))
      )
    ))))
    (ECatchEmptyError (ESome hd) ENone) (TOption tau)
#pop-options

#push-options "--fuel 9 --ifuel 2 --z3rlimit 80"
let process_exceptions_applied_stepping
  (tau: ty)
  (acc: typed_l_exp (TOption tau){is_value acc /\ not (is_error acc)})
  (hd: typed_l_exp tau)
    : Lemma (take_l_steps (TOption tau) (process_exceptions_applied tau acc hd) 3 ==
      Some (process_exceptions_applied_stepped tau acc hd))
  =
  let acc_invariant (s: var_to_exp) : Lemma (subst s acc == acc) [SMTPat (subst s acc)] =
    well_typed_terms_invariant_by_subst s acc (TOption tau)
  in
  [@inline_let]
  let inner_process_exceptions0 (hd: exp) = EApp
    (EAbs (TOption tau) (EMatchOption acc tau (EVar 0) (EAbs tau (
        EMatchOption (EVar 1) tau acc (EAbs tau (ELit (LError ConflictError)))))))
    (ECatchEmptyError (ESome (EApp hd (ELit LUnit) TUnit)) ENone)
    (TOption tau)
  in
  let e1 = EApp
    (EAbs (TArrow TUnit tau) (inner_process_exceptions0 (EVar 0)))
    (EThunk hd) (TArrow TUnit tau)
  in
  let e2 = inner_process_exceptions0 (EThunk hd) in
  assert_norm(step (process_exceptions_applied tau acc hd) == Some e1);
  assert(step e1 == Some e2);
  let hd0 = (ECatchEmptyError (ESome (EApp (EThunk hd) (ELit LUnit) TUnit)) ENone) in
  let hd1 = (ECatchEmptyError (ESome hd) ENone) in
  assert(step hd0 == Some hd1);
  [@inline_let]
  let inner_process_exceptions1 = EApp
    (EAbs (TOption tau) (EMatchOption acc tau (EVar 0) (EAbs tau (
        EMatchOption (EVar 1) tau acc (EAbs tau (ELit (LError ConflictError)))))))
    (ECatchEmptyError (ESome hd) ENone)
    (TOption tau)
  in
  let e3 = inner_process_exceptions1 in
  assert_norm(step e2 == Some e3);
  assert(e3 == process_exceptions_applied_stepped tau acc hd);
  preservation (process_exceptions_applied tau acc hd) (TOption tau);
  preservation e1 (TOption tau);
  preservation e2 (TOption tau);
  take_l_steps_transitive (TOption tau) (process_exceptions_applied tau acc hd) e1 1 1;
  take_l_steps_transitive (TOption tau) (process_exceptions_applied tau acc hd) e2 2 1
#pop-options

#push-options "--fuel 2 --ifuel 1 --z3rlimit 40"
let exceptions_head_lift_steps_to_error
  (tau: ty)
  (tl: list exp{is_value_list tl /\ typing_list empty tl (TArrow TUnit tau)})
  (acc: typed_l_exp (TOption tau){is_value acc})
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))
    : Lemma (take_l_steps tau
      (exceptions_head_lift tau tl acc just cons (ELit (LError ConflictError))) 5 ==
        Some (ELit (LError ConflictError)))
  =
  let e = exceptions_head_lift tau tl acc just cons (ELit (LError ConflictError)) in
  let e_plus_3 : typed_l_exp tau =
    exceptions_init_lift tau tl just cons (ELit (LError ConflictError))
  in
  let open FStar.Tactics in
  assert(take_l_steps tau e 3 == Some e_plus_3) by begin
    compute ();
    smt ()
  end;
  let e_plus_4 : typed_l_exp tau = EMatchOption
    (ELit (LError ConflictError))
    tau
    (EIf
      just cons
      (ELit (LError EmptyError)))
    (EAbs tau (EVar 0))
  in
  assert(step e_plus_3 == Some e_plus_4) by begin
    compute ();
    smt ()
  end;
  preservation e_plus_3 tau;
  assert(Some e_plus_4 == take_l_steps tau e_plus_3 1);
  assert(step e_plus_4 ==  Some (ELit (LError ConflictError)));
  assert(take_l_steps tau e_plus_4 1 == Some (ELit (LError ConflictError)));
  take_l_steps_transitive tau e e_plus_3 3 1;
  take_l_steps_transitive tau e e_plus_4 4 1
#pop-options

#push-options "--fuel 4 --ifuel 1 --z3rlimit 20"
let exception_init_lift_conflict_error
  (tau: ty)
  (tl: list exp{is_value_list tl /\ typing_list empty tl (TArrow TUnit tau)})
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))
    : Lemma (
      take_l_steps tau (exceptions_init_lift tau tl just cons (ELit (LError ConflictError))) 2 ==
        Some (ELit (LError ConflictError)))
  =
  let c_err = ELit (LError ConflictError) in
  let e0 = exceptions_init_lift tau tl just cons (ELit (LError ConflictError)) in
  let e1 = EMatchOption c_err tau (EIf just cons (ELit (LError EmptyError))) (EAbs tau (EVar 0)) in
  assert(step e0 == Some e1);
  assert(step e1 == Some c_err);
  preservation e0 tau;
  preservation e1 tau;
  take_l_steps_transitive tau e0 e1 1 1
#pop-options

let is_option_value_non_error (g: env) (e: exp) (tau: ty)
    : Lemma (requires (is_value e /\ not (is_error e) /\ (typing g e (TOption tau))))
      (ensures
        (match e with
          | ESome _ -> True
          | ENone -> True
          | _ -> False)) = ()

#push-options "--fuel 8 --ifuel 1 --z3rlimit 80"
let step_exceptions_head_value_error
  (tau: ty)
  (tl: list exp{is_value_list tl /\ typing_list empty tl (TArrow TUnit tau)})
  (acc: (typed_l_exp (TOption tau)))
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))
  (hd_err: err)
    : Pure (typed_l_exp (TOption tau) & nat)
      (requires (is_value acc /\ not (is_error acc)))
      (ensures (fun (new_acc, n) ->
        is_value new_acc /\
        take_l_steps tau (exceptions_head_lift tau tl acc just cons (ELit (LError hd_err))) n ==
          Some (exceptions_init_lift tau tl just cons new_acc)
      ))
  =
  typ_process_exceptions_f empty tau;
  typing_empty_can_be_extended acc (TOption tau) (extend empty (TOption tau));
  typing_empty_can_be_extended acc (TOption tau)
    (extend (extend empty (TOption tau)) tau);
  let hd = ELit (LError hd_err) in
  let init0 : typed_l_exp (TOption tau) = EApp (EAbs (TOption tau) (
    EMatchOption acc tau (EVar 0) (EAbs tau (EMatchOption (EVar 1) tau acc (EAbs tau (
      ELit (LError ConflictError))))))) (ECatchEmptyError (ESome hd) ENone) (TOption tau)
  in
  let match_arg0  =
    EFoldLeft (process_exceptions_f tau) init0 (TOption tau) (EList tl) (TArrow TUnit tau)
  in
  let c_err = ELit (LError ConflictError) in
  let match_none0 = EIf just cons (ELit (LError EmptyError)) in
  let match_some0 = EAbs tau (EVar 0) in
  assert(exceptions_head_lift tau tl acc just cons hd ==
    EMatchOption match_arg0 tau match_none0 match_some0);
  assert(exceptions_head_lift tau tl acc just cons hd ==
    exceptions_init_lift tau tl just cons init0);
  let acc_invariant (s: var_to_exp) : Lemma (subst s acc == acc) [SMTPat (subst s acc)] =
    well_typed_terms_invariant_by_subst s acc (TOption tau)
  in
  let init1 = EApp (EAbs (TOption tau) (
    EMatchOption acc tau (EVar 0) (EAbs tau (EMatchOption (EVar 1) tau acc (EAbs tau (
      ELit (LError ConflictError))))))) (ECatchEmptyError hd ENone) (TOption tau)
  in
  assert(step init0 == Some init1);
  match hd_err with
  | ConflictError ->
    let init2 = EApp (EAbs (TOption tau) (
      EMatchOption acc tau (EVar 0) (EAbs tau (EMatchOption (EVar 1) tau acc (EAbs tau (
        ELit (LError ConflictError))))))) hd (TOption tau)
    in
    assert(step init1 == Some init2); assert(step init2 == Some c_err);
    preservation init0 (TOption tau); preservation init1 (TOption tau);
    preservation init2 (TOption tau);
    take_l_steps_transitive (TOption tau) init0 init1 1 1;
    take_l_steps_transitive (TOption tau) init0 init2 2 1;
    lift_multiple_l_steps (TOption tau) tau init0 c_err 3
      (exceptions_init_lift tau tl just cons);
    exception_init_lift_conflict_error tau tl just cons;
    c_err, 3
  | EmptyError ->
    let init2 = EApp (EAbs (TOption tau) (
      EMatchOption acc tau (EVar 0) (EAbs tau (EMatchOption (EVar 1) tau acc (EAbs tau (
        ELit (LError ConflictError))))))) ENone (TOption tau)
    in
    assert(step init1 == Some init2);
    let init3 = EMatchOption acc tau ENone (EAbs tau (EMatchOption ENone tau acc (EAbs tau (
      ELit (LError ConflictError)))))
    in
    assert(step init2 == Some init3);
    is_option_value_non_error empty acc tau;
    match acc with
    | ENone ->
      assert(step init3 == Some ENone);
      preservation init0 (TOption tau); preservation init1 (TOption tau);
      preservation init2 (TOption tau); preservation init3 (TOption tau);
      take_l_steps_transitive (TOption tau) init0 init1 1 1;
      take_l_steps_transitive (TOption tau) init0 init2 2 1;
      take_l_steps_transitive (TOption tau) init0 init3 3 1;
      lift_multiple_l_steps (TOption tau) tau init0 ENone 4
        (exceptions_init_lift tau tl just cons);
      ENone, 4
    | ESome acc_inner ->
       let init4 = (EApp (EAbs tau (EMatchOption ENone tau acc (EAbs tau (
         ELit (LError ConflictError))))) acc_inner tau)
       in
       assert(step init3 == Some init4);
       let init5 = EMatchOption ENone tau acc (EAbs tau (
         ELit (LError ConflictError)))
       in
       assert(step init4 == Some init5);
       assert(step init5 == Some acc);
       preservation init0 (TOption tau); preservation init1 (TOption tau);
       preservation init2 (TOption tau); preservation init3 (TOption tau);
       preservation init4 (TOption tau); preservation init5 (TOption tau);
       take_l_steps_transitive (TOption tau) init0 init1 1 1;
       take_l_steps_transitive (TOption tau) init0 init2 2 1;
       take_l_steps_transitive (TOption tau) init0 init3 3 1;
       take_l_steps_transitive (TOption tau) init0 init4 4 1;
       take_l_steps_transitive (TOption tau) init0 init5 5 1;
       lift_multiple_l_steps (TOption tau) tau init0 acc 6
        (exceptions_init_lift tau tl just cons);
       acc, 6
#pop-options

#push-options "--fuel 8 --ifuel 1 --z3rlimit 90"
let step_exceptions_head_value_non_error
  (tau: ty)
  (tl: list exp{is_value_list tl /\ typing_list empty tl (TArrow TUnit tau)})
  (acc: (typed_l_exp (TOption tau)))
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))
  (hd: typed_l_exp tau)
    : Pure (typed_l_exp (TOption tau) & nat)
      (requires (is_value hd /\ not (is_error hd) /\ is_value acc /\ not (is_error acc)))
      (ensures (fun (new_acc, n) ->
        is_value new_acc /\
        take_l_steps tau (exceptions_head_lift tau tl acc just cons hd) n ==
          Some (exceptions_init_lift tau tl just cons new_acc)
      ))
  =
  typ_process_exceptions_f empty tau;
  typing_empty_can_be_extended acc (TOption tau) (extend empty (TOption tau));
  typing_empty_can_be_extended acc (TOption tau)
    (extend (extend empty (TOption tau)) tau);
  let init0 : typed_l_exp (TOption tau) = EApp (EAbs (TOption tau) (
    EMatchOption acc tau (EVar 0) (EAbs tau (EMatchOption (EVar 1) tau acc (EAbs tau (
      ELit (LError ConflictError))))))) (ECatchEmptyError (ESome hd) ENone) (TOption tau)
  in
  let match_arg0  =
    EFoldLeft (process_exceptions_f tau) init0 (TOption tau) (EList tl) (TArrow TUnit tau)
  in
  let c_err = ELit (LError ConflictError) in
  let match_none0 = EIf just cons (ELit (LError EmptyError)) in
  let match_some0 = EAbs tau (EVar 0) in
  assert(exceptions_head_lift tau tl acc just cons hd ==
    EMatchOption match_arg0 tau match_none0 match_some0);
  assert(exceptions_head_lift tau tl acc just cons hd ==
    exceptions_init_lift tau tl just cons init0);
  let acc_invariant (s: var_to_exp) : Lemma (subst s acc == acc) [SMTPat (subst s acc)] =
    well_typed_terms_invariant_by_subst s acc (TOption tau)
  in
  let some_hd_invariant (s: var_to_exp) : Lemma (subst s (ESome hd) == ESome hd)
      [SMTPat (subst s (ESome hd))]
    =
    well_typed_terms_invariant_by_subst s (ESome hd) (TOption tau)
  in
  let init1 = EApp (EAbs (TOption tau) (
    EMatchOption acc tau (EVar 0) (EAbs tau (EMatchOption (EVar 1) tau acc (EAbs tau (
      ELit (LError ConflictError))))))) (ESome hd) (TOption tau)
  in
  assert(step init0 == Some init1);
  let init2 = EMatchOption acc tau (ESome hd) (EAbs tau (EMatchOption (ESome hd) tau acc (EAbs tau (
    ELit (LError ConflictError)))))
  in
  assert(step init1 == Some init2);
  is_option_value_non_error empty acc tau;
  match acc with
  | ENone ->
    assert(step init2 == Some (ESome hd));
    preservation init0 (TOption tau); preservation init1 (TOption tau);
    preservation init2 (TOption tau);
    take_l_steps_transitive (TOption tau) init0 init1 1 1;
    take_l_steps_transitive (TOption tau) init0 init2 2 1;
    lift_multiple_l_steps (TOption tau) tau init0 (ESome hd) 3
      (exceptions_init_lift tau tl just cons);
    ESome hd, 3
  | ESome acc_inner ->
    let init3 = EApp (EAbs tau (EMatchOption (ESome hd) tau acc
      (EAbs tau (ELit (LError ConflictError))))) acc_inner tau
    in
    assert(step init2 == Some init3);
    let init4 = EMatchOption (ESome hd) tau acc (EAbs tau (ELit (LError ConflictError))) in
    assert(step init3 == Some init4);
    let init5 = EApp (EAbs tau (ELit (LError ConflictError))) hd tau in
    assert(step init4 == Some init5);
    let c_err = ELit (LError ConflictError) in
    assert(step init5 == Some c_err);
    preservation init0 (TOption tau); preservation init1 (TOption tau);
    preservation init2 (TOption tau); preservation init3 (TOption tau);
    preservation init4 (TOption tau); preservation init5 (TOption tau);
    take_l_steps_transitive (TOption tau) init0 init1 1 1;
    take_l_steps_transitive (TOption tau) init0 init2 2 1;
    take_l_steps_transitive (TOption tau) init0 init3 3 1;
    take_l_steps_transitive (TOption tau) init0 init4 4 1;
    take_l_steps_transitive (TOption tau) init0 init5 5 1;
    lift_multiple_l_steps (TOption tau) tau init0 c_err 6
     (exceptions_init_lift tau tl just cons);
    c_err, 6
#pop-options

let step_exceptions_head_value
  (tau: ty)
  (tl: list exp{is_value_list tl /\ typing_list empty tl (TArrow TUnit tau)})
  (acc: (typed_l_exp (TOption tau)))
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))
  (hd: (typed_l_exp tau))
    : Pure (typed_l_exp (TOption tau) & nat)
      (requires (is_value hd /\ is_value acc /\ not (is_error acc)))
      (ensures (fun (new_acc, n) ->
        is_value new_acc /\
        take_l_steps tau (exceptions_head_lift tau tl acc just cons hd) n ==
          Some (exceptions_init_lift tau tl just cons new_acc)
      ))
  =
  match hd with
  | ELit (LError hd_err) -> step_exceptions_head_value_error tau tl acc just cons hd_err
  | _ -> step_exceptions_head_value_non_error tau tl acc just cons hd

let step_exceptions_head_value_same_acc_result
  (tau: ty)
  (tl: list exp{is_value_list tl /\ typing_list empty tl (TArrow TUnit tau)})
  (tl': list exp{is_value_list tl' /\ typing_list empty tl' (TArrow TUnit tau)})
  (acc: typed_l_exp (TOption tau){is_value acc /\ not (is_error acc)})
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))
  (hd: (typed_l_exp tau){is_value hd})
    : Lemma (
      let new_acc, _ = step_exceptions_head_value tau tl acc just cons hd in
      let new_acc', _ = step_exceptions_head_value tau tl' acc just cons hd in
      new_acc == new_acc'
    )
  =
  admit()

let step_exceptions_head_value_go_through
  (tau: ty)
  (tl: list exp{is_value_list tl /\ typing_list empty tl (TArrow TUnit tau)})
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))

    : Lemma (
      let new_acc, _ =
        step_exceptions_head_value tau tl ENone just cons (ELit (LError EmptyError)) in
      new_acc = ENone
    )
  =
  admit()

let step_exceptions_empty_conflict_error
  (tau: ty)
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))
    : Pure nat
      (requires (True))
      (ensures (fun n ->
      build_default_translation_typing [] (ELit (LError ConflictError)) just cons tau empty;
        take_l_steps tau
          (build_default_translation [] (ELit (LError ConflictError)) just cons tau) n ==
            Some (ELit (LError ConflictError))))
  =
  build_default_translation_typing [] (ELit (LError ConflictError)) just cons tau empty;
  assert_norm(take_l_steps tau
          (build_default_translation [] (ELit (LError ConflictError)) just cons tau) 2 ==
            Some (ELit (LError ConflictError)));
  2

#push-options "--fuel 4 --ifuel 1 --z3rlimit 40"
let step_exceptions_empty_some_acc
  (tau: ty)
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))
  (acc: (typed_l_exp tau))
    : Pure nat
      (requires (is_value acc /\ not (is_error acc)))
      (ensures (fun n ->
      build_default_translation_typing [] (ESome acc) just cons tau empty;
        take_l_steps tau
          (build_default_translation [] (ESome acc) just cons tau) n ==
            Some acc))
  =
  let one_step : typed_l_exp tau =
    EMatchOption (ESome acc) tau
              (EIf just cons (ELit (LError (EmptyError))))
              (EAbs tau (EVar 0))
  in
  build_default_translation_typing [] (ESome acc) just cons tau empty;
  assert(take_l_steps tau
          (build_default_translation [] (ESome acc) just cons tau) 1 ==
            Some one_step);
  let two_step : typed_l_exp tau =
    EApp (EAbs tau (EVar 0)) acc tau
  in
  assert(take_l_steps tau one_step 1 == Some two_step);
  assert(take_l_steps tau two_step 1 == Some acc);
  take_l_steps_transitive tau (build_default_translation [] (ESome acc) just cons tau) one_step 1 1;
  take_l_steps_transitive tau (build_default_translation [] (ESome acc) just cons tau) two_step 2 1;
  3
#pop-options

#push-options "--fuel 4 --ifuel 1 --z3rlimit 40"
let step_exceptions_empty_none
  (tau: ty)
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))
    : Pure nat
      (requires (True))
      (ensures (fun n ->
      build_default_translation_typing [] ENone just cons tau empty;
        take_l_steps tau
          (build_default_translation [] ENone just cons tau) n ==
            Some (EIf just cons (ELit (LError (EmptyError))))))
  =
  let one_step : typed_l_exp tau =
    EMatchOption ENone tau
              (EIf just cons (ELit (LError (EmptyError))))
              (EAbs tau (EVar 0))
  in
  build_default_translation_typing [] ENone just cons tau empty;
  assert(take_l_steps tau
          (build_default_translation [] ENone just cons tau) 1 ==
            Some one_step);
  let two_step : typed_l_exp tau =
    (EIf just cons (ELit (LError (EmptyError))))
  in
  assert(take_l_steps tau one_step 1 == Some two_step);
  take_l_steps_transitive tau (build_default_translation [] ENone just cons tau) one_step 1 1;
  2
#pop-options


#push-options "--fuel 4 --ifuel 1 --z3rlimit 40"
let step_exceptions_cons_conflict_error
  (tau: ty)
  (just: (typed_l_exp TBool))
  (cons: (typed_l_exp tau))
  (hd: typed_l_exp tau)
  (tl: list exp)
    : Pure nat
      (requires (is_value hd /\ is_value_list tl /\ typing_list empty tl (TArrow TUnit tau)))
      (ensures (fun n ->
      build_default_translation_typing
        ((EThunk hd)::tl) (ELit (LError ConflictError)) just cons tau empty;
      take_l_steps tau
        (build_default_translation ((EThunk hd)::tl) (ELit (LError ConflictError)) just cons tau) n
          == Some (ELit (LError ConflictError))))
  =
  let l_err: typed_l_exp (TOption tau) = (ELit (LError ConflictError)) in
  build_default_translation_typing
    ((EThunk hd)::tl)
    (ELit (LError ConflictError)) just cons tau empty;
  let one_step : typed_l_exp tau =
    EMatchOption l_err tau
              (EIf just cons (ELit (LError (EmptyError))))
              (EAbs tau (EVar 0))
  in
  assert(take_l_steps tau
    (build_default_translation ((EThunk hd)::tl) (ELit (LError ConflictError)) just cons tau) 1 ==
      Some one_step);
  let l_err': typed_l_exp tau = (ELit (LError ConflictError)) in
  assert(take_l_steps tau one_step 1 == Some l_err');
  take_l_steps_transitive tau
     (build_default_translation ((EThunk hd)::tl) (ELit (LError ConflictError)) just cons tau)
     one_step 1 1;
  2
#pop-options