summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--backends/hol4/divDefProto2Script.sml527
-rw-r--r--backends/hol4/divDefProto2Theory.sig400
2 files changed, 417 insertions, 510 deletions
diff --git a/backends/hol4/divDefProto2Script.sml b/backends/hol4/divDefProto2Script.sml
index 985b930f..074006c9 100644
--- a/backends/hol4/divDefProto2Script.sml
+++ b/backends/hol4/divDefProto2Script.sml
@@ -15,8 +15,8 @@ val _ = new_theory "divDefProto2"
* TODO: this works! Cleanup.
*)
val fix_fuel_def = Define ‘
- (fix_fuel (0 : num) (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result = Diverge) ∧
- (fix_fuel (SUC n) (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result = f (fix_fuel n f) x)
+ (fix_fuel (0 : num) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = Diverge) ∧
+ (fix_fuel (SUC n) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = f (fix_fuel n f) x)
val fix_fuel_P_def = Define ‘
@@ -24,7 +24,7 @@ val fix_fuel_P_def = Define ‘
val fix_def = Define ‘
- fix (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result =
+ fix (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result =
if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
@@ -288,391 +288,188 @@ Proof
Cases_on ‘f (fix_fuel n'' f) x’ >> fs [] >> metis_tac []
QED
-(*
-Type ft = ``: 'a -> ('a result + (num # num # 'a))``
-
-val fix_fuel_def = Define ‘
- (fix_fuel (0 : num) (fs : ('a ft) list)
- (i : num) (x : 'a) : 'a result = Diverge) ∧
-
- (fix_fuel (SUC n) fs i x =
- case EL i fs x of
- | INL r => r
- | INR (j, k, y) =>
- case fix_fuel n fs j y of
- | Fail e => Fail e
- | Diverge => Diverge
- | Return z =>
- fix_fuel n fs k z)
-’
-
-val fix_fuel_P_def = Define ‘
- fix_fuel_P fs i x n = ~(is_diverge (fix_fuel n fs i x))
-’
-
-val fix_def = Define ‘
- fix (fs : ('a ft) list) (i : num) (x : 'a) : 'a result =
- if (∃ n. fix_fuel_P fs i x n)
- then fix_fuel ($LEAST (fix_fuel_P fs i x)) fs i x
- else Diverge
-’
-
-Theorem fix_fuel_mono:
- ∀f. is_valid_fp_body f ⇒
- ∀n x. fix_fuel_P f x n ⇒
- ∀ m. n ≤ m ⇒
- fix_fuel n f x = fix_fuel m f x
+Theorem fix_fixed_eq:
+ ∀N f. is_valid_fp_body N f ⇒ ∀x. fix f x = f (fix f) x
Proof
- ntac 2 strip_tac >>
- Induct_on ‘n’ >> rpt strip_tac
- >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >>
- Cases_on ‘m’ >- int_tac >> fs [] >>
- fs [is_valid_fp_body_def] >>
- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
-
- (*(* Use the validity property *)
- last_assum (qspec_assume ‘x’) >> (* TODO: consume? *) *)
-
- (*pop_assum ignore_tac >> (* TODO: not sure *) *)
- Induct_on ‘N’ >- fs [eval_ftree_def] >>
- rw [] >>
- rw [eval_ftree_def] >>
- Cases_on ‘h x’ >> fs [] >>
- Cases_on ‘y’ >> fs [] >>
- Cases_on ‘y'’ >> fs [] >>
-
- last_assum (qspec_assume ‘q’) >>
- Cases_on ‘fix_fuel n f q’ >> fs [] >>
-
- Cases_on ‘N’ >> fs [eval_ftree_def] >>
-
- Cases_on ‘y’ >> fs [] >>
- Cases_on ‘y'’ >> fs [] >>
rw [] >>
- (* This makes a case disjunction on the validity property *)
- rw []
- >-((* Case 1: the continuation doesn't matter *) fs []) >>
- (* Case 2: the continuation *does* matter (i.e., there is a recursive call *)
- (* Instantiate the validity property with the different continuations *)
- first_assum (qspec_assume ‘fix_fuel n f’) >>
- first_assum (qspec_assume ‘fix_fuel n' f’) >>
- last_assum (qspec_assume ‘y’) >>
- fs []
-QED
-
-
-
-Type ft = ``: ('a -> 'a result) -> 'a -> ('a result + (num # 'a))``
-
-val fix_fuel_def = Define ‘
- (fix_fuel (0 : num) (fs : ('a ft) list) (g : 'a -> 'a result)
- (i : num) (x : 'a) : 'a result = Diverge) ∧
-
- (fix_fuel (SUC n) fs g i x =
- case EL i fs g x of
- | INL r => r
- | INR (j, y) =>
- case g y of
- | Fail e => Fail e
- | Diverge => Diverge
- | Return z => fix_fuel n fs g j z)
-’
-
-val fix_fuel_def = Define ‘
- (fix_fuel (0 : num) (fs : ('a ft) list) g (i : num) (x : 'a) : 'a result = Diverge) ∧
-
- (fix_fuel (SUC n) fs g i x =
- case EL i fs x of
- | INL r => r
- | INR (j, y) =>
- case g y of
- | Fail e => Fail e
- | Diverge => Diverge
- | Return z => fix_fuel n fs g j z)
-’
-
-val fix_fuel_def = Define ‘
- (fix_fuel (0 : num) (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result = Diverge) ∧
- (fix_fuel (SUC n) (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result = f (fix_fuel n f) x)
-’
-
-val fix_fuel_P_def = Define ‘
- fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x))
-’
+ Cases_on ‘∃n. fix_fuel_P f x n’
+ >- (irule fix_fixed_terminates >> metis_tac []) >>
+ irule fix_fixed_diverges >>
+ metis_tac []
+QED
-val fix_def = Define ‘
- fix (f : ('a -> 'a result) -> 'a -> 'a result) (x : 'a) : 'a result =
- if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
+(*
+ * 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
-(*Datatype:
- ftree = Rec (('a -> ('a result + ('a # num))) # ftree list) | NRec ('a -> 'a result)
+(* Testing on an example *)
+Datatype:
+ list_t =
+ ListCons 't list_t
+ | ListNil
End
-Type frtree = ``: ('b -> ('b result + ('a # num))) list``
-Type ftree = “: ('a, 'b) frtree # ('b result + ('a # num))”
-*)
-
-val eval_ftree_def = Define ‘
- (eval_ftree 0 (g : 'a -> 'a result)
- (fs : ('a -> ('a result + ('a # num))) list) x = Diverge) ∧
-
- (eval_ftree (SUC n) g fs x =
+(* We use this version of the body to prove that the body is valid *)
+val nth_body_valid_def = Define ‘
+ nth_body_valid (f : (('t list_t # u32) + 't) -> (('t list_t # u32) + 't) result)
+ (x : (('t list_t # u32) + 't)) :
+ (('t list_t # u32) + 't) result =
case x of
- | INL r => r
- | INR (y, i) =>
- case g y of
- | Fail e => Fail e
- | Diverge => Diverge
- | Return z =>
- let f = EL i fs in
- eval_ftree n g fs (f z))
+ | INL x => (
+ let (ls, i) = x in
+ case ls of
+ | ListCons x tl =>
+ if u32_to_int i = (0:int)
+ then Return (INR x)
+ else
+ do
+ i0 <- u32_sub i (int_to_u32 1);
+ r <- f (INL (tl, i0));
+ case r of
+ | INL _ => Fail Failure
+ | INR i1 => Return (INR i1)
+ od
+ | ListNil => Fail Failure)
+ | INR _ => Fail Failure
-Theorem fix_fuel_mono:
- ∀N fs i.
- let f = (\g x. eval_ftree N g fs (INR (x, i))) in
- ∀n x. fix_fuel_P f x n ⇒
- ∀ m. n ≤ m ⇒ fix_fuel n f x = fix_fuel m f x
+(* TODO: move *)
+Theorem is_valid_suffice:
+ ∃y. ∀g. g x = g y
Proof
- Induct_on ‘N’
- >-(
- fs [eval_ftree_def] >>
-
- ntac 2 strip_tac >>
- Induct_on ‘n’ >> rpt strip_tac
- >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >>
- Cases_on ‘m’ >- int_tac >> fs [] >>
- fs [is_valid_fp_body_def] >>
- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
-
-
-val is_valid_fp_body_def = Define ‘
- is_valid_fp_body (f : ('a -> 'b result) -> 'a -> 'b result) =
- (∃N ft. ∀x g. f g x = eval_ftree N g ft (x, i))
-’
-
-val eval_ftree_def = Define ‘
- (eval_ftree 0 (g : 'a -> 'b result)
- (fs : ('b -> ('b result + ('a # num))) list, x : 'b result + ('a # num)) = Diverge) ∧
-
- (eval_ftree (SUC n) g (fs, x) =
- case x of
- | INL r => r
- | INR (y, i) =>
- case g y of
- | Fail e => Fail e
- | Diverge => Diverge
- | Return z =>
- let f = EL i fs in
- eval_ftree n g (fs, f z))
-’
-
-val is_valid_fp_body_def = Define ‘
- is_valid_fp_body (f : ('a -> 'b result) -> 'a -> 'b result) =
- (∃N ft h. ∀x g. f g x = eval_ftree N g (ft, h x))
-’
-
-Theorem fix_fuel_mono:
- let f = (\x. eval_ftree N g (ft, h x)) in
- ∀n x. fix_fuel_P f x n ⇒
- ∀ m. n ≤ m ⇒ fix_fuel n f x = fix_fuel m f x
-Proof
-
-
-Theorem fix_fuel_mono:
- ∀f. is_valid_fp_body f ⇒
- ∀n x. fix_fuel_P f x n ⇒
- ∀ m. n ≤ m ⇒
- fix_fuel n f x = fix_fuel m f x
-Proof
- ntac 2 strip_tac >>
- Induct_on ‘n’ >> rpt strip_tac
- >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >>
- Cases_on ‘m’ >- int_tac >> fs [] >>
- fs [is_valid_fp_body_def] >>
- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >>
-
- (*(* Use the validity property *)
- last_assum (qspec_assume ‘x’) >> (* TODO: consume? *) *)
-
- (*pop_assum ignore_tac >> (* TODO: not sure *) *)
- Induct_on ‘N’ >- fs [eval_ftree_def] >>
- rw [] >>
- rw [eval_ftree_def] >>
- Cases_on ‘h x’ >> fs [] >>
- Cases_on ‘y’ >> fs [] >>
- Cases_on ‘y'’ >> fs [] >>
-
- last_assum (qspec_assume ‘q’) >>
- Cases_on ‘fix_fuel n f q’ >> fs [] >>
-
- Cases_on ‘N’ >> fs [eval_ftree_def] >>
-
- Cases_on ‘y’ >> fs [] >>
- Cases_on ‘y'’ >> fs [] >>
- rw [] >>
- (* This makes a case disjunction on the validity property *)
- rw []
- >-((* Case 1: the continuation doesn't matter *) fs []) >>
- (* Case 2: the continuation *does* matter (i.e., there is a recursive call *)
- (* Instantiate the validity property with the different continuations *)
- first_assum (qspec_assume ‘fix_fuel n f’) >>
- first_assum (qspec_assume ‘fix_fuel n' f’) >>
- last_assum (qspec_assume ‘y’) >>
- fs []
+ metis_tac []
QED
-
-val length_ftree = “
-(
- [
- (\n. INL (return (1 + n)))
- ],
- (case ls of
- | ListCons x tl =>
- INR (tl, 0)
- | ListNil => INL (return 0))
-) : ('a list_t, int) ftree
-”
-
-val eval_length_ftree = mk_icomb (“eval_ftree 1 g”, length_ftree)
-
-Theorem length_body_eq:
- eval_ftree (SUC (SUC 0)) g
- (
- [
- (\n. INL (Return (1 + n)))
- ],
- (case ls of
- | ListCons x tl =>
- INR (tl, 0)
- | ListNil => INL (Return 0))
- ) =
- case ls of
- | ListCons x tl =>
- do
- n <- g tl;
- Return (1 + n)
- od
- | ListNil => Return 0
+Theorem nth_body_valid_is_valid:
+ is_valid_fp_body (SUC (SUC 0)) nth_body_valid
Proof
- fs [eval_ftree_def, bind_def] >>
- Cases_on ‘ls’ >> fs []
+ pure_once_rewrite_tac [is_valid_fp_body_def] >>
+ gen_tac >>
+ (* TODO: automate this *)
+ Cases_on ‘x’ >> fs [] >>
+ (* Expand *)
+ fs [nth_body_valid_def, bind_def] >>
+ (* Explore all paths *)
+ Cases_on ‘x'’ >> fs [] >>
+ Cases_on ‘q’ >> fs [] >>
+ Cases_on ‘u32_to_int r = 0’ >> fs [] >>
+ Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs [] >>
+ disj2_tac >>
+ (* This is hard *)
+ qexists ‘\g x. case x of | INL _ => Fail Failure | INR i1 => Return (INR i1)’ >>
+ qexists ‘INL (l, a)’ >>
+ conj_tac
+ >-(
+ (* Prove that the body of h is valid *)
+ sg ‘1 = SUC 0’ >- fs [] >>
+ pop_assum (fn th => pure_rewrite_tac [th]) >>
+ pure_once_rewrite_tac [is_valid_fp_body_def] >>
+ (* *)
+ fs []) >>
+ gen_tac >>
+ (* Explore all paths *)
+ Cases_on ‘g (INL (l,a))’ >> fs [] >>
+ Cases_on ‘a'’ >> fs []
QED
-val eval_ftree_def = Define ‘
- eval_ftree 0 (fs : ('a, 'b) ftree) (g : 'a -> 'b result) (x : 'b result + ('a # num)) = Diverge ∧
-
- eval_ftree (SUC n) fs g x =
+(* We prove that ‘nth_body_valid’ is equivalent to ‘nth_body’ *)
+val nth_body1_def = Define ‘
+ nth_body1 (f : (('t list_t # u32) + 't) -> (('t list_t # u32) + 't) result)
+ (x : (('t list_t # u32) + 't)) :
+ (('t list_t # u32) + 't) result =
case x of
- | INL r => r
- | INR (y, i) =>
- case g y of
- | Fail e => Fail e
- | Diverge => Diverge
- | Return z =>
- let f = EL i fs in
- eval_ftree n fs g (f z)
+ | INL x => (
+ let (ls, i) = x in
+ case ls of
+ | ListCons x tl =>
+ if u32_to_int i = (0:int)
+ then Return (INR x)
+ else
+ do
+ i0 <- u32_sub i (int_to_u32 1);
+ r <- case f (INL (tl, i0)) of
+ | Fail e => Fail e
+ | Diverge => Diverge
+ | Return r =>
+ case r of
+ | INL _ => Fail Failure
+ | INR i1 => Return i1;
+ Return (INR r)
+ od
+ | ListNil => Fail Failure)
+ | INR _ => Fail Failure
-val length_body_funs_def = Define
-
-“
-[
- (\ls. case ls of
- | ListCons x tl =>
- INR (tl, 1)
- | ListNil => INL (return 0)),
- (\n. INL (return (1 + n)))
-]
-”
-
-
-
-“:('a, 'b) FT”
-
-Define
-
-val nth_body = Define ‘
-
+Theorem nth_body_valid_eq:
+ nth_body_valid = nth_body1
+Proof
+ ntac 2 (irule EQ_EXT >> gen_tac) >>
+ pure_rewrite_tac [nth_body_valid_def, nth_body1_def, bind_def, LET_DEF] >>
+ (* TODO: automate *)
+ Cases_on ‘x'’ >> fs [] >>
+ Cases_on ‘x''’ >> fs [] >>
+ Cases_on ‘q’ >> fs [] >>
+ Cases_on ‘u32_to_int r = 0’ >> fs [] >>
+ Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs [] >>
+ Cases_on ‘x (INL (l,a))’ >> fs [] >>
+ Cases_on ‘a'’ >> fs []
+QED
+val nth_raw_def = Define ‘
+ nth (ls : 't list_t) (i : u32) =
+ case fix nth_body1 (INL (ls, i)) of
+ | Fail e => Fail e
+ | Diverge => Diverge
+ | Return r =>
+ case r of
+ | INL _ => Fail Failure
+ | INR x => Return x
-“INL”
-“INR”
-
-“
- Rec (
+Theorem nth_def:
+ ∀ls i. nth (ls : 't list_t) (i : u32) : 't result =
case ls of
| ListCons x tl =>
- do
- INR (tl, 0)
- od
- | ListNil => INL (return 0),
- [NRec (\n. return (1 + n))])
-”
-
-“
- case ls of
- | ListCons x tl =>
- if u32_to_int i = (0:int)
- then (Return x)
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- y <- nth tl i0;
- return y
- od
- | ListNil => Fail Failure
-”
-
-
-“:'a + 'b”
-“:'a # 'b”
-
-(*** Encoding of a function *)
-Datatype:
- ('a, 'b) test = Return ('a -> 'b)
-End
-
-val tyax =
- new_type_definition ("three",
- Q.prove(`?p. (\(x,y). ~(x /\ y)) p`, cheat))
-
-val three_bij = define_new_type_bijections
- {name="three_tybij", ABS="abs3", REP="rep3", tyax=tyax}
-type_of “rep3”
-type_of “abs3”
-
-m “”
-
- Q.EXISTS_TAC `(F,F)` THEN GEN_BETA_TAC THEN REWRITE_TAC []));
-
-“Return (\x. x)”
-
-Datatype:
- ftree = Rec ('a -> ('a result + ('a # ftree))) | NRec ('a -> 'a result)
-End
-
-Datatype:
- 'a ftree = Rec ('a -> ('a result + ('a # ftree))) | NRec ('a -> 'a result)
-End
-
-Datatype:
- ftree = Rec ('a -> ('a result + ('a # ftree))) | NRec ('a -> 'a result)
-End
-
-Datatype:
- result = Return 'a | Fail error | Diverge
-End
-
-Type M = ``: 'a result``
-
-
-val fix_def = Define ‘
- fix (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result =
- if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
-’
+ if u32_to_int i = (0:int)
+ then (Return x)
+ else
+ do
+ i0 <- u32_sub i (int_to_u32 1);
+ nth tl i0
+ od
+ | ListNil => Fail Failure
+Proof
+ rpt strip_tac >>
+ (* Expand the raw definition *)
+ pure_rewrite_tac [nth_raw_def] >>
+ (* Use the fixed-point equality *)
+ sg ‘fix nth_body1 (INL (ls,i)) = nth_body1 (fix nth_body1) (INL (ls,i))’
+ >- (
+ pure_rewrite_tac [GSYM nth_body_valid_eq] >>
+ simp_tac bool_ss [HO_MATCH_MP fix_fixed_eq nth_body_valid_is_valid]) >>
+ pop_assum (fn th => pure_asm_rewrite_tac [th]) >>
+ (* Expand the body definition *)
+ qspecl_assume [‘fix nth_body1’, ‘(INL (ls, i))’] nth_body1_def >>
+ pop_assum (fn th => pure_rewrite_tac [th, LET_THM]) >>
+ (* Do we really have to explore all the paths again? If yes, nth_body1 is useless *)
+ fs [bind_def] >>
+ Cases_on ‘ls’ >> fs [] >>
+ Cases_on ‘u32_to_int i = 0’ >> fs [] >>
+ Cases_on ‘u32_sub i (int_to_u32 1)’ >> fs [] >>
+ Cases_on ‘fix nth_body1 (INL (l,a))’ >> fs [] >>
+ Cases_on ‘a'’ >> fs []
+QED
val _ = export_theory ()
diff --git a/backends/hol4/divDefProto2Theory.sig b/backends/hol4/divDefProto2Theory.sig
index 349aabf7..7ce4b194 100644
--- a/backends/hol4/divDefProto2Theory.sig
+++ b/backends/hol4/divDefProto2Theory.sig
@@ -6,25 +6,41 @@ sig
val fix_def : thm
val fix_fuel_P_def : thm
val fix_fuel_def : thm
- val ftree_TY_DEF : thm
- val ftree_case_def : thm
- val ftree_size_def : thm
val is_valid_fp_body_def : thm
+ 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
(* Theorems *)
- val datatype_ftree : thm
- val eval_ftree_compute : thm
- val eval_ftree_def : thm
- val eval_ftree_ind : thm
+ val datatype_list_t : thm
+ val fix_fixed_diverges : thm
+ val fix_fixed_eq : thm
+ val fix_fixed_terminates : thm
+ val fix_fuel_P_least : thm
val fix_fuel_compute : thm
- val ftree_11 : thm
- val ftree_Axiom : thm
- val ftree_case_cong : thm
- val ftree_case_eq : thm
- val ftree_distinct : thm
- val ftree_induction : thm
- val ftree_nchotomy : thm
- val ftree_size_eq : thm
+ val fix_fuel_eq_fix : thm
+ val fix_fuel_mono : thm
+ val fix_fuel_mono_aux : thm
+ val fix_fuel_mono_least : thm
+ val fix_fuel_not_diverge_eq_fix : thm
+ val fix_fuel_not_diverge_eq_fix_aux : thm
+ 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
+ val list_t_case_eq : thm
+ 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_def : thm
val divDefProto2_grammars : type_grammar.grammar * term_grammar.grammar
(*
@@ -47,124 +63,130 @@ sig
⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧
∀n f x. fix_fuel (SUC n) f x = f (fix_fuel n f) x
- [ftree_TY_DEF] Definition
+ [is_valid_fp_body_def] Definition
+
+ ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧
+ ∀n f.
+ is_valid_fp_body (SUC n) f ⇔
+ ∀x. (∀g h. f g x = f h x) ∨
+ ∃h y.
+ is_valid_fp_body n h ∧ ∀g. f g x = do z <- g y; h g z od
+
+ [list_t_TY_DEF] Definition
⊢ ∃rep.
TYPE_DEFINITION
(λa0'.
- ∀ $var$('ftree') $var$('@temp @ind_typedivDefProto20prod')
- $var$('@temp @ind_typedivDefProto21list').
+ ∀ $var$('list_t').
(∀a0'.
- (∃a. a0' =
- (λa.
- ind_type$CONSTR 0 (ARB,ARB)
- (ind_type$FCONS a (λn. ind_type$BOTTOM)))
- a ∧
- $var$('@temp @ind_typedivDefProto20prod') a) ∨
- (∃a. a0' =
- (λa.
- ind_type$CONSTR (SUC 0) (a,ARB)
- (λn. ind_type$BOTTOM)) a) ⇒
- $var$('ftree') a0') ∧
- (∀a1'.
(∃a0 a1.
- a1' =
+ a0' =
(λa0 a1.
- ind_type$CONSTR (SUC (SUC 0)) (ARB,a0)
+ ind_type$CONSTR 0 a0
(ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
- a0 a1 ∧
- $var$('@temp @ind_typedivDefProto21list') a1) ⇒
- $var$('@temp @ind_typedivDefProto20prod') a1') ∧
- (∀a2.
- a2 =
- ind_type$CONSTR (SUC (SUC (SUC 0))) (ARB,ARB)
- (λn. ind_type$BOTTOM) ∨
- (∃a0 a1.
- a2 =
- (λa0 a1.
- ind_type$CONSTR (SUC (SUC (SUC (SUC 0))))
- (ARB,ARB)
- (ind_type$FCONS a0
- (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
- a0 a1 ∧ $var$('ftree') a0 ∧
- $var$('@temp @ind_typedivDefProto21list') a1) ⇒
- $var$('@temp @ind_typedivDefProto21list') a2) ⇒
- $var$('ftree') a0') rep
+ a0 a1 ∧ $var$('list_t') a1) ∨
+ a0' =
+ ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
+ $var$('list_t') a0') ⇒
+ $var$('list_t') a0') rep
- [ftree_case_def] Definition
+ [list_t_case_def] Definition
- ⊢ (∀a f f1. ftree_CASE (Rec a) f f1 = f a) ∧
- ∀a f f1. ftree_CASE (NRec a) f f1 = f1 a
+ ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
+ ∀f v. list_t_CASE ListNil f v = v
- [ftree_size_def] Definition
+ [list_t_size_def] Definition
- ⊢ (∀f a. ftree_size f (Rec a) = 1 + ftree1_size f a) ∧
- (∀f a. ftree_size f (NRec a) = 1) ∧
- (∀f a0 a1. ftree1_size f (a0,a1) = 1 + ftree2_size f a1) ∧
- (∀f. ftree2_size f [] = 0) ∧
- ∀f a0 a1.
- ftree2_size f (a0::a1) = 1 + (ftree_size f a0 + ftree2_size f a1)
+ ⊢ (∀f a0 a1.
+ list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧
+ ∀f. list_t_size f ListNil = 0
- [is_valid_fp_body_def] Definition
+ [nth_body1_def] Definition
- ⊢ ∀f. is_valid_fp_body f ⇔ ∀x. ∃n ft. ∀g. f g x = eval_ftree n g ft
-
- [datatype_ftree] Theorem
-
- ⊢ DATATYPE (ftree Rec NRec)
-
- [eval_ftree_compute] Theorem
-
- ⊢ (∀x g fs. eval_ftree 0 g (fs,x) = Diverge) ∧
- (∀x n g fs.
- eval_ftree (NUMERAL (BIT1 n)) g (fs,x) =
- case x of
- INL r => r
- | INR (y,i) =>
- case g y of
- Return z =>
- (let
- f = EL i fs
- in
- eval_ftree (NUMERAL (BIT1 n) − 1) g (fs,f z))
- | Fail e => Fail e
- | Diverge => Diverge) ∧
- ∀x n g fs.
- eval_ftree (NUMERAL (BIT2 n)) g (fs,x) =
+ ⊢ ∀f x.
+ nth_body1 f x =
case x of
- INL r => r
- | INR (y,i) =>
- case g y of
- Return z =>
- (let
- f = EL i fs
- in
- eval_ftree (NUMERAL (BIT1 n)) g (fs,f z))
- | Fail e => Fail e
- | Diverge => Diverge
-
- [eval_ftree_def] Theorem
-
- ⊢ (∀x g fs. eval_ftree 0 g (fs,x) = Diverge) ∧
- ∀x n g fs.
- eval_ftree (SUC n) g (fs,x) =
+ 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
+
+ ⊢ ∀f x.
+ nth_body_valid f x =
case x of
- INL r => r
- | INR (y,i) =>
- case g y of
- Return z => (let f = EL i fs in eval_ftree n g (fs,f z))
- | Fail e => Fail e
- | Diverge => Diverge
-
- [eval_ftree_ind] Theorem
-
- ⊢ ∀P. (∀g fs x. P 0 g (fs,x)) ∧
- (∀n g fs x.
- (∀v1 y i z f.
- x = INR v1 ∧ v1 = (y,i) ∧ g y = Return z ∧ f = EL i fs ⇒
- P n g (fs,f z)) ⇒
- P (SUC n) g (fs,x)) ⇒
- ∀v v1 v2 v3. P v v1 (v2,v3)
+ 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 <- f (INL (tl,i0));
+ case r of
+ INL v => Fail Failure
+ | INR i1 => Return (INR i1)
+ od
+ | 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)
+
+ [fix_fixed_diverges] Theorem
+
+ ⊢ ∀N f.
+ is_valid_fp_body N f ⇒
+ ∀x. ¬(∃n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x
+
+ [fix_fixed_eq] Theorem
+
+ ⊢ ∀N f. is_valid_fp_body N f ⇒ ∀x. fix f x = f (fix f) x
+
+ [fix_fixed_terminates] Theorem
+
+ ⊢ ∀N f.
+ is_valid_fp_body N f ⇒
+ ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x
+
+ [fix_fuel_P_least] Theorem
+
+ ⊢ ∀f n x.
+ fix_fuel n f x ≠ Diverge ⇒
+ fix_fuel_P f x ($LEAST (fix_fuel_P f x))
[fix_fuel_compute] Theorem
@@ -176,49 +198,137 @@ sig
fix_fuel (NUMERAL (BIT2 n)) f x =
f (fix_fuel (NUMERAL (BIT1 n)) f) x
- [ftree_11] Theorem
+ [fix_fuel_eq_fix] Theorem
+
+ ⊢ ∀N f.
+ is_valid_fp_body N f ⇒
+ ∀n x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix f x
+
+ [fix_fuel_mono] Theorem
+
+ ⊢ ∀N f.
+ is_valid_fp_body N f ⇒
+ ∀n x.
+ fix_fuel_P f x n ⇒ ∀m. n ≤ m ⇒ fix_fuel n f x = fix_fuel m f x
+
+ [fix_fuel_mono_aux] Theorem
+
+ ⊢ ∀n N M g f.
+ is_valid_fp_body M f ⇒
+ is_valid_fp_body N g ⇒
+ ∀x. ¬is_diverge (g (fix_fuel n f) x) ⇒
+ ∀m. n ≤ m ⇒ g (fix_fuel n f) x = g (fix_fuel m f) x
+
+ [fix_fuel_mono_least] Theorem
+
+ ⊢ ∀N f.
+ is_valid_fp_body N f ⇒
+ ∀n x.
+ fix_fuel_P f x n ⇒
+ fix_fuel n f x = fix_fuel ($LEAST (fix_fuel_P f x)) f x
+
+ [fix_fuel_not_diverge_eq_fix] Theorem
+
+ ⊢ ∀N f.
+ is_valid_fp_body N f ⇒
+ ∀n x.
+ f (fix_fuel n f) x ≠ Diverge ⇒ f (fix f) x = f (fix_fuel n f) x
+
+ [fix_fuel_not_diverge_eq_fix_aux] Theorem
+
+ ⊢ ∀N M g f.
+ is_valid_fp_body M f ⇒
+ is_valid_fp_body N g ⇒
+ ∀n x.
+ g (fix_fuel n f) x ≠ Diverge ⇒ g (fix f) x = g (fix_fuel n f) x
+
+ [fix_not_diverge_implies_fix_fuel] Theorem
+
+ ⊢ ∀N f.
+ is_valid_fp_body N f ⇒
+ ∀x. f (fix f) x ≠ Diverge ⇒ ∃n. f (fix f) x = f (fix_fuel n f) x
+
+ [fix_not_diverge_implies_fix_fuel_aux] Theorem
+
+ ⊢ ∀N M g f.
+ is_valid_fp_body M f ⇒
+ is_valid_fp_body N g ⇒
+ ∀x. g (fix f) x ≠ Diverge ⇒
+ ∃n. g (fix f) x = g (fix_fuel n f) x ∧
+ ∀m. n ≤ m ⇒ g (fix_fuel m f) x = g (fix_fuel n f) x
+
+ [is_valid_fp_body_compute] Theorem
+
+ ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧
+ (∀n f.
+ is_valid_fp_body (NUMERAL (BIT1 n)) f ⇔
+ ∀x. (∀g h. f g x = f h x) ∨
+ ∃h y.
+ is_valid_fp_body (NUMERAL (BIT1 n) − 1) h ∧
+ ∀g. f g x = do z <- g y; h g z od) ∧
+ ∀n f.
+ is_valid_fp_body (NUMERAL (BIT2 n)) f ⇔
+ ∀x. (∀g h. f g x = f h x) ∨
+ ∃h y.
+ 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'.
+ ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
+
+ [list_t_Axiom] Theorem
+
+ ⊢ ∀f0 f1. ∃fn.
+ (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧
+ fn ListNil = f1
+
+ [list_t_case_cong] Theorem
- ⊢ (∀a a'. Rec a = Rec a' ⇔ a = a') ∧ ∀a a'. NRec a = NRec a' ⇔ a = a'
+ ⊢ ∀M M' f v.
+ M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
+ (M' = ListNil ⇒ v = v') ⇒
+ list_t_CASE M f v = list_t_CASE M' f' v'
- [ftree_Axiom] Theorem
+ [list_t_case_eq] Theorem
- ⊢ ∀f0 f1 f2 f3 f4. ∃fn0 fn1 fn2.
- (∀a. fn0 (Rec a) = f0 a (fn1 a)) ∧ (∀a. fn0 (NRec a) = f1 a) ∧
- (∀a0 a1. fn1 (a0,a1) = f2 a0 a1 (fn2 a1)) ∧ fn2 [] = f3 ∧
- ∀a0 a1. fn2 (a0::a1) = f4 a0 a1 (fn0 a0) (fn2 a1)
+ ⊢ list_t_CASE x f v = v' ⇔
+ (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
- [ftree_case_cong] Theorem
+ [list_t_distinct] Theorem
- ⊢ ∀M M' f f1.
- M = M' ∧ (∀a. M' = Rec a ⇒ f a = f' a) ∧
- (∀a. M' = NRec a ⇒ f1 a = f1' a) ⇒
- ftree_CASE M f f1 = ftree_CASE M' f' f1'
+ ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
- [ftree_case_eq] Theorem
+ [list_t_induction] Theorem
- ⊢ ftree_CASE x f f1 = v ⇔
- (∃p. x = Rec p ∧ f p = v) ∨ ∃f'. x = NRec f' ∧ f1 f' = v
+ ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
- [ftree_distinct] Theorem
+ [list_t_nchotomy] Theorem
- ⊢ ∀a' a. Rec a ≠ NRec a'
+ ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
- [ftree_induction] Theorem
+ [nth_body_valid_eq] Theorem
- ⊢ ∀P0 P1 P2.
- (∀p. P1 p ⇒ P0 (Rec p)) ∧ (∀f. P0 (NRec f)) ∧
- (∀l. P2 l ⇒ ∀f. P1 (f,l)) ∧ P2 [] ∧
- (∀f l. P0 f ∧ P2 l ⇒ P2 (f::l)) ⇒
- (∀f. P0 f) ∧ (∀p. P1 p) ∧ ∀l. P2 l
+ ⊢ nth_body_valid = nth_body1
- [ftree_nchotomy] Theorem
+ [nth_body_valid_is_valid] Theorem
- ⊢ ∀ff. (∃p. ff = Rec p) ∨ ∃f. ff = NRec f
+ ⊢ is_valid_fp_body (SUC (SUC 0)) nth_body_valid
- [ftree_size_eq] Theorem
+ [nth_def] Theorem
- ⊢ ftree1_size f = pair_size (λv. 0) (list_size (ftree_size f)) ∧
- ftree2_size f = list_size (ftree_size f)
+ ⊢ ∀ls i.
+ nth ls i =
+ case ls of
+ ListCons x tl =>
+ if u32_to_int i = 0 then Return x
+ else do i0 <- u32_sub i (int_to_u32 1); nth tl i0 od
+ | ListNil => Fail Failure
*)