Stream: Beginner Questions

Topic: Order of conjuncts of induction principle

Yiming Xu (Oct 21 2024 at 05:45):

I found the induction principles in Isabelle is not my favorite form, say, for transitive closure

(?x1.0, ?x2.0) ∈ ?r⇧+ ⟹
(⋀a b. (a, b) ∈ ?r ⟹ ?P a b) ⟹
(⋀a b c. (a, b) ∈ ?r⇧+ ⟹ ?P a b ⟹ (b, c) ∈ ?r ⟹ ?P a c) ⟹ ?P ?x1.0 ?x2.0

What I like instead is:

(⋀a b. (a, b) ∈ ?r ⟹ ?P a b) ⟹
(⋀a b c. (a, b) ∈ ?r⇧+ ⟹ ?P a b ⟹ (b, c) ∈ ?r ⟹ ?P a c) ⟹
(?x1.0, ?x2.0) ∈ ?r⇧+ ⟹ ?P ?x1.0 ?x2.0

When proving theorems, my goal usually looks like "(?x1.0, ?x2.0) ∈ ?r⇧+ ⟹ ?P ?x1.0 ?x2.0", so I would like Isabelle to ask me to prove:

(⋀a b. (a, b) ∈ ?r ⟹ ?P a b)  &&&
(⋀a b c. (a, b) ∈ ?r⇧+ ⟹ ?P a b ⟹ (b, c) ∈ ?r ⟹ ?P a c)

Reflected in the proof procedure. Applying this principle gives me:

1. ⋀a b. (t1, t2) ∈ (gen_birel Op (unrav_rel Op R))⇧+ ⟹
           (a, b) ∈ gen_birel Op (unrav_rel Op R) ⟹ length a < length b
 2. ⋀a b c.
       (t1, t2) ∈ (gen_birel Op (unrav_rel Op R))⇧+ ⟹
       (a, b) ∈ (gen_birel Op (unrav_rel Op R))⇧+ ⟹
       length a < length b ⟹ (b, c) ∈ gen_birel Op (unrav_rel Op R) ⟹ length a < length c

The assumption " (t1, t2) ∈ (gen_birel Op (unrav_rel Op R))⇧+" is useless, and makes the thing looks a bit messy.

Yiming Xu (Oct 21 2024 at 05:46):

I can live with it, but not as comfortable. Is there any way to obtain the thing I like instead? Or is there any good reason to convince me that this is a reasonable design for Isabelle?

Mathias Fleury (Oct 21 2024 at 05:49):

The assumption (t1, t2) ∈ (gen_birel Op (unrav_rel Op R))⇧++ should be consumed as you can see here:

lemma
  assumes "⋀a b. (a, b) ∈ r ⟹ P a b" and
  "⋀a b c. (a, b) ∈ r⇧+ ⟹ P a b ⟹ (b, c) ∈ r ⟹ P a c"
  "(x1, x2) ∈ r⇧+"
shows "P x1 x2"
  using assms(3,2,1)
  apply (induction rule: trancl_induct)

Are you sure that you not passing it twice as argument cannot be as would be renamed it again as argument later in the proof?

Yiming Xu (Oct 21 2024 at 05:52):

Does it mean the assumption should not be there at all? Then I may wrote something wrong!

Yiming Xu (Oct 21 2024 at 05:52):

I wrote:

lemma unrav_rel_trancl_length:
"(t1, t2) ∈ (gen_birel Op (unrav_rel Op R))⇧+ ⟹ length t1 < length t2"
proof (induct_tac rule:trancl.induct, assumption)

Mathias Fleury (Oct 21 2024 at 05:52):

Use induction and it will be gone

Yiming Xu (Oct 21 2024 at 05:53):

Induction reports error. Maybe because I use "assumes shows" instead?

Mathias Fleury (Oct 21 2024 at 05:53):

either induction or induct_tac + assumption

Yiming Xu (Oct 21 2024 at 05:53):

image.png

Mathias Fleury (Oct 21 2024 at 05:54):

induction does the assumption for you directly

Yiming Xu (Oct 21 2024 at 05:54):

An I see.

Yiming Xu (Oct 21 2024 at 05:55):

Thank you that is exactly what I want:
image.png

Last updated: Dec 21 2024 at 16:20 UTC