Stream: Beginner Questions

Topic: Proof involving datatype partially?

waynee95 (Aug 09 2022 at 14:55):

I have a datatype that looks something like this

datatype t =
  A
  | B
  | C t
  | D t t
  | E t x
  | F t x

I want to prove

lemma "f t = g t"

but only for t equal toA to D. This shall be an auxiliary lemma for a bigger proof that involves all the cases for t.

Is there a way to do this in a neat fashion or do I need to write multiple lemmas where t is hardcoded to be A etc.

Maximilian Schaeffeler (Aug 10 2022 at 09:39):

I don't think this works with a list of lemmas, since t appears recursively.
Depending on the situation, I might either introduce a new, restricted datatype or add a predicate that only allows A to D as an assumption.

Last updated: Apr 16 2024 at 12:28 UTC