ee (Apr 09 2024 at 17:32): ee (Apr 09 2024 at 17:32):I'm trying to prove a lemmu using list induction. I need to use a function I defined on a list, and I need the induction to be on the reverse of a list(I need the cases to be ""Nil" | "snoc xs x" " instead of " "Nil" | x # xs"). I can't use "proof(induct l1 rule: comp.induct rev_induct)" since it throws an error "Failed to join given rules into one mutual rule". I tried defining the function differently:
"fun comp :: "'a list ⇒ 'a" where
"comp [x] = x"
| "comp [x,f,y] = f"
| "comp xs = (if (length xs > 3) then (comp (drop 2 xs) #0 (hd (tl (rev xs)))) else undefined )" " but this doesn't work either.
I also tried defining a new variable as "ys = rev xs" but then my inductive hypothesis has things
like
" v # vb = ys⟹ P ys⟹ Q ys"
and " v # vb # vc = ys" which makes it very hard (or maybe impossible) to prove things.
TIA
Mathias Fleury (Apr 09 2024 at 17:35):You are giving two rules instead of one. If you give only one it will work:
fun comp :: "'a list ⇒ 'a" where
"comp [x] = x"
| "comp [x,f,y] = f"
| "comp xs = (if (length xs > 3) then comp (drop 2 xs @ [hd (tl (rev xs))]) else undefined )"
lemma "comp xs ∈ set xs"
apply (induction xs rule: rev_induct)
apply auto
sorry
But if you want to compose rules, you need to define your own induction principle.
Mathias Fleury (Apr 09 2024 at 17:37):For 2: not, this would not be computable
ee (Apr 09 2024 at 18:02):Mathias Fleury said:
But if you want to compose rules, you need to define your own induction principle.
Yeah that's what I figured. Thanks!
Manuel Eberl (Apr 09 2024 at 18:27):Mathias Fleury said:
For 2: not, this would not be computable
I would not necessarily recommend doing this, but it can be done by setting up "append at the back" as a free constructor:
definition snoc where "snoc xs x = xs @ [x]"
definition case_list_rev :: "'a ⇒ ('b list ⇒ 'b ⇒ 'a) ⇒ 'b list ⇒ 'a" where
"case_list_rev x f xs = (if xs = [] then x else f (butlast xs) (last xs))"
free_constructors case_list_rev for Nil | snoc
unfolding snoc_def using rev_exhaust by auto
lemma length_snoc [termination_simp]: "length (snoc xs x) = Suc (length xs)"
by (simp add: snoc_def)
fun f :: "'a list ⇒ nat" where
"f [] = 0"
| "f (snoc xs x) = f xs + 1"
Manuel Eberl said:
Mathias Fleury said:
For 2: not, this would not be computable
I would not necessarily recommend doing this, but it can be done by setting up "append at the back" as a free constructor:
definition snoc where "snoc xs x = xs @ [x]" definition case_list_rev :: "'a ⇒ ('b list ⇒ 'b ⇒ 'a) ⇒ 'b list ⇒ 'a" where "case_list_rev x f xs = (if xs = [] then x else f (butlast xs) (last xs))" free_constructors case_list_rev for Nil | snoc unfolding snoc_def using rev_exhaust by auto lemma length_snoc [termination_simp]: "length (snoc xs x) = Suc (length xs)" by (simp add: snoc_def) fun f :: "'a list ⇒ nat" where "f [] = 0" | "f (snoc xs x) = f xs + 1"
Never mind, this is a very bad idea because 1. the code generation doesn't work for this and 2. it overwrites the existing constructors of the list type.
ee (Apr 10 2024 at 08:08):Manuel Eberl said:
Mathias Fleury said:
For 2: not, this would not be computable
I would not necessarily recommend doing this, but it can be done by setting up "append at the back" as a free constructor:
definition snoc where "snoc xs x = xs @ [x]" definition case_list_rev :: "'a ⇒ ('b list ⇒ 'b ⇒ 'a) ⇒ 'b list ⇒ 'a" where "case_list_rev x f xs = (if xs = [] then x else f (butlast xs) (last xs))" free_constructors case_list_rev for Nil | snoc unfolding snoc_def using rev_exhaust by auto lemma length_snoc [termination_simp]: "length (snoc xs x) = Suc (length xs)" by (simp add: snoc_def) fun f :: "'a list ⇒ nat" where "f [] = 0" | "f (snoc xs x) = f xs + 1"
Uh could you still explain how this works a little? I' m not at all familiar with the sytax and keywords you are using, it seems like something that could be useful in the future.
Mathias Fleury (Apr 10 2024 at 08:12):free_constructors appears 7 times in the entire AFP, so not really useful
Mathias Fleury (Apr 10 2024 at 08:12):The idea is that you can set your own constructors as definition for the BNF
Manuel Eberl (Apr 10 2024 at 08:32):Yeah, it allows you to do pattern matching on something that isn't a datatype. It's also used for e.g. the nat type, which looks like a datatype but actually isn't.
Manuel Eberl (Apr 10 2024 at 08:34):But unlike what I initially thought, it appears that you can only have one set of "free constructors" per datatype, so it only makes sense to do this exactly once per type and only with constructors that are really "canonical".
ee (Apr 10 2024 at 12:13):Mathias Fleury said:
But if you want to compose rules, you need to define your own induction principle.
Sorry, could I have some insight into how I can do this properly?
theorem inductC:
fixes P :: "'a list ⇒ bool"
and a0 :: "'a list"
assumes h0:"P []"
assumes h1:"⋀ x. comp [x] ∧ P [x]"
and h2:"⋀ x f y. (comp [x, f, y] ∧ P [x, f, y]) "
and
ind: "⋀ f v g. comp v ∧ comp [last v, f, g] ∧
P (v ) ⟹ P ( append v [f,g])"
and "comp a0"
shows "P a0"
I saw an example that used a format like this, but then when I try to use this to prove a lemma, some of the states don't pick any of the assumptions, eg
"proof (state)
this:
goal (4 subgoals):" .
The only one that does is the inductive steps case actually. I was thinking h0 h1 h2 would act as the base cases(they can be proved using the definition of "comp") but there's nothing in the scope I can use to prove them.
Mathias Fleury (Apr 10 2024 at 12:54):Look at list.induct and rev.induct to see what the format is
Last updated: May 06 2024 at 16:21 UTC