Stream: Beginner Questions

Topic: How to prove a simple cases of

view this post on Zulip Moritz R (Dec 29 2024 at 13:34):

I can't seem to close this goal, although it should be trivial, no?

goal (1 subgoal):
 1. ⋀br i x2.
       map Tm (case x2 of [] ⇒ [] | [Nt B] ⇒ [] | [Nt B, Nt C] ⇒ [] | Nt B # Nt C # _ ⇒ [] | Nt B # Tm t # lista ⇒ [] | [Tm a] ⇒ if br = Op ∧ i = 1 then [a] else [] | Tm a # ab # lista ⇒ [])

=

              (case x2 of [] ⇒ [] | [Nt B] ⇒ [] | [Nt B, Nt C] ⇒ [] | Nt B # Nt C # _ ⇒ [] | Nt B # Tm t # lista ⇒ [] | [Tm a] ⇒ if br = Op ∧ i = 1 then [Tm a] else [] | Tm a # ab # lista ⇒ [])

view this post on Zulip Moritz R (Dec 29 2024 at 13:37):

All of these but the if-clause should be the empty list and as such equal. For the if clause one should use the definition of map

view this post on Zulip Yong Kiam (Dec 30 2024 at 01:23):

try using list.splits and foo.splits where foo is the type of Tm and Nt

view this post on Zulip Moritz R (Dec 30 2024 at 12:04):

Thank you! This was the missing ingredient.

Last updated: Nov 02 2025 at 16:23 UTC