Stream: Beginner Questions

Topic: IMP Hoare logic

view this post on Zulip Hamed Hajisadeghian (Feb 27 2022 at 15:33):

Hi, I'm trying to prove this lemma :

lemma "⊢{λs. (s ''a'' = n) ∧ (s ''b'' = m) ∧ (n > 0) ∧ (m > 0)} wgcd {λs. s ''a'' = gcd n m}"

where gcd is the default gcd function and wgcd is imperative version of gcd algorithm written in IMP (I added Sub and Or to syntax and semantics and they work fine):

abbreviation "wgcd ==
  WHILE (Or (Less (V ''b'') (V ''a'')) (Less (V ''a'') (V ''b'')))
  DO (IF (Less (V ''b'') (V ''a'')) THEN
         (''a'' ::= Sub (V ''a'') (V ''b''))
      ELSE
         (''b'' ::= Sub (V ''b'') (V ''a'')))"

I wrote :

apply (rule While'[where P = "(λs. (s ''a'' > 0 ∧ s ''b'' > 0 ∧  gcd n m = gcd (s ''a'') (s ''b'')))"])

but it fails to apply proof method:

proof (prove)
goal (1 subgoal):
 1. ⊢ {λs. s ''a'' = n ∧ s ''b'' = m ∧ 0 < n ∧ 0 < m} wgcd {λs. s ''a'' = hoare_test.gcd n m}
Failed to apply proof method⌂:
goal (1 subgoal):
 1. ⊢ {λs. s ''a'' = n ∧ s ''b'' = m ∧ 0 < n ∧ 0 < m} wgcd {λs. s ''a'' = hoare_test.gcd n m}

What's the problem? is it precondition and postcondition or the invariant?
Thanks for your help in advance.

view this post on Zulip Simon Roßkopf (Feb 27 2022 at 16:29):

The precondition in the rule you want to apply does unify with the one in your goal. To compare the two:

{λs. 0 < s ''a'' ∧ 0 < s ''b'' ∧ gcd n m = gcd (s ''a'') (s ''b'')}
{λs. (s ''a'' = n) ∧ (s ''b'' = m) ∧ (n > 0) ∧ (m > 0)}

view this post on Zulip Hamed Hajisadeghian (Mar 10 2022 at 08:27):

I changed the loop invariant to unify with goal:

lemma "⊢{λs. s ''a'' = n ∧ s ''b'' = m ∧ n > 0 ∧ m > 0 ∧ (gcd (s ''a'') (s ''b'') = gcd (n) (m))}
        WHILE (Or (Less (V ''b'') (V ''a'')) (Less (V ''a'') (V ''b'')))
        DO (IF (Less (V ''b'') (V ''a'')) THEN
               (''a'' ::= Sub (V ''a'') (V ''b''))
            ELSE
               (''b'' ::= Sub (V ''b'') (V ''a'')))
        {λs. s ''a'' = gcd (s ''A'') (s ''B'')}"
  apply (rule While'[where P = "λs. s ''a'' = n ∧ s ''b'' = m ∧ 0 < n ∧ 0 < m ∧ gcd (s ''a'') (s ''b'') = gcd n m"])
  apply auto
    apply (rule Assign')
    apply auto
    prefer 2
    apply (rule Assign')
  apply auto

and now subgoals are:

proof (prove)
goal (3 subgoals):
 1. ⋀s. 0 < s ''a'' ⟹ m = s ''b'' ⟹ n = s ''a'' ⟹ s ''a'' < s ''b'' ⟹ False
 2. ⋀s. 0 < s ''b'' ⟹ m = s ''b'' ⟹ n = s ''a'' ⟹ s ''b'' < s ''a'' ⟹ False
 3. ⋀s. n = s ''a'' ⟹ m = s ''a'' ⟹ 0 < s ''a'' ⟹ s ''b'' = s ''a'' ⟹ s ''a'' = gcd (s ''A'') (s ''B'')

How should I continue? I also tried this definition from Arith2 library instead of default definition from GCD library:

definition cd :: "[nat, nat, nat] ⇒ bool"
  where "cd x m n ⟷ x dvd m ∧ x dvd n"

definition gcd :: "[nat, nat] ⇒ nat"
  where "gcd m n = (SOME x. x>0 ∧ cd x m n & (∀y.(cd y m n) ⟶ y dvd x))"

Which one should I use? should I define it myself?

view this post on Zulip Mathias Fleury (Mar 10 2022 at 08:37):

When trying to prove false you have to ask yourself: are my assumptions contradictory? Or is my goal false?

view this post on Zulip Mathias Fleury (Mar 10 2022 at 08:38):

Here the assumptions do not seem contradictory, so your goal is most likely false

view this post on Zulip Mathias Fleury (Mar 10 2022 at 08:39):

Your question really looks like an homework, so I don't want to spoil the fun of finding why the goal is false

Last updated: Apr 19 2024 at 20:15 UTC