summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--backends/hol4/divDefProto2Script.sml191
-rw-r--r--backends/hol4/divDefProto2Theory.sig107
2 files changed, 214 insertions, 84 deletions
diff --git a/backends/hol4/divDefProto2Script.sml b/backends/hol4/divDefProto2Script.sml
index 9da186c1..9dc43ea7 100644
--- a/backends/hol4/divDefProto2Script.sml
+++ b/backends/hol4/divDefProto2Script.sml
@@ -298,23 +298,9 @@ Proof
metis_tac []
QED
-(*
- * Attempt to make the lemmas work with more general types
- * (we want ‘: 'a -> 'b result’, not ‘:'a -> 'a result’).
- *)
-val simp_types_def = Define ‘
- simp_types (f : 'a -> 'b result) : ('a + 'b) -> ('a + 'b) result =
- \x. case x of
- | INL x =>
- (case f x of
- | Fail e => Fail e
- | Diverge => Diverge
- | Return y =>
- Return (INR y))
- | INR _ => Fail Failure
-’
-
-(* Testing on an example *)
+(*======================
+ * Example 1: nth
+ *======================*)
Datatype:
list_t =
ListCons 't list_t
@@ -326,6 +312,10 @@ val nth_body_def = Define ‘
nth_body (f : (('t list_t # u32) + 't) -> (('t list_t # u32) + 't) result)
(x : (('t list_t # u32) + 't)) :
(('t list_t # u32) + 't) result =
+ (* Destruct the input. We need this to call the proper function in case
+ of mutually recursive definitions, but also to eliminate arguments
+ which correspond to the output value (the input type is the same
+ as the output type). *)
case x of
| INL x => (
let (ls, i) = x in
@@ -337,6 +327,8 @@ val nth_body_def = Define ‘
do
i0 <- u32_sub i (int_to_u32 1);
r <- f (INL (tl, i0));
+ (* Eliminate the invalid outputs. This is not necessary here,
+ but it is in the case of non tail call recursive calls. *)
case r of
| INL _ => Fail Failure
| INR i1 => Return (INR i1)
@@ -345,13 +337,6 @@ val nth_body_def = Define ‘
| INR _ => Fail Failure
-(* TODO: move *)
-Theorem is_valid_suffice:
- ∃y. ∀g. g x = g y
-Proof
- metis_tac []
-QED
-
(* We first prove the theorem with ‘SUC (SUC n)’ where ‘n’ is a variable
to prevent this quantity from being rewritten to 2 *)
Theorem nth_body_is_valid_aux:
@@ -401,6 +386,10 @@ val nth_raw_def = Define ‘
| INR x => Return x
+(* Rewrite the goal once, and on the left part of the goal seen as an application *)
+fun pure_once_rewrite_left_tac ths =
+ CONV_TAC (PATH_CONV "l" (PURE_ONCE_REWRITE_CONV ths))
+
Theorem nth_def:
∀ls i. nth (ls : 't list_t) (i : u32) : 't result =
case ls of
@@ -417,13 +406,10 @@ Proof
rpt strip_tac >>
(* Expand the raw definition *)
pure_rewrite_tac [nth_raw_def] >>
- (* Use the fixed-point equality *)
- sg ‘fix nth_body (INL (ls,i)) = nth_body (fix nth_body) (INL (ls,i))’
- >- (simp_tac bool_ss [HO_MATCH_MP fix_fixed_eq nth_body_is_valid]) >>
- pop_assum (fn th => pure_asm_rewrite_tac [th]) >>
+ (* Use the fixed-point equality - the rewrite must only be applied *on the left* of the equality, in the goal *)
+ pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq nth_body_is_valid] >>
(* Expand the body definition *)
- qspecl_assume [‘fix nth_body’, ‘(INL (ls, i))’] nth_body_def >>
- pop_assum (fn th => pure_rewrite_tac [th, LET_THM]) >>
+ pure_rewrite_tac [nth_body_def] >>
(* Explore all the paths - maybe we can be smarter, but this is fast and really easy *)
fs [bind_def] >>
Cases_on ‘ls’ >> fs [] >>
@@ -433,4 +419,149 @@ Proof
Cases_on ‘a'’ >> fs []
QED
+(*======================
+ * Example 2: even, odd
+ *======================*)
+
+val even_odd_body_def = Define ‘
+ even_odd_body
+ (f : (int + int + bool) -> (int + int + bool) result)
+ (x : int + int + bool) : (int + int + bool) result =
+ case x of
+ | INL i =>
+ (* Even *)
+ if i = 0 then Return (INR (INR T))
+ else
+ (case f (INR (INL (i - 1))) of
+ | Fail e => Fail e
+ | Diverge => Diverge
+ | Return r =>
+ (* Eliminate the unwanted results *)
+ case r of
+ | INL _ => Fail Failure
+ | INR (INL _) => Fail Failure
+ | INR (INR b) => Return (INR (INR b))
+ )
+ | INR x =>
+ case x of
+ | INL i =>
+ (* Odd *)
+ if i = 0 then Return (INR (INR F))
+ else
+ (case f (INL (i - 1)) of
+ | Fail e => Fail e
+ | Diverge => Diverge
+ | Return r =>
+ (* Eliminate the unwanted results *)
+ case r of
+ | INL _ => Fail Failure
+ | INR (INL _) => Fail Failure
+ | INR (INR b) => Return (INR (INR b))
+ )
+ | INR _ =>
+ (* This case is for the return value *)
+ Fail Failure
+’
+
+Theorem even_odd_body_is_valid_aux:
+ is_valid_fp_body (SUC (SUC n)) even_odd_body
+Proof
+ pure_once_rewrite_tac [is_valid_fp_body_def] >>
+ gen_tac >>
+ (* Expand *)
+ fs [even_odd_body_def, bind_def] >>
+ (* TODO: automate this *)
+ Cases_on ‘x’ >> fs []
+ >-(
+ Cases_on ‘x' = 0’ >> fs [] >>
+ (* Recursive call *)
+ disj2_tac >>
+ qexists ‘\g x. case x of | INL _ => Fail Failure | INR (INL _) => Fail Failure | INR (INR i1) => Return (INR (INR i1))’ >>
+ qexists ‘INR (INL (x' − 1))’ >>
+ conj_tac
+ >-(pure_once_rewrite_tac [is_valid_fp_body_def] >> fs []) >>
+ fs []) >>
+ Cases_on ‘y’ >> fs [] >>
+ Cases_on ‘x = 0’ >> fs [] >>
+ (* Recursive call *)
+ disj2_tac >>
+ qexists ‘\g x. case x of | INL _ => Fail Failure | INR (INL _) => Fail Failure | INR (INR i1) => Return (INR (INR i1))’ >>
+ qexists ‘INL (x − 1)’ >>
+ conj_tac
+ >-(pure_once_rewrite_tac [is_valid_fp_body_def] >> fs []) >>
+ fs []
+QED
+
+Theorem even_odd_body_is_valid:
+ is_valid_fp_body (SUC (SUC 0)) even_odd_body
+Proof
+ irule even_odd_body_is_valid_aux
+QED
+
+val even_raw_def = Define ‘
+ even (i : int) =
+ case fix even_odd_body (INL i) of
+ | Fail e => Fail e
+ | Diverge => Diverge
+ | Return r =>
+ case r of
+ | INL _ => Fail Failure
+ | INR (INL _) => Fail Failure
+ | INR (INR b) => Return b
+’
+
+val odd_raw_def = Define ‘
+ odd (i : int) =
+ case fix even_odd_body (INR (INL i)) of
+ | Fail e => Fail e
+ | Diverge => Diverge
+ | Return r =>
+ case r of
+ | INL _ => Fail Failure
+ | INR (INL _) => Fail Failure
+ | INR (INR b) => Return b
+’
+
+Theorem even_def:
+ ∀i. even (i : int) : bool result =
+ if i = 0 then Return T else odd (i - 1)
+Proof
+ gen_tac >>
+ (* Expand the definition *)
+ pure_once_rewrite_tac [even_raw_def] >>
+ (* Use the fixed-point equality *)
+ pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq even_odd_body_is_valid] >>
+ (* Expand the body definition *)
+ pure_rewrite_tac [even_odd_body_def] >>
+ (* Expand all the definitions from the group *)
+ pure_rewrite_tac [even_raw_def, odd_raw_def] >>
+ (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *)
+ fs [bind_def] >>
+ Cases_on ‘i = 0’ >> fs [] >>
+ Cases_on ‘fix even_odd_body (INR (INL (i − 1)))’ >> fs [] >>
+ Cases_on ‘a’ >> fs [] >>
+ Cases_on ‘y’ >> fs []
+QED
+
+Theorem odd_def:
+ ∀i. odd (i : int) : bool result =
+ if i = 0 then Return F else even (i - 1)
+Proof
+ gen_tac >>
+ (* Expand the definition *)
+ pure_once_rewrite_tac [odd_raw_def] >>
+ (* Use the fixed-point equality *)
+ pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq even_odd_body_is_valid] >>
+ (* Expand the body definition *)
+ pure_rewrite_tac [even_odd_body_def] >>
+ (* Expand all the definitions from the group *)
+ pure_rewrite_tac [even_raw_def, odd_raw_def] >>
+ (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *)
+ fs [bind_def] >>
+ Cases_on ‘i = 0’ >> fs [] >>
+ Cases_on ‘fix even_odd_body (INL (i − 1))’ >> fs [] >>
+ Cases_on ‘a’ >> fs [] >>
+ Cases_on ‘y’ >> fs []
+QED
+
val _ = export_theory ()
diff --git a/backends/hol4/divDefProto2Theory.sig b/backends/hol4/divDefProto2Theory.sig
index 7ce4b194..77d5631e 100644
--- a/backends/hol4/divDefProto2Theory.sig
+++ b/backends/hol4/divDefProto2Theory.sig
@@ -3,6 +3,7 @@ sig
type thm = Thm.thm
(* Definitions *)
+ val even_odd_body_def : thm
val fix_def : thm
val fix_fuel_P_def : thm
val fix_fuel_def : thm
@@ -10,12 +11,13 @@ sig
val list_t_TY_DEF : thm
val list_t_case_def : thm
val list_t_size_def : thm
- val nth_body1_def : thm
- val nth_body_valid_def : thm
- val simp_types_def : thm
+ val nth_body_def : thm
(* Theorems *)
val datatype_list_t : thm
+ val even_def : thm
+ val even_odd_body_is_valid : thm
+ val even_odd_body_is_valid_aux : thm
val fix_fixed_diverges : thm
val fix_fixed_eq : thm
val fix_fixed_terminates : thm
@@ -30,7 +32,6 @@ sig
val fix_not_diverge_implies_fix_fuel : thm
val fix_not_diverge_implies_fix_fuel_aux : thm
val is_valid_fp_body_compute : thm
- val is_valid_suffice : thm
val list_t_11 : thm
val list_t_Axiom : thm
val list_t_case_cong : thm
@@ -38,14 +39,38 @@ sig
val list_t_distinct : thm
val list_t_induction : thm
val list_t_nchotomy : thm
- val nth_body_valid_eq : thm
- val nth_body_valid_is_valid : thm
+ val nth_body_is_valid : thm
+ val nth_body_is_valid_aux : thm
val nth_def : thm
+ val odd_def : thm
val divDefProto2_grammars : type_grammar.grammar * term_grammar.grammar
(*
[primitives] Parent theory of "divDefProto2"
+ [even_odd_body_def] Definition
+
+ ⊢ ∀f x.
+ even_odd_body f x =
+ case x of
+ INL 0 => Return (INR (INR T))
+ | INL i =>
+ (case f (INR (INL (i − 1))) of
+ Return (INL v) => Fail Failure
+ | Return (INR (INL v2)) => Fail Failure
+ | Return (INR (INR b)) => Return (INR (INR b))
+ | Fail e => Fail e
+ | Diverge => Diverge)
+ | INR (INL 0) => Return (INR (INR F))
+ | INR (INL i) =>
+ (case f (INL (i − 1)) of
+ Return (INL v) => Fail Failure
+ | Return (INR (INL v2)) => Fail Failure
+ | Return (INR (INR b)) => Return (INR (INR b))
+ | Fail e => Fail e
+ | Diverge => Diverge)
+ | INR (INR v5) => Fail Failure
+
[fix_def] Definition
⊢ ∀f x.
@@ -101,36 +126,10 @@ sig
list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧
∀f. list_t_size f ListNil = 0
- [nth_body1_def] Definition
-
- ⊢ ∀f x.
- nth_body1 f x =
- case x of
- INL x =>
- (let
- (ls,i) = x
- in
- case ls of
- ListCons x tl =>
- if u32_to_int i = 0 then Return (INR x)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- r <-
- case f (INL (tl,i0)) of
- Return (INL v) => Fail Failure
- | Return (INR i1) => Return i1
- | Fail e => Fail e
- | Diverge => Diverge;
- Return (INR r)
- od
- | ListNil => Fail Failure)
- | INR v3 => Fail Failure
-
- [nth_body_valid_def] Definition
+ [nth_body_def] Definition
⊢ ∀f x.
- nth_body_valid f x =
+ nth_body f x =
case x of
INL x =>
(let
@@ -150,22 +149,22 @@ sig
| ListNil => Fail Failure)
| INR v2 => Fail Failure
- [simp_types_def] Definition
-
- ⊢ ∀f. simp_types f =
- (λx'.
- case x' of
- INL x =>
- (case f x of
- Return y => Return (INR y)
- | Fail e => Fail e
- | Diverge => Diverge)
- | INR v1 => Fail Failure)
-
[datatype_list_t] Theorem
⊢ DATATYPE (list_t ListCons ListNil)
+ [even_def] Theorem
+
+ ⊢ ∀i. even i = if i = 0 then Return T else odd (i − 1)
+
+ [even_odd_body_is_valid] Theorem
+
+ ⊢ is_valid_fp_body (SUC (SUC 0)) even_odd_body
+
+ [even_odd_body_is_valid_aux] Theorem
+
+ ⊢ is_valid_fp_body (SUC (SUC n)) even_odd_body
+
[fix_fixed_diverges] Theorem
⊢ ∀N f.
@@ -273,10 +272,6 @@ sig
is_valid_fp_body (NUMERAL (BIT1 n)) h ∧
∀g. f g x = do z <- g y; h g z od
- [is_valid_suffice] Theorem
-
- ⊢ ∃y. ∀g. g x = g y
-
[list_t_11] Theorem
⊢ ∀a0 a1 a0' a1'.
@@ -312,13 +307,13 @@ sig
⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
- [nth_body_valid_eq] Theorem
+ [nth_body_is_valid] Theorem
- ⊢ nth_body_valid = nth_body1
+ ⊢ is_valid_fp_body (SUC (SUC 0)) nth_body
- [nth_body_valid_is_valid] Theorem
+ [nth_body_is_valid_aux] Theorem
- ⊢ is_valid_fp_body (SUC (SUC 0)) nth_body_valid
+ ⊢ is_valid_fp_body (SUC (SUC n)) nth_body
[nth_def] Theorem
@@ -330,6 +325,10 @@ sig
else do i0 <- u32_sub i (int_to_u32 1); nth tl i0 od
| ListNil => Fail Failure
+ [odd_def] Theorem
+
+ ⊢ ∀i. odd i = if i = 0 then Return F else even (i − 1)
+
*)
end