diff options
| -rw-r--r-- | backends/hol4/divDefProto2Script.sml | 527 | ||||
| -rw-r--r-- | backends/hol4/divDefProto2Theory.sig | 400 |
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 *) |