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: Sep 23 2023 at 14:01 UTC