Stream: Beginner Questions

Topic: Isar proof of conjunctions not working

Chengsong Tan (Feb 05 2024 at 12:43):

Hi,

I was trying to prove a lemma with many conjuncts: P ==> a /\ b /\ c ....
I was wondering if there's a nice way in Isar that allows me to prove each conjunct as a subgoal in a localised way.
I tried to follow

lemma my_lemma: "A ∧ B  ⟹ B ∧ A"
proof -
  assume  "A ∧ B " thus "B" ..
next
  assume "A ∧ B" thus "A" ..
qed

from the textbook of Isar (https://courses.grainger.illinois.edu/cs576/sp2015/doc/isar-overview.pdf)
however it doesn't work.
Isabelle says "failed to refine any pending goal" on the thus keyword.
Any ideas how to fix this?

Best wishes,
Chengsong

Mathias Fleury (Feb 05 2024 at 12:47):

Remove the "-" after proof.

Mathias Fleury (Feb 05 2024 at 12:48):

The hyphen means "do not anything to my goal". Hence the conjuction is not split.

Chengsong Tan (Feb 05 2024 at 14:55):

Mathias Fleury said:

The hyphen means "do not anything to my goal". Hence the conjuction is not split.

Thanks Mathias! I am now trying this:

lemma my_lemma: "A ∧ B ∧ C ⟹ B ∧ A ∧ C"
proof
  assume  "A ∧ B ∧ C " thus "B" by simp
next
  assume "A ∧ B ∧ C" thus "A" by simp
qed

However the second thus already gives a "not able to refine any pending goal" error.

Mathias Fleury (Feb 05 2024 at 16:23):

the standard rule use by proof is applied only once, splitting only one conjunction, not two

Mathias Fleury (Feb 05 2024 at 16:23):

If you look at the state panel you will see exactly what comes out of the default rule

Mathias Fleury (Feb 05 2024 at 16:24):

lemma my_lemma: "A ∧ B ∧ C ⟹ B ∧ A ∧ C"
proof (intro conjI)
  assume  "A ∧ B ∧ C " thus "B" by simp
next
  assume "A ∧ B ∧ C" thus "A" by simp
next
  assume "A ∧ B ∧ C" thus "C" by simp
qed

Chengsong Tan (Feb 06 2024 at 01:44):

Mathias Fleury said:

the standard rule use by proof is applied only once, splitting only one conjunction, not two

Thank you! That makes sense.

Last updated: Dec 21 2024 at 16:20 UTC