Stream: Beginner Questions

Topic: IMP Hoare logic

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?

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)}
``````

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?

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?

Mathias Fleury (Mar 10 2022 at 08:38):

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

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: Feb 27 2024 at 08:17 UTC