mirror of
https://github.com/CatalaLang/catala.git
synced 2024-09-20 00:41:05 +03:00
Proof went until the end, now havee to remove admits
This commit is contained in:
parent
b2d9407c2b
commit
1071f3232d
@ -89,6 +89,11 @@ type empty_count_result =
|
|||||||
| OneNonEmpty of exp
|
| OneNonEmpty of exp
|
||||||
| Conflict
|
| Conflict
|
||||||
|
|
||||||
|
type exceptions_count_result =
|
||||||
|
| NoStep
|
||||||
|
| IllFormed
|
||||||
|
| SomeStep of exp
|
||||||
|
|
||||||
let rec empty_count (acc: empty_count_result) (l: list exp) : Tot empty_count_result (decreases l) =
|
let rec empty_count (acc: empty_count_result) (l: list exp) : Tot empty_count_result (decreases l) =
|
||||||
match l with
|
match l with
|
||||||
| [] -> acc
|
| [] -> acc
|
||||||
@ -178,14 +183,17 @@ and step_exceptions
|
|||||||
(just: exp{just << e})
|
(just: exp{just << e})
|
||||||
(cons: exp{cons << e})
|
(cons: exp{cons << e})
|
||||||
(tau: ty)
|
(tau: ty)
|
||||||
: Tot (option exp) (decreases %[ e; 3 ]) =
|
: Tot exceptions_count_result (decreases %[ e; 3 ]) =
|
||||||
if List.Tot.for_all (fun except -> is_value except) exceptions
|
if List.Tot.for_all is_value exceptions
|
||||||
then
|
then
|
||||||
match empty_count AllEmpty exceptions with
|
match empty_count AllEmpty exceptions with
|
||||||
| AllEmpty -> None
|
| AllEmpty -> NoStep
|
||||||
| OneNonEmpty e' -> Some e' (* D-DefaultOneException *)
|
| OneNonEmpty e' -> SomeStep e' (* D-DefaultOneException *)
|
||||||
| Conflict -> Some (ELit LConflictError) (* D-DefaultExceptionConflict *)
|
| Conflict -> SomeStep (ELit LConflictError) (* D-DefaultExceptionConflict *)
|
||||||
else step_exceptions_left_to_right e exceptions just cons tau
|
else
|
||||||
|
match step_exceptions_left_to_right e exceptions just cons tau with
|
||||||
|
| None -> IllFormed
|
||||||
|
| Some e' -> SomeStep e'
|
||||||
|
|
||||||
and step_default
|
and step_default
|
||||||
(e: exp)
|
(e: exp)
|
||||||
@ -195,22 +203,16 @@ and step_default
|
|||||||
(tau: ty)
|
(tau: ty)
|
||||||
: Tot (option exp) (decreases %[ e; 4 ]) =
|
: Tot (option exp) (decreases %[ e; 4 ]) =
|
||||||
match step_exceptions e exceptions just cons tau with
|
match step_exceptions e exceptions just cons tau with
|
||||||
| Some e' -> Some e'
|
| IllFormed -> None
|
||||||
| None ->
|
| SomeStep e' -> Some e'
|
||||||
|
| NoStep ->
|
||||||
if is_value just then
|
if is_value just then
|
||||||
match just with
|
match just with
|
||||||
| ELit LConflictError -> Some c_err (* D-ContextConflictError *)
|
| ELit LConflictError -> Some c_err (* D-ContextConflictError *)
|
||||||
| ELit LEmptyError -> Some e_err (* D-ContextEmptyError *)
|
| ELit LEmptyError -> Some e_err (* D-ContextEmptyError *)
|
||||||
| _ ->
|
| _ ->
|
||||||
match just with
|
match just with
|
||||||
| ELit LTrue ->
|
| ELit LTrue -> Some cons (* D-DefaultTrueNoExceptions*)
|
||||||
if is_value cons
|
|
||||||
then Some cons
|
|
||||||
else
|
|
||||||
(match (step cons) with
|
|
||||||
| Some (ELit LConflictError) -> Some c_err (* D-ContextConflictError *)
|
|
||||||
| Some cons' -> Some (EDefault exceptions just cons' tau) (* D-DefaultTrueNoExceptions*)
|
|
||||||
| None -> None)
|
|
||||||
| ELit LFalse -> Some e_err (* D-DefaultFalseNoExceptions *)
|
| ELit LFalse -> Some e_err (* D-DefaultFalseNoExceptions *)
|
||||||
| _ -> None
|
| _ -> None
|
||||||
else
|
else
|
||||||
@ -282,7 +284,7 @@ let typing_conserved_by_list_reduction (g: env) (subs: list exp) (tau: ty)
|
|||||||
|
|
||||||
(**** Progress theorem *)
|
(**** Progress theorem *)
|
||||||
|
|
||||||
#push-options "--fuel 2 --ifuel 1"
|
#push-options "--fuel 2 --ifuel 1 --z3rlimit 20"
|
||||||
let rec progress (e: exp) (tau: ty)
|
let rec progress (e: exp) (tau: ty)
|
||||||
: Lemma (requires (typing empty e tau))
|
: Lemma (requires (typing empty e tau))
|
||||||
(ensures (is_value e \/ (Some? (step e))))
|
(ensures (is_value e \/ (Some? (step e))))
|
||||||
@ -305,14 +307,17 @@ and progress_default
|
|||||||
(cons: exp{cons << e})
|
(cons: exp{cons << e})
|
||||||
(tau: ty)
|
(tau: ty)
|
||||||
: Lemma (requires (
|
: Lemma (requires (
|
||||||
~(is_value e) /\
|
|
||||||
e == EDefault exceptions just cons tau /\ (typing empty e tau)
|
e == EDefault exceptions just cons tau /\ (typing empty e tau)
|
||||||
))
|
))
|
||||||
(ensures (Some? (step_default e exceptions just cons tau)))
|
(ensures (Some? (step_default e exceptions just cons tau)))
|
||||||
(decreases %[ e; 2 ]) =
|
(decreases %[ e; 2 ]) =
|
||||||
match step_exceptions e exceptions just cons tau with
|
match step_exceptions e exceptions just cons tau with
|
||||||
| Some _ -> ()
|
| IllFormed ->
|
||||||
| None ->
|
assert(step_exceptions_left_to_right e exceptions just cons tau == None);
|
||||||
|
assert(~(List.Tot.for_all is_value exceptions));
|
||||||
|
progress_default_exceptions e exceptions just cons tau
|
||||||
|
| SomeStep _ -> ()
|
||||||
|
| NoStep ->
|
||||||
if is_value just then
|
if is_value just then
|
||||||
(is_bool_value_cannot_be_abs empty just;
|
(is_bool_value_cannot_be_abs empty just;
|
||||||
match just, cons with
|
match just, cons with
|
||||||
@ -322,6 +327,27 @@ and progress_default
|
|||||||
| ELit LEmptyError, _ -> ()
|
| ELit LEmptyError, _ -> ()
|
||||||
| ELit LConflictError, _ -> ())
|
| ELit LConflictError, _ -> ())
|
||||||
else progress just TBool
|
else progress just TBool
|
||||||
|
and progress_default_exceptions
|
||||||
|
(e: exp)
|
||||||
|
(exceptions: list exp {exceptions << e})
|
||||||
|
(just: exp{just << e})
|
||||||
|
(cons: exp{cons << e})
|
||||||
|
(tau: ty)
|
||||||
|
: Lemma (requires (
|
||||||
|
typing_list empty exceptions tau /\
|
||||||
|
step_exceptions_left_to_right e exceptions just cons tau == None /\
|
||||||
|
~(List.Tot.for_all is_value exceptions)
|
||||||
|
))
|
||||||
|
(ensures (False))
|
||||||
|
(decreases %[ e; 1; exceptions ])
|
||||||
|
=
|
||||||
|
match exceptions with
|
||||||
|
| [] -> ()
|
||||||
|
| hd::tl ->
|
||||||
|
progress hd tau;
|
||||||
|
if is_value hd then begin
|
||||||
|
progress_default_exceptions e tl just cons tau
|
||||||
|
end else ()
|
||||||
#pop-options
|
#pop-options
|
||||||
|
|
||||||
(*** Preservation *)
|
(*** Preservation *)
|
||||||
@ -504,7 +530,7 @@ let rec preservation (e: exp) (tau: ty)
|
|||||||
match empty_count AllEmpty exceptions with
|
match empty_count AllEmpty exceptions with
|
||||||
| AllEmpty ->
|
| AllEmpty ->
|
||||||
begin if not (is_value just) then preservation just TBool else match just with
|
begin if not (is_value just) then preservation just TBool else match just with
|
||||||
| ELit LTrue -> if not (is_value cons) then preservation cons tau
|
| ELit LTrue -> ()
|
||||||
| _ -> ()
|
| _ -> ()
|
||||||
end
|
end
|
||||||
| OneNonEmpty e' -> empty_count_preserves_type AllEmpty exceptions empty tau
|
| OneNonEmpty e' -> empty_count_preserves_type AllEmpty exceptions empty tau
|
||||||
|
@ -810,14 +810,16 @@ let translation_correctness_exceptions_step
|
|||||||
Some? (D.step de) /\
|
Some? (D.step de) /\
|
||||||
de == D.EDefault dexceptions djust dcons dtau /\
|
de == D.EDefault dexceptions djust dcons dtau /\
|
||||||
D.typing D.empty de dtau /\
|
D.typing D.empty de dtau /\
|
||||||
D.step de == D.step_exceptions de dexceptions djust dcons dtau
|
(match D.step de, D.step_exceptions de dexceptions djust dcons dtau with
|
||||||
|
| Some de', D.SomeStep de'' -> de' == de''
|
||||||
|
| _ -> False)
|
||||||
))
|
))
|
||||||
(ensures (fun (n1, target_e, n2) ->
|
(ensures (fun (n1, target_e, n2) ->
|
||||||
translation_preserves_empty_typ de dtau;
|
translation_preserves_empty_typ de dtau;
|
||||||
let lexceptions = translate_exp_list dexceptions in
|
let lexceptions = translate_exp_list dexceptions in
|
||||||
let ljust = translate_exp djust in
|
let ljust = translate_exp djust in
|
||||||
let lcons = translate_exp dcons in
|
let lcons = translate_exp dcons in
|
||||||
let Some de' = D.step_exceptions de dexceptions djust dcons dtau in
|
let D.SomeStep de' = D.step_exceptions de dexceptions djust dcons dtau in
|
||||||
let le' = translate_exp de' in
|
let le' = translate_exp de' in
|
||||||
D.preservation de dtau;
|
D.preservation de dtau;
|
||||||
let ltau = translate_ty dtau in
|
let ltau = translate_ty dtau in
|
||||||
@ -835,7 +837,49 @@ let translation_correctness_exceptions_step
|
|||||||
end else
|
end else
|
||||||
translation_correctness_exceptions_left_to_right_step
|
translation_correctness_exceptions_left_to_right_step
|
||||||
de dexceptions djust dcons dtau L.ENone rec_lemma
|
de dexceptions djust dcons dtau L.ENone rec_lemma
|
||||||
|
#pop-options
|
||||||
|
|
||||||
|
let final_default_subexp
|
||||||
|
(tau: L.ty)
|
||||||
|
(just: typed_l_exp L.TBool) (cons: typed_l_exp tau)
|
||||||
|
: Tot (typed_l_exp tau)
|
||||||
|
=
|
||||||
|
L.EIf just cons (L.ELit (L.LError L.EmptyError))
|
||||||
|
|
||||||
|
#push-options "--fuel 2 --ifuel 1 --z3rlimit 150"
|
||||||
|
let translation_correctness_exceptions_no_exceptions_triggered
|
||||||
|
(de: D.exp)
|
||||||
|
(dexceptions: list D.exp {dexceptions << de})
|
||||||
|
(djust: D.exp{djust << de})
|
||||||
|
(dcons: D.exp{dcons << de})
|
||||||
|
(dtau: D.ty)
|
||||||
|
: Pure nat
|
||||||
|
(requires (
|
||||||
|
D.typing D.empty de dtau /\
|
||||||
|
D.typing_list D.empty dexceptions dtau /\
|
||||||
|
D.typing D.empty djust D.TBool /\
|
||||||
|
D.typing D.empty dcons dtau /\
|
||||||
|
List.Tot.for_all D.is_value dexceptions /\
|
||||||
|
(D.step de == D.step_default de dexceptions djust dcons dtau) /\
|
||||||
|
(D.step_exceptions de dexceptions djust dcons dtau == D.NoStep)
|
||||||
|
))
|
||||||
|
(ensures (fun n ->
|
||||||
|
translate_empty_is_empty ();
|
||||||
|
translation_preserves_typ_exceptions D.empty de dexceptions dtau;
|
||||||
|
translation_preserves_empty_typ djust D.TBool;
|
||||||
|
translation_preserves_empty_typ dcons dtau;
|
||||||
|
let lexceptions = translate_exp_list dexceptions in
|
||||||
|
let ljust = translate_exp djust in
|
||||||
|
let lcons = translate_exp dcons in
|
||||||
|
let ltau = translate_ty dtau in
|
||||||
|
let l_err : typed_l_exp ltau = L.ELit (L.LError L.ConflictError) in
|
||||||
|
build_default_translation_typing lexceptions L.ENone ljust lcons ltau L.empty;
|
||||||
|
take_l_steps ltau (build_default_translation lexceptions L.ENone ljust lcons ltau) n
|
||||||
|
== Some (final_default_subexp ltau ljust lcons)
|
||||||
|
))
|
||||||
|
(decreases dexceptions)
|
||||||
|
=
|
||||||
|
admit()
|
||||||
#pop-options
|
#pop-options
|
||||||
|
|
||||||
#push-options "--fuel 2 --ifuel 1 --z3rlimit 50"
|
#push-options "--fuel 2 --ifuel 1 --z3rlimit 50"
|
||||||
@ -864,41 +908,41 @@ let rec translation_correctness_step (de: D.exp) (dtau: D.ty)
|
|||||||
| D.ELit _ -> 0, le, 0
|
| D.ELit _ -> 0, le, 0
|
||||||
| D.EAbs _ _ -> 0, le, 0
|
| D.EAbs _ _ -> 0, le, 0
|
||||||
| D.EIf de1 de2 de3 ->
|
| D.EIf de1 de2 de3 ->
|
||||||
let le1 = translate_exp de1 in
|
let le1 = translate_exp de1 in
|
||||||
let le2 = translate_exp de2 in
|
let le2 = translate_exp de2 in
|
||||||
let le3 = translate_exp de3 in
|
let le3 = translate_exp de3 in
|
||||||
if not (D.is_value de1) then begin
|
if not (D.is_value de1) then begin
|
||||||
let de1' = Some?.v (D.step de1) in
|
let de1' = Some?.v (D.step de1) in
|
||||||
D.preservation de1 D.TBool;
|
D.preservation de1 D.TBool;
|
||||||
translation_preserves_empty_typ de1 D.TBool;
|
translation_preserves_empty_typ de1 D.TBool;
|
||||||
translation_preserves_empty_typ de2 dtau;
|
translation_preserves_empty_typ de2 dtau;
|
||||||
translation_preserves_empty_typ de3 dtau;
|
translation_preserves_empty_typ de3 dtau;
|
||||||
translation_preserves_empty_typ de1' D.TBool;
|
translation_preserves_empty_typ de1' D.TBool;
|
||||||
let le1' : typed_l_exp L.TBool = translate_exp de1' in
|
let le1' : typed_l_exp L.TBool = translate_exp de1' in
|
||||||
let n1_e1, target_e1, n2_e1 = translation_correctness_step de1 D.TBool in
|
let n1_e1, target_e1, n2_e1 = translation_correctness_step de1 D.TBool in
|
||||||
assert(take_l_steps L.TBool le1 n1_e1 == Some target_e1);
|
assert(take_l_steps L.TBool le1 n1_e1 == Some target_e1);
|
||||||
assert(take_l_steps L.TBool le1' n2_e1 == Some target_e1);
|
assert(take_l_steps L.TBool le1' n2_e1 == Some target_e1);
|
||||||
lift_multiple_l_steps L.TBool ltau le1 target_e1 n1_e1
|
lift_multiple_l_steps L.TBool ltau le1 target_e1 n1_e1
|
||||||
(if_cond_lift ltau le2 le3);
|
(if_cond_lift ltau le2 le3);
|
||||||
lift_multiple_l_steps L.TBool ltau le1' target_e1 n2_e1
|
lift_multiple_l_steps L.TBool ltau le1' target_e1 n2_e1
|
||||||
(if_cond_lift ltau le2 le3);
|
(if_cond_lift ltau le2 le3);
|
||||||
n1_e1, if_cond_lift ltau le2 le3 target_e1, n2_e1
|
n1_e1, if_cond_lift ltau le2 le3 target_e1, n2_e1
|
||||||
end else (1, le', 0)
|
end else (1, le', 0)
|
||||||
| D.EApp de1 de2 dtau_arg ->
|
| D.EApp de1 de2 dtau_arg ->
|
||||||
let le1 = translate_exp de1 in
|
let le1 = translate_exp de1 in
|
||||||
let le2 = translate_exp de2 in
|
let le2 = translate_exp de2 in
|
||||||
let ltau_arg = translate_ty dtau_arg in
|
let ltau_arg = translate_ty dtau_arg in
|
||||||
if not (D.is_value de1) then begin
|
if not (D.is_value de1) then begin
|
||||||
let de1' = Some?.v (D.step de1) in
|
let de1' = Some?.v (D.step de1) in
|
||||||
let le1' = translate_exp de1' in
|
let le1' = translate_exp de1' in
|
||||||
let n1_e1, target_e1, n2_e1 = translation_correctness_step de1 (D.TArrow dtau_arg dtau) in
|
let n1_e1, target_e1, n2_e1 = translation_correctness_step de1 (D.TArrow dtau_arg dtau) in
|
||||||
assert(take_l_steps (L.TArrow ltau_arg ltau) le1 n1_e1 == Some target_e1);
|
assert(take_l_steps (L.TArrow ltau_arg ltau) le1 n1_e1 == Some target_e1);
|
||||||
assert(take_l_steps (L.TArrow ltau_arg ltau) le1' n2_e1 == Some target_e1);
|
assert(take_l_steps (L.TArrow ltau_arg ltau) le1' n2_e1 == Some target_e1);
|
||||||
lift_multiple_l_steps (L.TArrow ltau_arg ltau) ltau le1 target_e1 n1_e1
|
lift_multiple_l_steps (L.TArrow ltau_arg ltau) ltau le1 target_e1 n1_e1
|
||||||
(app_f_lift ltau_arg ltau le2);
|
(app_f_lift ltau_arg ltau le2);
|
||||||
lift_multiple_l_steps (L.TArrow ltau_arg ltau) ltau le1' target_e1 n2_e1
|
lift_multiple_l_steps (L.TArrow ltau_arg ltau) ltau le1' target_e1 n2_e1
|
||||||
(app_f_lift ltau_arg ltau le2);
|
(app_f_lift ltau_arg ltau le2);
|
||||||
n1_e1, app_f_lift ltau_arg ltau le2 target_e1, n2_e1
|
n1_e1, app_f_lift ltau_arg ltau le2 target_e1, n2_e1
|
||||||
end else begin match de1 with
|
end else begin match de1 with
|
||||||
| D.ELit D.LConflictError -> 1, le', 0
|
| D.ELit D.LConflictError -> 1, le', 0
|
||||||
| D.ELit D.LEmptyError -> 1, le', 0
|
| D.ELit D.LEmptyError -> 1, le', 0
|
||||||
@ -924,10 +968,61 @@ let rec translation_correctness_step (de: D.exp) (dtau: D.ty)
|
|||||||
| D.EDefault dexceptions djust dcons dtau' ->
|
| D.EDefault dexceptions djust dcons dtau' ->
|
||||||
if dtau' <> dtau then 0, le', 0 else begin
|
if dtau' <> dtau then 0, le', 0 else begin
|
||||||
match D.step_exceptions de dexceptions djust dcons dtau with
|
match D.step_exceptions de dexceptions djust dcons dtau with
|
||||||
| Some _ ->
|
| D.SomeStep _ ->
|
||||||
translation_correctness_exceptions_step de dexceptions djust dcons dtau
|
translation_correctness_exceptions_step de dexceptions djust dcons dtau
|
||||||
(fun df tf -> translation_correctness_step df tf)
|
(fun df tf -> translation_correctness_step df tf)
|
||||||
| None -> admit()
|
| D.NoStep ->
|
||||||
|
let n1_final =
|
||||||
|
translation_correctness_exceptions_no_exceptions_triggered
|
||||||
|
de dexceptions djust dcons dtau
|
||||||
|
in
|
||||||
|
let ltau = translate_ty dtau in
|
||||||
|
let ljust = translate_exp djust in
|
||||||
|
let lcons = translate_exp dcons in
|
||||||
|
let l_err = L.ELit (L.LError L.EmptyError) in
|
||||||
|
assert(take_l_steps ltau le n1_final = Some (final_default_subexp ltau ljust lcons));
|
||||||
|
if not (D.is_value djust) then begin
|
||||||
|
let djust' = Some?.v (D.step djust) in
|
||||||
|
D.preservation djust D.TBool;
|
||||||
|
translation_preserves_empty_typ djust D.TBool;
|
||||||
|
translation_preserves_empty_typ dcons dtau;
|
||||||
|
translation_preserves_empty_typ djust' D.TBool;
|
||||||
|
let ljust' : typed_l_exp L.TBool = translate_exp djust' in
|
||||||
|
let n1_just, target_just, n2_just = translation_correctness_step djust D.TBool in
|
||||||
|
assert(take_l_steps L.TBool ljust n1_just == Some target_just);
|
||||||
|
assert(take_l_steps L.TBool ljust' n2_just == Some target_just);
|
||||||
|
lift_multiple_l_steps L.TBool ltau ljust target_just n1_just
|
||||||
|
(if_cond_lift ltau lcons l_err);
|
||||||
|
lift_multiple_l_steps L.TBool ltau ljust' target_just n2_just
|
||||||
|
(if_cond_lift ltau lcons l_err);
|
||||||
|
take_l_steps_transitive ltau le (final_default_subexp ltau ljust lcons) n1_final n1_just;
|
||||||
|
assert(take_l_steps ltau le (n1_final + n1_just) == Some (L.EIf target_just lcons l_err));
|
||||||
|
assert(de' == D.EDefault dexceptions djust' dcons dtau);
|
||||||
|
assume(D.step_exceptions de dexceptions djust dcons dtau ==
|
||||||
|
D.step_exceptions de' dexceptions djust' dcons dtau);
|
||||||
|
// Should be easy enough, djust does not influence the result
|
||||||
|
let n2_final =
|
||||||
|
translation_correctness_exceptions_no_exceptions_triggered
|
||||||
|
de' dexceptions djust' dcons dtau
|
||||||
|
in
|
||||||
|
take_l_steps_transitive ltau le' (final_default_subexp ltau ljust' lcons) n2_final n2_just;
|
||||||
|
n1_final + n1_just, L.EIf target_just lcons l_err, n2_final + n2_just
|
||||||
|
end else begin
|
||||||
|
D.is_bool_value_cannot_be_abs D.empty djust;
|
||||||
|
match djust with
|
||||||
|
| D.ELit D.LTrue ->
|
||||||
|
take_l_steps_transitive ltau le (final_default_subexp ltau ljust lcons) n1_final 1;
|
||||||
|
n1_final + 1, lcons, 0
|
||||||
|
| D.ELit D.LFalse ->
|
||||||
|
take_l_steps_transitive ltau le (final_default_subexp ltau ljust lcons) n1_final 1;
|
||||||
|
n1_final + 1, l_err, 0
|
||||||
|
| D.ELit D.LConflictError ->
|
||||||
|
take_l_steps_transitive ltau le (final_default_subexp ltau ljust lcons) n1_final 1;
|
||||||
|
n1_final + 1, L.ELit (L.LError L.ConflictError), 0
|
||||||
|
| D.ELit D.LEmptyError ->
|
||||||
|
take_l_steps_transitive ltau le (final_default_subexp ltau ljust lcons) n1_final 1;
|
||||||
|
n1_final + 1, l_err, 0
|
||||||
|
end
|
||||||
end
|
end
|
||||||
|
|
||||||
(*** Wrap-up theorem *)
|
(*** Wrap-up theorem *)
|
||||||
|
Loading…
Reference in New Issue
Block a user