Thank you Roger for those additional suggestions. I am still trying to wrap my head around how to apply them, and I have looked at USR013 but don't quite see an example that shows me how to do this kind of equational derivation (yet). I have an attempt in the attached link, but I know that (similar to earlier attempts), I have trouble turning my TERMs into THMs, which is what I need in order to use the deduction theorem. I don't think my L3 through L8 are in the right format...somehow they should be THMs, not TERMS. But what format would that be? Is it some sort of substitution of equals? -Dave https://www.dropbox.com/s/ifxxtsp8tpp1f6j/induction.PNG?dl=0
On Fri, Apr 3, 2015 at 6:37 AM, Roger Bishop Jones <[email protected]> wrote: > On 31/03/15 22:39, David Topham wrote: > > I have been studying the idea of "equational logic" as described in this > link by Gries and wonder if anyone has used ProofPower in this way. If so, > I would love to see a sample. > >> One reason for my interest in this approach is because it seems more in >> line with proof by induction (which is a major topic of Discrete Math). >> For example, to prove that 2^n > n^2 for n >= 4 using induction seems >> like it would be clearest using equational logic. >> -Dave >> >> I looked closer at the rules specified by Gries and came up with > some > further suggestions as follows. > > Substitution: > > Provided x is not free in the assumptions then > you can use ∀_intro followed by ∀_elim. > > Leibniz: > > You could start with refl_conv to get |- E[P] = E[P] > then use subst_rule to substitute the Q for some instance of P. > > Alternatively use app_fun_rule, something like: > > fun leibniz_rule t = ((conv_rule (TRY_C(TOP_MAP_C β_conv)))) o > (app_fun_rule t); > > leibniz_rule (λx.E) (asm_rule (P ⇔ Q)); > > Transitivity: - see eq_trans_rule > > Equanimity: ⇔_mp_rule > > You will find as you get into things more complex than the propositional > calculus that the penalty for using forward proof increases and things > can get quite cumbersome. > Typically in a goal oriented proof sight of the goal will allow the > tactics to work out details themselves which in a forward proof > you may have to specify in detail yourself, e.g. exactly which occurrences > of some expression need to be substituted for. > > Roger Jones >
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
