Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Induction with Case Analysis

Email Gateway (Aug 22 2022 at 17:06):

From: Jun Inoue <jun.lambda@gmail.com>
Dear all,

Is there a good way to induct and case-analyze (like the cases method)
simultaneously? Here's a stripped down example using a fragment of
propositional logic:

{* begin example *}
theory PropLogic
imports Main
begin

datatype formula =
Atomic string ("^_" [150])
| Not formula
| And formula formula (infix "&&" 80)
| Or formula formula (infix "||" 70)

abbreviation flip_insert (infixl "." 60) where
"Γ . A ≡ insert A Γ"

(* ⊢ Γ means at least one formula in Γ is true *)
inductive derivation :: "formula set ⇒ bool" ("⊢ _" [30] 30) where
Assm: "⊢ Γ . Not A . A"
| AndI: "⟦ ⊢ Γ . A; ⊢ Γ . B ⟧ ⟹ ⊢ Γ . A && B"
| OrI: "⟦ ⊢ Γ . A . B ⟧ ⟹ ⊢ Γ . A || B"

lemma strong_inversion_And:
assumes "⊢ Γ . A && B"
shows "⊢ Γ . A"
using assms
apply (induct rule: derivation.induct)
{* end example *}

Here, my goal is to prove something like inversion for conjunction,
but the A && B may not have been introduced by the last rule used in
the derivation, so it requires induction.

Unfortunately, because the premise I'm inducting on (⊢ Γ . A && B) has
a parameter of a very specific shape, the higher-order unifier can't
infer an appropriate instantiation of the derivation.induct, giving a
useless goal state:

1. ⋀Γ' Aa. ⊢ Γ . A
2. ⋀Γ' Aa B. ⊢ Γ' . Aa ⟹ ⊢ Γ . A ⟹ ⊢ Γ' . B ⟹ ⊢ Γ . A ⟹ ⊢ Γ . A
3. ⋀Γ' Aa B. ⊢ Γ' . Aa . B ⟹ ⊢ Γ . A ⟹ ⊢ Γ . A

The first subgoal is the very lemma I'm trying to prove. I rather
need something like

⋀Γ' Aa. ⟦ Γ . A = Γ' . Not Aa . Aa⟧ ⟹ ⊢ Γ . A

Using apply(induct rule: derivation.cases) instead of induct does give
something like this, but then in the other subgoals I won't have an
inductive hypothesis.

How can I get around this problem? Is there a method or attribute
that can combine cases and induct?

Email Gateway (Aug 22 2022 at 17:06):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hello Jun,

you can specify the instantiation to perform to the induction method, for example:

apply (induction "Γ . A && B" rule: derivation.induct)

However, I am not sure whether this helps you to perform the proof, since it gives you another non-trivial goal:

⋀Γ' Aa. Γ' . formula.Not Aa . Aa = Γ . A && B ⟹ ⊢ Γ . A

Using apply(induct rule: derivation.cases) instead of induct does give
something like this, but then in the other subgoals I won't have an
inductive hypothesis.

How can I get around this problem? Is there a method or attribute
that can combine cases and induct?

You can also write your own induction rule.

Unless there are more rules that you have not shown, I am not sure that your theorem holds, because you have no semantic of Not in your predicate derivation: I expect ‹⊢ {} . formula.Not (A || B) . A› to be true in propositional logic, but you can't derive this from your predicate "derivation".

Best,
Mathias

On 21. Apr 2018, at 19:54, Jun Inoue <jun.lambda@gmail.com> wrote:

Dear all,

Is there a good way to induct and case-analyze (like the cases method)
simultaneously? Here's a stripped down example using a fragment of
propositional logic:

{* begin example *}
theory PropLogic
imports Main
begin

datatype formula =
Atomic string ("^_" [150])
| Not formula
| And formula formula (infix "&&" 80)
| Or formula formula (infix "||" 70)

abbreviation flip_insert (infixl "." 60) where
"Γ . A ≡ insert A Γ"

(* ⊢ Γ means at least one formula in Γ is true *)
inductive derivation :: "formula set ⇒ bool" ("⊢ _" [30] 30) where
Assm: "⊢ Γ . Not A . A"
| AndI: "⟦ ⊢ Γ . A; ⊢ Γ . B ⟧ ⟹ ⊢ Γ . A && B"
| OrI: "⟦ ⊢ Γ . A . B ⟧ ⟹ ⊢ Γ . A || B"

lemma strong_inversion_And:
assumes "⊢ Γ . A && B"
shows "⊢ Γ . A"
using assms
apply (induct rule: derivation.induct)
{* end example *}

Here, my goal is to prove something like inversion for conjunction,
but the A && B may not have been introduced by the last rule used in
the derivation, so it requires induction.

Unfortunately, because the premise I'm inducting on (⊢ Γ . A && B) has
a parameter of a very specific shape, the higher-order unifier can't
infer an appropriate instantiation of the derivation.induct, giving a
useless goal state:

1. ⋀Γ' Aa. ⊢ Γ . A
2. ⋀Γ' Aa B. ⊢ Γ' . Aa ⟹ ⊢ Γ . A ⟹ ⊢ Γ' . B ⟹ ⊢ Γ . A ⟹ ⊢ Γ . A
3. ⋀Γ' Aa B. ⊢ Γ' . Aa . B ⟹ ⊢ Γ . A ⟹ ⊢ Γ . A

The first subgoal is the very lemma I'm trying to prove. I rather
need something like

⋀Γ' Aa. ⟦ Γ . A = Γ' . Not Aa . Aa⟧ ⟹ ⊢ Γ . A

Using apply(induct rule: derivation.cases) instead of induct does give
something like this, but then in the other subgoals I won't have an
inductive hypothesis.

How can I get around this problem? Is there a method or attribute
that can combine cases and induct?

--
Jun Inoue

Email Gateway (Aug 22 2022 at 17:07):

From: Jun Inoue <jun.lambda@gmail.com>
Hello Mathias,

Yes, that's exactly what I was looking for! Thank you!

On Sun, Apr 22, 2018 at 5:50 PM, Mathias Fleury
<mathias.fleury12@gmail.com> wrote:

Hello Jun,

you can specify the instantiation to perform to the induction method, for
example:

apply (induction "Γ . A && B" rule: derivation.induct)

However, I am not sure whether this helps you to perform the proof, since it
gives you another non-trivial goal:

⋀Γ' Aa. Γ' . formula.Not Aa . Aa = Γ . A && B ⟹ ⊢ Γ . A

Using apply(induct rule: derivation.cases) instead of induct does give
something like this, but then in the other subgoals I won't have an
inductive hypothesis.

How can I get around this problem? Is there a method or attribute
that can combine cases and induct?

You can also write your own induction rule.

Unless there are more rules that you have not shown, I am not sure that your
theorem holds, because you have no semantic of Not in your predicate
derivation: I expect ‹⊢ {} . formula.Not (A || B) . A› to be true in
propositional logic, but you can't derive this from your predicate
"derivation".

That's right, what I showed was meant as a stripped down, (nearly)
minimal example, including just enough rules to make it desirable to
combine case analysis and induction. The actual development I'm
working on has lots more stuff that I didn't want to force people to
wade through. My apologies for the awkwardness.

Best,
Mathias

On 21. Apr 2018, at 19:54, Jun Inoue <jun.lambda@gmail.com> wrote:

Dear all,

Is there a good way to induct and case-analyze (like the cases method)
simultaneously? Here's a stripped down example using a fragment of
propositional logic:

{* begin example *}
theory PropLogic
imports Main
begin

datatype formula =
Atomic string ("^_" [150])
| Not formula
| And formula formula (infix "&&" 80)
| Or formula formula (infix "||" 70)

abbreviation flip_insert (infixl "." 60) where
"Γ . A ≡ insert A Γ"

(* ⊢ Γ means at least one formula in Γ is true *)
inductive derivation :: "formula set ⇒ bool" ("⊢ _" [30] 30) where
Assm: "⊢ Γ . Not A . A"
| AndI: "⟦ ⊢ Γ . A; ⊢ Γ . B ⟧ ⟹ ⊢ Γ . A && B"
| OrI: "⟦ ⊢ Γ . A . B ⟧ ⟹ ⊢ Γ . A || B"

lemma strong_inversion_And:
assumes "⊢ Γ . A && B"
shows "⊢ Γ . A"
using assms
apply (induct rule: derivation.induct)
{* end example *}

Here, my goal is to prove something like inversion for conjunction,
but the A && B may not have been introduced by the last rule used in
the derivation, so it requires induction.

Unfortunately, because the premise I'm inducting on (⊢ Γ . A && B) has
a parameter of a very specific shape, the higher-order unifier can't
infer an appropriate instantiation of the derivation.induct, giving a
useless goal state:

1. ⋀Γ' Aa. ⊢ Γ . A
2. ⋀Γ' Aa B. ⊢ Γ' . Aa ⟹ ⊢ Γ . A ⟹ ⊢ Γ' . B ⟹ ⊢ Γ . A ⟹ ⊢ Γ . A
3. ⋀Γ' Aa B. ⊢ Γ' . Aa . B ⟹ ⊢ Γ . A ⟹ ⊢ Γ . A

The first subgoal is the very lemma I'm trying to prove. I rather
need something like

⋀Γ' Aa. ⟦ Γ . A = Γ' . Not Aa . Aa⟧ ⟹ ⊢ Γ . A

Using apply(induct rule: derivation.cases) instead of induct does give
something like this, but then in the other subgoals I won't have an
inductive hypothesis.

How can I get around this problem? Is there a method or attribute
that can combine cases and induct?

--
Jun Inoue

Last updated: Nov 21 2024 at 12:39 UTC