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 <postmas...@rbjones.com>
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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to