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.

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

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?

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

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

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