## Stream: Coq users

### Topic: ✔ Beginner : need help on a cpdt exercise

#### kumar (Aug 09 2021 at 10:50):

There is a theorem in CPDT which is brushed off with a solution using a custom tactic (crush) defined by the author

``````Theorem length_app : ∀ ls1 ls2 : list, length (app ls1 ls2 ) = plus (length ls1) (length ls2).
induction ls1; crush.
Qed.
``````

And I'm trying to use built-in tactics to understand this proof and prove this.
I am stuck at a point where I need to prove the following

``````T: Set
t: T
ls2: list
IHls2: length ls2 = plus O (length ls2)
-----------------------------------------------------------------------
(1/1)
S (length ls2) = plus (S O) (length ls2)
``````

and I want to be able to remove the church notation S. But I don't know what tactic I should use

#### Ali Caglayan (Aug 09 2021 at 10:57):

If you do `Search plus S` you can find lemmas about `S` and `plus`. There ought to be a lemma about turning `plus (S x) y = S (plus x y)`

#### Ali Caglayan (Aug 09 2021 at 10:58):

Then you can use `rewrite` along that equality.

#### Ali Caglayan (Aug 09 2021 at 10:58):

or `rewrite <-` if it needs to go the otherway

#### Ali Caglayan (Aug 09 2021 at 10:59):

There is also a lemma about `plus O x = x` somewhere but you probably don't need that since `IHls2` gives you what you want.

#### Ali Caglayan (Aug 09 2021 at 11:00):

The lemma `f_equal` should help with proving `S x = S y` from `x = y`. You can just `apply` it.

#### kumar (Aug 09 2021 at 11:53):

Thanks @Ali Caglayan that worked!

#### Notification Bot (Aug 09 2021 at 11:54):

Ali Caglayan has marked this topic as resolved.

Last updated: Jan 31 2023 at 13:02 UTC