Stream: Beginner Questions

Topic: Proving lemma about IMP codes


view this post on Zulip Hamed Hajisadeghian (Oct 06 2021 at 20:12):

Hi, I've been reading IMP section from concrete-semantics up to Small-Step Semantics, I defined syntax and semantics for Irem which acts like mod operator. I wanted to prove following lemma about equivalence of imperative and declarative way of calculating gcd:

lemma "{map t [''m'', ''n'', ''M'', ''N'', ''c''] |t.
  (''M''::= V ''m'';;
   ''N''::= V ''n'';;
   WHILE Less (N 0) (V ''N'') DO
   (
       ''c'' ::= V ''M'';;
       ''M'' ::= V ''N'';;
       ''N'' ::= Irem (V ''c'') (V ''N'')
   ),
   <''m'' := m, ''n'' := n, ''M'' := 0, ''N'' := 0, ''c'' := 0>) ⇒ t} = {[m, n, (gcd m n), 0, (n - (gcd m n))]}"

How to prove this lemma or is there a better way of implementing imperative algorithms and proving their correctness (specially the equivalence of imperative and declarative form)? Thanks for your help.

view this post on Zulip Simon Wimmer (Nov 09 2021 at 14:01):

Hamed Hajisadeghian said:

Hi, I've been reading IMP section from concrete-semantics up to Small-Step Semantics, I defined syntax and semantics for Irem which acts like mod operator. I wanted to prove following lemma about equivalence of imperative and declarative way of calculating gcd:

lemma "{map t [''m'', ''n'', ''M'', ''N'', ''c''] |t.
  (''M''::= V ''m'';;
   ''N''::= V ''n'';;
   WHILE Less (N 0) (V ''N'') DO
   (
       ''c'' ::= V ''M'';;
       ''M'' ::= V ''N'';;
       ''N'' ::= Irem (V ''c'') (V ''N'')
   ),
   <''m'' := m, ''n'' := n, ''M'' := 0, ''N'' := 0, ''c'' := 0>) ⇒ t} = {[m, n, (gcd m n), 0, (n - (gcd m n))]}"

How to prove this lemma or is there a better way of implementing imperative algorithms and proving their correctness (specially the equivalence of imperative and declarative form)? Thanks for your help.

Hi Hamed,

you could try to prove this by induction. But then you would need to generalize your statement first and then you probably would use an induction on the value of V "N". However, this will likely be tedious.
If you read on in the book and eventually get to the chapter on Hoare logic, you will have the proper tools to prove your statement :)


Last updated: Jul 15 2022 at 23:21 UTC