Email Gateway (Aug 22 2022 at 13:08): Email Gateway (Aug 22 2022 at 13:08):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I have the following datatype:
datatype "term" =
Const string |
Free string |
Abs "term" ("Λ _" [71] 71) |
Bound nat |
App "term" "term" (infixl "$" 70)
I define a sub-term relation:
inductive direct_sub_term :: "term ⇒ term ⇒ bool" where
left: "direct_sub_term t (t $ u)" |
right: "direct_sub_term u (t $ u)" |
abs: "direct_sub_term t (Λ t)"
abbreviation sub_term :: "term ⇒ term ⇒ bool" (infix "◃" 50) where
"sub_term ≡ direct_sub_term⇧+⇧+"
I have no idea whether this is in fact a proper well-ordering, but I'd
like to at least prove the induction principle:
lemma sub_term_induct[case_names sub]:
assumes "⋀t. (⋀u. u ◃ t ⟹ P u) ⟹ P t"
shows "P t"
The proof is rather mechanical, but it took me a while to figure out (by
looking at the corresponding proof for natural numbers).
I wonder if there's existing automation to derive the "◃" predicate and
the corresponding proof.
Cheers
Lars
Email Gateway (Aug 22 2022 at 13:08):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lars,
AFAIK there is no automation support for this.
For finitely branching, tree-like data structures, the subterm relation is well-founded
(as a proof, just take the size of the tree as a measure). So I'd expect that you can
prove the induction statement using induction_schema and lexicographic_order (after some
setup for tranclp and direct_sub_term).
If you have an infinitely branching tree (or recursion through other BNFs without a size
function), then well-foundedness of the subterm relation cannot be proven with measures.
In these cases, I normally manually write definitions similar to yours and prove
well-foundedness, which I can then use in termination proofs for the function package.
So if you have the time to automate these steps, I'd be all in favour of it. I guess that
this should not be too hard with the new datatype package, but it definitely requires some
work, but Dmitriy and Jasmin are in a better position to estimate the effort needed.
Andreas
Email Gateway (Aug 22 2022 at 13:08):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Lars and Andreas,
Yes, it would be nice to have this automated. Back in the days when designing the new datatype package, we thought of adding this as well,
but eventually renounced in order to keep the effort size manageable.
Here is my pattern for proving this for finitely branching datatypes (which constitute 99 percent of those in current use).
The following lemma transports well-foundedness back from the order on naturals:
lemma wfP_lt:
assumes "∀ x y. r x y ⟶ (f x::nat) < f y"
shows "wfP r"
proof-
have "{(x, y). r x y} ⊆ inv_image {(x,y) . x < y} f"
using assms unfolding inv_image_def by auto
thus ?thesis unfolding wfP_def
using wf_inv_image wf_less wf_subset by blast
qed
Then the following are absolute routine (and are presumably not hard to automate, but have the usual
complications coming from "mutual" and "nested"):
lemma size_direct_sub_term[simp]:
assumes "direct_sub_term t u" shows "size t < size u"
using assms by induction auto
lemma sub_term[simp]:
assumes "sub_term t u" shows "size t < size u"
using assms apply(induction, simp_all)
using dual_order.strict_trans size_direct_sub_term by blast
lemma wfP_sub_term: "wfP sub_term"
using sub_term wfP_lt by blast
lemma sub_term_induct[case_names sub]:
assumes "⋀t. (⋀u. u ◃ t ⟹ P u) ⟹ P t"
shows "P t"
using assms wfP_sub_term by (metis wfP_induct_rule)
All the best,
Andrei
Email Gateway (Aug 22 2022 at 13:08):From: Lars Hupel <hupel@in.tum.de>
Hi,
thanks everyone. Also, Peter pointed out to me that it's actually rather
simple, so automation is already there (with "auto", "induction_schema"
etc.) I should've asked yesterday ... Now I feel stupid :-)
Cheers
Lars
Email Gateway (Aug 22 2022 at 13:09):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Lars,
this would be useful indeed. Here is my pattern for proving this for arbitrary datatypes (which constitute 100 percent of those in current use ;-) ).
Note that my definitions and proofs are done on what we call the low-level (where there is only one constructor).
Jasmin is usually the one lifting lemmas (in particular the intro rules and the induction principle of ◃⇩1) to multiple constructors. But I presume this should not be harder than usual in this case.
Dmitriy
theory Scratch
imports "~~/src/HOL/Library/BNF_Axiomatization"
begin
declare [[typedef_overloaded]]
bnf_axiomatization 'a F [wits: "'a F"]
datatype T = C "T F"
inductive direct_sub_term :: "T ⇒ T ⇒ bool" (infix "◃⇩1" 50) where
"y ∈ set_F x ⟹ y ◃⇩1 C x"
abbreviation sub_term :: "T ⇒ T ⇒ bool" (infix "◃" 50) where
"sub_term ≡ direct_sub_term⇧+⇧+"
inductive_cases direct_sub_termE[elim!]: "y ◃⇩1 C x"
inductive_cases sub_termE[elim!]: "y ◃ C x"
lemma sub_term_induct_aux[THEN spec, THEN mp, rotated]:
assumes [intro]: "⋀t. (⋀u. u ◃ t ⟹ P u) ⟹ P t"
shows "∀u. u ◃ t ⟶ P u"
apply (induct t)
apply auto
done
lemma sub_term_induct[case_names sub]:
assumes IH: "⋀t. (⋀u. u ◃ t ⟹ P u) ⟹ P t"
shows "P t"
apply (cases t; hypsubst_thin)
apply (rule IH)
apply (erule sub_term_induct_aux)
by (rule IH)
end
Email Gateway (Aug 22 2022 at 13:09):From: Peter Lammich <lammich@in.tum.de>
On set-based relations, there is a constant "measure", such that the
proof could be done by showing
inductive_set direct_sub_term :: "(term × term) set" where
left: "(t, t $ u) ∈ direct_sub_term " |
right: "(u, t $ u) ∈ direct_sub_term" |
abs: "(t, (Λ t)) ∈ direct_sub_term"
abbreviation sub_term :: "(term × term) set" where
"sub_term ≡ direct_sub_term⇧+"
lemma wf: "wf direct_sub_term"
apply (rule wf_subset)
apply (rule wf_measure[where f=size])
by (auto elim: direct_sub_term.cases)
lemmas induct_rl = wf_induct[OF wf_trancl[OF wf]]
(* Produces (⋀x. ∀y. (y, x) ∈ sub_term ⟶ ?P y ⟹ ?P x) ⟹ ?P ?a *)
On predicates, the concept of "measure" seems to be missing in the
library, but there is also a wfP_trancl-lemma in the library, which
could simplify Andrei's proof a bit.
Last updated: Apr 16 2024 at 12:28 UTC