Stream: Beginner Questions

Topic: Lexicographic induction

Marvin Brieger (Sep 26 2023 at 12:17):

Hi everyone,
I like to prove a property P(X, Y) for all X, Y, where X and Y are subsets of countable carriers. I want to do so by lexicographic induction on the size of the sets, i.e. starting from X = {} and Y = {} (base case), I either increase X or X stays the same but Y is increased.

Is there a general blueprint how to do such proofs work or do I need to instrument Isabelle in a certain way to prepare for such inductions?

Manuel Eberl (Sep 26 2023 at 12:23):

Your X and Y are finite, right?

Marvin Brieger (Sep 26 2023 at 12:47):

Sure ;)

Manuel Eberl (Sep 26 2023 at 12:55):

Honestly I'm a bit surprised this is as tricky as it is. I would have thought there'd be more support from the induction command.

Manuel Eberl (Sep 26 2023 at 12:56):

You can do a well-founded induction on the pair (X, Y) or on the pair (card X, card Y) with the right relation (that relation being a lexicographic product of measure (card ∘ fst) and measure (card ∘snd) or measure fst and measure snd, respectively).

Manuel Eberl (Sep 26 2023 at 12:57):

You can also do something like this, using the induction_schema method to prove your custom induction scheme admissible directly:

lemma foo_induct:
  assumes "P {} {}"
  assumes "⋀X Y. (⋀Y'. card Y' < card Y ⟹ P X Y') ⟹ P X Y"
  assumes "⋀X Y. (⋀X' Y'. card X' < card X ⟹ P X' Y') ⟹ P X Y"
  shows   "P X Y"
  using assms
  apply induction_schema
     apply blast
    apply (rule wf_mlex[OF wf_measure[of "card ∘ snd"], of "card ∘ fst"])
   apply (auto simp: mlex_prod_def)
  done

Manuel Eberl (Sep 26 2023 at 12:58):

You can then do something like

lemma
  fixes X Y
  assumes fin: "finite X" "finite Y"
  shows "foo X Y"
using fin
proof (induction X Y rule: foo_induct)
  …

Manuel Eberl (Sep 26 2023 at 12:58):

You can also add the finiteness stuff directly into your induction rule – might make things a bit nicer

Manuel Eberl (Sep 26 2023 at 12:58):

lemma foo_induct' [consumes 2]:
  assumes "finite X" "finite Y"
  assumes "P {} {}"
  assumes "⋀X Y. finite X ⟹ finite Y ⟹ (⋀Y'. finite Y' ⟹ card Y' < card Y ⟹ P X Y') ⟹ P X Y"
  assumes "⋀X Y. finite X ⟹ finite Y ⟹ (⋀X' Y'. finite X' ⟹ finite Y' ⟹ card X' < card X ⟹ P X' Y') ⟹ P X Y"
  shows   "P X Y"
  using assms(3-)
  apply -
  using assms(1,2)
  apply induction_schema
     apply blast
    apply (rule wf_mlex[OF wf_measure[of "card ∘ snd"], of "card ∘ fst"])
   apply (auto simp: mlex_prod_def)
  done

Manuel Eberl (Sep 26 2023 at 12:59):

Note that depending on what you need exactly you might have to/want to tweak this a bit. For example, if you also want to be able to change the X in the first inductive case (just its size has to stay the same) you will have to generalise the above.

Manuel Eberl (Sep 26 2023 at 13:00):

In the other direction, if the sets you instantiate the induction hypothesis with are actually subsets of the original ones, you can forgo using cardinalities entirely and rather work with the (proper) subset relations, which often makes things much easier because fiddling with cardinalities is a bit annoying.

Manuel Eberl (Sep 26 2023 at 13:01):

It would be nicer to have some built-in support for lexicographic induction in the induction command. But I'm not sure what that would look like.

Marvin Brieger (Sep 27 2023 at 09:23):

Manuel Eberl said:

Honestly I'm a bit surprised this is as tricky as it is. I would have thought there'd be more support from the induction command.

Many thx so far! I somewhat expected it to look like this but wouldn't have been able to figure out the intricate details.

Wolfgang Jeltsch (Sep 27 2023 at 10:46):

Manuel Eberl said:

You can also do something like this, using the induction_schema method to prove your custom induction scheme admissible directly: […]

I’ve never heard of this proof method. Where is it documented?

Generally, I have the impression that Isabelle’s documentation is by no means complete. For example, I’ve seen Sledgehammer suggesting using proof methods that don’t seem to be covered by the documentation.

Fabian Huch (Sep 27 2023 at 17:14):

It's certainly complete, the caveat is that some of it is only available in the standardized ML format ;)
Seriously though, the best way to find out which methods is available is the print_methods command.

Yutaka Nagashima (Sep 27 2023 at 22:24):

Wolfgang Jeltsch said:

I’ve never heard of this proof method. Where is it documented?

Generally, I have the impression that Isabelle’s documentation is by no means complete. For example, I’ve seen Sledgehammer suggesting using proof methods that don’t seem to be covered by the documentation.

When I explored the standard library and the AFP, I discovered around 200 proof methods. Pages 13-16 of this paper display the list of proof methods I identified, along with their frequency of use.

Manuel Eberl (Sep 29 2023 at 11:27):

Another way is to directly use wf_induct directly and then split_format.

Last updated: Apr 27 2024 at 20:14 UTC