David, Phil,
Phil's post gives a nice little introduction to programming with conversions
(things like plus_1_conv) and conversionals (functions that create new
conversions from old like THEN_C). Phil's conversion is focussed and efficient.
Going for comfort rather than speed, an alternative is to prove a theorem that
recasts the recursion equations into a form that can be used as a rewrite rule.
This gives a cheap and cheerful solution which isn't much more complicated to
code than rewriting with the definition of the length function (where the the
problem with numeric literals doesn't arise, because despite appearances[1; 2;
3] does match the pattern Cons h t). See my code below.
Regards,
Rob.
open_theory "hol"; new_theory "t";
set_pc"basic_hol1"; (* say, see comments on all_summ_conv below *)
(*
Define summ as David did.
*)
ⓈHOLCONST
│ summ : ℕ → ℕ
├──────
│ summ 0 = 0
│ ∧ ∀n⦁ summ (n + 1) = summ n + n + 1
■
(*
Get an ML name for the defining theorem.
*)
val summ_def = get_spec⌜summ⌝;
(*
Prove a theorem recasting the recursion equations as a rewrite rule.
*)
set_goal([], ⌜∀n⦁ summ n = if n = 0 then 0 else summ (n - 1) + n⌝);
a(REPEAT strip_tac);
a(induction_tac⌜n:ℕ⌝ THEN rewrite_tac[summ_def]);
val summ_thm = save_thm("summ_thm", pop_thm());
(*
Result:
val summ_thm = ⊢ ∀ n⦁ summ n = (if n = 0 then 0 else summ (n - 1) + n): THM
*)
(*
The following conversion will simplify all subterms of the form ⌜summ n⌝
where n is a numeric literal on the assumption that the current proof context
(like basic_hol1) includes 'ℕ_lit (so it simplifies natural number arithmetic
expressions involving literals automatically).
The conversion repeatedly attempts to use summ_thm once as a rewrite rule
followed by rewriting with what is built into the proof context (to perform
arithmetic simplications and to simplify the if-then-else terms).
(You can use PC_C1 to force the conversion to use your choice of proof context,
if you want something that is a bit more general-purpose.)
*)
val all_summ_conv = REPEAT_C (once_rewrite_conv[summ_thm] THEN_C
rewrite_conv[]);
val egs = map all_summ_conv [⌜summ 0⌝, ⌜summ 1⌝, ⌜summ 2⌝, ⌜summ 42 + summ
99⌝];
(*
Result:
val egs = [⊢ summ 0 = 0, ⊢ summ 1 = 1, ⊢ summ 2 = 3, ⊢ summ 42 + summ 99 =
5853]: THM list
*)
> On 31 Mar 2020, at 20:36, Phil Clayton <[email protected]> wrote:
>
> The problem is that ⌜n + 1⌝ can't be matched with a numeric literal. It may
> be possible to add such a matching capability but this is easily worked
> around by converting the operand first. For a numeric literal, as in your
> example, plus1_conv can be used. With this, you can build up a conversion
> evaluate your summ function. I've included my steps below to build up such a
> conversion. Hopefully you can see what's going on at each step.
>
> Phil
>
>
> (* Use plus1_conv to get the operand in the right form *)
>
> plus1_conv ⌜3⌝;
> (*
> * val it = ⊢ 3 = 2 + 1: THM
> *)
>
> (* Convert the argument if non-zero then rewrite *)
>
> (RAND_C (TRY_C plus1_conv) THEN_C pure_once_rewrite_conv [get_spec ⌜summ⌝])
> ⌜summ 0⌝;
> (RAND_C (TRY_C plus1_conv) THEN_C pure_once_rewrite_conv [get_spec ⌜summ⌝])
> ⌜summ 3⌝;
> (*
> * val it = ⊢ summ 0 = 0: THM
> * val it = ⊢ summ 3 = summ 2 + 2 + 1: THM
> *)
>
> (* Give this conversion a name and define a conversion that
> * recursively applies it to the left operand of the resulting
> * '+' term until is fails *)
>
> val summ_step_conv =
> RAND_C (TRY_C plus1_conv) THEN_C pure_once_rewrite_conv [get_spec ⌜summ⌝];
> fun summ_conv t = (summ_step_conv THEN_TRY_C LEFT_C summ_conv) t;
>
> summ_conv ⌜summ 0⌝;
> summ_conv ⌜summ 3⌝;
> (*
> * val it = ⊢ summ 0 = 0: THM
> * val it = ⊢ summ 3 = ((0 + 0 + 1) + 1 + 1) + 2 + 1: THM
> *)
>
> (* Add up the resulting '+' tree *)
>
> (summ_conv THEN_C MAP_C plus_conv) ⌜summ 3⌝;
> (*
> * val it = ⊢ summ 3 = 6: THM
> *)
>
>
> (* We want summ_conv to reduce the '+' terms so sum as we go.
> * Redefine the above. *)
>
> val summ_step_conv =
> RAND_C (TRY_C plus1_conv) THEN_C pure_once_rewrite_conv [get_spec ⌜summ⌝]
> THEN_C TRY_C (RIGHT_C plus_conv);
>
> summ_step_conv ⌜summ 0⌝;
> summ_step_conv ⌜summ 3⌝;
> (*
> * val it = ⊢ summ 0 = 0: THM
> * val it = ⊢ summ 3 = summ 2 + 3: THM
> *)
>
> fun summ_conv t =
> (summ_step_conv THEN_TRY_C (LEFT_C summ_conv THEN_C plus_conv)) t;
>
> summ_conv ⌜summ 0⌝;
> summ_conv ⌜summ 3⌝;
> (*
> * val it = ⊢ summ 0 = 0: THM
> * val it = ⊢ summ 3 = 6: THM
> *)
>
> map summ_conv (map (fn n => mk_app (⌜summ⌝, mk_ℕ (integer_of_int n)))
> (interval 0 50));
> (*
> * val it =
> * [⊢ summ 0 = 0, ⊢ summ 1 = 1, ⊢ summ 2 = 3, ⊢ summ 3 = 6,
> * ⊢ summ 4 = 10, ⊢ summ 5 = 15, ⊢ summ 6 = 21, ⊢ summ 7 = 28,
> * ⊢ summ 8 = 36, ⊢ summ 9 = 45, ⊢ summ 10 = 55,
> * ⊢ summ 11 = 66, ⊢ summ 12 = 78, ⊢ summ 13 = 91,
> * ⊢ summ 14 = 105, ⊢ summ 15 = 120, ⊢ summ 16 = 136,
> * ⊢ summ 17 = 153, ⊢ summ 18 = 171, ⊢ summ 19 = 190,
> * ⊢ summ 20 = 210, ⊢ summ 21 = 231, ⊢ summ 22 = 253,
> * ⊢ summ 23 = 276, ⊢ summ 24 = 300, ⊢ summ 25 = 325,
> * ⊢ summ 26 = 351, ⊢ summ 27 = 378, ⊢ summ 28 = 406,
> * ⊢ summ 29 = 435, ⊢ summ 30 = 465, ⊢ summ 31 = 496,
> * ⊢ summ 32 = 528, ⊢ summ 33 = 561, ⊢ summ 34 = 595,
> * ⊢ summ 35 = 630, ⊢ summ 36 = 666, ⊢ summ 37 = 703,
> * ⊢ summ 38 = 741, ⊢ summ 39 = 780, ⊢ summ 40 = 820,
> * ⊢ summ 41 = 861, ⊢ summ 42 = 903, ⊢ summ 43 = 946,
> * ⊢ summ 44 = 990, ⊢ summ 45 = 1035, ⊢ summ 46 = 1081,
> * ⊢ summ 47 = 1128, ⊢ summ 48 = 1176, ⊢ summ 49 = 1225,
> * ⊢ summ 50 = 1275]: THM list
> *)
>
>
> On 31/03/20 17:09, David Topham wrote:
>> I have been able to get the length sample for HOLCONST from user013 to
>> work, but when I try
>> my own function, I get an error. Can anyone see what my problem is?
>> I suspect it may be setting the correct proof context since I needed to add
>> set_pc "hol2"
>> to get the length function to work. I have tried several contexts such as
>> "lin_arith", "R", "misc", but I have not seen how to find the correct one
>> (if that is even the problem).
>> This one OK:
>> :) force_delete_theory "cs113" handle Fail _ => ();
>> val it = (): unit
>> :) open_theory "hol"; new_theory "cs113";
>> val it = (): unit
>> val it = (): unit
>> :) set_pc "hol2";
>> val it = (): unit
>> :) ⓈHOLCONST
>> :# │ length:'a LIST→ℕ
>> :# ├──
>> :# │ length [] = 0
>> :# │ ∧ ∀ h t⦁ length (Cons h t) = length t + 1
>> :# │
>> :# ■
>> val it = ⊢ length [] = 0 ∧ (∀ h t⦁ length (Cons h t) = length t + 1): THM
>> :) get_spec⌜length⌝;
>> val it = ⊢ length [] = 0 ∧ (∀ h t⦁ length (Cons h t) = length t + 1): THM
>> :) rewrite_conv[get_spec⌜length⌝] ⌜length [1;2;3;4]⌝;
>> val it = ⊢ length [1; 2; 3; 4] = 4: THM
>> But not this one:
>> :) ⓈHOLCONST
>> :# │ summ:ℕ→ℕ
>> :# ├──
>> :# │ summ 0 = 0
>> :# │ ∧ ∀n⦁ summ (n + 1) = (summ n) + (n + 1)
>> :# │
>> :# ■
>> val it = ⊢ summ 0 = 0 ∧ (∀ n⦁ summ (n + 1) = summ n + n + 1): THM
>> :# get_spec⌜summ⌝;
>> val it = ⊢ summ 0 = 0 ∧ (∀ n⦁ summ (n + 1) = summ n + n + 1): THM
>> :) rewrite_conv[get_spec⌜summ⌝] ⌜summ 2⌝;
>> Exception Fail * no rewriting occurred [rewrite_conv.26001] * raised
>> _______________________________________________
>> Proofpower mailing list
>> [email protected]
>> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
>
> _______________________________________________
> Proofpower mailing list
> [email protected]
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
