ee (May 07 2024 at 09:06): ee (May 07 2024 at 09:06):I have functions defined on lists case splitting the regular way "Nil | Cons (h ## t)", but I'd like to prove lemmas on a "t @ [h]" structure(assuming finite length lists)
I tried defining my own inductive hyptohesis but Isablelle wont let me use those, says it's ill-instantiated.
I tried using the regular rev_induct but it doesn't give me what I need.
I also tried defining a function case splitting from the end by defining a local variable hoping to be able to show extensional equality but that didn't work either.
Is there any way I can do this w/o just assuming that it holds?
TIA
Mathias Fleury (May 07 2024 at 09:08):I tried using the regular rev_induct but it doesn't give me what I need.
Can you be more precise here?
Mathias Fleury (May 07 2024 at 09:08):I tried defining my own inductive hyptohesis but Isablelle wont let me use those, says it's ill-instantiated.
Without showing it, it is not possible to say what is wrong…
ee (May 07 2024 at 09:59):Mathias Fleury said:
I tried using the regular rev_induct but it doesn't give me what I need.
Can you be more precise here?
The inductive hypothesis depends on something I can't prove, as the function has 3 arguments and if I have ' P a b (xs @ [x])', I can't prove 'P a b xs'(the latter I need to use the inductive hypothesis produced by rev_induct)
Mathias Fleury (May 07 2024 at 11:14):So what induction principle would you want to have?
ee (May 09 2024 at 08:28):Mathias Fleury said:
So what induction principle would you want to have?
Sorry about the late response. I basically have a function that boils down to
fun f1:: "'a ⇒ 'a ⇒ 'a list ⇒ bool" where
ni: "f1 x y Nil = (x=y)"
| co: "f1 x y (a#ll) = ((f2 a = x ∧ f1 (f2 a) y ll) ∨ ((f3 a) = x ∧ f1 (f3 a) y ll))"
``` and I just want to prove that if I know that this holds for some list of finite length, the "f2 a = x " etc equalities should hold for the elements at the end of the list, but I can't :upside_down:
What are you trying to prove exactly? This is what I understand:
definition f2 :: ‹'a ⇒ 'a› where
‹f2 a = undefined›
definition f3 :: ‹'a ⇒ 'a› where
‹f3 a = undefined›
fun f1:: "'a ⇒ 'a ⇒ 'a list ⇒ bool" where
ni: "f1 x y Nil = (x=y)"
| co: "f1 x y (a#ll) = ((f2 a = x ∧ f1 (f2 a) y ll) ∨ ((f3 a) = x ∧ f1 (f3 a) y ll))"
lemma
‹f1 x y xs ⟹ xs ≠ [] ⟹ f2 (last xs) = y ∨ f3 (last xs) = y›
by (induction x y xs rule: f1.induct)
auto
Mathias Fleury said:
lemma ‹f1 x y xs ⟹ xs ≠ [] ⟹ f2 (last xs) = y ∨ f3 (last xs) = y› by (induction x y xs rule: f1.induct) auto
Thank you!! I didn't know I could use three variables to do induction that was the problem :melting_face:
Last updated: Dec 21 2024 at 16:20 UTC